diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/theory/theory_engine.h | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 05ecc0e91..21d0905e5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -59,7 +59,7 @@ struct NodeTheoryPair { Node node; theory::TheoryId theory; size_t timestamp; - NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp) + NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0) : node(node), theory(theory), timestamp(timestamp) {} NodeTheoryPair() : theory(theory::THEORY_LAST) {} @@ -263,7 +263,7 @@ class TheoryEngine { { } - void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { + void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { spendResource(ammount); if (d_engine->d_interrupted) { throw theory::Interrupted(); @@ -294,14 +294,14 @@ class TheoryEngine { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory: theory::THEORY_LAST); + return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); + return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory); } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { @@ -448,7 +448,8 @@ class TheoryEngine { bool negated, bool removable, bool preprocess, - theory::TheoryId atomsTo); + theory::TheoryId atomsTo, + theory::TheoryId ownerTheory); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); @@ -719,6 +720,12 @@ public: Node getExplanation(TNode node); /** + * Returns an explanation of the node propagated to the SAT solver and the theory + * that propagated it. + */ + NodeTheoryPair getExplanationAndExplainer(TNode node); + + /** * collect model info */ void collectModelInfo( theory::TheoryModel* m, bool fullModel ); @@ -783,8 +790,8 @@ public: */ void printSynthSolution( std::ostream& out ); - /** - * Get instantiations + /** + * Get instantiations */ void getInstantiations( std::map< Node, std::vector< Node > >& insts ); |