@@ -72,7 +107,7 @@ private NativeUtils() {
* (restriction of {@link File#createTempFile(java.lang.String, java.lang.String)}).
* @throws FileNotFoundException If the file could not be found inside the JAR.
*/
- static void loadLibraryFromJar(String path) throws IOException {
+ public static void loadLibraryFromJar(String path) throws IOException {
if (null == path || !path.startsWith("/")) {
throw new IllegalArgumentException("The path has to be absolute (start with '/').");
diff --git a/src/main/java/org/jetbrains/research/boolector/TypeNode.java b/src/main/java/org/jetbrains/research/boolector/TypeNode.java
new file mode 100644
index 0000000..6b39c1e
--- /dev/null
+++ b/src/main/java/org/jetbrains/research/boolector/TypeNode.java
@@ -0,0 +1,7 @@
+package org.jetbrains.research.boolector;
+
+public enum TypeNode {
+ ARRAYNODE,
+ BOOLNODE,
+ BITVECNODE
+}
\ No newline at end of file
diff --git a/src/main/java/org/jetbrains/research/boolector/UninterpretedFunction.java b/src/main/java/org/jetbrains/research/boolector/UninterpretedFunction.java
new file mode 100644
index 0000000..6046ccb
--- /dev/null
+++ b/src/main/java/org/jetbrains/research/boolector/UninterpretedFunction.java
@@ -0,0 +1,19 @@
+package org.jetbrains.research.boolector;
+
+public class UninterpretedFunction extends BoolectorFunction {
+ private final String name;
+
+ private UninterpretedFunction(Btor btor, long ref, String name) {
+ super(btor, ref);
+ this.name = name;
+ }
+
+ public String getName() {
+ return name;
+ }
+
+ public static UninterpretedFunction func(String name, BoolectorSort sort) {
+ Btor btor = sort.getBtor();
+ return new UninterpretedFunction(btor, Native.uf(btor.getRef(), sort.ref, name), name);
+ }
+}
diff --git a/java/src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java b/src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java
similarity index 71%
rename from java/src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java
rename to src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java
index 8c2b970..80dcc35 100644
--- a/java/src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java
+++ b/src/test/java/org/jetbrains/research/boolector/BitvecSortTest.java
@@ -10,9 +10,9 @@ public class BitvecSortTest {
@Test
public void bitvecSort() {
Btor btor = new Btor();
- BitvecSort sort = BitvecSort.bitvecSort(8);
+ BitvecSort sort = BitvecSort.bitvecSort(btor, 8);
assertTrue(sort.isBitvecSort());
- assertEquals(8,sort.getWidth());
- btor.btorRelease();
+ assertEquals(8, sort.getWidth());
+ btor.release();
}
}
\ No newline at end of file
diff --git a/java/src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java b/src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java
similarity index 53%
rename from java/src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java
rename to src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java
index 6edddd8..a9e4449 100644
--- a/java/src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java
+++ b/src/test/java/org/jetbrains/research/boolector/BoolectorNodeTest.java
@@ -2,8 +2,6 @@
import org.junit.Test;
-import java.util.List;
-
import static org.junit.Assert.*;
public class BoolectorNodeTest {
@@ -11,17 +9,17 @@ public class BoolectorNodeTest {
@Test
public void bitvecNodeFirst() {
Btor btor = new Btor();
- BitvecSort sort = BitvecSort.bitvecSort(8);
+ BitvecSort sort = BitvecSort.bitvecSort(btor, 8);
BitvecNode x = BitvecNode.var(sort, "nullINc", true);
BitvecNode y = BitvecNode.var(sort, "nullINc", true);
BitvecNode ansXor = x.xor(y);
BitvecNode ansOr = andNot(x, y).or(andNot(y, x));
- BoolNode eq = ansXor.eq(ansOr); //fdskfdjsfkjdsklfjdskfjkldsjfkl
+ BoolNode eq = ansXor.eq(ansOr);
BoolNode formula = eq.not();
formula.assertForm();
- BoolectorSat.Status result = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.UNSAT, result);
- btor.btorRelease();
+ Btor.Status result = btor.check();
+ assertEquals(Btor.Status.UNSAT, result);
+ btor.release();
}
private BitvecNode andNot(BitvecNode x, BitvecNode y) {
@@ -31,7 +29,7 @@ private BitvecNode andNot(BitvecNode x, BitvecNode y) {
@Test
public void bitvecNodeSecond() {
Btor btor = new Btor();
- BitvecSort sort = BitvecSort.bitvecSort(8);
+ BitvecSort sort = BitvecSort.bitvecSort(btor, 8);
BitvecNode x = BitvecNode.var(sort, "nullINc", true);
BitvecNode y = BitvecNode.var(sort, "nullINc", true);
BitvecNode zero = BitvecNode.zero(sort);
@@ -39,52 +37,50 @@ public void bitvecNodeSecond() {
BoolNode ySgtZero = y.sgt(zero);
BoolNode varsSgtZero = xSgtZero.and(ySgtZero);
- BitvecNode add = x.add(y); // saddo???
+ BitvecNode add = x.add(y);
BoolNode addSgtZero = add.sgt(zero);
BoolNode overflow = add.sgt(x);
BoolNode varsSgt = varsSgtZero.and(overflow);
BoolNode ans = varsSgt.implies(addSgtZero);
- BoolectorSat.simplify();
- assertFormuls(btor, ans);
+ btor.simplify();
+ assertFormulae(btor, ans);
}
@Test
public void BitveNodeTest() {
Btor btor = new Btor();
- BitvecNode x, y, longConst, sext, uext, slice, neg, add, sub, mul, sdiv, udiv, smod, urem, sll, srl, sra, concat;
- BoolNode sgt, sgte, slt, slte;
- x = BitvecNode.constBitvec("000101");
- y = BitvecNode.constBitvec("000011");
- BitvecSort long_sort = BitvecSort.bitvecSort(64);
- longConst = BitvecNode.constLong(3000000000L, long_sort);
-
-
- sext = x.sext(10);
- uext = x.uext(10);
- slice = x.slice(2, 0);
- neg = x.neg();
- add = x.add(y);
- sub = x.sub(y);
- mul = x.mul(y);
- sdiv = x.sdiv(y);
- udiv = x.udiv(y);
- smod = x.smod(y);
- urem = x.urem(y);
- sgt = x.sgt(y);
- sgte = x.sgte(y);
- slt = x.slt(y);
- slte = x.slte(y);
- sll = x.sll(y);
- srl = x.srl(y);
- sra = x.sra(y);
- concat = x.concat(y);
- BitvecNode var = BitvecNode.var(long_sort, "test", false);
- BitvecNode noFresh = BitvecNode.var(long_sort, "test", false);
- x = BitvecNode.constInt(-5, long_sort);
- BoolectorSat.getBoolectorSat();
+ BitvecNode x = BitvecNode.constBitvec(btor, "000101");
+ BitvecNode y = BitvecNode.constBitvec(btor, "000011");
+ BitvecSort longSort = BitvecSort.bitvecSort(btor, 64);
+ BitvecNode longConst = BitvecNode.constLong(3000000000L, longSort);
+
+
+ BitvecNode sext = x.sext(10);
+ BitvecNode uext = x.uext(10);
+ BitvecNode slice = x.slice(2, 0);
+ BitvecNode neg = x.neg();
+ BitvecNode add = x.add(y);
+ BitvecNode sub = x.sub(y);
+ BitvecNode mul = x.mul(y);
+ BitvecNode sdiv = x.sdiv(y);
+ BitvecNode udiv = x.udiv(y);
+ BitvecNode smod = x.smod(y);
+ BitvecNode urem = x.urem(y);
+ BoolNode sgt = x.sgt(y);
+ BoolNode sgte = x.sgte(y);
+ BoolNode slt = x.slt(y);
+ BoolNode slte = x.slte(y);
+ BitvecNode sll = x.sll(y);
+ BitvecNode srl = x.srl(y);
+ BitvecNode sra = x.sra(y);
+ BitvecNode concat = x.concat(y);
+ BitvecNode var = BitvecNode.var(longSort, "test", false);
+ BitvecNode noFresh = BitvecNode.var(longSort, "test", false);
+ x = BitvecNode.constInt(-5, longSort);
+ btor.check();
long assignment = x.assignment();
- BoolNode test = BoolNode.constBool(true);
+ BoolNode test = BoolNode.constBool(btor, true);
boolectorAssert("0000000000000000000000000000000010110010110100000101111000000000", longConst);
boolectorAssert("0000000101", sext);
boolectorAssert("0000000101", uext);
@@ -108,96 +104,82 @@ public void BitveNodeTest() {
assertEquals(-5, assignment);
assertEquals(var.ref, noFresh.ref);
assertTrue(test.assigment());
- btor.btorRelease();
+ btor.release();
}
@Test
public void BoolNodeTest() {
Btor btor = new Btor();
- BoolNode x, y, or, xor, iff;
- x = BoolNode.constBool(true);
- y = BoolNode.constBool(false);
- or = x.or(y);
- xor = x.xor(y);
- iff = x.iff(y);
- BoolectorSat.getBoolectorSat();
+ BoolNode x = BoolNode.constBool(btor, true);
+ BoolNode y = BoolNode.constBool(btor, false);
+ BoolNode or = x.or(y);
+ BoolNode xor = x.xor(y);
+ BoolNode iff = x.iff(y);
+ btor.check();
boolectorAssert("1", or);
boolectorAssert("1", xor);
boolectorAssert("0", iff);
- btor.btorRelease();
+ btor.release();
}
@Test
public void boolectorNodeTest() {
Btor btor = new Btor();
- BoolectorNode x, y, bool, bitvec, ite;
- x = BitvecNode.constBitvec("000101");
- y = BitvecNode.constBitvec("000011");
+ BoolectorNode x = BitvecNode.constBitvec(btor, "000101");
+ BoolectorNode y = BitvecNode.constBitvec(btor, "000011");
- bool = BitvecNode.constBitvec("1");
- ite = x.ite(bool.toBoolNode(), y);
- BoolectorSort getSort = x.getSort();
- bitvec = BitvecNode.var(getSort.toBitvecSort(), "test", false);
+ BoolNode bool = BoolNode.constBool(btor, true);
+ BoolectorNode ite = x.ite(bool, y);
+ BoolectorNode bitvec = BitvecNode.var((BitvecSort) x.getSort(), "test", false);
x.getID();
- BoolectorSat.getBoolectorSat();
+ btor.check();
boolectorAssert("000101", ite);
assertEquals("test", bitvec.getSymbol());
assertFalse(x.isBoolNode());
assertTrue(bitvec.isBitvecNode());
- int i = 0;
- try {
- bitvec.toArrayNode();
- } catch (ClassCastException e) {
- ++i;
- }
- assertEquals(1, i);
-
- btor.btorRelease();
+ btor.release();
}
@Test
- public void printerTest() {
+ public void tempFiles() {
Btor btor = new Btor();
- BoolNode x = BoolNode.constBool(true);
+ BoolNode x = BoolNode.constBool(btor, true);
x.assertForm();
- BoolectorSat.getBoolectorSat();
- assertEquals("(\n)", btor.printModel());
+ btor.check();
+ assertEquals("(model )\n", btor.printModel());
assertEquals("(set-logic QF_BV)\n" +
"(assert true)\n" +
"(check-sat)\n" +
- "(exit)", btor.dumpSmt2());
- btor.btorRelease();
+ "(exit)\n", btor.dumpSmt2());
+ btor.release();
}
@Test
public void arrayNodeTest() {
Btor btor = new Btor();
- BitvecNode x, i, j;
- ArrayNode arrayConst, array;
- BitvecSort index;
- x = BitvecNode.constBitvec("000101");
- i = BitvecNode.constBitvec("000000");
- j = BitvecNode.constBitvec("100000");
+ BitvecNode x = BitvecNode.constBitvec(btor, "000101");
+ BitvecNode i = BitvecNode.constBitvec(btor, "000000");
+ BitvecNode j = BitvecNode.constBitvec(btor, "100000");
- index = x.getSort().toBitvecSort();
+ BitvecSort index = (BitvecSort) x.getSort();
ArraySort sort = ArraySort.arraySort(index, index);
- array = ArrayNode.arrayNode(sort, "Temp");
+ ArrayNode array = ArrayNode.arrayNode(sort, "Temp");
- arrayConst = ArrayNode.constArrayNode(index, x);
+ ArrayNode arrayConst = ArrayNode.constArrayNode(index, x);
BoolNode eq = arrayConst.read(i).eq(arrayConst.read(j));
- BoolectorSat.getBoolectorSat();
+ btor.check();
boolectorAssert("1", eq);
- btor.btorRelease();
+ btor.release();
}
@Test
public void arrayNodeTest1() {
Btor btor = new Btor();
- BitvecSort sortIndex = BitvecSort.bitvecSort(3);
- BitvecSort sortElem = BitvecSort.bitvecSort(8);
+ BitvecSort sortIndex = BitvecSort.bitvecSort(btor, 3);
+ BitvecSort sortElem = BitvecSort.bitvecSort(btor, 8);
ArraySort sortArray = ArraySort.arraySort(sortIndex, sortElem);
BitvecNode[] indices = new BitvecNode[8];
@@ -211,7 +193,7 @@ public void arrayNodeTest1() {
for (int i = 1; i < 8; i++) {
read = array.read(indices[i]);
BoolNode ugt = read.ugt(max);
- BitvecNode temp = read.ite(ugt, max).toBitvecNode();
+ BitvecNode temp = (BitvecNode) read.ite(ugt, max);
max.release();
max = temp;
read.release();
@@ -223,17 +205,17 @@ public void arrayNodeTest1() {
BoolNode formula = read.ugt(max);
formula.assertForm();
- BoolectorSat.Status result = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.UNSAT, result);
- btor.btorRelease();
+ Btor.Status result = btor.check();
+ assertEquals(Btor.Status.UNSAT, result);
+ btor.release();
}
@Test
public void arrayNodeTest2() {
Btor btor = new Btor();
- BitvecSort sortIndex = BitvecSort.bitvecSort(1);
- BitvecSort sortElem = BitvecSort.bitvecSort(8);
+ BitvecSort sortIndex = BitvecSort.bitvecSort(btor, 1);
+ BitvecSort sortElem = BitvecSort.bitvecSort(btor, 8);
ArraySort sortArray = ArraySort.arraySort(sortIndex, sortElem);
ArrayNode array = ArrayNode.arrayNode(sortArray, null);
@@ -244,25 +226,25 @@ public void arrayNodeTest2() {
BoolectorNode eq = index1.eq(index2);
BoolectorNode ne = read1.eq(read2).not();
eq.assertForm();
- BoolectorSat.Status result = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.SAT, result);
+ Btor.Status result = btor.check();
+ assertEquals(Btor.Status.SAT, result);
ne.assume();
- result = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.UNSAT, result);
- result = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.SAT, result);
- btor.btorRelease();
+ result = btor.check();
+ assertEquals(Btor.Status.UNSAT, result);
+ result = btor.check();
+ assertEquals(Btor.Status.SAT, result);
+ btor.release();
}
- private static void assertFormuls(Btor btor, BoolNode node) {
+ private static void assertFormulae(Btor btor, BoolNode node) {
BoolNode formula = node.not();
formula.assertForm();
- BoolectorSat.Status ans = BoolectorSat.getBoolectorSat();
- assertEquals(BoolectorSat.Status.UNSAT, ans);
- btor.btorRelease();
+ Btor.Status ans = btor.check();
+ assertEquals(Btor.Status.UNSAT, ans);
+ btor.release();
}
private static void boolectorAssert(String ans, BoolectorNode node) {
- assertTrue(Native.boolectorAssert(ans, node.ref));
+ assertTrue(Native.boolectorAssert(node.getBtor().getRef(), ans, node.ref));
}
-}
+}
\ No newline at end of file
diff --git a/src/test/java/org/jetbrains/research/boolector/FunctionDeclTest.java b/src/test/java/org/jetbrains/research/boolector/FunctionDeclTest.java
new file mode 100644
index 0000000..84a7171
--- /dev/null
+++ b/src/test/java/org/jetbrains/research/boolector/FunctionDeclTest.java
@@ -0,0 +1,42 @@
+package org.jetbrains.research.boolector;
+
+import org.junit.Test;
+
+import java.util.Arrays;
+import java.util.List;
+
+import static junit.framework.TestCase.assertEquals;
+
+public class FunctionDeclTest {
+
+ @Test
+ public void testAll() {
+ Btor btor = new Btor();
+ BitvecSort sort = BitvecSort.bitvecSort(btor, 8);
+ BitvecNode x = BitvecNode.var(sort, "x", true);
+ BitvecNode y = BitvecNode.var(sort, "y", true);
+ BitvecNode a = BitvecNode.constInt(10, sort);
+ BitvecNode b = BitvecNode.constInt(20, sort);
+ a.add(b);
+
+ BitvecNode temp = x.add(y);
+ FunctionDecl.FunctionParam firstParam = FunctionDecl.FunctionParam.param(sort, null);
+ FunctionDecl.FunctionParam secondParam = FunctionDecl.FunctionParam.param(sort, null);
+ List