More bug fixes for interval models.

8 files changed, 112 insertions, 62 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 60d62391b..be6844a1e 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -665,4 +665,16 @@ bool FirstOrderModelFmc::isInterval(Node n) {
 
 Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
   return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub );
-}
\ No newline at end of file
+}
+
+bool FirstOrderModelFmc::isInRange( Node v, Node i ) {
+  for( unsigned b=0; b<2; b++ ){
+    if( !isStar( i[b] ) ){
+      if( ( b==0 && i[b].getConst<Rational>() > v.getConst<Rational>() ) ||
+          ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 14e9441b4..f6e012660 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -155,6 +155,7 @@ public:
   Node getSomeDomainElement(TypeNode tn);
   bool isInterval(Node n);
   Node getInterval( Node lb, Node ub );
+  bool isInRange( Node v, Node i );
 };
 
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ed5dea679..2be9de91c 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -97,17 +97,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
           exit( 11 );

         }

         //check if it is in the range

-        bool inRange = true;

-        for( unsigned b=0; b<2; b++ ){

-          if( !m->isStar( it->first[b] ) ){

-            if( ( b==0 && it->first[b].getConst<Rational>() > inst[index].getConst<Rational>() ) ||

-                ( b==1 && it->first[b].getConst<Rational>() <= inst[index].getConst<Rational>() ) ){

-              inRange = false;

-              break;

-            }

-          }

-        }

-        if( inRange ){

+        if( m->isInRange(inst[index], it->first )  ){

           int gindex = it->second.getGeneralizationIndex(m, inst, index+1);

           if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){

             minIndex = gindex;

@@ -292,7 +282,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
       std::vector< Node > nc;

       nc.push_back( cc.getOperator() );

       for( unsigned j=0; j< cc.getNumChildren(); j++){

-        nc.push_back(m->getStar(cc[j].getType()));

+        nc.push_back(m->getStarElement(cc[j].getType()));

       }

       cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );

       //re-add the entries

@@ -331,19 +321,15 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);

 }

 

+bool FullModelChecker::optBuildAtFullModel() {

+  //need to build after full model has taken effect if we are constructing interval models

+  //  this is because we need to have a constant in all integer equivalence classes

+  return options::fmfFmcInterval();

+}

+

 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){

   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();

-  if( fullModel ){

-    //make function values

-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){

-      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );

-    }

-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );

-    //mark that the model has been set

-    fm->markModelSet();

-    //debug the model

-    debugModel( fm );

-  }else{

+  if( fullModel==optBuildAtFullModel() ){

     Trace("fmc") << "---Full Model Check reset() " << std::endl;

     fm->initialize( d_considerAxioms );

     d_quant_models.clear();

@@ -464,6 +450,9 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         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;

+          }

           children.push_back(ri);

           if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){

             if (fm->isModelBasisTerm(ri) ) {

@@ -475,7 +464,10 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           entry_children.push_back(ri);

         }

         Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );

-        Node nv = fm->getUsedRepresentative( v);

+        Node nv = fm->getUsedRepresentative( v );

+        if( !nv.getType().isSort() && !nv.isConst() ){

+          Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;

+        }

         Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );

         if( std::find(conds.begin(), conds.end(), n )==conds.end() ){

           Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;

@@ -555,6 +547,17 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       Trace("fmc-model") << std::endl;

     }

   }

+  if( fullModel ){

+    //make function values

+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){

+      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );

+    }

+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );

+    //mark that the model has been set

+    fm->markModelSet();

+    //debug the model

+    debugModel( fm );

+  }

 }

 

 void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {

@@ -722,6 +725,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
           riter.d_bounds[b][i] = c[i][b];

         }

       }

+    }else if( !fm->isStar(c[i]) ){

+      riter.d_bounds[0][i] = c[i];

+      riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );

     }

   }

   //initialize

@@ -915,19 +921,23 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
   if (eq[0]==eq[1]){

     d.addEntry(fm, mkCond(cond), d_true);

   }else{

-    int j = getVariableId(f, eq[0]);

-    int k = getVariableId(f, eq[1]);

     TypeNode tn = eq[0].getType();

-    if( !fm->d_rep_set.hasType( tn ) ){

-      getSomeDomainElement( fm, tn );  //to verify the type is initialized

-    }

-    for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {

-      Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );

-      cond[j+1] = r;

-      cond[k+1] = r;

-      d.addEntry( fm, mkCond(cond), d_true);

+    if( tn.isSort() ){

+      int j = getVariableId(f, eq[0]);

+      int k = getVariableId(f, eq[1]);

+      if( !fm->d_rep_set.hasType( tn ) ){

+        getSomeDomainElement( fm, tn );  //to verify the type is initialized

+      }

+      for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {

+        Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );

+        cond[j+1] = r;

+        cond[k+1] = r;

+        d.addEntry( fm, mkCond(cond), d_true);

+      }

+      d.addEntry( fm, mkCondDefault(fm, f), d_false);

+    }else{

+      d.addEntry( fm, mkCondDefault(fm, f), Node::null());

     }

-    d.addEntry( fm, mkCondDefault(fm, f), d_false);

   }

 }

 

