git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk...

diff --git a/Makefile b/Makefile
index f7d8638776216d73ade19f718ff42015ddeb044d..9b84ae47f1c04c304af5a284f772a6dcb51e826c 100644 (file)
--- 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 f7d8638776216d73ade19f718ff42015ddeb044d..9b84ae47f1c04c304af5a284f772a6dcb51e826c 100644 (file)
--- 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 3cecef53a006a3869895d9e4cb7d58ee08873bf1..bbc0218dc7deb2171cf082f41fd190700f7a95bf 100644 (file)
--- 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 9ad8664e9ac7b7feff9ccb5389e2d7370d09ec74..5d7570801b6a44163450ad2fc21f54a1eaa96833 100644 (file)
--- 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));
-
        //########################################
        //########################################