diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a66e36a07..6e3b6ae2f 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -23,6 +23,7 @@ #include <queue> using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace prop { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5dd57610d..76be5d6d8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -49,14 +49,14 @@ PropEngine::~PropEngine() { delete d_satSolver; } -void PropEngine::assertFormula(const Node& node) { +void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable d_cnfStream->convertAndAssert(node); } -void PropEngine::assertLemma(const Node& node) { +void PropEngine::assertLemma(TNode node) { Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as removable d_cnfStream->convertAndAssert(node); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d4007e73a..4ea5e3b78 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -77,14 +77,14 @@ public: * The formula is asserted permanently for the current context. * @param node the formula to assert */ - void assertFormula(const Node& node); + void assertFormula(TNode node); /** * Converts the given formula to CNF and assert the CNF to the sat solver. * The formula can be removed by the sat solver. * @param node the formula to assert */ - void assertLemma(const Node& node); + void assertLemma(TNode node); /** * Checks the current context for satisfiability. |