@@ -1058,14 +1068,22 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }

     }else{

       if( !v.isNull() ){

-        if (curr.d_child.find(v)!=curr.d_child.end()) {

-          Trace("fmc-uf-process") << "follow value..." << std::endl;

-          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);

-        }

-        Node st = fm->getStarElement(v.getType());

-        if (curr.d_child.find(st)!=curr.d_child.end()) {

-          Trace("fmc-uf-process") << "follow star..." << std::endl;

-          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);

+        if( options::fmfFmcInterval() && v.getType().isInteger() ){

+          for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {

+            if( fm->isInRange( v, it->first ) ){

+              doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);

+            }

+          }

+        }else{

+          if (curr.d_child.find(v)!=curr.d_child.end()) {

+            Trace("fmc-uf-process") << "follow value..." << std::endl;

+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);

+          }

+          Node st = fm->getStarElement(v.getType());

+          if (curr.d_child.find(st)!=curr.d_child.end()) {

+            Trace("fmc-uf-process") << "follow star..." << std::endl;

+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);

+          }

         }

       }

     }

@@ -1187,6 +1205,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
 }

 

 void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {

+  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;

   //get function symbol for f

   cond.push_back(d_quant_cond[f]);

   for (unsigned i=0; i<f[0].getNumChildren(); i++) {

@@ -1277,7 +1296,7 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
 

 

 bool FullModelChecker::useSimpleModels() {

-  return options::fmfFullModelCheckSimple();

+  return options::fmfFmcSimple();

 }

 

 void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 2cb2198ef..8ebef640c 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -130,6 +130,8 @@ public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );

   ~FullModelChecker(){}

 

+  bool optBuildAtFullModel();

+

   int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }

 

   void debugPrintCond(const char * tr, Node n, bool dispStar = false);

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index b1851cfa4..073f7057b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -50,6 +50,9 @@ bool QModelBuilder::optUseModel() {
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
   if( Trace.isOn("quant-model-warn") ){
+    Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl;
+    int tests = 0;
+    int bad = 0;
     for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
       std::vector< Node > vars;
@@ -57,20 +60,30 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
         vars.push_back( f[0][j] );
       }
       RepSetIterator riter( d_qe, &(fm->d_rep_set) );
-      riter.setQuantifier( f );
-      while( !riter.isFinished() ){
-        std::vector< Node > terms;
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          terms.push_back( riter.getTerm( i ) );
+      if( riter.setQuantifier( f ) ){
+        while( !riter.isFinished() ){
+          tests++;
+          std::vector< Node > terms;
+          for( int i=0; i<riter.getNumTerms(); i++ ){
+            terms.push_back( riter.getTerm( i ) );
+          }
+          Node n = d_qe->getInstantiation( f, vars, terms );
+          Node val = fm->getValue( n );
+          if( val!=fm->d_true ){
+            Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
+            Trace("quant-model-warn") << "         " << f << std::endl;
+            Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+            bad++;
+          }
+          riter.increment();
         }
-        Node n = d_qe->getInstantiation( f, vars, terms );
-        Node val = fm->getValue( n );
-        if( val!=fm->d_true ){
-          Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
-          Trace("quant-model-warn") << "         " << f << std::endl;
-          Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+        Trace("quant-model-warn") << "Tested " << tests << " instantiations";
+        if( bad>0 ){
+          Trace("quant-model-warn") << ", " << bad << " failed" << std::endl;
         }
-        riter.increment();
+        Trace("quant-model-warn") << "." << std::endl;
+      }else{
+        Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 0d7c146ba..b96c58767 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -42,6 +42,8 @@ public:
   virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
+  //whether to construct model at fullModel = true
+  virtual bool optBuildAtFullModel() { return false; }
   //consider axioms
   bool d_considerAxioms;
   /** number of lemmas generated while building model */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index c0fe23b94..0678e230f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -55,6 +55,7 @@ void ModelEngine::check( Theory::Effort e ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
     }
     ++(d_statistics.d_inst_rounds);
+    bool buildAtFullModel = d_builder->optBuildAtFullModel();
     //two effort levels: first try exhaustive instantiation without axioms, then with.
     int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
     for( int effort=startEffort; effort<2; effort++ ){
@@ -66,7 +67,7 @@ void ModelEngine::check( Theory::Effort e ){
         Trace("model-engine-debug") << "Build model..." << std::endl;
         d_builder->d_considerAxioms = effort>=1;
         d_builder->d_addedLemmas = 0;
-        d_builder->buildModel( fm, false );
+        d_builder->buildModel( fm, buildAtFullModel );
         addedLemmas += (int)d_builder->d_addedLemmas;
         //if builder has lemmas, add and return
         if( addedLemmas==0 ){
@@ -103,7 +104,7 @@ void ModelEngine::check( Theory::Effort e ){
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      if( options::produceModels() ){
+      if( options::produceModels() && !buildAtFullModel ){
         // finish building the model
         d_builder->buildModel( fm, true );
       }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 1e6f04162..d44f2e770 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -95,10 +95,10 @@ option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
 
 option fmfFullModelCheck --fmf-fmc bool :default false
  enable full model check for finite model finding
-option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
+option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
  disable simple models in full model check for finite model finding
-option fmfFmcCoverSimplify --fmf-fmc-cover-simplify bool :default false
- apply covering simplification technique to fmc models
+option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
+ disable covering simplification of fmc models
 option fmfFmcInterval --fmf-fmc-interval bool :default false
  construct interval models for fmc models