Fix term component projection JNI errors

Author: disteph

src/main/java/com/sri/yices/Yices.java

@@ -396,7 +396,7 @@ public static int mkRationalConstant(BigInteger num, BigInteger den) {
 
     public static SumComponent<?> sumComponent(int x, int idx) {
         SumComponent<?> result = null;
-        if (Yices.termIsArithmetic(x)) {
+        if (Yices.termIsSum(x)) {
           byte[] num = sumComponentNumAsBytes(x, idx);
           byte[] den = sumComponentDenAsBytes(x, idx);
           int term = sumComponentTerm(x, idx);
@@ -405,7 +405,7 @@ public static SumComponent<?> sumComponent(int x, int idx) {
             result = new SumComponent<>(new BigRational(num, den), term);
           }
         }
-        if (Yices.termIsBitvector(x)) {
+        if (Yices.termIsBvSum(x)) {
           boolean[] factor = bvSumComponentFactor(x, idx);
           int term = bvSumComponentTerm(x, idx);
 

src/main/java/com/sri/yices/yicesJNI.cpp

@@ -2659,7 +2659,7 @@ JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentDenAsBytes(JNI
 }
 
 JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_sumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
-  jint result;
+  jint result = -1;
   mpq_t q;
 
   mpq_init(q);
@@ -2674,21 +2674,25 @@ JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvSumComponentFactor(JN
   jint t = -1;
 
   int32_t n = yices_term_bitsize(x);
-  assert(n >= 0);
+  if (n < 0) {
+    return NULL;
+  }
 
   if (n <= 64) {
     // this should be the common case
     int32_t a[64];
     int32_t code = yices_bvsum_component(x, idx, a, &t);
-    assert(code >= 0);
-    result = convertToBoolArray(env, n, a);
+    if (code >= 0) {
+      result = convertToBoolArray(env, n, a);
+    }
 
   } else {
     try {
       int32_t *tmp =  new int32_t[n];
       int32_t code = yices_bvsum_component(x, idx, tmp, &t);
-      assert(code >= 0);
-      result = convertToBoolArray(env, n, tmp);
+      if (code >= 0) {
+        result = convertToBoolArray(env, n, tmp);
+      }
       delete [] tmp;
     } catch (std::bad_alloc&) {
       out_of_mem_exception(env);
@@ -2702,19 +2706,19 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_bvSumComponentTerm(JNIEnv *env,
   jint result = -1;
 
   int32_t n = yices_term_bitsize(x);
-  assert(n >= 0);
+  if (n < 0) {
+    return result;
+  }
 
   if (n <= 64) {
     // this should be the common case
     int32_t a[64];
-    int32_t code = yices_bvsum_component(x, idx, a, &result);
-    assert(code >= 0);
+    yices_bvsum_component(x, idx, a, &result);
 
   } else {
     try {
       int32_t *tmp =  new int32_t[n];
-      int32_t code = yices_bvsum_component(x, idx, tmp, &result);
-      assert(code >= 0);
+      yices_bvsum_component(x, idx, tmp, &result);
       delete [] tmp;
     } catch (std::bad_alloc&) {
       out_of_mem_exception(env);

src/main/java/com/sri/yices/yicesJNIforWindows.cpp

@@ -2630,6 +2630,120 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_termProjArg(JNIEnv *env, jclass,
   return yices_proj_arg(x);
 }
 
+JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentNumAsBytes(JNIEnv *env, jclass, jint x, jint idx) {
+  jbyteArray result = NULL;
+  mpq_t q;
+  jint t = -1;
+
+  mpq_init(q);
+  if (yices_sum_component(x, idx, q, &t) >= 0) {
+    result = mpz_to_byte_array(env, mpq_numref(q));
+  }
+  mpq_clear(q);
+
+  return result;
+}
+
+JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentDenAsBytes(JNIEnv *env, jclass, jint x, jint idx) {
+  jbyteArray result = NULL;
+  mpq_t q;
+  jint t = -1;
+
+  mpq_init(q);
+  if (yices_sum_component(x, idx, q, &t) >= 0) {
+    result = mpz_to_byte_array(env, mpq_denref(q));
+  }
+  mpq_clear(q);
+
+  return result;
+}
+
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_sumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
+  jint result = -1;
+  mpq_t q;
+
+  mpq_init(q);
+  yices_sum_component(x, idx, q, &result);
+  mpq_clear(q);
+
+  return result;
+}
+
+JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvSumComponentFactor(JNIEnv *env, jclass, jint x, jint idx) {
+  jbooleanArray result = NULL;
+  jint t = -1;
+
+  int32_t n = yices_term_bitsize(x);
+  if (n < 0) {
+    return NULL;
+  }
+
+  if (n <= 64) {
+    // this should be the common case
+    int32_t a[64];
+    int32_t code = yices_bvsum_component(x, idx, a, &t);
+    if (code >= 0) {
+      result = convertToBoolArray(env, n, a);
+    }
+
+  } else {
+    try {
+      int32_t *tmp =  new int32_t[n];
+      int32_t code = yices_bvsum_component(x, idx, tmp, &t);
+      if (code >= 0) {
+        result = convertToBoolArray(env, n, tmp);
+      }
+      delete [] tmp;
+    } catch (std::bad_alloc&) {
+      out_of_mem_exception(env);
+    }
+  }
+
+  return result;
+}
+
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_bvSumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
+  jint result = -1;
+
+  int32_t n = yices_term_bitsize(x);
+  if (n < 0) {
+    return result;
+  }
+
+  if (n <= 64) {
+    // this should be the common case
+    int32_t a[64];
+    yices_bvsum_component(x, idx, a, &result);
+
+  } else {
+    try {
+      int32_t *tmp =  new int32_t[n];
+      yices_bvsum_component(x, idx, tmp, &result);
+      delete [] tmp;
+    } catch (std::bad_alloc&) {
+      out_of_mem_exception(env);
+    }
+  }
+
+  return result;
+}
+
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
+  uint32_t p = 0;
+  jint t = -1;
+
+  yices_product_component(x, idx, &t, &p);
+  return t;
+}
+
+JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentPower(JNIEnv *env, jclass, jint x, jint idx) {
+  uint32_t p = 0;
+  jint t = -1;
+
+  yices_product_component(x, idx, &t, &p);
+  return p;
+}
+
 JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_boolConstValue(JNIEnv *env, jclass, jint x) {
   int32_t val;
   jint result;