Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 38ee4a57f2c3dde424500f6b90c0d49adde12011..3e0f13e4b10870b212f106c98fedbe84cda3bc5d 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -198,7 +198,9 @@ void InstantiationEngine::check( Theory::Effort e ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if we have found the skolemized negation is unsat
-      if( options::cbqi() && hasAddedCbqiLemma( n ) ){
+      if( n.hasAttribute(QRewriteRuleAttribute()) ){
+        d_quant_active[n] = false;
+      }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
         bool active, value;
         bool ceValue = false;
@@ -228,8 +230,6 @@ void InstantiationEngine::check( Theory::Effort e ){
         }
         Debug("quantifiers") << std::endl;
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
-      }else if( n.hasAttribute(QRewriteRuleAttribute()) ){
-        d_quant_active[n] = false;
       }else{
         d_quant_active[n] = true;
         quantActive = true;
@@ -238,6 +238,7 @@ void InstantiationEngine::check( Theory::Effort e ){
       Debug("quantifiers-relevance")  << "Quantifier : " << n << std::endl;
       Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
       Debug("quantifiers") << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+      Trace("inst-engine-debug") << "Process : " << n << " " << d_quant_active[n] << std::endl;
     }
     if( quantActive ){
       bool addedLemmas = doInstantiationRound( e );

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 5bdce5face63041a61e491b9cdc3bee5cbfc9c81..909c9c3888598876afa36a24421003379360c379 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -32,6 +32,10 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
       Trace("quant-attr") << "Set conjecture " << n << std::endl;
       ConjectureAttribute ca;
       n.setAttribute( ca, true );
+    }else if( attr=="rr_priority" ){
+      //Trace("quant-attr") << "Set rr priority " << n << std::endl;
+      //RrPriorityAttribute rra;
+
     }
   }else{
     for( size_t i=0; i<n.getNumChildren(); i++ ){

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 878d3ac504a0e1f68a2fa8c8613353e4fa981a83..1aebbfcc5b3e0e920f7273568c2f2e6bd265f72a 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -34,6 +34,10 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
 struct ConjectureAttributeId {};
 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
 
+/** Attribute priority for rewrite rules */
+//struct RrPriorityAttributeId {};
+//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
+
 struct QuantifiersAttributes
 {
   /** set user attribute

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index aa0569ef43c483d0070f12557d8568c1ce5b966d..e278de9e15405c79f55178ca4ca5b4a08579b1ad 100755 (executable)
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/model_engine.h"\r
 #include "theory/quantifiers/options.h"\r
 #include "theory/quantifiers/inst_match_generator.h"\r
+#include "theory/theory_engine.h"\r
 \r
 using namespace CVC4;\r
 using namespace std;\r
@@ -25,20 +26,67 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;\r
 using namespace CVC4::kind;\r
 \r
+struct PrioritySort {\r
+  std::vector< double > d_priority;\r
+  bool operator() (int i,int j) {\r
+    return d_priority[i] < d_priority[j];\r
+  }\r
+};\r
+\r
+\r
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {\r
 \r
 }\r
 \r
+double RewriteEngine::getPriority( Node f ) {\r
+  Node rr = f.getAttribute(QRewriteRuleAttribute());\r
+  Node rrr = rr[2];\r
+  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;\r
+  bool deterministic = rrr[1].getKind()!=OR;\r
+  if( rrr.getKind()==RR_REWRITE ){\r
+    return deterministic ? 0.0 : 3.0;\r
+  }else if( rrr.getKind()==RR_DEDUCTION ){\r
+    return deterministic ? 1.0 : 4.0;\r
+  }else if( rrr.getKind()==RR_REDUCTION ){\r
+    return deterministic ? 2.0 : 5.0;\r
+  }else{\r
+    return 6.0;\r
+  }\r
+}\r
+\r
 void RewriteEngine::check( Theory::Effort e ) {\r
   if( e==Theory::EFFORT_LAST_CALL ){\r
+    if( !d_quantEngine->getModel()->isModelSet() ){\r
+      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );\r
+    }\r
     if( d_true.isNull() ){\r
       d_true = NodeManager::currentNM()->mkConst( true );\r
     }\r
+    std::vector< Node > priority_order;\r
+    PrioritySort ps;\r
+    std::vector< int > indicies;\r
+    for( int i=0; i<(int)d_rr_quant.size(); i++ ){\r
+      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );\r
+      indicies.push_back( i );\r
+    }\r
+    std::sort( indicies.begin(), indicies.end(), ps );\r
+    for( unsigned i=0; i<indicies.size(); i++ ){\r
+      priority_order.push_back( d_rr_quant[indicies[i]] );\r
+    }\r
+\r
     //apply rewrite rules\r
     int addedLemmas = 0;\r
-    for( unsigned i=0; i<d_rr_quant.size(); i++ ) {\r
-      addedLemmas += checkRewriteRule( d_rr_quant[i] );\r
+    //per priority level\r
+    int index = 0;\r
+    bool success = true;\r
+    while( success && index<(int)priority_order.size() ) {\r
+      addedLemmas += checkRewriteRule( priority_order[index] );\r
+      index++;\r
+      if( index<(int)priority_order.size() ){\r
+        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );\r
+      }\r
     }\r
+\r
     Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;\r
     if (addedLemmas==0) {\r
     }else{\r
@@ -49,7 +97,7 @@ void RewriteEngine::check( Theory::Effort e ) {
 }\r
 \r
 int RewriteEngine::checkRewriteRule( Node f ) {\r
-  Trace("rewrite-engine-inst") << "Check " << f << "..." << std::endl;\r
+  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;\r
   int addedLemmas = 0;\r
   //reset triggers\r
   Node rr = f.getAttribute(QRewriteRuleAttribute());\r
@@ -102,6 +150,12 @@ int RewriteEngine::checkRewriteRule( Node f ) {
           if( d_quantEngine->addInstantiation( f, m ) ){\r
             addedLemmas++;\r
             Trace("rewrite-engine-inst-debug") << "success" << std::endl;\r
+            //set the no-match attribute (the term is rewritten and can be ignored)\r
+            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;\r
+            //if( !m.d_matched.isNull() ){\r
+            //  NoMatchAttribute nma;\r
+            //  m.d_matched.setAttribute(nma,true);\r
+            //}\r
           }else{\r
             Trace("rewrite-engine-inst-debug") << "failure." << std::endl;\r
           }\r

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index fe8daca5fa23786f26c48c6328940673d13d19b5..6783b20d019c9a15c383b3bd5310520519025602 100755 (executable)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -36,6 +36,7 @@ class RewriteEngine : public QuantifiersModule
   Node d_true;\r
   /** explicitly provided patterns */\r
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;\r
+  double getPriority( Node f );\r
 private:\r
   int checkRewriteRule( Node f );\r
 public:\r

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e1a953e1b35665be2fd481d14ed3a30310c7027e..5569f684346b915f942f01786e70291e856e734f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -433,16 +433,19 @@ Node TermDb::getSkolemizedBody( Node f ){
 Node TermDb::getFreeVariableForInstConstant( Node n ){
   TypeNode tn = n.getType();
   if( d_free_vars.find( tn )==d_free_vars.end() ){
-    //if integer or real, make zero
-    if( tn.isInteger() || tn.isReal() ){
-      Rational z(0);
-      d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
-    }else{
-      if( d_type_map[ tn ].empty() ){
-        d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" );
-        Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
+       for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
+         if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
+           d_free_vars[tn] = d_type_map[ tn ][ i ];
+         }
+       }
+       if( d_free_vars.find( tn )==d_free_vars.end() ){
+      //if integer or real, make zero
+      if( tn.isInteger() || tn.isReal() ){
+        Rational z(0);
+        d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
       }else{
-        d_free_vars[tn] = d_type_map[ tn ][ 0 ];
+           d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" );
+           Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl;
       }
     }
   }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bc1a6929d2bbb158671a6e70a093a5890aeae5ac..f94a8774821ea9410e5130caacac7530f6e78038 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -63,15 +63,9 @@ d_lemmas_produced_c(u){
   }else{
     d_inst_engine = NULL;
   }
-  bool reqModel = options::finiteModelFind() || options::rewriteRulesAsAxioms();
-  if( reqModel ){
+  if( options::finiteModelFind()  ){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
-  }else{
-    d_model_engine = NULL;
-  }
-
-  if( options::finiteModelFind() ){
     if( options::fmfBoundInt() ){
       d_bint = new quantifiers::BoundedIntegers( c, this );
       d_modules.push_back( d_bint );
@@ -79,6 +73,7 @@ d_lemmas_produced_c(u){
       d_bint = NULL;
     }
   }else{
+    d_model_engine = NULL;
     d_bint = NULL;
   }
   if( options::rewriteRulesAsAxioms() ){
@@ -652,18 +647,24 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         int r_best_score = -1;
         for( size_t i=0; i<eqc.size(); i++ ){
           int score = getRepScore( eqc[i], f, index );
-          if( optInternalRepSortInference() ){
-            int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
-            if( score>=0 && e_sortId!=sortId ){
-              score += 100;
+          if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){
+            if( optInternalRepSortInference() ){
+              int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
+              if( score>=0 && e_sortId!=sortId ){
+                score += 100;
+              }
             }
-          }
-          //score prefers earliest use of this term as a representative
-          if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
-            r_best = eqc[i];
-            r_best_score = score;
-          }
+            //score prefers earliest use of this term as a representative
+            if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
+              r_best = eqc[i];
+              r_best_score = score;
+            }
+                 }
         }
+        if( r_best.isNull() ){
+             Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
+                 r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+               }
         //now, make sure that no other member of the class is an instance
         if( !optInternalRepSortInference() ){
           r_best = getInstance( r_best, eqc );