Speedup. if (xor a b) is found, replaced a with (not b) throughout.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 18a3e463ca79ec62062f2a773891906b8814d13b..50a80207b40f244e29fdca94386bbc7712f94909 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -125,6 +125,38 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
       return output;
     }
 
+  if (XOR == k)
+  {
+         if (a.Degree() !=2)
+                 return output;
+
+         int to = TermOrder(a[0],a[1]);
+         if (0 == to)
+                 return output;
+
+         ASTNode symbol,rhs;
+         if (to==1)
+         {
+                 symbol = a[0];
+                 rhs = a[1];
+         }
+         else
+         {
+                 symbol = a[0];
+                 rhs = a[1];
+         }
+
+         assert(symbol.GetKind() == SYMBOL);
+
+         // If either side is already solved for.
+         if (CheckSubstitutionMap(symbol) || CheckSubstitutionMap(rhs))
+                 return output;
+
+         (*SolverMap)[symbol] = bm->CreateNode(NOT,rhs);
+      return ASTTrue;
+  }
+
+
   if (AND == k)
     {
       ASTVec o;

diff --git a/unit_test/unit_test.sh b/unit_test/unit_test.sh
index a374cf1c9fe20f575edc6af1631f82b461611a56..449961ed263b5a9d733e831b8b74dc21e258c239 100755 (executable)
--- a/unit_test/unit_test.sh
+++ b/unit_test/unit_test.sh
@@ -10,6 +10,7 @@ for f in $files; do
        stp --simplifying-minisat --output-CNF $f
        cnf=`cat output_*.cnf  | wc -l`
        if [ $cnf -gt 3 ] ; then
+               echo --fail
                exit 10
        fi
 

diff --git a/unit_test/xor.smt2 b/unit_test/xor.smt2
new file mode 100644 (file)
index 0000000..aa2a7fd
--- /dev/null
+++ b/unit_test/xor.smt2
@@ -0,0 +1,16 @@
+
+(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 )
+
+; This should be simplifed to v_0 <=> -v_1 before bitblasing.
+(assert (xor v0 v1))
+
+(check-sat)
+(exit)
+
+