From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 Jun 2010 08:44:09 +0000 (+0000)
Subject: Speedups.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7e379dccc8cee7dbb7d0829448a984d6d350a9f1;p=francis%2Fstp.git

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 d998c76..e5f2601 100644
--- 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 4f7ca98..18a3e46 100644
--- 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 df03da0..dff8db1 100644
--- 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
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
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 cb2d7d6..a374cf1 100755
--- 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