diff options
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 4 | ||||
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.cpp | 60 | ||||
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 35 |
7 files changed, 100 insertions, 32 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; } } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bc1a6929d..f94a87748 100644 --- 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 ); |