Add support for interval models in bounded integers MBQI (in progress).

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 37bf6436bf76ed46070dda9ccd78bb34e15ddd55..d893a9ff2de9cd56f4cb695796ee3cc26b4d8fa0 100755 (executable)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -135,7 +135,9 @@ bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
   return false;\r
 }\r
 \r
-void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {\r
+void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,\r
+                                      std::map< int, std::map< Node, Node > >& bound_lit_map,\r
+                                      std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {\r
   if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
     std::map< Node, Node > msum;\r
     if (QuantArith::getMonomialSumLit( lit, msum )){\r
@@ -176,7 +178,10 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
             if( !isBound( f, bv ) ){\r
               if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {\r
                 Trace("bound-int-debug") << "The bound is relevant." << std::endl;\r
-                d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
+                int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1;\r
+                d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
+                bound_lit_map[loru][bv] = lit;\r
+                bound_lit_pol_map[loru][bv] = pol;\r
               }\r
             }\r
           }\r
@@ -189,16 +194,18 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
   }\r
 }\r
 \r
-void BoundedIntegers::process( Node f, Node n, bool pol ){\r
+void BoundedIntegers::process( Node f, Node n, bool pol,\r
+                               std::map< int, std::map< Node, Node > >& bound_lit_map,\r
+                               std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){\r
   if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){\r
     for( unsigned i=0; i<n.getNumChildren(); i++) {\r
       bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;\r
-      process( f, n[i], newPol );\r
+      process( f, n[i], newPol, bound_lit_map, bound_lit_pol_map );\r
     }\r
   }else if( n.getKind()==NOT ){\r
-    process( f, n[0], !pol );\r
+    process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );\r
   }else {\r
-    processLiteral( f, n, pol );\r
+    processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );\r
   }\r
 }\r
 \r
@@ -232,10 +239,10 @@ void BoundedIntegers::registerQuantifier( Node f ) {
   if( hasIntType ){\r
     bool success;\r
     do{\r
-      //std::map< int, std::map< Node, Node > > bound_lit_map;\r
-      //std::map< int, std::map< Node, bool > > bound_lit_pol_map;\r
+      std::map< int, std::map< Node, Node > > bound_lit_map;\r
+      std::map< int, std::map< Node, bool > > bound_lit_pol_map;\r
       success = false;\r
-      process( f, f[1], true );\r
+      process( f, f[1], true, bound_lit_map, bound_lit_pol_map );\r
       for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){\r
         Node v = it->first;\r
         if( !isBound(f,v) ){\r
@@ -243,6 +250,14 @@ void BoundedIntegers::registerQuantifier( Node f ) {
             d_set[f].push_back(v);\r
             d_set_nums[f].push_back(numMap[v]);\r
             success = true;\r
+            //set Attributes on literals\r
+            for( unsigned b=0; b<2; b++ ){\r
+              Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );\r
+              Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );\r
+              BoundIntLitAttribute bila;\r
+              bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );\r
+            }\r
+            Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;\r
           }\r
         }\r
       }\r

diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index f40e2180ca2958196944c839b0e4b7557ce2fad9..96d2a3d204063d1035f70f144c6cbb933cb44cdb 100755 (executable)
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -45,8 +45,12 @@ private:
   std::map< Node, std::map< Node, Node > > d_range;\r
   std::map< Node, std::map< Node, Node > > d_nground_range;\r
   void hasFreeVar( Node f, Node n );\r
-  void process( Node f, Node n, bool pol );\r
-  void processLiteral( Node f, Node lit, bool pol );\r
+  void process( Node f, Node n, bool pol,\r
+                std::map< int, std::map< Node, Node > >& bound_lit_map,\r
+                std::map< int, std::map< Node, bool > >& bound_lit_pol_map );\r
+  void processLiteral( Node f, Node lit, bool pol,\r
+                       std::map< int, std::map< Node, Node > >& bound_lit_map,\r
+                       std::map< int, std::map< Node, bool > >& bound_lit_pol_map  );\r
   std::vector< Node > d_bound_quants;\r
 private:\r
   class RangeModel {\r

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index ad433edf5a23ddd6571ac062d9a84a948cb5df6c..60d62391bb21d9fc144f440d2feb4472b5b9d2e9 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -601,6 +601,14 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) {
   return d_type_star[tn];
 }
 
+Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
+  Node st = getStar(tn);
+  if( options::fmfFmcInterval() && tn.isInteger() ){
+    st = getInterval( st, st );
+  }
+  return st;
+}
+
 bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
   return n==getModelBasisTerm(n.getType());
 }
@@ -630,7 +638,14 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       Node cond = d_models[op]->d_cond[i];
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
-        if (!isStar(cond[j])){
+        if (isInterval(cond[j])){
+          if( !isStar(cond[j][0]) ){
+            children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
+          }
+          if( !isStar(cond[j][1]) ){
+            children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
+          }
+        }else if (!isStar(cond[j])){
           Node c = getUsedRepresentative( cond[j] );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index d79171f68d2501f942ad7e3327bbca63ace66f3f..14e9441b4a16878bd007f9a517b94aaa7a3031b9 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -149,6 +149,7 @@ public:
 
   bool isStar(Node n);
   Node getStar(TypeNode tn);
+  Node getStarElement(TypeNode tn);
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
   Node getSomeDomainElement(TypeNode tn);

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 7f30a045e7e0614f13d0578eda0d65aeae159d3c..ed5dea6796ba3d09c28f6a3987b9c560f494fffa 100755 (executable)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -59,22 +59,24 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;\r
       }\r
     }\r
-    //for star: check if all children are defined and have generalizations\r
-    if( options::fmfFmcCoverSimplify() && c[index]==st ){\r
-      //check if all children exist and are complete\r
-      int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
-      if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
-        bool complete = true;\r
-        for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
-          if( !m->isStar(it->first) ){\r
-            if( !it->second.hasGeneralization(m, c, index+1) ){\r
-              complete = false;\r
-              break;\r
+    if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){\r
+      //for star: check if all children are defined and have generalizations\r
+      if( options::fmfFmcCoverSimplify() && c[index]==st ){\r
+        //check if all children exist and are complete\r
+        int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
+        if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
+          bool complete = true;\r
+          for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+            if( !m->isStar(it->first) ){\r
+              if( !it->second.hasGeneralization(m, c, index+1) ){\r
+                complete = false;\r
+                break;\r
+              }\r
             }\r
           }\r
-        }\r
-        if( complete ){\r
-          return true;\r
+          if( complete ){\r
+            return true;\r
+          }\r
         }\r
       }\r
     }\r
@@ -88,15 +90,41 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     return d_data;\r
   }else{\r
     int minIndex = -1;\r
-    Node st = m->getStar(inst[index].getType());\r
-    if(d_child.find(st)!=d_child.end()) {\r
-      minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);\r
-    }\r
-    Node cc = inst[index];\r
-    if( cc!=st && d_child.find( cc )!=d_child.end() ){\r
-      int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);\r
-      if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
-        minIndex = gindex;\r
+    if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){\r
+      for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+        if( !m->isInterval( it->first ) ){\r
+          std::cout << "Not an interval during getGenIndex " << it->first << std::endl;\r
+          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
+          int gindex = it->second.getGeneralizationIndex(m, inst, index+1);\r
+          if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
+            minIndex = gindex;\r
+          }\r
+        }\r
+      }\r
+    }else{\r
+      Node st = m->getStar(inst[index].getType());\r
+      if(d_child.find(st)!=d_child.end()) {\r
+        minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);\r
+      }\r
+      Node cc = inst[index];\r
+      if( cc!=st && d_child.find( cc )!=d_child.end() ){\r
+        int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);\r
+        if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
+          minIndex = gindex;\r
+        }\r
       }\r
     }\r
     return minIndex;\r
@@ -143,39 +171,6 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & c
   }\r
 }\r
 \r
