Experimental. Convert IFF to XOR during simplification. This causes XORs of the attac...

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 3961f92b165b005f8766760ffdfffaed64c00852..ec8c31301e6c6c4f1964bec0b710b71fc1f8d194 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1465,7 +1465,7 @@ namespace BEEV
       }
     else
       {
-        output = nf->CreateNode(IFF, c0, c1);
+        output = nf->CreateNode(XOR, nf->CreateNode(NOT,c0), c1);
       }
 
     //memoize

diff --git a/unit_test/xor3.smt2 b/unit_test/xor3.smt2
new file mode 100644 (file)
index 0000000..5d3e5c4
--- /dev/null
+++ b/unit_test/xor3.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 )
+
+; Checks that =, that is IFF, will be mixed in with xor.
+(assert (xor (not (xor v0 v1))  (= v2 v1)))
+
+(check-sat)
+(exit)
+
+