summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cadical.cpp4
-rw-r--r--src/prop/cadical.h3
-rw-r--r--src/prop/cnf_stream.cpp193
-rw-r--r--src/prop/cnf_stream.h28
-rw-r--r--src/prop/minisat/core/Solver.cc1
-rw-r--r--src/prop/proof_cnf_stream.h1
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/sat_solver_factory.cpp4
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback