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

6 files changed, 82 insertions, 15 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 38ee4a57f..3e0f13e4b 100644
--- 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 5bdce5fac..909c9c388 100644
--- 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 878d3ac50..1aebbfcc5 100644
--- 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 aa0569ef4..e278de9e1 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/model_engine.h"

 #include "theory/quantifiers/options.h"

 #include "theory/quantifiers/inst_match_generator.h"

+#include "theory/theory_engine.h"

 

 using namespace CVC4;

 using namespace std;

@@ -25,20 +26,67 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;

 using namespace CVC4::kind;

 

+struct PrioritySort {

+  std::vector< double > d_priority;

+  bool operator() (int i,int j) {

+    return d_priority[i] < d_priority[j];

+  }

+};

+

+

 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {

 

 }

 

+double RewriteEngine::getPriority( Node f ) {

+  Node rr = f.getAttribute(QRewriteRuleAttribute());

+  Node rrr = rr[2];

+  Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl;

+  bool deterministic = rrr[1].getKind()!=OR;

+  if( rrr.getKind()==RR_REWRITE ){

+    return deterministic ? 0.0 : 3.0;

+  }else if( rrr.getKind()==RR_DEDUCTION ){

+    return deterministic ? 1.0 : 4.0;

+  }else if( rrr.getKind()==RR_REDUCTION ){

+    return deterministic ? 2.0 : 5.0;

+  }else{

+    return 6.0;

+  }

+}

+

 void RewriteEngine::check( Theory::Effort e ) {

   if( e==Theory::EFFORT_LAST_CALL ){

+    if( !d_quantEngine->getModel()->isModelSet() ){

+      d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true );

+    }

     if( d_true.isNull() ){

       d_true = NodeManager::currentNM()->mkConst( true );

     }

+    std::vector< Node > priority_order;

+    PrioritySort ps;

+    std::vector< int > indicies;

+    for( int i=0; i<(int)d_rr_quant.size(); i++ ){

+      ps.d_priority.push_back( getPriority( d_rr_quant[i] ) );

+      indicies.push_back( i );

+    }

+    std::sort( indicies.begin(), indicies.end(), ps );

+    for( unsigned i=0; i<indicies.size(); i++ ){

+      priority_order.push_back( d_rr_quant[indicies[i]] );

+    }

+

     //apply rewrite rules

     int addedLemmas = 0;

-    for( unsigned i=0; i<d_rr_quant.size(); i++ ) {

-      addedLemmas += checkRewriteRule( d_rr_quant[i] );

+    //per priority level

+    int index = 0;

+    bool success = true;

+    while( success && index<(int)priority_order.size() ) {

+      addedLemmas += checkRewriteRule( priority_order[index] );

+      index++;

+      if( index<(int)priority_order.size() ){

+        success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] );

+      }

     }

+

     Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;

     if (addedLemmas==0) {

     }else{

@@ -49,7 +97,7 @@ void RewriteEngine::check( Theory::Effort e ) {
 }

 

 int RewriteEngine::checkRewriteRule( Node f ) {

-  Trace("rewrite-engine-inst") << "Check " << f << "..." << std::endl;

+  Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl;

   int addedLemmas = 0;

   //reset triggers

   Node rr = f.getAttribute(QRewriteRuleAttribute());

@@ -102,6 +150,12 @@ int RewriteEngine::checkRewriteRule( Node f ) {
           if( d_quantEngine->addInstantiation( f, m ) ){

             addedLemmas++;

             Trace("rewrite-engine-inst-debug") << "success" << std::endl;

+            //set the no-match attribute (the term is rewritten and can be ignored)

+            //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl;

+            //if( !m.d_matched.isNull() ){

+            //  NoMatchAttribute nma;

+            //  m.d_matched.setAttribute(nma,true);

+            //}

           }else{

             Trace("rewrite-engine-inst-debug") << "failure." << std::endl;

           }

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index fe8daca5f..6783b20d0 100755
--- 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;

   /** explicitly provided patterns */

   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;

+  double getPriority( Node f );

 private:

   int checkRewriteRule( Node f );

 public:

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e1a953e1b..5569f6843 100644
--- 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;
       }
     }
   }