-\r
-bool EntryTrie::isCovered(FirstOrderModelFmc * m, Node c, int index) {\r
-  if (index==(int)c.getNumChildren()) {\r
-    return false;\r
-  }else{\r
-    TypeNode tn = c[index].getType();\r
-    Node st = m->getStar(tn);\r
-    if( c[index]==st ){\r
-      //check if all children exist and are complete\r
-      int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
-      if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
-        bool complete = true;\r
-        for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
-          if( !m->isStar(it->first) ){\r
-            if( !it->second.isComplete(m, c, index+1) ){\r
-              complete = false;\r
-              break;\r
-            }\r
-          }\r
-        }\r
-        if( complete ){\r
-          return true;\r
-        }\r
-      }\r
-    }\r
-    if( d_child.find(c[index])!=d_child.end() ){\r
-      return d_child[c[index]].isCovered(m, c, index+1);\r
-    }else{\r
-      return false;\r
-    }\r
-  }\r
-}\r
-\r
 void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {\r
   if (index==(int)c.getNumChildren()) {\r
     if( d_data!=-1 ){\r
@@ -209,12 +204,6 @@ bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
   if (d_et.hasGeneralization(m, c)) {\r
     return false;\r
   }\r
-  //if( options::fmfFmcCoverSimplify() ){\r
-  //  if( d_et.isCovered(m, c, 0) ){\r
-  //    Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;\r
-  //    return false;\r
-  //  }\r
-  //}\r
   int newIndex = (int)d_cond.size();\r
   if (!d_has_simplified) {\r
     std::vector<int> compat;\r
@@ -247,6 +236,7 @@ Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
   if (gindex!=-1) {\r
     return d_value[gindex];\r
   }else{\r
+    Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;\r
     return Node::null();\r
   }\r
 }\r
@@ -280,7 +270,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
     bool last_all_stars = true;\r
     Node cc = d_cond[d_cond.size()-1];\r
     for( unsigned i=0; i<cc.getNumChildren(); i++ ){\r
-      if( !m->isStar(cc[i]) ){\r
+      if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){\r
         last_all_stars = false;\r
         break;\r
       }\r
@@ -475,10 +465,12 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         for( unsigned i=0; i<c.getNumChildren(); i++) {\r
           Node ri = fm->getUsedRepresentative( c[i]);\r
           children.push_back(ri);\r
-          if (fm->isModelBasisTerm(ri)) {\r
-            ri = fm->getStar( ri.getType() );\r
-          }else{\r
-            hasNonStar = true;\r
+          if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){\r
+            if (fm->isModelBasisTerm(ri) ) {\r
+              ri = fm->getStar( ri.getType() );\r
+            }else{\r
+              hasNonStar = true;\r
+            }\r
           }\r
           entry_children.push_back(ri);\r
         }\r
@@ -510,8 +502,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       for (int i=0; i<(int)indices.size(); i++) {\r
         fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);\r
       }\r
-      fm->d_models[op]->debugPrint("fmc-model", op, this);\r
-      Trace("fmc-model") << std::endl;\r
+\r
 \r
       if( options::fmfFmcInterval() ){\r
         Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;\r
@@ -523,21 +514,45 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         }\r
         std::map< int, std::map< int, Node > > changed_vals;\r
         makeIntervalModel( fm, op, indices, 0, changed_vals );\r
-        for( std::map< int, std::map< int, Node > >::iterator it = changed_vals.begin(); it != changed_vals.end(); ++it ){\r
-          Trace("fmc-interval-model") << "Entry #" << it->first << " changed : ";\r
-          for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
-            Trace("fmc-interval-model") << it2->first << " -> " << it2->second << ", ";\r
+\r
+        std::vector< Node > conds;\r
+        std::vector< Node > values;\r
+        for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){\r
+          if( changed_vals.find(i)==changed_vals.end() ){\r
+            conds.push_back( fm->d_models[op]->d_cond[i] );\r
+          }else{\r
+            std::vector< Node > children;\r
+            children.push_back( op );\r
+            for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){\r
+              if( changed_vals[i].find(j)==changed_vals[i].end() ){\r
+                children.push_back( fm->d_models[op]->d_cond[i][j] );\r
+              }else{\r
+                children.push_back( changed_vals[i][j] );\r
+              }\r
+            }\r
+            Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+            conds.push_back( nc );\r
+            Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";\r
+            debugPrintCond("fmc-interval-model", nc, true );\r
+            Trace("fmc-interval-model") << std::endl;\r
           }\r
-          Trace("fmc-interval-model") << std::endl;\r
+          values.push_back( fm->d_models[op]->d_value[i] );\r
+        }\r
+        fm->d_models[op]->reset();\r
+        for( unsigned i=0; i<conds.size(); i++ ){\r
+          fm->d_models[op]->addEntry(fm, conds[i], values[i] );\r
         }\r
       }\r
 \r
+      Trace("fmc-model-simplify") << "Before simplification : " << std::endl;\r
+      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
+      Trace("fmc-model-simplify") << std::endl;\r
 \r
       Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;\r
       fm->d_models[op]->simplify( this, fm );\r
-      Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
-      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
-      Trace("fmc-model-simplify") << std::endl;\r
+\r
+      fm->d_models[op]->debugPrint("fmc-model", op, this);\r
+      Trace("fmc-model") << std::endl;\r
     }\r
   }\r
 }\r
