From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 7 Sep 2010 13:09:42 +0000 (+0000)
Subject: Experimental. Convert IFF to XOR during simplification. This causes XORs of the attac... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ace7a76ace534b017178c55163fcd531b9c234e6;p=francis%2Fstp.git

Experimental. Convert IFF to XOR during simplification. This causes XORs of the attached unit test to flatten further.

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 3961f92..ec8c313 100644
--- 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
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)
+
+