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.

4 files changed, 21 insertions, 91 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 390ac280b..c68e9cf54 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -40,6 +40,7 @@
 #include "theory/arith/constraint.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
+#include "theory/model.h"
 
 #include <stdint.h>
 
@@ -1464,12 +1465,12 @@ void TheoryArith::check(Effort effortLevel){
     d_qflraStatus = Result::UNSAT;
     if(previous == Result::SAT){
       ++d_statistics.d_revertsOnConflicts;
-      Debug("arith::bt") << "clearing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl; 
+      Debug("arith::bt") << "clearing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
       revertOutOfConflict();
       d_simplex.clearQueue();
     }else{
       ++d_statistics.d_commitsOnConflicts;
-      Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl; 
+      Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
       d_partialModel.commitAssignmentChanges();
       revertOutOfConflict();
     }
@@ -1492,7 +1493,7 @@ void TheoryArith::check(Effort effortLevel){
       ++d_statistics.d_nontrivialSatChecks;
     }
 
-    Debug("arith::bt") << "committing sap inConflit"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl; 
+    Debug("arith::bt") << "committing sap inConflit"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
     d_partialModel.commitAssignmentChanges();
     d_unknownsInARow = 0;
     if(Debug.isOn("arith::consistency")){
@@ -1503,7 +1504,7 @@ void TheoryArith::check(Effort effortLevel){
     ++d_unknownsInARow;
     ++(d_statistics.d_unknownChecks);
     Assert(!fullEffort(effortLevel));
-    Debug("arith::bt") << "committing unknown"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl; 
+    Debug("arith::bt") << "committing unknown"  << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
     d_partialModel.commitAssignmentChanges();
     d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
     break;
@@ -1922,80 +1923,8 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   }
 }
 
-Node TheoryArith::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
+void TheoryArith::collectModelInfo( TheoryModel* m ){
 
-  Assert(d_qflraStatus == Result::SAT);
-
-  switch(n.getKind()) {
-  case kind::VARIABLE: {
-    ArithVar var = d_arithvarNodeMap.asArithVar(n);
-
-    DeltaRational drat = d_partialModel.getAssignment(var);
-    const Rational& delta = d_partialModel.getDelta();
-    Debug("getValue") << n << " " << drat << " " << delta << endl;
-    return nodeManager->
-      mkConst( drat.getNoninfinitesimalPart() +
-               drat.getInfinitesimalPart() * delta );
-  }
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  case kind::PLUS: { // 2+ args
-    Rational value(0);
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      value += d_valuation.getValue(*i).getConst<Rational>();
-    }
-    return nodeManager->mkConst(value);
-  }
-
-  case kind::MULT: { // 2+ args
-    Rational value(1);
-    for(TNode::iterator i = n.begin(),
-            iend = n.end();
-          i != iend;
-          ++i) {
-      value *= d_valuation.getValue(*i).getConst<Rational>();
-    }
-    return nodeManager->mkConst(value);
-  }
-
-  case kind::MINUS: // 2 args
-    // should have been rewritten
-    Unreachable();
-
-  case kind::UMINUS: // 1 arg
-    // should have been rewritten
-    Unreachable();
-
-  case kind::DIVISION: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() /
-                                 d_valuation.getValue(n[1]).getConst<Rational>() );
-
-  case kind::LT: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() <
-                                 d_valuation.getValue(n[1]).getConst<Rational>() );
-
-  case kind::LEQ: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() <=
-                                 d_valuation.getValue(n[1]).getConst<Rational>() );
-
-  case kind::GT: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() >
-                                 d_valuation.getValue(n[1]).getConst<Rational>() );
-
-  case kind::GEQ: // 2 args
-    return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() >=
-                                 d_valuation.getValue(n[1]).getConst<Rational>() );
-
-  default:
-    Unhandled(n.getKind());
-  }
 }
 
 bool TheoryArith::safeToReset() const {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index fd2925bf6..35fcca406 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -323,7 +323,7 @@ public:
   void propagate(Effort e);
   Node explain(TNode n);
 
-  Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
 
   void shutdown(){ }
 
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index f1b870c52..c4cb2f493 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/arith/theory_arith_instantiator.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
@@ -40,7 +41,7 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   d_counter++;
 }
 