@@ -600,7 +615,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
       Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
       d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
       Trace("fmc") << std::endl;\r
-      //consider all entries going to false\r
+\r
+      //consider all entries going to non-true\r
       for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {\r
         if( d_quant_models[f].d_value[i]!=d_true) {\r
           Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;\r
@@ -610,6 +626,21 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {\r
               hasStar = true;\r
               inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
+            }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){\r
+              hasStar = true;\r
+              //if interval, find a sample point\r
+              if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){\r
+                if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){\r
+                  inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));\r
+                }else{\r
+                  Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],\r
+                                                              NodeManager::currentNM()->mkConst( Rational(1) ) );\r
+                  nn = Rewriter::rewrite( nn );\r
+                  inst.push_back( nn );\r
+                }\r
+              }else{\r
+                inst.push_back(d_quant_models[f].d_cond[i][j][0]);\r
+              }\r
             }else{\r
               inst.push_back(d_quant_models[f].d_cond[i][j]);\r
             }\r
@@ -683,13 +714,24 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
   debugPrintCond("fmc-exh", c, true);\r
   Trace("fmc-exh")<< std::endl;\r
+  //set the bounds on the iterator based on intervals\r
+  for( unsigned i=0; i<c.getNumChildren(); i++ ){\r
+    if( fm->isInterval(c[i]) ){\r
+      for( unsigned b=0; b<2; b++ ){\r
+        if( !fm->isStar(c[i][b]) ){\r
+          riter.d_bounds[b][i] = c[i][b];\r
+        }\r
+      }\r
+    }\r
+  }\r
+  //initialize\r
   if( riter.setQuantifier( f ) ){\r
     //set the domains based on the entry\r
     for (unsigned i=0; i<c.getNumChildren(); i++) {\r
       if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {\r
         TypeNode tn = c[i].getType();\r
         if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
-          if( fm->isStar(c[i]) ){\r
+          if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){\r
             //add the full range\r
           }else{\r
             if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
@@ -704,8 +746,10 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         }\r
       }\r
     }\r
+    int addedLemmas = 0;\r
     //now do full iteration\r
     while( !riter.isFinished() ){\r
+      d_triedLemmas++;\r
       Trace("fmc-exh-debug") << "Inst : ";\r
       std::vector< Node > inst;\r
       for( int i=0; i<riter.getNumTerms(); i++ ){\r
@@ -719,29 +763,27 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);\r
       Trace("fmc-exh-debug") << ", index = " << ev_index;\r
       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
-      bool successAdd = false;\r
       if (ev!=d_true) {\r
         InstMatch m;\r
         for( int i=0; i<riter.getNumTerms(); i++ ){\r
           m.set( d_qe, f, i, riter.getTerm( i ) );\r
         }\r
         Trace("fmc-exh-debug") << ", add!";\r
-        d_triedLemmas++;\r
         //add as instantiation\r
         if( d_qe->addInstantiation( f, m ) ){\r
           Trace("fmc-exh-debug")  << " ...success.";\r
-          d_addedLemmas++;\r
-          successAdd = true;\r
+          addedLemmas++;\r
         }\r
       }\r
       Trace("fmc-exh-debug") << std::endl;\r
       int index = riter.increment();\r
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;\r
-      if (index>=0 && successAdd && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {\r
+      if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {\r
         Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;\r
         riter.increment2( index-1 );\r
       }\r
     }\r
+    d_addedLemmas += addedLemmas;\r
     return true;\r
   }else{\r
     return false;\r
@@ -750,9 +792,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
 \r
 void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {\r
   Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;\r
-  if( n.getKind() == kind::BOUND_VARIABLE ){\r
+  //first check if it is a bounding literal\r
+  if( n.hasAttribute(BoundIntLitAttribute()) ){\r
+    Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;\r
+    d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );\r
+  }else if( n.getKind() == kind::BOUND_VARIABLE ){\r
     d.addEntry(fm, mkCondDefault(fm, f), n);\r
-    Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;\r
   }\r
   else if( n.getKind() == kind::NOT ){\r
     //just do directly\r
@@ -792,10 +837,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   }\r
   else if( n.getNumChildren()==0 ){\r
     Node r = n;\r
-    if( !fm->hasTerm(n) ){\r
-      r = getSomeDomainElement(fm, n.getType() );\r
+    if( !n.isConst() ){\r
+      if( !fm->hasTerm(n) ){\r
+        r = getSomeDomainElement(fm, n.getType() );\r
+      }\r
+      r = fm->getUsedRepresentative( r );\r
     }\r
-    r = fm->getUsedRepresentative( r);\r
     d.addEntry(fm, mkCondDefault(fm, f), r);\r
   }\r
   else{\r
@@ -983,7 +1030,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){\r
       int j = getVariableId(f, v);\r
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;\r
-      if (!fm->isStar(cond[j+1])) {\r
+      if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {\r
         v = cond[j+1];\r
       }else{\r
         bind_var = true;\r
@@ -992,18 +1039,30 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
     if (bind_var) {\r
       Trace("fmc-uf-process") << "bind variable..." << std::endl;\r
       int j = getVariableId(f, v);\r
-      for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
-        cond[j+1] = it->first;\r
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
+      if( fm->isStar(cond[j+1]) ){\r
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
+          cond[j+1] = it->first;\r
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
+        }\r
+        cond[j+1] = fm->getStar(v.getType());\r
+      }else{\r
+        Node orig = cond[j+1];\r
+        for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
+          Node nw = doIntervalMeet( fm, it->first, orig );\r
+          if( !nw.isNull() ){\r
+            cond[j+1] = nw;\r
+            doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
+          }\r
+        }\r
+        cond[j+1] = orig;\r
       }\r
-      cond[j+1] = fm->getStar(v.getType());\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->getStar(v.getType());\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
@@ -1050,29 +1109,73 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 }\r
 \r
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
+  Trace("fmc-debug2") << "isCompat " << c << std::endl;\r
   Assert(cond.size()==c.getNumChildren()+1);\r
   for (unsigned i=1; i<cond.size(); i++) {\r
-    if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {\r
-      return 0;\r
+    if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){\r
+      Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );\r
+      if( iv.isNull() ){\r
+        return 0;\r
+      }\r
+    }else{\r
+      if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {\r
+        return 0;\r
+      }\r
     }\r
   }\r
   return 1;\r
 }\r
 \r
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {\r
+  Trace("fmc-debug2") << "doMeet " << c << std::endl;\r
   Assert(cond.size()==c.getNumChildren()+1);\r
   for (unsigned i=1; i<cond.size(); i++) {\r
     if( cond[i]!=c[i-1] ) {\r
-      if( fm->isStar(cond[i]) ){\r
-        cond[i] = c[i-1];\r
-      }else if( !fm->isStar(c[i-1]) ){\r
-        return false;\r
+      if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){\r
+        Node iv = doIntervalMeet( fm, cond[i], c[i-1] );\r
+        if( !iv.isNull() ){\r
+          cond[i] = iv;\r
+        }else{\r
+          return false;\r
+        }\r
+      }else{\r
+        if( fm->isStar(cond[i]) ){\r
+          cond[i] = c[i-1];\r
+        }else if( !fm->isStar(c[i-1]) ){\r
+          return false;\r
+        }\r
       }\r
     }\r
   }\r
   return true;\r
 }\r
 \r
+Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {\r
+  if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){\r
+    std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;\r
+    exit( 0 );\r
+  }\r
+  Node b[2];\r
+  for( unsigned j=0; j<2; j++ ){\r
+    Node b1 = i1[j];\r
+    Node b2 = i2[j];\r
+    if( fm->isStar( b1 ) ){\r
+      b[j] = b2;\r
+    }else if( fm->isStar( b2 ) ){\r
+      b[j] = b1;\r
+    }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){\r
+      b[j] = j==0 ? b2 : b1;\r
+    }else{\r
+      b[j] = j==0 ? b1 : b2;\r
+    }\r
+  }\r
+  if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){\r
+    return mk ? fm->getInterval( b[0], b[1] ) : i1;\r
+  }else{\r
+    return Node::null();\r
+  }\r
+}\r
+\r
 Node FullModelChecker::mkCond( std::vector< Node > & cond ) {\r
   return NodeManager::currentNM()->mkNode(APPLY_UF, cond);\r
 }\r
@@ -1087,7 +1190,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v
   //get function symbol for f\r
   cond.push_back(d_quant_cond[f]);\r
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
-    Node ts = fm->getStar( f[0][i].getType() );\r
+    Node ts = fm->getStarElement( f[0][i].getType() );\r
     cond.push_back(ts);\r
   }\r
 }\r
