diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 49 |
1 files changed, 39 insertions, 10 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3d70ffa6b..f55c7c258 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,13 +42,14 @@ #include "util/cache.h" #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" +#include "theory/model.h" namespace CVC4 { /** - * A pair of a theory and a node. This is used to mark the flow of + * A pair of a theory and a node. This is used to mark the flow of * propagations between theories. - */ + */ struct NodeTheoryPair { Node node; theory::TheoryId theory; @@ -57,7 +58,7 @@ struct NodeTheoryPair { : node(node), theory(theory), timestamp(timestamp) {} NodeTheoryPair() : theory(theory::THEORY_LAST) {} - // Comparison doesn't take into account the timestamp + // Comparison doesn't take into account the timestamp bool operator == (const NodeTheoryPair& pair) const { return node == pair.node && theory == pair.theory; } @@ -84,7 +85,7 @@ class DecisionEngine; * CVC4. */ class TheoryEngine { - + /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; @@ -125,6 +126,15 @@ class TheoryEngine { */ theory::QuantifiersEngine* d_quantEngine; + /** + * Default model object + */ + theory::DefaultModel* d_curr_model; + /** + * Model builder object + */ + theory::TheoryEngineModelBuilder* d_curr_model_builder; + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; @@ -389,7 +399,7 @@ class TheoryEngine { * Adds a new lemma, returning its status. */ theory::LemmaStatus lemma(TNode node, bool negated, bool removable); - + /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -433,6 +443,13 @@ public: } /** + * Get a pointer to the underlying sat context. + */ + inline context::Context* getSatContext() const { + return d_context; + } + + /** * Get a pointer to the underlying quantifiers engine. */ theory::QuantifiersEngine* getQuantifiersEngine() const { @@ -472,12 +489,12 @@ private: void assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); /** - * Marks a theory propagation from a theory to a theory where a + * Marks a theory propagation from a theory to a theory where a * theory could be the THEORY_SAT_SOLVER for literals coming from * or being propagated to the SAT solver. If the receiving theory * already recieved the literal, the method returns false, otherwise * it returns true. - * + * * @param assertion the normalized assertion being sent * @param originalAssertion the actual assertion that was sent * @param toTheoryId the theory that is on the receiving end @@ -488,7 +505,7 @@ private: /** * Computes the explanation by travarsing the propagation graph and - * asking relevant theories to explain the propagations. Initially + * asking relevant theories to explain the propagations. Initially * the explanation vector should contain only the element (node, theory) * where the node is the one to be explained, and the theory is the * theory that sent the literal. @@ -623,9 +640,19 @@ public: Node getExplanation(TNode node); /** - * Returns the value of the given node. + * collect model info + */ + void collectModelInfo( theory::TheoryModel* m ); + + /** + * Get the current model */ - Node getValue(TNode node); + theory::TheoryModel* getModel(); + + /** + * Get the model builder + */ + theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; } /** * Get the theory associated to a given Node. @@ -685,6 +712,8 @@ public: Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector<Node>& assertions); + SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } + };/* class TheoryEngine */ }/* CVC4 namespace */ |