From d0ec84da973d3ba7054b61fd620a1eba0d459a48 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 18 Jul 2013 13:08:56 -0500 Subject: [PATCH] Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine. --- .../quantifiers/instantiation_engine.cpp | 7 ++- .../quantifiers/quantifiers_attributes.cpp | 4 ++ .../quantifiers/quantifiers_attributes.h | 4 ++ src/theory/quantifiers/rewrite_engine.cpp | 60 ++++++++++++++++++- src/theory/quantifiers/rewrite_engine.h | 1 + src/theory/quantifiers/term_database.cpp | 21 ++++--- 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 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; iaddInstantiation( 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; imkConst( 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; igetTheoryEngine()->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=0 && ( r_best_score<0 || scoregetTermDatabase()->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 ); -- 2.30.2