@@ -1189,7 +1292,7 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std:
       std::map< Node, std::vector< int > > new_indices;\r
       for( unsigned i=0; i<indices.size(); i++ ){\r
         Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
-        new_indices[v].push_back( i );\r
+        new_indices[v].push_back( indices[i] );\r
       }\r
 \r
       for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
@@ -1201,21 +1304,29 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std:
 \r
 void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
                                           std::map< int, std::map< int, Node > >& changed_vals ) {\r
+  Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";\r
+  for( unsigned i=0; i<indices.size(); i++ ){\r
+    Debug("fmc-interval-model-debug") << indices[i] << " ";\r
+  }\r
+  Debug("fmc-interval-model-debug") << std::endl;\r
+\r
   if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){\r
     TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();\r
     if( tn.isInteger() ){\r
       std::map< Node, std::vector< int > > new_indices;\r
       for( unsigned i=0; i<indices.size(); i++ ){\r
         Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
-        new_indices[v].push_back( i );\r
+        new_indices[v].push_back( indices[i] );\r
+        if( !v.isConst() ){\r
+          Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;\r
+          Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;\r
+        }\r
       }\r
 \r
       std::vector< Node > values;\r
       for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
         makeIntervalModel2( fm, op, it->second, index+1, changed_vals );\r
-        if( !fm->isStar(it->first) ){\r
-          values.push_back( it->first );\r
-        }\r
+        values.push_back( it->first );\r
       }\r
 \r
       if( tn.isInteger() ){\r
@@ -1236,6 +1347,7 @@ void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std
           }\r
           Node interval = fm->getInterval( lb, ub );\r
           for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){\r
+            Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;\r
             changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;\r
           }\r
           ub = lb;\r

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 45110b2b709050d405c225469459139438ba4d4c..2cb2198ef7c0d77d79c7c811a33a59e328838df7 100755 (executable)
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -39,7 +39,6 @@ public:
   int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );\r
   void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
 \r
