Speedup. Add solving for xors to the bitvector solver.

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 409735f832130668362441deb580bb9b01a2b208..f47deefb1bb037f393a90b9383b85461d2e5254f 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -42,6 +42,8 @@ namespace BEEV
   // NB: The boolean value is always true!
   bool BVTypeCheck(const ASTNode& n);
   
+  ASTVec FlattenKind(Kind k, const ASTVec &children);
+
   // Checks recursively all the way down.
   bool BVTypeCheckRecursive(const ASTNode& n);
 

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 13ee85430d02eb3d272167ef4e5a9d1cd59e2d74..8281cbd2383e394f061f87605e074955530c7df9 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -162,6 +162,33 @@ bool containsArrayOps(const ASTNode&n)
 }
 
 
+  // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)
+  // This is local to this file.
+  ASTVec FlattenKind(Kind k, const ASTVec &children)
+  {
+    ASTVec flat_children;
+
+    ASTVec::const_iterator ch_end = children.end();
+    for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
+      {
+        Kind ck = it->GetKind();
+        const ASTVec &gchildren = it->GetChildren();
+        if (k == ck)
+          {
+            // append grandchildren to children
+            flat_children.insert(flat_children.end(),
+                                 gchildren.begin(), gchildren.end());
+          }
+        else
+          {
+            flat_children.push_back(*it);
+          }
+      }
+
+    return flat_children;
+  }
+
+
   /* FUNCTION: Typechecker for terms and formulas
    *
    * TypeChecker: Assumes that the immediate Children of the input

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index d9413c2cfdf8210955b17d24440d2d35e6b5ad24..abb1857db1236fc7dfeb7beab222049b5d13fb1b 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -560,6 +560,91 @@ namespace BEEV
        }
   }
 
+  // Solve for XORs.
+  // to do. Flatten the XOR.
+  ASTNode BVSolver::solveForXOR(const ASTNode& xorNode)
+  {
+     if (xorNode.GetKind() != XOR)
+      {
+       return xorNode;
+      }
+
+    ASTVec children =  FlattenKind(XOR, xorNode.GetChildren());
+
+    bool foundSymbol = false;
+    for (ASTVec::const_iterator symbol = children.begin(), node_end =
+        children.end(); symbol != node_end; symbol++)
+      {
+        // Find a symbol in it.
+        if ((*symbol).GetKind() != SYMBOL)
+          {
+            continue;
+          }
+
+        bool duplicated = false;
+
+        for (ASTVec::const_iterator it2 = children.begin(); it2
+            != node_end; it2++)
+          {
+            if (it2 == symbol)
+              continue;
+            if (VarSeenInTerm(*symbol, *it2))
+              {
+                duplicated = true;
+                break;
+              }
+          }
+        foundSymbol = false;
+        if (!duplicated)
+          {
+            ASTVec rhs;
+            for (ASTVec::const_iterator it2 = children.begin(); it2
+                != node_end; it2++)
+              {
+              if (it2 != symbol)
+                rhs.push_back(*it2); // omit the symbol.
+              }
+
+            foundSymbol = _simp->UpdateSolverMap(*symbol, _bm->CreateNode(
+                NOT, _bm->CreateNode(XOR, rhs)));
+          }
+        if (foundSymbol)
+          break;
+      }
+    if (foundSymbol)
+      return ASTTrue;
+    else
+      return xorNode;
+}
+
+  // Solve for XORs.
+   // to do. Flatten the XOR.
+   ASTNode
+  BVSolver::solveForAndOfXOR(const ASTNode& n)
+  {
+    if (n.GetKind() != AND)
+      return n;
+
+    ASTVec output_children;
+
+    ASTVec c =  FlattenKind(AND, n.GetChildren());
+    bool changed=false;
+    //_simp->ResetSimplifyMaps();
+
+    for (ASTVec::const_iterator and_child = c.begin(), and_end = c.end(); and_child
+        != and_end; and_child++)
+      {
+      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula_TopLevel(*and_child,false));
+      if (r!=*and_child)
+        changed=true;
+      output_children.push_back(r);
+      }
+
+    return _bm->CreateNode(AND, output_children);
+
+  }
+
+
   //The toplevel bvsolver(). Checks if the formula has already been
   //solved. If not, the solver() is invoked. If yes, then simply drop
   //the formula
@@ -571,11 +656,7 @@ namespace BEEV
     //       }
          ASTNode input = _input;
 
-    Kind k = input.GetKind();
-    if (!(EQ == k || AND == k))
-      {
-        return input;
-      }
+
 
     ASTNode output = input;
     if (CheckAlreadySolvedMap(input, output))
@@ -584,6 +665,20 @@ namespace BEEV
         return output;
       }
 
+    Kind k = input.GetKind();
+    if (XOR ==k)
+    {
+       ASTNode output = solveForXOR(_input);
+       UpdateAlreadySolvedMap(_input, output);
+       return output;
+    }
+
+    if (!(EQ == k || AND == k))
+      {
+        return input;
+      }
+
+
     if (flatten_ands && AND == k)
     {
                ASTNode n = input;
@@ -698,6 +793,8 @@ namespace BEEV
       ASTTrue;
     output = _bm->CreateNode(AND, output, evens);
 
+    output = solveForAndOfXOR(output);
+
     UpdateAlreadySolvedMap(_input, output);
     _bm->GetRunTimes()->stop(RunTimes::BVSolver);
     return output;

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 0455a735348738231e7af615ac1b17e7be90f003..ee477ff8c623ca6ab73120db0fdb89a495e8e4a4 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -102,6 +102,8 @@ namespace BEEV
 
     void VarSeenInTerm(Symbols* term, SymbolPtrSet& visited, ASTNodeSet& found, vector<Symbols*>& av);
 
+    ASTNode solveForXOR(const ASTNode& n);
+    ASTNode solveForAndOfXOR(const ASTNode& n);
 
     //takes an even number "in" as input, and returns an odd number
     //(return value) and a power of 2 (as number_shifts by reference),

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index f3038559f7d686df670415ffd53b3c9ad0b9b9ea..4184b75af284aa65eb162a4adfad5a94b0a46b35 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -153,51 +153,6 @@ namespace BEEV
     return CreateSimpXor(children);
   }
 
-  // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)
-  // This is local to this file.
-  ASTVec FlattenKind(Kind k, ASTVec &children)
-  {
-
-    ASTVec flat_children;
-
-    ASTVec::const_iterator ch_end = children.end();
-
-    bool fflag = 0; // ***Temp debugging
-
-    // Experimental flattening code.
-
-    for (ASTVec::iterator it = children.begin(); it != ch_end; it++)
-      {
-        Kind ck = it->GetKind();
-        const ASTVec &gchildren = it->GetChildren();
-        if (k == ck)
-          {
-            fflag = 1; // For selective debug printing (below).
-            // append grandchildren to children
-            flat_children.insert(flat_children.end(), 
-                                 gchildren.begin(), gchildren.end());
-          }
-        else
-          {
-            flat_children.push_back(*it);
-          }
-      }
-
-    if (_trace_simpbool && fflag)
-      {
-        cout << "========" << endl;
-        cout << "Flattening " << k << ":" << endl;
-        lpvec(children);
-
-        cout << "--------" << endl;
-        cout << "Flattening result: " << endl;
-        lpvec(flat_children);
-      }
-
-    // FIXME: This unnecessarily copies the array.
-    return flat_children;
-  }
-
   ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, 
                                   const ASTNode& form1, const ASTNode& form2)
   {

diff --git a/unit_test/xor2.smt2 b/unit_test/xor2.smt2
new file mode 100644 (file)
index 0000000..5778a35
--- /dev/null
+++ b/unit_test/xor2.smt2
@@ -0,0 +1,21 @@
+
+(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 )
+(declare-fun v4 () Bool )
+(declare-fun v5 () Bool )
+
+; The variables appear only in this expression, so
+; they should be simplified out.
+(assert (xor (xor (not v0) (not v1)) (xor (not v3) (not v2))))
+(assert (xor v4 v5))
+
+(check-sat)
+(exit)
+
+