diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/theory/theory_engine.h | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 127 |
1 files changed, 99 insertions, 28 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5712b1502..dd642a865 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -98,6 +98,21 @@ class TheoryEngine { */ context::CDO<theory::Theory::Set> d_activeTheories; + // NotifyClass: template helper class for Shared Terms Database + class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass { + TheoryEngine& d_theoryEngine; + public: + NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {} + ~NotifyClass() {} + + void notify(TNode literal, TNode original, theory::TheoryId theory) { + d_theoryEngine.propagateSharedLiteral(literal, original, theory); + } + }; + + // Instance of NotifyClass + NotifyClass d_notify; + /** * The database of shared terms. */ @@ -106,9 +121,9 @@ class TheoryEngine { typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; /** - * Cache from proprocessing of atoms. + * Cache for theory-preprocessing of assertions */ - NodeMap d_atomPreprocessingCache; + NodeMap d_ppCache; /** * Used for "missed-t-propagations" dumping mode only. A set of all @@ -296,32 +311,55 @@ class TheoryEngine { return theory::Theory::setContains(theory, d_activeTheories); } - struct SharedEquality { + struct SharedLiteral { /** The node/theory pair for the assertion */ + /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */ NodeTheoryPair toAssert; - /** This is the node/theory pair that we will use to explain it */ - NodeTheoryPair toExplain; + /** This is the node that we will use to explain it */ + Node toExplain; - SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory) + SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory) : toAssert(assertion, receivingTheory), - toExplain(original, sendingTheory) + toExplain(original) { } - };/* struct SharedEquality */ + };/* struct SharedLiteral */ /** - * Map from equalities asserted to a theory, to the theory that can explain them. + * Map from nodes to theories. */ - typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap; + typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap; /** - * A map from asserted facts to where they came from (for explanations). + * All shared literals asserted to theory engine. + * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT). */ - SharedAssertionsMap d_sharedAssertions; + SharedLiteralsInMap d_sharedLiteralsIn; /** - * Assert a shared equalities propagated by theories. + * Map from literals asserted by theory engine to literal that can explain */ - void assertSharedEqualities(); + typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap; + + /** + * All literals asserted to theories from theory engine. + * Maps from literal/theory pair to literal that can explain this assertion. + */ + AssertedLiteralsOutMap d_assertedLiteralsOut; + + /** + * Shared literals queud up to be asserted to the individual theories. + */ + std::vector<SharedLiteral> d_propagatedSharedLiterals; + + void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory) + { + d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory)); + } + + /** + * Assert the shared literals that are queued up to the theories. + */ + void outputSharedLiterals(); /** * Literals that are propagated by the theory. Note that these are TNodes. @@ -336,11 +374,6 @@ class TheoryEngine { context::CDO<unsigned> d_propagatedLiteralsIndex; /** - * Shared term equalities that should be asserted to the individual theories. - */ - std::vector<SharedEquality> d_propagatedEqualities; - - /** * Decisions that are requested via propagateAsDecision(). The theory * can only request decisions on nodes that have an assigned litearl in * the SAT solver and are hence referenced in the SAT solver (making the @@ -466,6 +499,20 @@ public: return d_propEngine; } +private: + + /** + * Helper for preprocess + */ + Node ppTheoryRewrite(TNode term); + +public: + + /** + * Signal the start of a new round of assertion preprocessing + */ + void preprocessStart(); + /** * Runs theory specific preprocesssing on the non-Boolean parts of * the formula. This is only called on input assertions, after ITEs @@ -519,15 +566,6 @@ public: void preRegister(TNode preprocessed); /** - * Call the theories to perform one last rewrite on the theory atoms - * if they wish. This last rewrite is only performed on the input atoms. - * At this point it is ensured that atoms do not contain any Boolean - * strucure, i.e. there is no ITE nodes in them. - * - */ - Node preCheckRewrite(TNode node); - - /** * Assert the formula to the appropriate theory. * @param node the assertion */ @@ -568,6 +606,7 @@ public: void getPropagatedLiterals(std::vector<TNode>& literals) { for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { + Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); } } @@ -589,8 +628,40 @@ public: bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; + enum ExplainTaskKind { + // Literal sent out from the theory engine + SHARED_LITERAL_OUT, + // Explanation produced by a theory + THEORY_EXPLANATION, + // Explanation produced by the shared terms database + SHARED_DATABASE_EXPLANATION + }; + + struct ExplainTask { + Node node; + ExplainTaskKind kind; + theory::TheoryId theory; + ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) : + node(n), kind(k), theory(tid) {} + bool operator == (const ExplainTask& other) const { + return node == other.node && kind == other.kind && theory == other.theory; + } + }; + + struct ExplainTaskHashFunction { + size_t operator () (const ExplainTask& task) const { + size_t hash = 0; + hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node); + hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2); + hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2); + return hash; + } + }; + Node getExplanation(TNode node); + Node explain(ExplainTask toExplain); + Node getValue(TNode node); /** |