diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/theory/theory_engine.h | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 95 |
1 files changed, 58 insertions, 37 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2107bcb66..815a79a5a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -2,8 +2,8 @@ /*! \file theory_engine.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, dejan - ** Minor contributors (to current version): cconway, barrett + ** Major contributors: dejan + ** Minor contributors (to current version): cconway, barrett, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -26,7 +26,9 @@ #include <utility> #include "expr/node.h" +#include "expr/command.h" #include "prop/prop_engine.h" +#include "context/cdset.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/substitutions.h" @@ -77,6 +79,19 @@ class TheoryEngine { NodeMap d_atomPreprocessingCache; /** + * Used for "missed-t-propagations" dumping mode only. A set of all + * theory-propagable literals. + */ + std::vector<TNode> d_possiblePropagations; + + /** + * Used for "missed-t-propagations" dumping mode only. A + * context-dependent set of those theory-propagable literals that + * have been propagated. + */ + context::CDSet<TNode, TNodeHashFunction> d_hasPropagated; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -122,13 +137,16 @@ class TheoryEngine { d_explanationNode(context) { } - void newFact(TNode n); - void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_inConflict = true; + if(Dump.isOn("t-conflicts")) { + Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl + << CheckSatCommand(conflictNode.toExpr()) << std::endl; + } + Assert(d_engine->properConflict(conflictNode)); ++(d_engine->d_statistics.d_statConflicts); // Construct the lemma (note that no CNF caching should happen as all the literals already exists) @@ -144,6 +162,15 @@ class TheoryEngine { throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::propagate(" << lit << ")" << std::endl; + if(Dump.isOn("t-propagations")) { + Dump("t-propagations") + << CommentCommand("negation of theory propagation: expect valid") << std::endl + << QueryCommand(lit.toExpr()) << std::endl; + } + if(Dump.isOn("missed-t-propagations")) { + d_engine->d_hasPropagated.insert(lit); + } + Assert(d_engine->properPropagation(lit)); d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); } @@ -152,6 +179,10 @@ class TheoryEngine { throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; + if(Dump.isOn("t-lemmas")) { + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl + << QueryCommand(node.toExpr()) << std::endl; + } ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node, false, removable); @@ -161,12 +192,12 @@ class TheoryEngine { throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::explanation(" << explanationNode << ")" << std::endl; + // handle dumping of explanations elsewhere.. d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } - void setIncomplete() - throw(theory::Interrupted, AssertionException) { + void setIncomplete() throw(theory::Interrupted, AssertionException) { d_engine->d_incomplete = true; } };/* class EngineOutputChannel */ @@ -177,12 +208,6 @@ class TheoryEngine { SharedTermManager* d_sharedTermManager; /** - * Whether or not theory registration is on. May not be safe to - * turn off with some theories. - */ - bool d_theoryRegistration; - - /** * Debugging flag to ensure that shutdown() is called before the * destructor. */ @@ -224,14 +249,15 @@ public: * there is another theory it will be deleted. */ template <class TheoryClass> - void addTheory() { + inline void addTheory() { TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); d_theoryTable[theory->getId()] = theory; d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); } /** - * Set's the logic (smt-lib format). All theory specific setup/hacks should go in here. + * Sets the logic (SMT-LIB format). All theory specific setup/hacks + * should go in here. */ void setLogic(std::string logic); @@ -239,7 +265,7 @@ public: return d_sharedTermManager; } - void setPropEngine(prop::PropEngine* propEngine) { + inline void setPropEngine(prop::PropEngine* propEngine) { Assert(d_propEngine == NULL); d_propEngine = propEngine; } @@ -247,7 +273,7 @@ public: /** * Get a pointer to the underlying propositional engine. */ - prop::PropEngine* getPropEngine() const { + inline prop::PropEngine* getPropEngine() const { return d_propEngine; } @@ -260,7 +286,7 @@ public: /** * Return whether or not we are incomplete (in the current context). */ - bool isIncomplete() { + inline bool isIncomplete() { return d_incomplete; } @@ -269,21 +295,7 @@ public: * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory. */ - void shutdown() { - // Set this first; if a Theory shutdown() throws an exception, - // at least the destruction of the TheoryEngine won't confound - // matters. - d_hasShutDown = true; - - // Shutdown all the theories - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { - d_theoryTable[theoryId]->shutdown(); - } - } - - theory::Rewriter::shutdown(); - } + void shutdown(); /** * Get the theory associated to a given Node. @@ -367,7 +379,7 @@ public: return d_theoryOut.d_propagatedLiterals; } - void clearPropagatedLiterals() { + inline void clearPropagatedLiterals() { d_theoryOut.d_propagatedLiterals.clear(); } @@ -384,16 +396,25 @@ public: void propagate(); - inline Node getExplanation(TNode node, theory::Theory* theory) { - theory->explain(node); - return d_theoryOut.d_explanationNode; - } + Node getExplanation(TNode node, theory::Theory* theory); + + bool properConflict(TNode conflict) const; + bool properPropagation(TNode lit) const; + bool properExplanation(TNode node, TNode expl) const; inline Node getExplanation(TNode node) { d_theoryOut.d_explanationNode = Node::null(); TNode atom = node.getKind() == kind::NOT ? node[0] : node; theoryOf(atom)->explain(node); Assert(!d_theoryOut.d_explanationNode.get().isNull()); + if(Dump.isOn("t-explanations")) { + Dump("t-explanations") + << CommentCommand(std::string("theory explanation from ") + + theoryOf(atom)->identify() + ": expect valid") << std::endl + << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) + << std::endl; + } + Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); return d_theoryOut.d_explanationNode; } |