-  bool isCovered(FirstOrderModelFmc * m, Node c, int index);\r
   void collectIndices(Node c, int index, std::vector< int >& indices );\r
   bool isComplete(FirstOrderModelFmc * m, Node c, int index);\r
 };\r
@@ -118,6 +117,7 @@ private:
                              std::vector< Def > & dc, int index,\r
                              std::vector< Node > & cond, std::vector<Node> & val );\r
   int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );\r
+  Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true );\r
   bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );\r
   Node mkCond( std::vector< Node > & cond );\r
   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );\r

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index dc00b5f95a8ff7256c61616eee1203ea05183d83..e1a953e1b35665be2fd481d14ed3a30310c7027e 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -195,11 +195,15 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
     if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
-      std::stringstream ss;
-      ss << Expr::setlanguage(options::outputLanguage());
-      ss << "e_" << tn;
-      mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
-      Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+      if( tn.isInteger() || tn.isReal() ){
+        mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+      }else{
+        std::stringstream ss;
+        ss << Expr::setlanguage(options::outputLanguage());
+        ss << "e_" << tn;
+        mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
+        Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+      }
     }else{
       mbt = d_type_map[ tn ][ 0 ];
     }

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 180c4bbcf75660a05ef433c486392289549f2f4f..b44cc6779752d4888bcde19d7e228e44ef758ee8 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -139,7 +139,6 @@ bool RepSetIterator::initialize(){
     //store default domain
     d_domain.push_back( RepDomain() );
     TypeNode tn = d_types[i];
-    bool isSet = false;
     if( tn.isSort() ){
       if( !d_rep_set->hasType( tn ) ){
         Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
@@ -147,31 +146,36 @@ bool RepSetIterator::initialize(){
         d_rep_set->add( var );
       }
     }else if( tn.isInteger() ){
+      bool inc = false;
       //check if it is bound
       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
           Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
           d_enum_type.push_back( ENUM_RANGE );
-          isSet = true;
         }else{
-          Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
-          d_incomplete = true;
+          inc = true;
         }
       }else{
-        Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
-        d_incomplete = true;
+        inc = true;
       }
-    }else if( tn.isReal() ){
-      Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
-      d_incomplete = true;
-    //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
-    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+      if( inc ){
+        //check if it is otherwise bound
+        if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
+          Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl;
+          d_enum_type.push_back( ENUM_RANGE );
+        }else{
+          Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
+          d_incomplete = true;
+        }
+      }
+    //enumerate if the sort is reasonably small, the upper bound of 1000 is chosen arbitrarily for now
+    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
       d_rep_set->complete( tn );
     }else{
-      Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
+      Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
-    if( !isSet ){
+    if( d_enum_type.size()<=i ){
       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
       if( d_rep_set->hasType( tn ) ){
         for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
@@ -182,7 +186,7 @@ bool RepSetIterator::initialize(){
       }
     }
   }
-  //must set a variable index order
+  //must set a variable index order based on bounded integers
   if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
     std::vector< int > varOrder;
@@ -211,6 +215,7 @@ bool RepSetIterator::initialize(){
     Trace("bound-int-rsi") << std::endl;
     setIndexOrder(indexOrder);
   }
+  //now reset the indices
   for (unsigned i=0; i<d_index.size(); i++) {
     if (!resetIndex(i, true)){
       break;
@@ -255,6 +260,19 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
         return false;
       }else{
         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
+        for( unsigned b=0; b<2; b++ ){
+          if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
+            Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
+            if( b==0 && d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>() ){
+              l = d_bounds[b][ii];
+            }else if( b==1 && d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>() ){
+              u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
+                                                    NodeManager::currentNM()->mkConst( Rational(1) ) );
+              u = Rewriter::rewrite( u );
+            }
+          }
+        }
+
         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
         d_domain[ii].clear();

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 672f33b5406a00938aef50c156820613e3870df7..a619915ee8e0e41af7920a584d6d3c479909480f 100644 (file)
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -71,6 +71,8 @@ private:
   Node d_owner;
   //reset index
   bool resetIndex( int i, bool initial = false );
+  /** set index order */
+  void setIndexOrder( std::vector< int >& indexOrder );
 public:
   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
@@ -104,9 +106,9 @@ public:
   //  for example, if d_index_order = { 2, 0, 1 }
   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
   std::map< int, int > d_var_order;
+  //intervals
+  std::map< int, Node > d_bounds[2];
 public:
-  /** set index order */
-  void setIndexOrder( std::vector< int >& indexOrder );
   /** increment the iterator at index=counter */
   int increment2( int counter );
   /** increment the iterator */