From 2e1d0fc0d4e452aa7f5ac247d3fa321011a2f359 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 15 May 2010 12:28:53 +0000
Subject: [PATCH] * 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
---
 src/parser/Makefile           |  1 +
 src/simplifier/simplifier.cpp | 53 ++++++++++++++++++++++++++++++++++-
 src/to-sat/ToSAT.cpp          |  6 ++++
 3 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 2e17c61..e4c6c12 100644
--- 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 467193b..bb75dac 100644
--- 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 72a23d8..994dca3 100644
--- 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);
-- 
2.47.3