Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.

6 files changed, 96 insertions, 84 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index cc0b18ffe..345a5eaef 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -463,9 +463,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         lem = Rewriter::rewrite( lem );
         Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
         Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
-        d_quantEngine->addLemma( lem );
-        ++(d_statistics.d_cegqi_lemmas_refine);
-        conj->d_refine_count++;
+        bool res = d_quantEngine->addLemma( lem );
+        if( res ){
+          ++(d_statistics.d_cegqi_lemmas_refine);
+          conj->d_refine_count++;
+        }else{
+          Trace("cegqi-engine") << "  ...FAILED to add refinement!" << std::endl;
+        }
       }
     }
     conj->d_ce_sk.clear();
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index aa2a43fbf..272f16be8 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -90,15 +90,19 @@ void FirstOrderModel::initialize() {
     }
     processInitializeQuantifier( f );
     //initialize relevant models within bodies of all quantifiers
-    initializeModelForTerm( f[1] );
+    std::map< Node, bool > visited;
+    initializeModelForTerm( f[1], visited );
   }
   processInitialize( false );
 }
 
-void FirstOrderModel::initializeModelForTerm( Node n ){
-  processInitializeModelForTerm( n );
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    initializeModelForTerm( n[i] );
+void FirstOrderModel::initializeModelForTerm( Node n, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    processInitializeModelForTerm( n );
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      initializeModelForTerm( n[i], visited );
+    }
   }
 }
 
@@ -574,15 +578,6 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
         Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
       }
     }
-/*
-    Node r = getRepresentative(n);
-    if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){
-      if (r==d_model_basis_rep[tn]) {
-        r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-      }
-    }
-    return r;
-*/
     return getRepresentative(n);
   }
 }
@@ -609,7 +604,6 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) {
     for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
       it->second->reset();
     }
-    d_model_basis_rep.clear();
   }
 }
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index a31e85d7e..d42eb61e3 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -67,7 +67,7 @@ public: //for Theory Quantifiers:
   /** get number to reduce quantifiers */
   unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); }
   /** initialize model for term */
-  void initializeModelForTerm( Node n );
+  void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
   virtual void processInitializeModelForTerm( Node n ) = 0;
   virtual void processInitializeQuantifier( Node q ) {}
 public:
@@ -169,7 +169,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 private:
   /** models for UF */
   std::map<Node, Def * > d_models;
-  std::map<TypeNode, Node > d_model_basis_rep;
   std::map<TypeNode, Node > d_type_star;
   Node intervalOp;
   Node getUsedRepresentative(Node n, bool strict = false);
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index f0858f4e9..00a5241f5 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -325,11 +325,46 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
+void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+  FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+  if( !fullModel ){
+    Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+    d_preinitialized_types.clear();
+    //traverse equality engine
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+    std::map< TypeNode, int > typ_num;
+    while( !eqcs_i.isFinished() ){
+      TypeNode tr = (*eqcs_i).getType();
+      d_preinitialized_types[tr] = true;
+      ++eqcs_i;
+    }
+
+    //must ensure model basis terms exists in model for each relevant type
+    fm->initialize();
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      Node op = it->first;
+      TypeNode tno = op.getType();
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {
+        preInitializeType( fm, tno[i] );
+      }
+    }
+    //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
+    if( !options::fmfEmptySorts() ){
+      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node q = fm->getAssertedQuantifier( i );
+        //make sure all types are set
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          preInitializeType( fm, q[0][i].getType() );
+        }
+      }
+    }
+  }
+}
+
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   if( !fullModel ){
     Trace("fmc") << "---Full Model Check reset() " << std::endl;
-    fm->initialize();
     d_quant_models.clear();
     d_rep_ids.clear();
     d_star_insts.clear();
@@ -338,50 +373,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
          it != fm->d_rep_set.d_type_reps.end(); ++it ){
       if( it->first.isSort() ){
         Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
-        Node rmbt = fm->getUsedRepresentative( mbt);
-        int mbt_index = -1;
-        Trace("fmc") << "  Model basis term : " << mbt << std::endl;
         for( size_t a=0; a<it->second.size(); a++ ){
           Node r = fm->getUsedRepresentative( it->second[a] );
-          std::vector< Node > eqc;
-          ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
-          Trace("fmc-model-debug") << "   " << (it->second[a]==r) << (r==mbt);
-          Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
-          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
-          Trace("fmc-model-debug") << " {";
-          //find best selection for representative
-          for( size_t i=0; i<eqc.size(); i++ ){
-            Trace("fmc-model-debug") << eqc[i] << ", ";
-          }
-          Trace("fmc-model-debug") << "}" << std::endl;
-
-          //if this is the model basis eqc, replace with actual model basis term
-          if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
-            fm->d_model_basis_rep[it->first] = r;
-            r = mbt;
-            mbt_index = a;
+          if( Trace.isOn("fmc-model-debug") ){
+            std::vector< Node > eqc;
+            ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+            Trace("fmc-model-debug") << "   " << (it->second[a]==r);
+            Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+            //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+            Trace("fmc-model-debug") << " {";
+            for( size_t i=0; i<eqc.size(); i++ ){
+              Trace("fmc-model-debug") << eqc[i] << ", ";
+            }
+            Trace("fmc-model-debug") << "}" << std::endl;
           }
           d_rep_ids[it->first][r] = (int)a;
         }
         Trace("fmc-model-debug") << std::endl;
-
-        if (mbt_index==-1) {
-          std::cout << "   WARNING: model basis term is not a representative!" << std::endl;
-          exit(0);
-        }else{
-          Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
-        }
-      }
-    }
-    //also process non-rep set sorts
-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      Node op = it->first;
-      TypeNode tno = op.getType();
-      for( unsigned i=0; i<tno.getNumChildren(); i++) {
-        initializeType( fm, tno[i] );
       }
     }
