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 */