merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

4 files changed, 8 insertions, 152 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ca2d74cf7..e159c0e42 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1925,17 +1925,17 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   }
 }
 
-void TheoryArith::collectModelInfo( TheoryModel* m ){
+void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(d_qflraStatus ==  Result::SAT);
 
-  Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;  
+  Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
   // Delta lasts at least the duration of the function call
   const Rational& delta = d_partialModel.getDelta();
 
   // TODO:
   // This is not very good for user push/pop....
-  // Revisit when implementing push/pop 
+  // Revisit when implementing push/pop
   for(ArithVar v = 0; v < d_variables.size(); ++v){
     if(!isSlackVariable(v)){
       Node term = d_arithvarNodeMap.asNode(v);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 35fcca406..a8c025452 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);
 
-  void collectModelInfo( TheoryModel* m );
+  void collectModelInfo( TheoryModel* m, bool fullModel );
 
   void shutdown(){ }
 
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index 51e3a6638..8d0815ee7 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -27,11 +27,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-#define ARITH_INSTANTIATOR_USE_DELTA
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
-#define ARITH_INSTANTIATOR_STRONG_DELTA_LEMMA
-
-#define USE_ARITH_INSTANTIATION
 
 InstStrategySimplex::InstStrategySimplex( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
     InstStrategy( ie ), d_th( th ), d_counter( 0 ){
@@ -97,87 +93,6 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
   return STATUS_UNKNOWN;
 }
 
-//void InstStrategySimplexUfMatch::resetInstantiationRound(){
-//
-//}
-//
-//int InstStrategySimplexUfMatch::process( Node f, int effort ){
-//  if( effort<2 ){
-//    return STATUS_UNFINISHED;
-//  }else if( effort==2 ){
-//    for( int j=0; j<(int)d_th->d_instRows[f].size(); j++ ){
-//      ArithVar x = d_th->d_instRows[f][j];
-//      if( !d_th->d_ceTableaux[x].empty() && !d_th->d_tableaux_ce_term[x].empty() ){
-//        if( d_tableaux_ce_term_trigger.find( x )==d_tableaux_ce_term_trigger.end() ){
-//          std::vector< Node > terms;
-//          for( std::map< Node, Node >::iterator it = d_th->d_tableaux_ce_term[x].begin(); it != d_th->d_tableaux_ce_term[x].end(); ++it ){
-//            terms.push_back( it->first );
-//          }
-//          d_tableaux_ce_term_trigger[x] = new Trigger( d_quantEngine, f, terms );
-//        }else{
-//          d_tableaux_ce_term_trigger[x]->resetInstantiationRound();
-//        }
-//        Node term;
-//        bool addedLemma = false;
-//        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 ) ){
-//              ++(d_th->d_statistics.d_instantiations_match_pure);
-//              ++(d_th->d_statistics.d_instantiations);
-//              addedLemma = true;
-//            }
-//          }else{
-//            NodeBuilder<> plus_term(kind::PLUS);
-//            plus_term << d_th->d_tableaux_term[x];
-//            //Debug("quant-arith") << "Produced this match for ce_term_tableaux: " << std::endl;
-//            //m->debugPrint("quant-arith");
-//            //Debug("quant-arith") << std::endl;
-//            std::vector< Node > vars;
-//            std::vector< Node > matches;
-//            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 ] );
-//              }
-//            }
-//            Node var;
-//            //otherwise try to find a variable that is not specified in m
-//            for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
-//              if( m->d_map[ it->first ]!=Node::null() ){
-//                plus_term << NodeManager::currentNM()->mkNode( MULT, it->second, d_th->getTableauxValue( m->d_map[ it->first ] ) );
-//              }else if( var==Node::null() ){
-//                var = it->first;
-//              }
-//            }
-//            for( std::map< Node, Node >::iterator it = d_th->d_tableaux_ce_term[x].begin(); it != d_th->d_tableaux_ce_term[x].end(); ++it ){
-//              Node n = it->first;
-//              //substitute in matches
-//              n = n.substitute( vars.begin(), vars.end(), matches.begin(), matches.end() );
-//              plus_term << NodeManager::currentNM()->mkNode( MULT, it->second, d_th->getTableauxValue( n ) );
-//            }
-//            term = plus_term.getNumChildren()==1 ? plus_term.getChild( 0 ) : plus_term;
-//            if( var!=Node::null() ){
-//              if( d_th->doInstantiation( f, term, x, m, var ) ){
-//                addedLemma = true;
-//                ++(d_th->d_statistics.d_instantiations_match_var);
-//              }
-//            }else{
-//              if( d_quantEngine->addInstantiation( f, m ) ){
-//                addedLemma = true;
-//                ++(d_th->d_statistics.d_instantiations_match_no_var);
-//                ++(d_th->d_statistics.d_instantiations);
-//              }
-//            }
-//          }
-//        }
-//      }
-//    }
-//  }
-//  return STATUS_UNKNOWN;
-//}
-
 InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
 Instantiator( c, ie, th ){
   if( options::cbqi() ){
@@ -392,59 +307,21 @@ Node InstantiatorTheoryArith::getTableauxValue( Node n, bool minus_delta ){
 }
 
 Node InstantiatorTheoryArith::getTableauxValue( ArithVar v, bool minus_delta ){
+  const Rational& delta = ((TheoryArith*)getTheory())->d_partialModel.getDelta();
   DeltaRational drv = ((TheoryArith*)getTheory())->d_partialModel.getAssignment( v );
-  Node val = NodeManager::currentNM()->mkConst( drv.getNoninfinitesimalPart() );
-#ifdef ARITH_INSTANTIATOR_USE_DELTA
-  //the tableaux value for v may contain an infinitesemal part: getDelta( val ) will return a fresh variable "delta"
-  //  (one for each sort) for which the lemma ( delta > 0 ) is asserted.
-  if( drv.getInfinitesimalPart()!=0 ){
-    Node delta = NodeManager::currentNM()->mkNode( MULT, getDelta( val ),
-                                                    NodeManager::currentNM()->mkConst( drv.getInfinitesimalPart() ) );
-    // add (or subtract) this delta component from the value of v
-    val = NodeManager::currentNM()->mkNode( minus_delta ? MINUS : PLUS, val, delta );
-  }
-#endif
-  return val;
-}
-
-Node InstantiatorTheoryArith::getDelta( Node n ){
-  std::map< TypeNode, Node >::iterator it = d_deltas.find( n.getType() );
-  if( it==d_deltas.end() ){
-    std::ostringstream os;
-    os << "delta_" << d_deltas.size();
-    Node delta = NodeManager::currentNM()->mkSkolem( os.str(), n.getType() );
-    d_deltas[ n.getType() ] = delta;
-    Node gt = NodeManager::currentNM()->mkNode( GT, delta, NodeManager::currentNM()->mkConst( Rational(0) ) );
-    //add split
-#ifdef ARITH_INSTANTIATOR_STRONG_DELTA_LEMMA
-    d_quantEngine->addLemma( gt );
-#else
-    gt = Rewriter::rewrite( gt );
-    d_quantEngine->addSplit( gt, true, true );
-#endif
-    return delta;
-  }
-  return it->second;
+  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
+  return mkRationalNode(qmodel);
 }
 
 InstantiatorTheoryArith::Statistics::Statistics():
   d_instantiations("InstantiatorTheoryArith::Instantiations_Total", 0),
-  d_instantiations_minus("InstantiatorTheoryArith::Instantiations_minus_delta", 0),
-  d_instantiations_match_pure("InstantiatorTheoryArith::Instantiations_via_pure_matching", 0),
-  d_instantiations_match_var("InstantiatorTheoryArith::Instantiations_via_matching_var", 0),
-  d_instantiations_match_no_var("InstantiatorTheoryArith::Instantiations_via_matching_no_var", 0)
+  d_instantiations_minus("InstantiatorTheoryArith::Instantiations_minus_delta", 0)
 {
   StatisticsRegistry::registerStat(&d_instantiations);
   StatisticsRegistry::registerStat(&d_instantiations_minus);
-  StatisticsRegistry::registerStat(&d_instantiations_match_pure);
-  StatisticsRegistry::registerStat(&d_instantiations_match_var);
-  StatisticsRegistry::registerStat(&d_instantiations_match_no_var);
 }
 
 InstantiatorTheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_instantiations);
   StatisticsRegistry::unregisterStat(&d_instantiations_minus);
-  StatisticsRegistry::unregisterStat(&d_instantiations_match_pure);
-  StatisticsRegistry::unregisterStat(&d_instantiations_match_var);
-  StatisticsRegistry::unregisterStat(&d_instantiations_match_no_var);
 }
diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h
index 406478a2a..a7602cf28 100644
--- a/src/theory/arith/theory_arith_instantiator.h
+++ b/src/theory/arith/theory_arith_instantiator.h
@@ -48,22 +48,6 @@ public:
   /** identify */
   std::string identify() const { return std::string("Simplex"); }
 };
-//
-//class InstStrategySimplexUfMatch : public InstStrategy{
-//private:
-//  /** InstantiatorTheoryUf class */
-//  InstantiatorTheoryArith* d_th;
-//  /** trigger for instantiation rows */
-//  std::map< ArithVar, Trigger* > d_tableaux_ce_term_trigger;
-//public:
-//  InstStrategySimplexUfMatch( InstantiatorTheoryArith* th, QuantifiersEngine* ie ) :
-//      InstStrategy( ie ), d_th( th ){}
-//  ~InstStrategySimplexUfMatch(){}
-//  void resetInstantiationRound();
-//  int process( Node f, Theory::Effort effort, int e, int instLimit );
-//  /** identify */
-//  std::string identify() const { return std::string("SimplexUfMatch"); }
-//};
 
 class InstantiatorTheoryArith : public Instantiator{
   friend class QuantifiersEngine;
@@ -105,16 +89,11 @@ private:
   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 */
-  Node getDelta( Node n );
 
   class Statistics {
   public:
     IntStat d_instantiations;
     IntStat d_instantiations_minus;
-    IntStat d_instantiations_match_pure;
-    IntStat d_instantiations_match_var;
-    IntStat d_instantiations_match_no_var;
     Statistics();
     ~Statistics();
   };