+
     //now, make models
     for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
       Node op = it->first;
@@ -433,24 +444,26 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         entry_children.push_back(op);
         bool hasNonStar = false;
         for( unsigned i=0; i<c.getNumChildren(); i++) {
-          Node ri = fm->getUsedRepresentative( c[i]);
-          if( !ri.getType().isSort() && !ri.isConst() ){
-            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
-            Assert( false );
-          }
+          Node ri = fm->getUsedRepresentative( c[i] );
           children.push_back(ri);
+          bool isStar = false;
           if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
             if (fm->isModelBasisTerm(ri) ) {
               ri = fm->getStar( ri.getType() );
+              isStar = true;
             }else{
               hasNonStar = true;
             }
           }
+          if( !isStar && !ri.isConst() ){
+            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
+            Assert( false );
+          }
           entry_children.push_back(ri);
         }
         Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
         Node nv = fm->getUsedRepresentative( v );
-        if( !nv.getType().isSort() && !nv.isConst() ){
+        if( !nv.isConst() ){
           Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;
           Assert( false );
         }
@@ -523,20 +536,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
   }
 }
 
-void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
-  if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
-    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
-    Node mbn;
-    if (!fm->d_rep_set.hasType(tn)) {
-      mbn = fm->getSomeDomainElement(tn);
-    }else{
-      mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
+  if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
+    d_preinitialized_types[tn] = true;
+    Node mb = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    if( !mb.isConst() ){
+      Trace("fmc") << "...add model basis term to EE of model " << mb << " " << tn << std::endl;
+      fm->d_equalityEngine->addTerm( mb );
+      fm->addTerm( mb );
     }
-    Trace("fmc") << "Get used rep for " << mbn << std::endl;
-    Node mbnr = fm->getUsedRepresentative( mbn );
-    Trace("fmc") << "...got  " << mbnr << std::endl;
-    fm->d_model_basis_rep[tn] = mbnr;
-    Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
   }
 }
 
@@ -591,10 +599,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" );
         d_quant_cond[f] = op;
       }
-      //make sure all types are set
-      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-        initializeType( fmfmc, f[0][i].getType() );
-      }
 
       if( options::mbqiMode()==MBQI_NONE ){
         //just exhaustive instantiate
@@ -643,6 +647,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
               Node ev = d_quant_models[f].evaluate(fmfmc, inst);
               if (ev==d_true) {
                 addInst = false;
+                Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl;
               }
             }else{
               //for debugging
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 29913d98d..c7bfcd189 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -92,8 +92,9 @@ protected:
   std::map<Node, Node > d_quant_cond;
   std::map< TypeNode, Node > d_array_cond;
   std::map< Node, Node > d_array_term_cond;
-  std::map<Node, std::vector< int > > d_star_insts;
-  void initializeType( FirstOrderModelFmc * fm, TypeNode tn );
+  std::map< Node, std::vector< int > > d_star_insts;
+  std::map< TypeNode, bool > d_preinitialized_types;
+  void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn );
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
 protected:
@@ -142,7 +143,8 @@ public:
 
   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
 
-  /** process build model */
+  /** process build model */  
+  void preProcessBuildModel(TheoryModel* m, bool fullModel); 
   void processBuildModel(TheoryModel* m, bool fullModel);
   /** get current model value */
   Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6dfd4c737..8bc9689bd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -971,7 +971,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
     }
     ret = NodeManager::currentNM()->mkNode( OR, nret, n_str_ind );
   }
-  Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
+  Trace("quantifiers-sk-debug") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
   //if it has an instantiation level, set the skolemized body to that level
   if( f.hasAttribute(InstLevelAttribute()) ){
     theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
@@ -1002,6 +1002,14 @@ Node TermDb::getSkolemizedBody( Node f ){
         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
       }
     }
+    if( Trace.isOn("quantifiers-sk") ){
+      Trace("quantifiers-sk") << "Skolemize : ";
+      for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
+        Trace("quantifiers-sk") << d_skolem_constants[f][i] << " ";
+      }
+      Trace("quantifiers-sk") << "for " << std::endl;
+      Trace("quantifiers-sk") << "   " << f << std::endl;
+    }
   }
   return d_skolem_body[ f ];
 }