Skip to content

Commit d906d07

Browse files
distephdisteph
committed
Merge branch 'pr-8'
2 parents 69bf2a7 + 5e4f35b commit d906d07

8 files changed

Lines changed: 330 additions & 12 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ public Status check(Parameters params, boolean buildModel) {
3535
int[] tarr = { 0 };
3636
long[] marr = { 0 };
3737
if (!buildModel) { marr = null; }
38-
int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params.getPtr(), marr, tarr);
38+
int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params == null ? 0 : params.getPtr(), marr, tarr);
3939
Status status = Status.idToStatus(code);
4040
if (status == Status.ERROR) {
4141
throw new YicesException();

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -398,7 +398,7 @@ public YVal[] expandTuple(YVal yval) throws YicesException {
398398

399399
public VectorValue expandFunction(YVal yval) throws YicesException {
400400
int n = Yices.valFunctionCardinality(ptr, yval.tag.ordinal(), yval.id);
401-
if (n <= 0) throw new YicesException();
401+
if (n < 0) throw new YicesException();
402402
YVal[] vector = new YVal[n];
403403
YVal[] value = new YVal[1];
404404
int code = Yices.valExpandFunction(ptr, yval.tag.ordinal(), yval.id, value, vector);

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package com.sri.yices;
2+
3+
public class ProductComponent {
4+
private final int power;
5+
private final int term;
6+
7+
public ProductComponent(int pTerm, int pPower) {
8+
power = pPower;
9+
term = pTerm;
10+
}
11+
12+
public int getTerm() {
13+
return term;
14+
}
15+
16+
public int getPower() {
17+
return power;
18+
}
19+
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package com.sri.yices;
2+
3+
public class SumComponent<T> {
4+
private final T factor;
5+
private final int term;
6+
7+
public SumComponent(T pFactor, int pTerm) {
8+
factor = pFactor;
9+
term = pTerm;
10+
}
11+
12+
public T getFactor() {
13+
return factor;
14+
}
15+
16+
public int getTerm() {
17+
return term;
18+
}
19+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1258,6 +1258,17 @@ static public int projArg(int x) throws YicesException {
12581258
return t;
12591259
}
12601260

1261+
static public SumComponent<?> projSum(int x, int idx) throws YicesException {
1262+
SumComponent<?> c = Yices.sumComponent(x, idx);
1263+
if (c == null) throw new YicesException();
1264+
return c;
1265+
}
1266+
1267+
static public ProductComponent projProduct(int x, int idx) throws YicesException {
1268+
ProductComponent c = Yices.productComponent(x, idx);
1269+
if (c == null) throw new YicesException();
1270+
return c;
1271+
}
12611272

12621273
/*
12631274
* Check whether term x is a constant

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

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,10 @@ public final class Yices {
1313
*/
1414
static {
1515
try {
16-
System.loadLibrary("yices2java");
16+
String skip = System.getProperty("yices.skipAutoloader", "false");
17+
if (!Boolean.parseBoolean(skip)) {
18+
System.loadLibrary("yices2java");
19+
}
1720
init();
1821
is_ready = true;
1922
} catch (LinkageError e) {
@@ -384,6 +387,49 @@ public static int mkRationalConstant(BigInteger num, BigInteger den) {
384387
public static native int termProjIndex(int x);
385388
public static native int termProjArg(int x);
386389

390+
public static native byte[] sumComponentNumAsBytes(int x, int idx);
391+
public static native byte[] sumComponentDenAsBytes(int x, int idx);
392+
public static native int sumComponentTerm(int x, int idx);
393+
394+
public static native boolean[] bvSumComponentFactor(int x, int idx);
395+
public static native int bvSumComponentTerm(int x, int idx);
396+
397+
public static SumComponent<?> sumComponent(int x, int idx) {
398+
SumComponent<?> result = null;
399+
if (Yices.termIsSum(x)) {
400+
byte[] num = sumComponentNumAsBytes(x, idx);
401+
byte[] den = sumComponentDenAsBytes(x, idx);
402+
int term = sumComponentTerm(x, idx);
403+
404+
if (num != null && den != null) {
405+
result = new SumComponent<>(new BigRational(num, den), term);
406+
}
407+
}
408+
if (Yices.termIsBvSum(x)) {
409+
boolean[] factor = bvSumComponentFactor(x, idx);
410+
int term = bvSumComponentTerm(x, idx);
411+
412+
if (factor != null) {
413+
result = new SumComponent<>(factor, term);
414+
}
415+
}
416+
return result;
417+
}
418+
419+
public static native int productComponentTerm(int x, int idx);
420+
public static native int productComponentPower(int x, int idx);
421+
422+
public static ProductComponent productComponent(int x, int idx) {
423+
int power = productComponentPower(x, idx);
424+
int term = productComponentTerm(x, idx);
425+
426+
if (term >= 0) {
427+
return new ProductComponent(term, power);
428+
} else {
429+
return null;
430+
}
431+
}
432+
387433
/*
388434
* Values of constant terms
389435
* To access the value of rational constants, we provide two functions:

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

Lines changed: 118 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2630,6 +2630,120 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_termProjArg(JNIEnv *env, jclass,
26302630
return yices_proj_arg(x);
26312631
}
26322632

2633+
JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentNumAsBytes(JNIEnv *env, jclass, jint x, jint idx) {
2634+
jbyteArray result = NULL;
2635+
mpq_t q;
2636+
jint t = -1;
2637+
2638+
mpq_init(q);
2639+
if (yices_sum_component(x, idx, q, &t) >= 0) {
2640+
result = mpz_to_byte_array(env, mpq_numref(q));
2641+
}
2642+
mpq_clear(q);
2643+
2644+
return result;
2645+
}
2646+
2647+
JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentDenAsBytes(JNIEnv *env, jclass, jint x, jint idx) {
2648+
jbyteArray result = NULL;
2649+
mpq_t q;
2650+
jint t = -1;
2651+
2652+
mpq_init(q);
2653+
if (yices_sum_component(x, idx, q, &t) >= 0) {
2654+
result = mpz_to_byte_array(env, mpq_denref(q));
2655+
}
2656+
mpq_clear(q);
2657+
2658+
return result;
2659+
}
2660+
2661+
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_sumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
2662+
jint result = -1;
2663+
mpq_t q;
2664+
2665+
mpq_init(q);
2666+
yices_sum_component(x, idx, q, &result);
2667+
mpq_clear(q);
2668+
2669+
return result;
2670+
}
2671+
2672+
JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvSumComponentFactor(JNIEnv *env, jclass, jint x, jint idx) {
2673+
jbooleanArray result = NULL;
2674+
jint t = -1;
2675+
2676+
int32_t n = yices_term_bitsize(x);
2677+
if (n < 0) {
2678+
return NULL;
2679+
}
2680+
2681+
if (n <= 64) {
2682+
// this should be the common case
2683+
int32_t a[64];
2684+
int32_t code = yices_bvsum_component(x, idx, a, &t);
2685+
if (code >= 0) {
2686+
result = convertToBoolArray(env, n, a);
2687+
}
2688+
2689+
} else {
2690+
try {
2691+
int32_t *tmp = new int32_t[n];
2692+
int32_t code = yices_bvsum_component(x, idx, tmp, &t);
2693+
if (code >= 0) {
2694+
result = convertToBoolArray(env, n, tmp);
2695+
}
2696+
delete [] tmp;
2697+
} catch (std::bad_alloc&) {
2698+
out_of_mem_exception(env);
2699+
}
2700+
}
2701+
2702+
return result;
2703+
}
2704+
2705+
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_bvSumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
2706+
jint result = -1;
2707+
2708+
int32_t n = yices_term_bitsize(x);
2709+
if (n < 0) {
2710+
return result;
2711+
}
2712+
2713+
if (n <= 64) {
2714+
// this should be the common case
2715+
int32_t a[64];
2716+
yices_bvsum_component(x, idx, a, &result);
2717+
2718+
} else {
2719+
try {
2720+
int32_t *tmp = new int32_t[n];
2721+
yices_bvsum_component(x, idx, tmp, &result);
2722+
delete [] tmp;
2723+
} catch (std::bad_alloc&) {
2724+
out_of_mem_exception(env);
2725+
}
2726+
}
2727+
2728+
return result;
2729+
}
2730+
2731+
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentTerm(JNIEnv *env, jclass, jint x, jint idx) {
2732+
uint32_t p = 0;
2733+
jint t = -1;
2734+
2735+
yices_product_component(x, idx, &t, &p);
2736+
return t;
2737+
}
2738+
2739+
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentPower(JNIEnv *env, jclass, jint x, jint idx) {
2740+
uint32_t p = 0;
2741+
jint t = -1;
2742+
2743+
yices_product_component(x, idx, &t, &p);
2744+
return p;
2745+
}
2746+
26332747
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_boolConstValue(JNIEnv *env, jclass, jint x) {
26342748
int32_t val;
26352749
jint result;
@@ -4577,7 +4691,6 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valFunctionCardinality(JNIEnv *e
45774691
JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, jclass cls, jlong mdl, jint tag, jint id, jobjectArray def, jobjectArray mappings){
45784692
yval_t yval;
45794693
int32_t cardinality;
4580-
jsize ndef;
45814694
jsize nmap;
45824695
int32_t code;
45834696
yval_t ydef;
@@ -4588,22 +4701,18 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, j
45884701
return -1;
45894702
}
45904703
cardinality = Java_com_sri_yices_Yices_valFunctionCardinality(env, cls, mdl, tag, id);
4591-
if (cardinality <= 0) {
4592-
return -2;
4593-
}
4594-
ndef = env->GetArrayLength(def);
4595-
if (ndef < 1) {
4596-
return -3;
4704+
if (cardinality < 0) {
4705+
return -1;
45974706
}
45984707

45994708
nmap = env->GetArrayLength(mappings);
46004709
if (nmap < cardinality) {
4601-
return -4;
4710+
return -1;
46024711
}
46034712
yices_init_yval_vector(&ymaps);
46044713
code = yices_val_expand_function(reinterpret_cast<model_t *>(mdl), &yval, &ydef, &ymaps);
46054714
if (code < 0) {
4606-
return -5;
4715+
return -1;
46074716
}
46084717

46094718
assert(static_cast<int32_t>(ymaps.size) == cardinality);

0 commit comments

Comments
 (0)