Minor fixes for bounded integers, rewrite engine.

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 2be9de91c52d259f08395ee7678e59255a1c279a..42d5bbd3a5a5a67a442fecda366e684563263d6f 100755 (executable)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -86,6 +86,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
 }\r
 \r
 int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {\r
+  Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;\r
   if (index==(int)inst.size()) {\r
     return d_data;\r
   }else{\r
@@ -717,21 +718,26 @@ 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
+  Trace("fmc-exh-debug") << "Set interval domains..." << 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
+    if( c[i].getType().isInteger() ){\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
+      }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
-    }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
+  Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;\r
   //initialize\r
   if( riter.setQuantifier( f ) ){\r
+    Trace("fmc-exh-debug") << "Set element domains..." << std::endl;\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
@@ -765,9 +771,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         Trace("fmc-exh-debug") << " ";\r
         inst.push_back(r);\r
       }\r
-\r
       int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);\r
-      Trace("fmc-exh-debug") << ", index = " << ev_index;\r
+      Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();\r
       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
       if (ev!=d_true) {\r
         InstMatch m;\r
@@ -780,6 +785,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
           Trace("fmc-exh-debug")  << " ...success.";\r
           addedLemmas++;\r
         }\r
+      }else{\r
+        Trace("fmc-exh-debug") << ", already true";\r
       }\r
       Trace("fmc-exh-debug") << std::endl;\r
       int index = riter.increment();\r

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 84d4655796046318447e408611e628cabf614326..aa0569ef43c483d0070f12557d8568c1ce5b966d 100755 (executable)
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -30,7 +30,10 @@ RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : Qua
 }\r
 \r
 void RewriteEngine::check( Theory::Effort e ) {\r
-  if( e==Theory::EFFORT_FULL ){\r
+  if( e==Theory::EFFORT_LAST_CALL ){\r
+    if( d_true.isNull() ){\r
+      d_true = NodeManager::currentNM()->mkConst( true );\r
+    }\r
     //apply rewrite rules\r
     int addedLemmas = 0;\r
     for( unsigned i=0; i<d_rr_quant.size(); i++ ) {\r
@@ -82,9 +85,19 @@ int RewriteEngine::checkRewriteRule( Node f ) {
       success = d_rr_triggers[f][i]->getNextMatch( f, m );\r
       if( success ){\r
         //see if instantiation is true in the model\r
-        bool trueInModel = false;\r
-\r
-        if( !trueInModel ){\r
+        Node rr = f.getAttribute(QRewriteRuleAttribute());\r
+        Node rrg = rr[1];\r
+        std::vector< Node > vars;\r
+        std::vector< Node > terms;\r
+        d_quantEngine->computeTermVector( f, m, vars, terms );\r
+        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;\r
+        Node inst = d_rr_guard[f];\r
+        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );\r
+        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;\r
+        FirstOrderModel * fm = d_quantEngine->getModel();\r
+        Node v = fm->getValue( inst );\r
+        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;\r
+        if( v==d_true ){\r
           Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;\r
           if( d_quantEngine->addInstantiation( f, m ) ){\r
             addedLemmas++;\r
@@ -106,6 +119,8 @@ void RewriteEngine::registerQuantifier( Node f ) {
     Node rr = f.getAttribute(QRewriteRuleAttribute());\r
     Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;\r
     d_rr_quant.push_back( f );\r
+    d_rr_guard[f] = rr[1];\r
+    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;\r
   }\r
 }\r
 \r

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 5160af602bfd8bf3d3de0b27118d9eb2a5da4e09..fe8daca5fa23786f26c48c6328940673d13d19b5 100755 (executable)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -32,6 +32,8 @@ class RewriteEngine : public QuantifiersModule
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;\r
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;\r
   std::vector< Node > d_rr_quant;\r
+  std::map< Node, Node > d_rr_guard;\r
+  Node d_true;\r
   /** explicitly provided patterns */\r
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;\r
 private:\r

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 40b043752a9c07baae5916815f5a4e46aa5fea8b..b075f7be86093af766cb6e9517493ffdb64eff19 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -83,6 +83,7 @@ class EqualityQueryQuantifiersEngine;
 class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
   friend class quantifiers::ModelEngine;
+  friend class quantifiers::RewriteEngine;
   friend class inst::InstMatch;
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index b44cc6779752d4888bcde19d7e228e44ef758ee8..647ef965ae18a97c23a9de14e7d2771870746257 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -250,29 +250,31 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
   Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
   //determine the current range
   if( d_enum_type[ii]==ENUM_RANGE ){
-    if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){
+    if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){
       Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
       Node l, u;
-      d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
+      if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){
+        d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
+      }
+      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 && (l.isNull() || d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>()) ){
+            l = d_bounds[b][ii];
+          }else if( b==1 && (u.isNull() || 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 );
+          }
+        }
+      }
+
       if( l.isNull() || u.isNull() ){
         //failed, abort the iterator
         d_index.clear();
         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();