-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int instLimit ){
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
   if( e<2 ){
     return STATUS_UNFINISHED;
   }else if( e==2 ){
@@ -99,7 +100,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int inst
 //
 //}
 //
-//int InstStrategySimplexUfMatch::process( Node f, int effort, int instLimit ){
+//int InstStrategySimplexUfMatch::process( Node f, int effort ){
 //  if( effort<2 ){
 //    return STATUS_UNFINISHED;
 //  }else if( effort==2 ){
@@ -120,7 +121,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int inst
 //        while( d_tableaux_ce_term_trigger[x]->getNextMatch() && !addedLemma ){
 //          InstMatch* m = d_tableaux_ce_term_trigger[x]->getCurrent();
 //          if( m->isComplete( f ) ){
-//            if( d_quantEngine->addInstantiation( f, m, true ) ){
+//            if( d_quantEngine->addInstantiation( f, m ) ){
 //              ++(d_th->d_statistics.d_instantiations_match_pure);
 //              ++(d_th->d_statistics.d_instantiations);
 //              addedLemma = true;
@@ -133,8 +134,8 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int inst
 //            //Debug("quant-arith") << std::endl;
 //            std::vector< Node > vars;
 //            std::vector< Node > matches;
-//            for( int i=0; i<d_quantEngine->getNumInstantiationConstants( f ); i++ ){
-//              Node ic = d_quantEngine->getInstantiationConstant( f, i );
+//            for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+//              Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
 //              if( m->d_map[ ic ]!=Node::null() ){
 //                vars.push_back( ic );
 //                matches.push_back( m->d_map[ ic ] );
@@ -162,7 +163,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e, int inst
 //                ++(d_th->d_statistics.d_instantiations_match_var);
 //              }
 //            }else{
-//              if( d_quantEngine->addInstantiation( f, m, true ) ){
+//              if( d_quantEngine->addInstantiation( f, m ) ){
 //                addedLemma = true;
 //                ++(d_th->d_statistics.d_instantiations_match_no_var);
 //                ++(d_th->d_statistics.d_instantiations);
@@ -242,7 +243,7 @@ void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort eff
   }
 }
 
-int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e, int instLimit ){
+int InstantiatorTheoryArith::process( Node f, Theory::Effort effort, int e ){
   Debug("quant-arith") << "Arith: Try to solve (" << effort << ") for " << f << "... " << std::endl;
   return InstStrategy::STATUS_UNKNOWN;
 }
@@ -316,11 +317,11 @@ void InstantiatorTheoryArith::debugPrint( const char* c ){
     Node f = d_quantEngine->getQuantifier( q );
     Debug(c) << f << std::endl;
     Debug(c) << "   Inst constants: ";
-    for( int i=0; i<(int)d_quantEngine->getNumInstantiationConstants( f ); i++ ){
+    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
       if( i>0 ){
         Debug( c ) << ", ";
       }
-      Debug( c ) << d_quantEngine->getInstantiationConstant( f, i );
+      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
     }
     Debug(c) << std::endl;
     Debug(c) << "   Instantiation rows: ";
@@ -377,7 +378,7 @@ bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, I
   //use as instantiation value for var
   m.d_map[ var ] = instVal;
   Debug("quant-arith") << "Add instantiation " << m << std::endl;
-  return d_quantEngine->addInstantiation( f, m, true );
+  return d_quantEngine->addInstantiation( f, m );
 }
 
 Node InstantiatorTheoryArith::getTableauxValue( Node n, bool minus_delta ){
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
index 3880a49a7..406478a2a 100644
--- a/src/theory/arith/theory_arith_instantiator.h
+++ b/src/theory/arith/theory_arith_instantiator.h
@@ -41,7 +41,7 @@ private:
   Node d_negOne;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e, int instLimit );
+  int process( Node f, Theory::Effort effort, int e );
 public:
   InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie );
   ~InstStrategySimplex(){}
@@ -56,7 +56,7 @@ public:
 //  /** trigger for instantiation rows */
 //  std::map< ArithVar, Trigger* > d_tableaux_ce_term_trigger;
 //public:
-//  InstStrategySimplexUfMatch( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) : 
+//  InstStrategySimplexUfMatch( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
 //      InstStrategy( ie ), d_th( th ){}
 //  ~InstStrategySimplexUfMatch(){}
 //  void resetInstantiationRound();
@@ -102,7 +102,7 @@ private:
   /**  reset instantiation */
   void processResetInstantiationRound( Theory::Effort effort );
   /** process at effort */
-  int process( Node f, Theory::Effort effort, int e, int instLimit );
+  int process( Node f, Theory::Effort effort, int e );
   /** add term to row */
   void addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t );
   /** get delta for node */