From: Mathias Preiner Date: Fri, 18 Jun 2021 17:31:53 +0000 (-0700) Subject: Make CnfStream::toCNF iterative (#6757) X-Git-Tag: cvc5-1.0.0~1589 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b15ba18c32ed78190b7e71b6bfb64f1f8b8dcab;p=cvc5.git Make CnfStream::toCNF iterative (#6757) This commit makes toCNF() iterative to avoid this issue. Note that the order in which nodes are visited and thus SatLiterals are created remains the same. Fixes #6111 --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f8a34ec42..40853b33a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -292,7 +292,7 @@ SatLiteral CnfStream::getLiteral(TNode node) { return literal; } -SatLiteral CnfStream::handleXor(TNode xorNode) +void CnfStream::handleXor(TNode xorNode) { Assert(!hasLiteral(xorNode)) << "Atom already mapped!"; Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!"; @@ -300,8 +300,8 @@ SatLiteral CnfStream::handleXor(TNode xorNode) Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n"; - SatLiteral a = toCNF(xorNode[0]); - SatLiteral b = toCNF(xorNode[1]); + SatLiteral a = getLiteral(xorNode[0]); + SatLiteral b = getLiteral(xorNode[1]); SatLiteral xorLit = newLiteral(xorNode); @@ -309,11 +309,9 @@ SatLiteral CnfStream::handleXor(TNode xorNode) assertClause(xorNode.negate(), ~a, ~b, ~xorLit); assertClause(xorNode, a, ~b, xorLit); assertClause(xorNode, ~a, b, xorLit); - - return xorLit; } -SatLiteral CnfStream::handleOr(TNode orNode) +void CnfStream::handleOr(TNode orNode) { Assert(!hasLiteral(orNode)) << "Atom already mapped!"; Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!"; @@ -322,37 +320,31 @@ SatLiteral CnfStream::handleOr(TNode orNode) Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n"; // Number of children - unsigned n_children = orNode.getNumChildren(); - - // Transform all the children first - TNode::const_iterator node_it = orNode.begin(); - TNode::const_iterator node_it_end = orNode.end(); - SatClause clause(n_children + 1); - for(int i = 0; node_it != node_it_end; ++node_it, ++i) { - clause[i] = toCNF(*node_it); - } + size_t numChildren = orNode.getNumChildren(); // Get the literal for this node SatLiteral orLit = newLiteral(orNode); - // lit <- (a_1 | a_2 | a_3 | ... | a_n) - // lit | ~(a_1 | a_2 | a_3 | ... | a_n) - // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) - for(unsigned i = 0; i < n_children; ++i) { + // Transform all the children first + SatClause clause(numChildren + 1); + for (size_t i = 0; i < numChildren; ++i) + { + clause[i] = getLiteral(orNode[i]); + + // lit <- (a_1 | a_2 | a_3 | ... | a_n) + // lit | ~(a_1 | a_2 | a_3 | ... | a_n) + // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) assertClause(orNode, orLit, ~clause[i]); } // lit -> (a_1 | a_2 | a_3 | ... | a_n) // ~lit | a_1 | a_2 | a_3 | ... | a_n - clause[n_children] = ~orLit; + clause[numChildren] = ~orLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(orNode.negate(), clause); - - // Return the literal - return orLit; } -SatLiteral CnfStream::handleAnd(TNode andNode) +void CnfStream::handleAnd(TNode andNode) { Assert(!hasLiteral(andNode)) << "Atom already mapped!"; Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!"; @@ -361,37 +353,32 @@ SatLiteral CnfStream::handleAnd(TNode andNode) Trace("cnf") << "handleAnd(" << andNode << ")\n"; // Number of children - unsigned n_children = andNode.getNumChildren(); - - // Transform all the children first (remembering the negation) - TNode::const_iterator node_it = andNode.begin(); - TNode::const_iterator node_it_end = andNode.end(); - SatClause clause(n_children + 1); - for(int i = 0; node_it != node_it_end; ++node_it, ++i) { - clause[i] = ~toCNF(*node_it); - } + size_t numChildren = andNode.getNumChildren(); // Get the literal for this node SatLiteral andLit = newLiteral(andNode); - // lit -> (a_1 & a_2 & a_3 & ... & a_n) - // ~lit | (a_1 & a_2 & a_3 & ... & a_n) - // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) - for(unsigned i = 0; i < n_children; ++i) { + // Transform all the children first (remembering the negation) + SatClause clause(numChildren + 1); + for (size_t i = 0; i < numChildren; ++i) + { + clause[i] = ~getLiteral(andNode[i]); + + // lit -> (a_1 & a_2 & a_3 & ... & a_n) + // ~lit | (a_1 & a_2 & a_3 & ... & a_n) + // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) assertClause(andNode.negate(), ~andLit, ~clause[i]); } // lit <- (a_1 & a_2 & a_3 & ... a_n) // lit | ~(a_1 & a_2 & a_3 & ... & a_n) // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n - clause[n_children] = andLit; + clause[numChildren] = andLit; // This needs to go last, as the clause might get modified by the SAT solver assertClause(andNode, clause); - - return andLit; } -SatLiteral CnfStream::handleImplies(TNode impliesNode) +void CnfStream::handleImplies(TNode impliesNode) { Assert(!hasLiteral(impliesNode)) << "Atom already mapped!"; Assert(impliesNode.getKind() == kind::IMPLIES) @@ -401,8 +388,8 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode) Trace("cnf") << "handleImplies(" << impliesNode << ")\n"; // Convert the children to cnf - SatLiteral a = toCNF(impliesNode[0]); - SatLiteral b = toCNF(impliesNode[1]); + SatLiteral a = getLiteral(impliesNode[0]); + SatLiteral b = getLiteral(impliesNode[1]); SatLiteral impliesLit = newLiteral(impliesNode); @@ -415,11 +402,9 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode) // (a | l) & (~b | l) assertClause(impliesNode, a, impliesLit); assertClause(impliesNode, ~b, impliesLit); - - return impliesLit; } -SatLiteral CnfStream::handleIff(TNode iffNode) +void CnfStream::handleIff(TNode iffNode) { Assert(!hasLiteral(iffNode)) << "Atom already mapped!"; Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!"; @@ -428,8 +413,8 @@ SatLiteral CnfStream::handleIff(TNode iffNode) Trace("cnf") << "handleIff(" << iffNode << ")\n"; // Convert the children to CNF - SatLiteral a = toCNF(iffNode[0]); - SatLiteral b = toCNF(iffNode[1]); + SatLiteral a = getLiteral(iffNode[0]); + SatLiteral b = getLiteral(iffNode[1]); // Get the now literal SatLiteral iffLit = newLiteral(iffNode); @@ -447,11 +432,9 @@ SatLiteral CnfStream::handleIff(TNode iffNode) // (~a | ~b | lit) & (a | b | lit) assertClause(iffNode, ~a, ~b, iffLit); assertClause(iffNode, a, b, iffLit); - - return iffLit; } -SatLiteral CnfStream::handleIte(TNode iteNode) +void CnfStream::handleIte(TNode iteNode) { Assert(!hasLiteral(iteNode)) << "Atom already mapped!"; Assert(iteNode.getKind() == kind::ITE); @@ -460,9 +443,9 @@ SatLiteral CnfStream::handleIte(TNode iteNode) Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")\n"; - SatLiteral condLit = toCNF(iteNode[0]); - SatLiteral thenLit = toCNF(iteNode[1]); - SatLiteral elseLit = toCNF(iteNode[2]); + SatLiteral condLit = getLiteral(iteNode[0]); + SatLiteral thenLit = getLiteral(iteNode[1]); + SatLiteral elseLit = getLiteral(iteNode[2]); SatLiteral iteLit = newLiteral(iteNode); @@ -485,47 +468,79 @@ SatLiteral CnfStream::handleIte(TNode iteNode) assertClause(iteNode, iteLit, ~thenLit, ~elseLit); assertClause(iteNode, iteLit, ~condLit, ~thenLit); assertClause(iteNode, iteLit, condLit, ~elseLit); - - return iteLit; } SatLiteral CnfStream::toCNF(TNode node, bool negated) { Trace("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")\n"; + + TNode cur; SatLiteral nodeLit; - Node negatedNode = node.notNode(); - - // If the non-negated node has already been translated, get the translation - if(hasLiteral(node)) { - Trace("cnf") << "toCNF(): already translated\n"; - nodeLit = getLiteral(node); - // Return the (maybe negated) literal - return !negated ? nodeLit : ~nodeLit; - } - // Handle each Boolean operator case - switch (node.getKind()) + std::vector visit; + std::unordered_map cache; + + visit.push_back(node); + while (!visit.empty()) { - case kind::NOT: nodeLit = ~toCNF(node[0]); break; - case kind::XOR: nodeLit = handleXor(node); break; - case kind::ITE: nodeLit = handleIte(node); break; - case kind::IMPLIES: nodeLit = handleImplies(node); break; - case kind::OR: nodeLit = handleOr(node); break; - case kind::AND: nodeLit = handleAnd(node); break; - case kind::EQUAL: - nodeLit = - node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node); - break; - default: + cur = visit.back(); + Assert(cur.getType().isBoolean()); + + if (hasLiteral(cur)) { - nodeLit = convertAtom(node); + visit.pop_back(); + continue; } - break; + + const auto& it = cache.find(cur); + if (it == cache.end()) + { + cache.emplace(cur, false); + Kind k = cur.getKind(); + // Only traverse Boolean nodes + if (k == kind::NOT || k == kind::XOR || k == kind::ITE + || k == kind::IMPLIES || k == kind::OR || k == kind::AND + || (k == kind::EQUAL && cur[0].getType().isBoolean())) + { + // Preserve the order of the recursive version + for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i) + { + visit.push_back(cur[size - 1 - i]); + } + } + continue; + } + else if (!it->second) + { + it->second = true; + Kind k = cur.getKind(); + switch (k) + { + case kind::NOT: Assert(hasLiteral(cur[0])); break; + case kind::XOR: handleXor(cur); break; + case kind::ITE: handleIte(cur); break; + case kind::IMPLIES: handleImplies(cur); break; + case kind::OR: handleOr(cur); break; + case kind::AND: handleAnd(cur); break; + default: + if (k == kind::EQUAL && cur[0].getType().isBoolean()) + { + handleIff(cur); + } + else + { + convertAtom(cur); + } + break; + } + } + visit.pop_back(); } - // Return the (maybe negated) literal + + nodeLit = getLiteral(node); Trace("cnf") << "toCNF(): resulting literal: " << (!negated ? nodeLit : ~nodeLit) << "\n"; - return !negated ? nodeLit : ~nodeLit; + return negated ? ~nodeLit : nodeLit; } void CnfStream::convertAndAssertAnd(TNode node, bool negated) diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 264e26777..2959ae726 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -191,16 +191,16 @@ class CnfStream { */ SatLiteral toCNF(TNode node, bool negated = false); - /** Specific clausifiers, based on the formula kinds, that clausify a formula, - * by calling toCNF into each of the formula's children under the respective - * kind, and introduce a literal definitionally equal to it. */ - SatLiteral handleNot(TNode node); - SatLiteral handleXor(TNode node); - SatLiteral handleImplies(TNode node); - SatLiteral handleIff(TNode node); - SatLiteral handleIte(TNode node); - SatLiteral handleAnd(TNode node); - SatLiteral handleOr(TNode node); + /** + * Specific clausifiers that clausify a formula based on the given formula + * kind and introduce a literal definitionally equal to it. + */ + void handleXor(TNode node); + void handleImplies(TNode node); + void handleIff(TNode node); + void handleIte(TNode node); + void handleAnd(TNode node); + void handleOr(TNode node); /** Stores the literal of the given node in d_literalToNodeMap. * diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 9972581c0..af131c2c3 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -133,7 +133,6 @@ class ProofCnfStream : public ProofGenerator * Specific clausifiers, based on the formula kinds, that clausify a formula, * by calling toCNF into each of the formula's children under the respective * kind, and introduce a literal definitionally equal to it. */ - SatLiteral handleNot(TNode node); SatLiteral handleXor(TNode node); SatLiteral handleImplies(TNode node); SatLiteral handleIff(TNode node); diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index e9fd47261..4811cca1b 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance) cvc5_add_api_test(two_solvers) cvc5_add_api_test(issue5074) cvc5_add_api_test(issue4889) +cvc5_add_api_test(issue6111) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp new file mode 100644 index 000000000..bd7be2ad0 --- /dev/null +++ b/test/api/issue6111.cpp @@ -0,0 +1,58 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Test for issue #6111 + * + */ +#include +#include + +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; +using namespace std; + +int main() +{ + Solver solver; + solver.setLogic("QF_BV"); + Sort bvsort12979 = solver.mkBitVectorSort(12979); + Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); + Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + + vector args1; + args1.push_back(zero); + args1.push_back(input2_1); + Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1); + solver.assertFormula(bvult_res); + + Sort bvsort4 = solver.mkBitVectorSort(4); + Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42"); + Sort bvsort8 = solver.mkBitVectorSort(8); + Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43"); + + vector args2; + args2.push_back(concat_result_42); + args2.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args2)); + + vector args3; + args3.push_back(concat_result_42); + args3.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args3)); + + cout << solver.checkSat() << endl; + + return 0; +}