From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 21 Aug 2009 23:10:21 +0000 (+0000)
Subject: git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=31f3b5e6da0635110e911e8632358f3d995576b1;p=francis%2Fstp.git

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

diff --git a/Makefile b/Makefile
index f7d8638..9b84ae4 100644
--- a/Makefile
+++ b/Makefile
@@ -18,7 +18,7 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
 	$(MAKE) -C $(SRC)/AST
-	$(MAKE) -C $(SRC)/sat core
+	$(MAKE) -C $(SRC)/sat simp
 	$(MAKE) -C $(SRC)/simplifier
 	$(MAKE) -C $(SRC)/bitvec
 	$(MAKE) -C $(SRC)/c_interface
diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index f7d8638..9b84ae4 100644
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -18,7 +18,7 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
 	$(MAKE) -C $(SRC)/AST
-	$(MAKE) -C $(SRC)/sat core
+	$(MAKE) -C $(SRC)/sat simp
 	$(MAKE) -C $(SRC)/simplifier
 	$(MAKE) -C $(SRC)/bitvec
 	$(MAKE) -C $(SRC)/c_interface
diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index 3cecef5..bbc0218 100644
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -1186,7 +1186,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
 
 	int res;
 	//solver instantiated here
-	MINISAT::Solver newS;
+	MINISAT::SimpSolver newS;
 	if (arrayread_refinement_flag)
 	{
 		counterexample_checking_during_refinement = true;
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 9ad8664..5d75708 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -140,7 +140,7 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b)
 	//a is of the form var, and b is const
 	if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && 
 	     (k2 == BVCONST)))
-	  // || 
+// 	      || 
 // 	      k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
 		return 1;
 
@@ -209,8 +209,8 @@ ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg)
 
 ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
 {
-	if (!optimize_flag)
-		return b;
+  if (!optimize_flag)
+    return b;
 
 	Kind kind = b.GetKind();
 	if (BOOLEAN_TYPE != b.GetType())
@@ -275,9 +275,8 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
 ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg)
 {
 	if (!optimize_flag)
-	{
-		return a;
-	}
+	  return a;
+
 
 	ASTNode output;
 	if (CheckSimplifyMap(a, output, pushNeg))
@@ -645,10 +644,10 @@ ASTNode BeevMgr::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2)
 	Kind k1 = in1.GetKind();
 	Kind k2 = in2.GetKind();
 
-	if (!optimize_flag)
-	{
-		return CreateNode(EQ, in1, in2);
-	}
+	// if (!optimize_flag)
+// 	{
+// 		return CreateNode(EQ, in1, in2);
+// 	}
 
 	if (in1 == in2)
 		//terms are syntactically the same
@@ -1110,7 +1109,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg)
 ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg)
 {
 	if (!optimize_flag)
-		return b;
+	  return b;
 
 	ASTNode output;
 	if (CheckSimplifyMap(b, output, pushNeg))
@@ -1246,12 +1245,12 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm)
 	//cout << "SimplifyTerm: input: " << a << endl;
 	if (!optimize_flag)
 	{
-		return inputterm;
+	  return inputterm;
 	}
 
+	
 	ASTNode output;
 	assert(BVTypeCheck(inputterm));
-
 	//########################################
 	//########################################