From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Jul 2013 18:40:26 +0000 (-0500)
Subject: Minor fixes for bounded integers, rewrite engine.
X-Git-Tag: cvc5-1.0.0~7287^2~75
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4d9d607c3a63a1b3842e291f06a621f71b0e966;p=cvc5.git

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 2be9de91c..42d5bbd3a 100755
--- 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 ) {
 }
 
 int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
+  Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;
   if (index==(int)inst.size()) {
     return d_data;
   }else{
@@ -717,21 +718,26 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
+  Trace("fmc-exh-debug") << "Set interval domains..." << std::endl;
   //set the bounds on the iterator based on intervals
   for( unsigned i=0; i<c.getNumChildren(); i++ ){
-    if( fm->isInterval(c[i]) ){
-      for( unsigned b=0; b<2; b++ ){
-        if( !fm->isStar(c[i][b]) ){
-          riter.d_bounds[b][i] = c[i][b];
+    if( c[i].getType().isInteger() ){
+      if( fm->isInterval(c[i]) ){
+        for( unsigned b=0; b<2; b++ ){
+          if( !fm->isStar(c[i][b]) ){
+            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 );
       }
-    }else if( !fm->isStar(c[i]) ){
-      riter.d_bounds[0][i] = c[i];
-      riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );
     }
   }
+  Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
   //initialize
   if( riter.setQuantifier( f ) ){
+    Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
     //set the domains based on the entry
     for (unsigned i=0; i<c.getNumChildren(); i++) {
       if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
@@ -765,9 +771,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         Trace("fmc-exh-debug") << " ";
         inst.push_back(r);
       }
-
       int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
-      Trace("fmc-exh-debug") << ", index = " << ev_index;
+      Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
       Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
       if (ev!=d_true) {
         InstMatch m;
@@ -780,6 +785,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
         }
+      }else{
+        Trace("fmc-exh-debug") << ", already true";
       }
       Trace("fmc-exh-debug") << std::endl;
       int index = riter.increment();
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 84d465579..aa0569ef4 100755
--- 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
 }
 
 void RewriteEngine::check( Theory::Effort e ) {
-  if( e==Theory::EFFORT_FULL ){
+  if( e==Theory::EFFORT_LAST_CALL ){
+    if( d_true.isNull() ){
+      d_true = NodeManager::currentNM()->mkConst( true );
+    }
     //apply rewrite rules
     int addedLemmas = 0;
     for( unsigned i=0; i<d_rr_quant.size(); i++ ) {
@@ -82,9 +85,19 @@ int RewriteEngine::checkRewriteRule( Node f ) {
       success = d_rr_triggers[f][i]->getNextMatch( f, m );
       if( success ){
         //see if instantiation is true in the model
-        bool trueInModel = false;
-
-        if( !trueInModel ){
+        Node rr = f.getAttribute(QRewriteRuleAttribute());
+        Node rrg = rr[1];
+        std::vector< Node > vars;
+        std::vector< Node > terms;
+        d_quantEngine->computeTermVector( f, m, vars, terms );
+        Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl;
+        Node inst = d_rr_guard[f];
+        inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+        Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl;
+        FirstOrderModel * fm = d_quantEngine->getModel();
+        Node v = fm->getValue( inst );
+        Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl;
+        if( v==d_true ){
           Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
           if( d_quantEngine->addInstantiation( f, m ) ){
             addedLemmas++;
@@ -106,6 +119,8 @@ void RewriteEngine::registerQuantifier( Node f ) {
     Node rr = f.getAttribute(QRewriteRuleAttribute());
     Trace("rewrite-engine") << "  rewrite rule is : " << rr << std::endl;
     d_rr_quant.push_back( f );
+    d_rr_guard[f] = rr[1];
+    Trace("rewrite-engine") << "  guard is : " << d_rr_guard[f] << std::endl;
   }
 }
 
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 5160af602..fe8daca5f 100755
--- 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;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   std::vector< Node > d_rr_quant;
+  std::map< Node, Node > d_rr_guard;
+  Node d_true;
   /** explicitly provided patterns */
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
 private:
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 40b043752..b075f7be8 100644
--- 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 b44cc6779..647ef965a 100644
--- 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();