From: trevor_hansen Date: Mon, 28 Jun 2010 11:48:38 +0000 (+0000) Subject: Speedup. Add solving for xors to the bitvector solver. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d8cda4b24e8b8a06af6465a1fdb523a75b202a51;p=francis%2Fstp.git 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 409735f..f47deef 100644 --- 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 13ee854..8281cbd 100644 --- 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 d9413c2..abb1857 100644 --- 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 0455a73..ee477ff 100644 --- 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& 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 f303855..4184b75 100644 --- 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 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) + +