diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2017-06-17 16:08:26 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2017-06-17 16:10:00 -0700 |
commit | b170abf9aa60298c0728c81baaeda701c4796a6e (patch) | |
tree | 3adae4c79c77916680562fdd01423394b4d35331 | |
parent | 0ae1bf84a2a2014946e5c516eec8cf0f617a5e0f (diff) |
test codetest
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/idl/theory_idl.cpp | 27 |
2 files changed, 18 insertions, 11 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index aba4f3ffc..ad001a2cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1025,6 +1025,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : const_cast<const LogicInfo&>(d_logic), d_channels); + d_private->addUseTheoryListListener(d_theoryEngine); + // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { TheoryConstructor::addTheory(d_theoryEngine, id); diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index a8fb2ba3e..4f3fa6782 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -19,17 +19,18 @@ namespace idl { TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo), - d_distances(c), - d_propagationEdges(c), - d_pathEdges(c), - d_varList(c), - d_propagatedLevels(c), - d_explanations(c), - d_distSetLevels(c), - d_assertions(c), - d_propagationIndices(c) -{} + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo), + d_distances(c), + d_propagationEdges(c), + d_pathEdges(c), + d_varList(c), + d_propagatedLevels(c), + d_explanations(c), + d_distSetLevels(c), + d_assertions(c), + d_propagationIndices(c) { + std::cout << __PRETTY_FUNCTION__ << std::endl; +} void TheoryIdl::preRegisterTerm(TNode node) { Assert(node.getKind() != kind::NOT); @@ -62,6 +63,7 @@ void TheoryIdl::postsolve() { } Node TheoryIdl::ppRewrite(TNode atom) { + std::cout << __PRETTY_FUNCTION__ << std::endl; Assert(atom.getKind() != kind::NOT); if (atom.getKind() == kind::EQUAL) { Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; @@ -91,6 +93,7 @@ void TheoryIdl::propagate(Effort level) { } Node TheoryIdl::explain(TNode n) { + std::cout << __PRETTY_FUNCTION__ << std::endl; Assert(d_propagationIndices.contains(n)); std::pair<unsigned, unsigned> indices = d_propagationIndices[n]; @@ -175,6 +178,7 @@ Node TheoryIdl::explain(TNode n) { } void TheoryIdl::check(Effort level) { + std::cout << __PRETTY_FUNCTION__ << std::endl; if (done() && !fullEffort(level)) { return; } @@ -212,6 +216,7 @@ void TheoryIdl::check(Effort level) { } bool TheoryIdl::processAssertion(const IDLAssertion& assertion) { + std::cout << __PRETTY_FUNCTION__ << std::endl; Assert(assertion.ok()); TNode x = assertion.getX(); |