Speedups.

* The substitution map now substitutes for (IFF SYMBOL SYMBOL)
* sim.smt2 is the test case to check the above substitution is working.
* The ArrayTransformer creates fewer new nodes.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index d998c76abee0792b1c1564747a2c99cc1cccaae7..e5f26018f2fe0d2ce85d3093bf116977fbf91b22 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -435,8 +435,13 @@ namespace BEEV
               o.push_back(TransformTerm(*it));
             }
 
-          result = nf->CreateTerm(k, width, o);
-          result.SetIndexWidth(indexwidth);
+          if (c!=o)
+          {
+                 result = nf->CreateTerm(k, width, o);
+                         result.SetIndexWidth(indexwidth);
+          }
+          else
+                 result = term;
 
           const Kind k = result.GetKind();
 

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 4f7ca98ec22cbeef9bf3a3d2abd30074795c6a5b..18a3e463ca79ec62062f2a773891906b8814d13b 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -38,7 +38,7 @@ int TermOrder(const ASTNode& a, const ASTNode& b)
     // == BVCONST)))
     return 1;
 
-  if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
+  if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2 || SYMBOL ==k2))
     return 1;
 
   //b is of the form READ(Arr,const), and a is const, or
@@ -52,14 +52,23 @@ int TermOrder(const ASTNode& a, const ASTNode& b)
   if (SYMBOL == k2
       && (BVCONST == k1
           || TRUE == k1
-          || FALSE == k1))
+          || FALSE == k1
+          || SYMBOL == k1
+      ))
     return -1;
 
   return 0;
 } //End of TermOrder()
 
 
-//This finds everything which is (= SYMBOL BVCONST) and everything that is (READ SYMBOL BVCONST).
+//This finds everything which is: (= SYMBOL BVCONST), (READ SYMBOL BVCONST),
+// (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
+// or (=SYMBOL BVCONST).
+// The bvsolver goes to a lot more trouble to make similar substitutions, the
+// main advantage that the below function has is that it doesn't need to check
+// (much) if the symbol being substituted for is on the RHS.
+//The UpdateSubstitionMap() function does all the checking that's needed.
+//
 //i.e. anything that has a termorder of 1 or -1.
 // The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap.
 
@@ -91,8 +100,11 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
 
   if (IFF == k || EQ == k)
     {
-      ASTVec c = a.GetChildren();
-      SortByArith(c);
+         ASTVec c = a.GetChildren();
+         SortByArith(c);
+
+         if (c[0] == c[1])
+                 return ASTTrue;
 
       ASTNode c1;
       if (EQ == k)

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index df03da09949acc21581768184252312015f5f5df..dff8db1c7e662f809a1d64100f54a9575b11b8c8 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -84,11 +84,21 @@ public:
                assert(e0.GetValueWidth() == e1.GetValueWidth());
                assert(e0.GetIndexWidth() == e1.GetIndexWidth());
 
+               if (SYMBOL == e1.GetKind() && CheckSubstitutionMap(e1))
+               {
+                       // if we didn't check this, scenarios like:
+                       // a <-> b
+                       // b <-> a
+                       // would cause a loop.
+                       return false;
+               }
+
                //e0 is of the form READ(Arr,const), and e1 is const, or
                //e0 is of the form var, and e1 is const
                if (1 == i && !CheckSubstitutionMap(e0)) {
                        assert((e1.GetKind() == TRUE) ||
                                        (e1.GetKind() == FALSE) ||
+                                       (e1.GetKind() == SYMBOL) ||
                                        (e1.GetKind() == BVCONST));
                        (*SolverMap)[e0] = e1;
                        return true;
@@ -99,6 +109,7 @@ public:
                if (-1 == i && !CheckSubstitutionMap(e1)) {
                        assert((e0.GetKind() == TRUE) ||
                                        (e0.GetKind() == FALSE) ||
+                                       (e0.GetKind() == SYMBOL) ||
                                        (e0.GetKind() == BVCONST));
                        (*SolverMap)[e1] = e0;
                        return true;

diff --git a/unit_test/output_0.cnf b/unit_test/output_0.cnf
deleted file mode 100644 (file)
index b5a3851..0000000
--- a/unit_test/output_0.cnf
+++ /dev/null
@@ -1,3 +0,0 @@
-p cnf 1 2
-1 0
-1 0

diff --git a/unit_test/sim.smt2 b/unit_test/sim.smt2
new file mode 100644 (file)
index 0000000..56cd1ba
--- /dev/null
+++ b/unit_test/sim.smt2
@@ -0,0 +1,20 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () Bool )
+(declare-fun v1 () Bool )
+(declare-fun v2 () Bool )
+(declare-fun v3 () Bool )
+
+; not xor is iff.
+
+(assert (not (xor v0 v1)))
+(assert (not (xor v1 v2)))
+(assert (not (xor v2 v3)))
+
+(check-sat)
+(exit)
+
+

diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
index cb2d7d6f9adc907c8b4ead8fed1cf116f1cb1fa7..a374cf1c9fe20f575edc6af1631f82b461611a56 100755 (executable)
--- a/unit_test/unit_test.sh
+++ b/unit_test/unit_test.sh
@@ -3,7 +3,7 @@
 #Each file should be simplified down to either true or false, so the CNF generated should
 #be very small if simplifications are working as they should.
 
-rm output_*.cnf
+rm -f output_*.cnf
 
 files=`ls -1 -S *.smt2`
 for f in $files; do