diff --git a/build.xml b/build.xml
index 8dceaf6..e77e7b6 100644
--- a/build.xml
+++ b/build.xml
@@ -223,7 +223,7 @@
Executing "make ${library}" in ${code}
+ failonerror="true">
@@ -233,7 +233,7 @@
+ failonerror="true">
@@ -250,7 +250,7 @@
+ failonerror="true">
diff --git a/src/main/java/com/sri/yices/Constructor.java b/src/main/java/com/sri/yices/Constructor.java
index 665436b..9e3bc70 100644
--- a/src/main/java/com/sri/yices/Constructor.java
+++ b/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 {
diff --git a/src/main/java/com/sri/yices/Context.java b/src/main/java/com/sri/yices/Context.java
index 53ac5b6..6803df5 100644
--- a/src/main/java/com/sri/yices/Context.java
+++ b/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) {
diff --git a/src/main/java/com/sri/yices/InterpolationContext.java b/src/main/java/com/sri/yices/InterpolationContext.java
index 2865ed5..d1a1e8a 100644
--- a/src/main/java/com/sri/yices/InterpolationContext.java
+++ b/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();
diff --git a/src/main/java/com/sri/yices/Model.java b/src/main/java/com/sri/yices/Model.java
index bcd710f..5cbab09 100644
--- a/src/main/java/com/sri/yices/Model.java
+++ b/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);
diff --git a/src/main/java/com/sri/yices/ProductComponent.java b/src/main/java/com/sri/yices/ProductComponent.java
new file mode 100644
index 0000000..94d6b20
--- /dev/null
+++ b/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;
+ }
+}
diff --git a/src/main/java/com/sri/yices/SumComponent.java b/src/main/java/com/sri/yices/SumComponent.java
new file mode 100644
index 0000000..12658de
--- /dev/null
+++ b/src/main/java/com/sri/yices/SumComponent.java
@@ -0,0 +1,19 @@
+package com.sri.yices;
+
+public class SumComponent {
+ 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;
+ }
+}
diff --git a/src/main/java/com/sri/yices/Terms.java b/src/main/java/com/sri/yices/Terms.java
index 1f2745c..b096a27 100644
--- a/src/main/java/com/sri/yices/Terms.java
+++ b/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
diff --git a/src/main/java/com/sri/yices/YValTag.java b/src/main/java/com/sri/yices/YValTag.java
index eb43561..a960762 100644
--- a/src/main/java/com/sri/yices/YValTag.java
+++ b/src/main/java/com/sri/yices/YValTag.java
@@ -13,6 +13,7 @@ public enum YValTag {
BOOL,
RATIONAL,
ALGEBRAIC,
+ FINITEFIELD,
BV,
SCALAR,
TUPLE,
diff --git a/src/main/java/com/sri/yices/Yices.java b/src/main/java/com/sri/yices/Yices.java
index cf628da..ea39201 100644
--- a/src/main/java/com/sri/yices/Yices.java
+++ b/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:
diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp
index 27290e2..03b8e30 100644
--- a/src/main/java/com/sri/yices/yicesJNI.cpp
+++ b/src/main/java/com/sri/yices/yicesJNI.cpp
@@ -2630,6 +2630,116 @@ 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;
+ 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);
+ assert(n >= 0);
+
+ 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);
+
+ } 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);
+ 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);
+ assert(n >= 0);
+
+ 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);
+
+ } else {
+ try {
+ int32_t *tmp = new int32_t[n];
+ int32_t code = yices_bvsum_component(x, idx, tmp, &result);
+ assert(code >= 0);
+ 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;
@@ -2674,7 +2784,7 @@ JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvConstValue(JNIEnv *en
assert(code >= 0);
result = convertToBoolArray(env, n, tmp);
delete [] tmp;
- } catch (std::bad_alloc) {
+ } catch (std::bad_alloc&) {
out_of_mem_exception(env);
}
}
@@ -3215,10 +3325,10 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithInterpolation(JN
ctx.model = NULL;
try {
result = yices_check_context_with_interpolation(&ctx, reinterpret_cast(params), build_model);
- if (result == STATUS_UNSAT) {
+ if (result == YICES_STATUS_UNSAT) {
// set the interpolant array
env->SetIntArrayRegion(interpolant, 0, 1, &ctx.interpolant);
- } else if(build_model && result == STATUS_SAT ) {
+ } else if(build_model && result == YICES_STATUS_SAT ) {
model_t *model = ctx.model;
jlong mdl = reinterpret_cast(model);
// set the model array
@@ -3817,7 +3927,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormula(JNIEnv *env, jclass
}
if (wantModel) {
code = yices_check_formula(formula, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
@@ -3873,7 +3983,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormulas(JNIEnv *env, jclas
}
if (wantModel) {
code = yices_check_formulas(tarr, n, ls, &model, ds);
- if (code == STATUS_SAT) {
+ if (code == YICES_STATUS_SAT) {
mdl = reinterpret_cast(model);
env->SetLongArrayRegion(marr, 0, 1, &mdl);
}
@@ -4577,7 +4687,6 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valFunctionCardinality(JNIEnv *e
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, jclass cls, jlong mdl, jint tag, jint id, jobjectArray def, jobjectArray mappings){
yval_t yval;
int32_t cardinality;
- jsize ndef;
jsize nmap;
int32_t code;
yval_t ydef;
@@ -4588,22 +4697,18 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, j
return -1;
}
cardinality = Java_com_sri_yices_Yices_valFunctionCardinality(env, cls, mdl, tag, id);
- if (cardinality <= 0) {
- return -2;
- }
- ndef = env->GetArrayLength(def);
- if (ndef < 1) {
- return -3;
+ if (cardinality < 0) {
+ return -1;
}
nmap = env->GetArrayLength(mappings);
if (nmap < cardinality) {
- return -4;
+ return -1;
}
yices_init_yval_vector(&ymaps);
code = yices_val_expand_function(reinterpret_cast(mdl), &yval, &ydef, &ymaps);
if (code < 0) {
- return -5;
+ return -1;
}
assert(static_cast(ymaps.size) == cardinality);