Bugfix. Thanks to Jingyue Wu for reporting sbvdiv was broken through the c-api.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1367 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 8c961098c2f54297af322ee3cc5b2663036469c1..8f8ebeb140a76e399e6d90575e647c9c9cb266c2 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -176,6 +176,12 @@ VC vc_createValidityChecker(void) {
                   bvsolver, arrayTransformer, 
                   tosat, Ctr_Example);
   
+  // This expects the simplifying node factory to be used to create all the nodes.
+  // i.e. for sbvdiv to be transformed away. The c-interface uses the hashing node
+  // factory. I tried to enable the simplfyingnode factory. But some c-api-tests
+  // failed with assertion errors.
+  bm->UserFlags.set("bitblast-simplification","0");
+
   BEEV::GlobalSTP = stp;
   decls = new BEEV::ASTVec();
   //created_exprs.clear();

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index e5392f7cd058ed6fb1239a63fc279e9d00605093..0b9fda4e94f48d940f10941210dcd5ac2cfd89fd 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -43,7 +43,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23
        g++  $(CXXFLAGS) push-pop-1.c  -o a7.out $(LIBS)
        ./a7.out
 8:
-       g++  $(CXXFLAGS)  sbvmod.c  -o a8.out $(LIBS)
+       g++  $(CXXFLAGS)  sbvdiv.c  -o a8.out $(LIBS)
        ./a8.out
 9:
        g++  $(CXXFLAGS)  simplify.c -o a9.out $(LIBS) 

diff --git a/tests/c-api-tests/sbvdiv.c b/tests/c-api-tests/sbvdiv.c
new file mode 100644 (file)
index 0000000..b1f5dad
--- /dev/null
+++ b/tests/c-api-tests/sbvdiv.c
@@ -0,0 +1,19 @@
+#include "c_interface.h"
+#include <stdio.h>
+#include <iostream>
+
+int main() {
+    VC vc = vc_createValidityChecker();
+    vc_setFlags(vc, 'p');
+
+    Type int_type = vc_bv32Type(vc);
+    Expr zero = vc_bv32ConstExprFromInt(vc, 0);
+    Expr int_max = vc_bvConstExprFromInt(vc, 32, 0x7fffffff);
+    Expr a = vc_varExpr(vc, "a", int_type);
+    Expr b = vc_varExpr(vc, "b", int_type);
+    vc_assertFormula(vc, vc_sbvGtExpr(vc, b, zero));
+    vc_assertFormula(vc, vc_sbvLeExpr(vc, a, vc_sbvDivExpr(vc, 32,int_max, b)));
+    std::cout << vc_query(vc, vc_falseExpr(vc)) << std::endl;
+}
+
+

diff --git a/tests/c-api-tests/sbvmod.c b/tests/c-api-tests/sbvmod.c
deleted file mode 100644 (file)
index 3ab5e52..0000000
--- a/tests/c-api-tests/sbvmod.c
+++ /dev/null
@@ -1,5 +0,0 @@
-#include <stdio.h>
-main() {
- signed x = -1 % -1;
- printf("output is %i \n",x);
-}