Interface Change. The c-interface now uses the simplifying node factory.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index ea70aa297947109fa5830cf51c53cc64e7505135..faa0c7f57af69f2a196c5b467be7f9b8a068cd15 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -39,7 +39,7 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
 
        // If all the parameters are constant, return the constant value.
        // The bitblaster calls CreateNode with a boolean vector. We don't try to simplify those.
-       if (kind != BEEV::UNDEFINED)
+       if (kind != BEEV::UNDEFINED && kind != BEEV::BITVECTOR && kind != BEEV::ARRAY)
        {
                bool allConstant = true;
 

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 8f8ebeb140a76e399e6d90575e647c9c9cb266c2..6d38a3fc81ebe35d1b350e4ea92249aadcfe896e 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -26,6 +26,7 @@ typedef BEEV::AbsRefine_CounterExample * ctrexamplestar;
 typedef BEEV::ASTVec                     nodelist;
 typedef BEEV::CompleteCounterExample*    CompleteCEStar;
 BEEV::ASTVec *decls = NULL;
+SimplifyingNodeFactory *simpNF = NULL;
 //vector<BEEV::ASTNode *> created_exprs;
 
 // persist holds a copy of ASTNodes so that the reference count of
@@ -176,11 +177,8 @@ 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");
+  simpNF = new SimplifyingNodeFactory(*(bm->hashingNodeFactory), *bm);
+  bm->defaultNodeFactory = simpNF;
 
   BEEV::GlobalSTP = stp;
   decls = new BEEV::ASTVec();
@@ -1911,6 +1909,7 @@ void vc_Destroy(VC vc) {
   BEEV::GlobalSTP = NULL;
   delete  BEEV::ParserBM;
   BEEV::ParserBM = NULL;
+  delete simpNF;
 }
 
 void vc_DeleteExpr(Expr e) {

diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
index 7b740b51f6b8b9f529c07e018370f4f6b3bed0fa..bb10cd963432b7ae6f0f47d18403d8c1b1eac292 100644 (file)
--- a/src/simplifier/EstablishIntervals.h
+++ b/src/simplifier/EstablishIntervals.h
@@ -307,7 +307,7 @@ namespace BEEV
       if (fromTo.size() > 0)
         {
           ASTNodeMap cache;
-          SimplifyingNodeFactory nf(*(top.GetSTPMgr()->defaultNodeFactory), *top.GetSTPMgr());
+          SimplifyingNodeFactory nf(*(top.GetSTPMgr()->hashingNodeFactory), *top.GetSTPMgr());
           bm.GetRunTimes()->stop(RunTimes::IntervalPropagation);
           return SubstitutionMap::replace(result,fromTo,cache,&nf);
         }

diff --git a/tests/c-api-tests/interface-check.c b/tests/c-api-tests/interface-check.c
index 07c52ddb21fb1a1a5deb64b7fa12429323810168..4e17e574042fb62ffef7e6282bf419abab4a3676 100644 (file)
--- a/tests/c-api-tests/interface-check.c
+++ b/tests/c-api-tests/interface-check.c
@@ -12,9 +12,6 @@ int main(int argc, char * argv [])
   ::Expr b2 = ::vc_falseExpr(vc);
   ::Expr andExpr = ::vc_andExpr(vc, b1, b2);
 
-  if(::getExprKind(andExpr) !=  ::AND )
-       throw new std::runtime_error("sadfas");
-
   ::Expr simplifiedExpr = ::vc_simplify(vc, andExpr);
 
        if (getExprKind(simplifiedExpr) !=  ::FALSE )