Update Yices bindings and add some missing features

build.xml

@@ -223,7 +223,7 @@
     <echo> Executing "make ${library}" in ${code} </echo>
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="${library}"/>
     </exec>
 
@@ -233,7 +233,7 @@
 
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="install"/>
     </exec>
 
@@ -250,7 +250,7 @@
 
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="clean"/>
     </exec>
   </target>

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

@@ -11,64 +11,66 @@ public enum Constructor {
     // atomic terms
     BOOL_CONSTANT(0),        // boolean constant
     ARITH_CONSTANT(1),       // rational constant
-    BV_CONSTANT(2),          // bitvector constant
-    SCALAR_CONSTANT(3),      // constant of uninterpreted or scalar type
-    VARIABLE(4),             // variable in quantifiers
-    UNINTERPRETED_TERM(5),   // (i.e., global variables, can't be bound)
+    FF_CONSTANT(2),          // finite field constant
+    BV_CONSTANT(3),          // bitvector constant
+    SCALAR_CONSTANT(4),      // constant of uninterpreted or scalar type
+    VARIABLE(5),             // variable in quantifiers
+    UNINTERPRETED_TERM(6),   // (i.e., global variables, can't be bound)
 
     // composite terms
-    ITE_TERM(6),             // if-then-else
-    APP_TERM(7),             // application of an uninterpreted function
-    UPDATE_TERM(8),          // function update
-    TUPLE_TERM(9),           // tuple constructor
-    EQ_TERM(10),             // equality
-    DISTINCT_TERM(11),       // distinct t_1 ... t_n
-    FORALL_TERM(12),         // quantifier
-    LAMBDA_TERM(13),         // lambda
-    NOT_TERM(14),            // (not t)
-    OR_TERM(15),             // n-ary OR
-    XOR_TERM(16),            // n-ary XOR
+    ITE_TERM(7),             // if-then-else
+    APP_TERM(8),             // application of an uninterpreted function
+    UPDATE_TERM(9),          // function update
+    TUPLE_TERM(10),           // tuple constructor
+    EQ_TERM(11),             // equality
+    DISTINCT_TERM(12),       // distinct t_1 ... t_n
+    FORALL_TERM(13),         // quantifier
+    LAMBDA_TERM(14),         // lambda
+    NOT_TERM(15),            // (not t)
+    OR_TERM(16),             // n-ary OR
+    XOR_TERM(17),            // n-ary XOR
 
-    BV_ARRAY(17),            // array of boolean terms
-    BV_DIV(18),              // unsigned division
-    BV_REM(19),              // unsigned remainder
-    BV_SDIV(20),             // signed division
-    BV_SREM(21),             // remainder in signed division (rounding to 0)
-    BV_SMOD(22),             // remainder in signed division (rounding to -infinity)
-    BV_SHL(23),              // shift left (padding with 0)
-    BV_LSHR(24),             // logical shift right (padding with 0)
-    BV_ASHR(25),             // arithmetic shift right (padding with sign bit)
-    BV_GE_ATOM(26),          // unsigned comparison: (t1 >= t2)
-    BV_SGE_ATOM(27),         // signed comparison (t1 >= t2)
-    ARITH_GE_ATOM(28),       // atom (t1 >= t2) for arithmetic terms: t2 is always 0
-    ARITH_ROOT_ATOM(29),     // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >=
+    BV_ARRAY(18),            // array of boolean terms
+    BV_DIV(19),              // unsigned division
+    BV_REM(20),              // unsigned remainder
+    BV_SDIV(21),             // signed division
+    BV_SREM(22),             // remainder in signed division (rounding to 0)
+    BV_SMOD(23),             // remainder in signed division (rounding to -infinity)
+    BV_SHL(24),              // shift left (padding with 0)
+    BV_LSHR(25),             // logical shift right (padding with 0)
+    BV_ASHR(26),             // arithmetic shift right (padding with sign bit)
+    BV_GE_ATOM(27),          // unsigned comparison: (t1 >= t2)
+    BV_SGE_ATOM(28),         // signed comparison (t1 >= t2)
+    ARITH_GE_ATOM(29),       // atom (t1 >= t2) for arithmetic terms: t2 is always 0
+    ARITH_ROOT_ATOM(30),     // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >=
 
-    ABS(30),                 // absolute value
-    CEIL(31),                // ceil
-    FLOOR(32),               // floor
-    RDIV(33),                // real division (as in x/y)
-    IDIV(34),                // integer division
-    IMOD(35),                // modulo
-    IS_INT_ATOM(36),         // integrality test: (is-int t)
-    DIVIDES_ATOM(37),        // divisibility test: (divides t1 t2)
+    ABS(31),                 // absolute value
+    CEIL(32),                // ceil
+    FLOOR(33),               // floor
+    RDIV(34),                // real division (as in x/y)
+    IDIV(35),                // integer division
+    IMOD(36),                // modulo
+    IS_INT_ATOM(37),         // integrality test: (is-int t)
+    DIVIDES_ATOM(38),        // divisibility test: (divides t1 t2)
 
     // projections
-    SELECT_TERM(38),         // tuple projection
-    BIT_TERM(39),            // bit-select: extract the i-th bit of a bitvector
+    SELECT_TERM(39),         // tuple projection
+    BIT_TERM(40),            // bit-select: extract the i-th bit of a bitvector
 
     // sums
-    BV_SUM(40),              // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term)
-    ARITH_SUM(41),           // sum of pairs a * t where a is a rational (and t is an arithmetic term)
+    BV_SUM(41),              // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term)
+    ARITH_SUM(42),           // sum of pairs a * t where a is a rational (and t is an arithmetic term)
+    FF_SUM(43),              // sum of pairs a * t where a is a finite-field constant (and t is a finite-field term)
 
     // products
-    POWER_PRODUCT(42)        // power products: (t1^d1 * ... * t_n^d_n)
+    POWER_PRODUCT(44)        // power products: (t1^d1 * ... * t_n^d_n)
     ;
 
     private int index;
     Constructor(int id) { this.index = id; }
     public int getIndex() { return index; }
 
-    public static final int NUM_CONSTRUCTORS = 43;
+    public static final int NUM_CONSTRUCTORS = 45;
     private static final Constructor[] table;
 
     static {

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

@@ -331,7 +331,7 @@ public int getModelInterpolant() {
 
     // Since 2.6.4
     public Status checkWithAssumptions(Parameters params, int[] assumptions) {
-        int code = Yices.checkContextWithAssumptions(ptr, params.getPtr(), assumptions);
+        int code = Yices.checkContextWithAssumptions(ptr, params == null ? 0 : params.getPtr(), assumptions);
         if (code < 0) {
             throw new YicesException();
         }
@@ -340,7 +340,7 @@ public Status checkWithAssumptions(Parameters params, int[] assumptions) {
 
     // Since 2.6.4
     public Status checkWithModel(Parameters params, Model model, int[] assumptions) {
-        int code = Yices.checkContextWithModel(ptr, params.getPtr(), model.getPtr(), assumptions);
+        int code = Yices.checkContextWithModel(ptr, params == null ? 0 : params.getPtr(), model.getPtr(), assumptions);
         if (code < 0) {
             YicesException error = YicesException.checkVersion(2, 6, 4);
             if (error == null) {

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

@@ -35,7 +35,7 @@ public Status check(Parameters params, boolean buildModel) {
         int[] tarr = { 0 };
         long[] marr = { 0 };
         if (!buildModel) { marr = null; }
-        int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params.getPtr(), marr, tarr);
+        int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params == null ? 0 : params.getPtr(), marr, tarr);
         Status status = Status.idToStatus(code);
         if (status == Status.ERROR) {
             throw new YicesException();

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

@@ -398,7 +398,7 @@ public YVal[] expandTuple(YVal yval) throws YicesException {
 
     public VectorValue expandFunction(YVal yval) throws YicesException {
         int n = Yices.valFunctionCardinality(ptr, yval.tag.ordinal(), yval.id);
-        if (n <= 0) throw new YicesException();
+        if (n < 0) throw new YicesException();
         YVal[] vector =  new YVal[n];
         YVal[] value = new YVal[1];
         int code = Yices.valExpandFunction(ptr, yval.tag.ordinal(), yval.id, value, vector);

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

@@ -0,0 +1,19 @@
+package com.sri.yices;
+
+public class ProductComponent {
+  private final int power;
+  private final int term;
+
+  public ProductComponent(int pTerm, int pPower) {
+    power = pPower;
+    term = pTerm;
+  }
+
+  public int getTerm() {
+    return term;
+  }
+
+  public int getPower() {
+    return power;
+  }
+}

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

@@ -0,0 +1,19 @@
+package com.sri.yices;
+
+public class SumComponent<T> {
+  private final T factor;
+  private final int term;
+
+  public SumComponent(T pFactor, int pTerm) {
+    factor = pFactor;
+    term = pTerm;
+  }
+
+  public T getFactor() {
+    return factor;
+  }
+
+  public int getTerm() {
+    return term;
+  }
+}

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

@@ -1258,6 +1258,17 @@ static public int projArg(int x) throws YicesException {
         return t;
     }
 
+    static public SumComponent<?> projSum(int x, int idx) throws YicesException {
+      SumComponent<?> c = Yices.sumComponent(x, idx);
+      if (c == null) throw new YicesException();
+      return c;
+    }
+
+    static public ProductComponent projProduct(int x, int idx) throws YicesException {
+      ProductComponent c = Yices.productComponent(x, idx);
+      if (c == null) throw new YicesException();
+      return c;
+    }
 
     /*
      * Check whether term x is a constant

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

@@ -13,6 +13,7 @@ public enum YValTag {
     BOOL,
     RATIONAL,
     ALGEBRAIC,
+    FINITEFIELD,
     BV,
     SCALAR,
     TUPLE,

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

@@ -13,7 +13,10 @@ public final class Yices {
      */
     static {
         try {
-            System.loadLibrary("yices2java");
+            String skip = System.getProperty("yices.skipAutoloader", "false");
+            if (!Boolean.parseBoolean(skip)) {
+              System.loadLibrary("yices2java");
+            }
             init();
             is_ready = true;
         } catch (LinkageError e) {
@@ -384,6 +387,49 @@ public static int mkRationalConstant(BigInteger num, BigInteger den) {
     public static native int termProjIndex(int x);
     public static native int termProjArg(int x);
 
+    public static native byte[] sumComponentNumAsBytes(int x, int idx);
+    public static native byte[] sumComponentDenAsBytes(int x, int idx);
+    public static native int sumComponentTerm(int x, int idx);
+
+    public static native boolean[] bvSumComponentFactor(int x, int idx);
+    public static native int bvSumComponentTerm(int x, int idx);
+
+    public static SumComponent<?> sumComponent(int x, int idx) {
+        SumComponent<?> result = null;
+        if (Yices.termIsArithmetic(x)) {
+          byte[] num = sumComponentNumAsBytes(x, idx);
+          byte[] den = sumComponentDenAsBytes(x, idx);
+          int term = sumComponentTerm(x, idx);
+
+          if (num != null && den != null) {
+            result = new SumComponent<>(new BigRational(num, den), term);
+          }
+        }
+        if (Yices.termIsBitvector(x)) {
+          boolean[] factor = bvSumComponentFactor(x, idx);
+          int term = bvSumComponentTerm(x, idx);
+
+          if (factor != null) {
+            result = new SumComponent<>(factor, term);
+          }
+        }
+        return result;
+    }
+
+    public static native int productComponentTerm(int x, int idx);
+    public static native int productComponentPower(int x, int idx);
+
+    public static ProductComponent productComponent(int x, int idx) {
+        int power = productComponentPower(x, idx);
+        int term = productComponentTerm(x, idx);
+
+        if (term >= 0) {
+            return new ProductComponent(term, power);
+        } else {
+            return null;
+        }
+    }
+
     /*
      * Values of constant terms
      * To access the value of rational constants, we provide two functions: