More bug fixes for interval models.

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 60d62391bb21d9fc144f440d2feb4472b5b9d2e9..be6844a1ec2b1ac8fe734f2080877318d339eda8 100644 (file)
--- 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 14e9441b4a16878bd007f9a517b94aaa7a3031b9..f6e01266063c4fece37f0dc108ef29ea20a7a965 100644 (file)
--- 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 ed5dea6796ba3d09c28f6a3987b9c560f494fffa..2be9de91c52d259f08395ee7678e59255a1c279a 100755 (executable)
--- 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 );\r
         }\r
         //check if it is in the range\r
-        bool inRange = true;\r
-        for( unsigned b=0; b<2; b++ ){\r
-          if( !m->isStar( it->first[b] ) ){\r
-            if( ( b==0 && it->first[b].getConst<Rational>() > inst[index].getConst<Rational>() ) ||\r
-                ( b==1 && it->first[b].getConst<Rational>() <= inst[index].getConst<Rational>() ) ){\r
-              inRange = false;\r
-              break;\r
-            }\r
-          }\r
-        }\r
-        if( inRange ){\r
+        if( m->isInRange(inst[index], it->first )  ){\r
           int gindex = it->second.getGeneralizationIndex(m, inst, index+1);\r
           if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
             minIndex = gindex;\r
@@ -292,7 +282,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
       std::vector< Node > nc;\r
       nc.push_back( cc.getOperator() );\r
       for( unsigned j=0; j< cc.getNumChildren(); j++){\r
-        nc.push_back(m->getStar(cc[j].getType()));\r
+        nc.push_back(m->getStarElement(cc[j].getType()));\r
       }\r
       cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );\r
       //re-add the entries\r
@@ -331,19 +321,15 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);\r
 }\r
 \r
+bool FullModelChecker::optBuildAtFullModel() {\r
+  //need to build after full model has taken effect if we are constructing interval models\r
+  //  this is because we need to have a constant in all integer equivalence classes\r
+  return options::fmfFmcInterval();\r
+}\r
+\r
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){\r
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();\r
-  if( fullModel ){\r
-    //make function values\r
-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){\r
-      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );\r
-    }\r
-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
-    //mark that the model has been set\r
-    fm->markModelSet();\r
-    //debug the model\r
-    debugModel( fm );\r
-  }else{\r
+  if( fullModel==optBuildAtFullModel() ){\r
     Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
     fm->initialize( d_considerAxioms );\r
     d_quant_models.clear();\r
@@ -464,6 +450,9 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         bool hasNonStar = false;\r
         for( unsigned i=0; i<c.getNumChildren(); i++) {\r
           Node ri = fm->getUsedRepresentative( c[i]);\r
+          if( !ri.getType().isSort() && !ri.isConst() ){\r
+            Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;\r
+          }\r
           children.push_back(ri);\r
           if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){\r
             if (fm->isModelBasisTerm(ri) ) {\r
@@ -475,7 +464,10 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           entry_children.push_back(ri);\r
         }\r
         Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
-        Node nv = fm->getUsedRepresentative( v);\r
+        Node nv = fm->getUsedRepresentative( v );\r
+        if( !nv.getType().isSort() && !nv.isConst() ){\r
+          Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;\r
+        }\r
         Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
         if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
           Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
@@ -555,6 +547,17 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       Trace("fmc-model") << std::endl;\r
     }\r
   }\r
+  if( fullModel ){\r
+    //make function values\r
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){\r
+      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );\r
+    }\r
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
+    //mark that the model has been set\r
+    fm->markModelSet();\r
+    //debug the model\r
+    debugModel( fm );\r
+  }\r
 }\r
 \r
 void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {\r
@@ -722,6 +725,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
           riter.d_bounds[b][i] = c[i][b];\r
         }\r
       }\r
+    }else if( !fm->isStar(c[i]) ){\r
+      riter.d_bounds[0][i] = c[i];\r
+      riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );\r
     }\r
   }\r
   //initialize\r
