Minor fixes for bounded integers, rewrite engine.

3 files changed, 37 insertions, 13 deletions

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: