diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cadical.cpp | 4 | ||||
-rw-r--r-- | src/prop/cadical.h | 3 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 193 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 28 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 1 | ||||
-rw-r--r-- | src/prop/proof_cnf_stream.h | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 |
8 files changed, 130 insertions, 107 deletions
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index ec8919b0b..ddf20f5a1 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -17,8 +17,6 @@ #include "prop/cadical.h" -#ifdef CVC5_USE_CADICAL - #include "base/check.h" #include "util/statistics_registry.h" @@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry, } // namespace prop } // namespace cvc5 - -#endif // CVC5_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index b5e26df9f..46c7c7e42 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -20,8 +20,6 @@ #ifndef CVC5__PROP__CADICAL_H #define CVC5__PROP__CADICAL_H -#ifdef CVC5_USE_CADICAL - #include "prop/sat_solver.h" #include <cadical.hpp> @@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC5_USE_CADICAL #endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f8a34ec42..4897f8e6a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -21,14 +21,15 @@ #include "base/output.h" #include "expr/node.h" #include "options/bv_options.h" +#include "printer/printer.h" #include "proof/clause_id.h" #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/dump.h" #include "smt/smt_engine.h" -#include "printer/printer.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -52,7 +53,8 @@ CnfStream::CnfStream(SatSolver* satSolver, d_registrar(registrar), d_name(name), d_removable(false), - d_resourceManager(rm) + d_resourceManager(rm), + d_stats(name) { } @@ -139,6 +141,7 @@ void CnfStream::ensureLiteral(TNode n) n.toString().c_str(), n.getType().toString().c_str()); Trace("cnf") << "ensureLiteral(" << n << ")\n"; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); if (hasLiteral(n)) { ensureMappingForLiteral(n); @@ -292,7 +295,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 +303,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 +312,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 +323,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 +356,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 +391,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 +405,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 +416,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 +435,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 +446,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 +471,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<TNode> visit; + std::unordered_map<TNode, bool> 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) @@ -707,6 +725,7 @@ void CnfStream::convertAndAssert(TNode node, << ", negated = " << (negated ? "true" : "false") << ", removable = " << (removable ? "true" : "false") << ")\n"; d_removable = removable; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); convertAndAssert(node, negated); } @@ -745,5 +764,11 @@ void CnfStream::convertAndAssert(TNode node, bool negated) } } +CnfStream::Statistics::Statistics(const std::string& name) + : d_cnfConversionTime(smtStatisticsRegistry().registerTimer( + name + "::CnfStream::cnfConversionTime")) +{ +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 264e26777..aeed97380 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. * @@ -309,6 +309,14 @@ class CnfStream { /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; + + private: + struct Statistics + { + Statistics(const std::string& name); + TimerStat d_cnfConversionTime; + } d_stats; + }; /* class CnfStream */ } // namespace prop diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fd86d3a42..6f99a47f0 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/check.h" #include "base/output.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/prop_options.h" #include "options/smt_options.h" 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/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fe3a5ecff..62b2f655c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -107,7 +107,8 @@ PropEngine::PropEngine(TheoryEngine* te, userContext, &d_outMgr, rm, - FormulaLitPolicy::TRACK); + FormulaLitPolicy::TRACK, + "prop"); // connect theory proxy d_theoryProxy->finishInit(d_cnfStream); diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 446f72451..0855cbda5 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry, SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry, const std::string& name) { -#ifdef CVC5_USE_CADICAL CadicalSolver* res = new CadicalSolver(registry, name); res->init(); return res; -#else - Unreachable() << "cvc5 was not compiled with CaDiCaL support."; -#endif } SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry, |