* Convert BVAND( ite(p,1,1) , ite(p2,0,1)) to ite(p and p2, 0,1).

* Add back simplify() for minisat.

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

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 2e17c61db3826d4883f4fe09fa617d6626d363e7..e4c6c12e5e9f580167666f6bfe0d5e6954004d94 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -10,6 +10,7 @@ LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitve
 CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
 
 libparser.a: $(OBJS)
+       rm -f $@
        $(AR) rc $@ $^
        $(RANLIB) $@
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 467193b3263eb3c2ef3e7614d7aa12d9c7be2d11..bb75dac6685b2f433854758e168b9114fbbf0520 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -28,7 +28,23 @@ namespace BEEV
     return n;
   }
 
-
+  // is it ITE(p,bv0[1], bv1[1])  OR  ITE(p,bv0[0], bv1[0])
+  bool isPropositionToTerm(const ASTNode& n)
+  {
+       if (n.GetType() != BITVECTOR_TYPE)
+               return false;
+       if (n.GetValueWidth() != 1)
+               return false;
+       if (n.GetKind() != ITE)
+               return false;
+       if (!n[1].isConstant())
+               return false;
+       if (!n[2].isConstant())
+               return false;
+       if (n[1] == n[0])
+               return false;
+       return true;
+  }
 
   bool Simplifier::CheckMap(ASTNodeMap* VarConstMap, 
                             const ASTNode& key, ASTNode& output)
@@ -2109,6 +2125,41 @@ namespace BEEV
                 }
               break;
             }
+
+          // This don't make it faster, just makes the graphs easier to understand.
+                       if (output.GetKind() == BVAND)
+                       {
+                               assert(output.Degree() != 0);
+                               bool allconv = true;
+                               for (ASTVec::const_iterator it = output.begin(), itend =
+                                               output.end(); it != itend; it++)
+                               {
+                                       if (!isPropositionToTerm(*it))
+                                       {
+                                               allconv = false;
+                                               break;
+                                       }
+                               }
+                               if (allconv)
+                               {
+                                       const ASTNode zero = _bm->CreateZeroConst(1);
+                                       ASTVec children;
+                                       for (ASTVec::const_iterator it = output.begin(), itend =
+                                                       output.end(); it != itend; it++)
+                                       {
+                                               const ASTNode& n = *it;
+
+                                               if (n[1] == zero)
+                                                       children.push_back(_bm->CreateNode(NOT, n[0]));
+                                               else
+                                                       children.push_back(n[0]);
+                                       }
+                                       output = _bm->CreateTerm(ITE, 1,
+                                                       _bm->CreateNode(AND, children), _bm->CreateOneConst(1),
+                                                       zero);
+                                       assert(BVTypeCheck(output));
+                               }
+                       }
           break;
         }
       case BVCONCAT:

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 72a23d8c4eaf5d5ce1663ddba765da705b10b7ce..994dca37592006daa312f2901aa4afe7d279b6e3 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -221,6 +221,12 @@ namespace BEEV
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);    
+
+    #ifdef CORE
+    // The call to simplify() was removed. I'm guessing because it didn't work well with cryptominisat.
+    // so I'm only enabling it for just minisat.
+               newSolver.simplify();
+       #endif
     newSolver.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newSolver);