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, 22 insertions, 42 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 217972dce..7d003bf25 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -50,6 +50,7 @@ namespace theory {
 class Instantiator;
 class InstStrategy;
 class QuantifiersEngine;
+class TheoryModel;
 
 /**
  * Information about an assertion for the theories.
@@ -330,12 +331,12 @@ public:
   static inline TheoryId theoryOf(TNode node) {
     return theoryOf(s_theoryOfMode, node);
   }
-  
+
   /** Set the theoryOf mode */
   static void setTheoryOfMode(TheoryOfMode mode) {
     s_theoryOfMode = mode;
   }
-  
+
   /**
    * Set the owner of the uninterpreted sort.
    */
@@ -545,40 +546,13 @@ public:
   }
 
   /**
-   * Return the value of a node (typically used after a ).  If the
-   * theory supports model generation but has no value for this node,
-   * it should return Node::null().  If the theory doesn't support
-   * model generation at all, or usually would but doesn't in its
-   * current state, it should throw an exception saying so.
-   *
-   * The TheoryEngine is passed in so that you can recursively request
-   * values for the Node's children.  This is important because the
-   * TheoryEngine takes care of simple cases (metakind CONSTANT,
-   * Boolean-valued VARIABLES, ...) and can dispatch to other theories
-   * if that's necessary.  Only call your own getValue() recursively
-   * if you *know* that you are responsible handle the Node you're
-   * asking for; other theories can use your types, so be careful
-   * here!  To be safe, it's best to delegate back to the
-   * TheoryEngine (by way of the Valuation proxy object, which avoids
-   * direct dependence on TheoryEngine).
-   *
-   * Usually, you need to handle at least the two cases of EQUAL and
-   * VARIABLE---EQUAL in case a value of yours is on the LHS of an
-   * EQUAL, and VARIABLE for variables of your types.  You also need
-   * to support any operators that can survive your rewriter.  You
-   * don't need to handle constants, as they are handled by the
-   * TheoryEngine.
-   *
-   * There are some gotchas here.  The user may be requesting the
-   * value of an expression that wasn't part of the satisfiable
-   * assertion, or has been declared since.  If you don't have a value
-   * and suspect this situation is the case, return Node::null()
-   * rather than throwing an exception.
-   */
-  virtual Node getValue(TNode n) {
-    Unimplemented("Theory %s doesn't support Theory::getValue interface",
+   * Get all relevant information in this theory regarding the current
+   * model.  This should be called after a call to check( FULL_EFFORT )
+   * for all theories with no conflicts and no lemmas added.
+   */
+  virtual void collectModelInfo( TheoryModel* m ){
+    Unimplemented("Theory %s doesn't support Theory::getModel interface",
                   identify().c_str());
-    return Node::null();
   }
 
   /**
@@ -824,7 +798,7 @@ protected:
   /** reset instantiation round */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process quantifier */
-  virtual int process( Node f, Theory::Effort effort, int e, int limitInst = 0 ) = 0;
+  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
 public:
   /** set has constraints from quantifier f */
   void setHasConstraintsFrom( Node f );
@@ -844,16 +818,22 @@ public:
   virtual void preRegisterTerm( Node t ) { }
   /** assertNode function, assertion was asserted to theory */
   virtual void assertNode( Node assertion ){}
-  /** reset instantiation round */
-  void resetInstantiationRound( Theory::Effort effort );
-  /** do instantiation method*/
-  int doInstantiation( Node f, Theory::Effort effort, int e, int limitInst = 0 );
   /** identify */
   virtual std::string identify() const { return std::string("Unknown"); }
   /** print debug information */
   virtual void debugPrint( const char* c ) {}
-  /** get status */
-  //int getStatus() { return d_status; }
+public:
+  /** reset instantiation round */
+  void resetInstantiationRound( Theory::Effort effort );
+  /** do instantiation method*/
+  int doInstantiation( Node f, Theory::Effort effort, int e );
+public:
+  /** general queries about equality */
+  virtual bool hasTerm( Node a ) { return false; }
+  virtual bool areEqual( Node a, Node b ) { return false; }
+  virtual bool areDisequal( Node a, Node b ) { return false; }
+  virtual Node getRepresentative( Node a ) { return a; }
+  virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); }
 };/* class Instantiator */
 
 inline Assertion Theory::get() {