merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

1 files changed, 12 insertions, 8 deletions

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index fb972b73f..7b6527517 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -123,14 +123,14 @@ private:
   bool propagateEquality(TNode equality, bool polarity);
 
   /** Theory engine */
-  TheoryEngine* d_theoryEngine;  
+  TheoryEngine* d_theoryEngine;
 
   /** Are we in conflict */
   context::CDO<bool> d_inConflict;
-  
+
   /** Conflicting terms, if any */
   Node d_conflictLHS, d_conflictRHS;
-  
+
   /** Polarity of the conflict */
   bool d_conflictPolarity;
 
@@ -166,7 +166,7 @@ public:
    */
   bool isKnown(TNode literal) const;
 
-  /** 
+  /**
    * Returns an explanation of the propagation that came from the database.
    */
   Node explain(TNode literal) const;
@@ -175,10 +175,10 @@ public:
    * Add an equality to propagate.
    */
   void addEqualityToPropagate(TNode equality);
-  
+
   /**
-   * Add a shared term to the database. The shared term is a subterm of the atom and 
-   * should be associated with the given theory. 
+   * Add a shared term to the database. The shared term is a subterm of the atom and
+   * should be associated with the given theory.
    */
   void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
 
@@ -211,7 +211,7 @@ public:
    * Get the theories that share the term and have been notified already.
    */
   theory::Theory::Set getNotifiedTheories(TNode term) const;
-   
+
   /**
    * Returns true if the term is currently registered as shared with some theory.
    */
@@ -238,6 +238,10 @@ public:
    */
   bool areDisequal(TNode a, TNode b) const;
 
+  /**
+   * get equality engine
+   */
+  theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 protected:
 
   /**