From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 28 Jun 2010 01:46:11 +0000 (+0000)
Subject: Speedup. if (xor a b) is found, replaced a with (not b) throughout.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d01b8afe55ec79cb1818f455167dbbc1e8868293;p=francis%2Fstp.git

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 18a3e46..50a8020 100644
--- 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 a374cf1..449961e 100755
--- 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
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)
+
+