@@ -915,19 +921,23 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
   if (eq[0]==eq[1]){\r
     d.addEntry(fm, mkCond(cond), d_true);\r
   }else{\r
-    int j = getVariableId(f, eq[0]);\r
-    int k = getVariableId(f, eq[1]);\r
     TypeNode tn = eq[0].getType();\r
-    if( !fm->d_rep_set.hasType( tn ) ){\r
-      getSomeDomainElement( fm, tn );  //to verify the type is initialized\r
-    }\r
-    for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
-      Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );\r
-      cond[j+1] = r;\r
-      cond[k+1] = r;\r
-      d.addEntry( fm, mkCond(cond), d_true);\r
+    if( tn.isSort() ){\r
+      int j = getVariableId(f, eq[0]);\r
+      int k = getVariableId(f, eq[1]);\r
+      if( !fm->d_rep_set.hasType( tn ) ){\r
+        getSomeDomainElement( fm, tn );  //to verify the type is initialized\r
+      }\r
+      for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
+        Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );\r
+        cond[j+1] = r;\r
+        cond[k+1] = r;\r
+        d.addEntry( fm, mkCond(cond), d_true);\r
+      }\r
+      d.addEntry( fm, mkCondDefault(fm, f), d_false);\r
+    }else{\r
+      d.addEntry( fm, mkCondDefault(fm, f), Node::null());\r
     }\r
-    d.addEntry( fm, mkCondDefault(fm, f), d_false);\r
   }\r
 }\r
 \r
@@ -1058,14 +1068,22 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }\r
     }else{\r
       if( !v.isNull() ){\r
-        if (curr.d_child.find(v)!=curr.d_child.end()) {\r
-          Trace("fmc-uf-process") << "follow value..." << std::endl;\r
-          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
-        }\r
-        Node st = fm->getStarElement(v.getType());\r
-        if (curr.d_child.find(st)!=curr.d_child.end()) {\r
-          Trace("fmc-uf-process") << "follow star..." << std::endl;\r
-          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
+        if( options::fmfFmcInterval() && v.getType().isInteger() ){\r
+          for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
+            if( fm->isInRange( v, it->first ) ){\r
+              doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
+            }\r
+          }\r
+        }else{\r
+          if (curr.d_child.find(v)!=curr.d_child.end()) {\r
+            Trace("fmc-uf-process") << "follow value..." << std::endl;\r
+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
+          }\r
+          Node st = fm->getStarElement(v.getType());\r
+          if (curr.d_child.find(st)!=curr.d_child.end()) {\r
+            Trace("fmc-uf-process") << "follow star..." << std::endl;\r
+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
+          }\r
         }\r
       }\r
     }\r
@@ -1187,6 +1205,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
 }\r
 \r
 void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {\r
+  Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;\r
   //get function symbol for f\r
   cond.push_back(d_quant_cond[f]);\r
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
@@ -1277,7 +1296,7 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
 \r
 \r
 bool FullModelChecker::useSimpleModels() {\r
-  return options::fmfFullModelCheckSimple();\r
+  return options::fmfFmcSimple();\r
 }\r
 \r
 void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 2cb2198ef7c0d77d79c7c811a33a59e328838df7..8ebef640ccfacd828a092e9db96f9b1252fc2cde 100755 (executable)
--- 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 );\r
   ~FullModelChecker(){}\r
 \r
+  bool optBuildAtFullModel();\r
+\r
   int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }\r
 \r
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);\r

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index b1851cfa4771bf9b612353f545e7b6f740e5be19..073f7057bef9752b92a9dcd0a5f1b569e1ffea41 100644 (file)
--- 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 0d7c146bac93600dabd001b2772c5b1acce90286..b96c58767e37148b43fc5dda70b8dc90c96f5683 100644 (file)
--- 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 c0fe23b943a1dacc97e8e7b17201f8f789f5e13f..0678e230f339255ba564cee697a693fa4143680d 100644 (file)
--- 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 1e6f04162188daf4fc98e042decb0051149aedfc..d44f2e7702dd2db55916f7481816fb11ee5c479d 100644 (file)
--- 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