From: ajreynol Date: Tue, 7 Oct 2014 13:34:56 +0000 (+0200) Subject: Refactor quantifiers attributes. X-Git-Tag: cvc5-1.0.0~6583 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33d0894b7707e3f590404cc51963af7740e7412a;p=cvc5.git Refactor quantifiers attributes. --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e7d614b85..366c76194 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1079,7 +1079,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr, attr] - { if( ( attr == ":pattern" || attr == ":no-pattern" ) && ! attexpr.isNull()) { + { if( ! attexpr.isNull()) { patexprs.push_back( attexpr ); } } @@ -1199,7 +1199,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] } std::string attr_name = attr; attr_name.erase( attr_name.begin() ); - Command* c = new SetUserAttributeCommand( attr_name, expr ); + //will set the attribute on auxiliary var (preserves attribute on formula through rewriting) + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( attr_name, avar ); c->setMuted(true); PARSER_STATE->preemptCommand(c); } else { @@ -1216,23 +1220,17 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":no-pattern"); retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr); } - | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL + | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL { Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); std::vector values; values.push_back( n ); - std::string attr_name("quant-inst-max-level"); - Command* c = new SetUserAttributeCommand( attr_name, expr, values ); - c->setMuted(true); - PARSER_STATE->preemptCommand(c); - } - | ATTRIBUTE_RR_PRIORITY_LEVEL INTEGER_LITERAL - { - Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); - std::vector values; - values.push_back( n ); - std::string attr_name("rr-priority"); - Command* c = new SetUserAttributeCommand( attr_name, expr, values ); + std::string attr_name(AntlrInput::tokenText($tok)); + attr_name.erase( attr_name.begin() ); + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( attr_name, avar, values ); c->setMuted(true); PARSER_STATE->preemptCommand(c); } diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 89f35bf05..6ce8efef9 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -724,6 +724,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa goto next_worklist; } switch(k) { + case kind::INST_ATTRIBUTE: case kind::BOUND_VAR_LIST: result.top() << top; worklist.pop(); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index a32e7f6b0..5f949789a 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -122,10 +122,10 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ - if( f.getNumChildren()==3 && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){ + if( hasUserPatterns( f ) && options::userPatternsQuant()==USER_PAT_MODE_TRUST ){ return STATUS_UNKNOWN; }else{ - int peffort = ( f.getNumChildren()==3 && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1; + int peffort = ( hasUserPatterns( f ) && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ) ? 2 : 1; //int peffort = 1; if( e::iterator it = d_hasUserPatterns.find( f ); + if( it==d_hasUserPatterns.end() ){ + bool hasPat = false; + for( unsigned i=0; isecond; + } + }else{ + return false; + } +} + void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) { Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 ); if( std::find( d_user_no_gen[f].begin(), d_user_no_gen[f].end(), pat[0] )==d_user_no_gen[f].end() ){ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 53ca5bf78..c2b4f7533 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -88,6 +88,10 @@ private: int process( Node f, Theory::Effort effort, int e ); /** generate triggers */ void generateTriggers( Node f, Theory::Effort effort, int e, int & status ); + /** has user patterns */ + bool hasUserPatterns( Node f ); + /** has user patterns */ + std::map< Node, bool > d_hasUserPatterns; public: /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all) rstrt is the relevance setting for trigger (use only relevant triggers vs. use all) diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 1fda30301..a8774440e 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -34,6 +34,7 @@ sort INST_PATTERN_TYPE \ # An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger. operator INST_PATTERN 1: "instantiation pattern" operator INST_NO_PATTERN 1 "instantiation no-pattern" +operator INST_ATTRIBUTE 1 "instantiation attribute" sort INST_PATTERN_LIST_TYPE \ Cardinality::INTEGERS \ @@ -48,6 +49,7 @@ typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule +typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule # for rewrite rules diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 4179dcbf5..2c9a33388 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -383,7 +383,7 @@ QModelBuilderIG::Statistics::~Statistics(){ bool QModelBuilderIG::isQuantifierActive( Node f ){ return !TermDb::isRewriteRule( f ) && - ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); + ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end(); } bool QModelBuilderIG::isTermActive( Node n ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 8d479c29e..f58e89c38 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -25,31 +25,25 @@ using namespace CVC4::theory::quantifiers; void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector node_values, std::string str_value ){ Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; - if( n.getKind()==FORALL ){ - if( attr=="axiom" ){ - Trace("quant-attr") << "Set axiom " << n << std::endl; - AxiomAttribute aa; - n.setAttribute( aa, true ); - }else if( attr=="conjecture" ){ - Trace("quant-attr") << "Set conjecture " << n << std::endl; - ConjectureAttribute ca; - n.setAttribute( ca, true ); - }else if( attr=="quant-inst-max-level" ){ - Assert( node_values.size()==1 ); - uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); - Trace("quant-attr") << "Set instantiation level " << n << " to " << lvl << std::endl; - QuantInstLevelAttribute qila; - n.setAttribute( qila, lvl ); - }else if( attr=="rr-priority" ){ - Assert( node_values.size()==1 ); - uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); - Trace("quant-attr") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; - RrPriorityAttribute rrpa; - n.setAttribute( rrpa, lvl ); - } - }else{ - for( size_t i=0; i().getNumerator().getLong(); + Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; + QuantInstLevelAttribute qila; + n.setAttribute( qila, lvl ); + }else if( attr=="rr-priority" ){ + Assert( node_values.size()==1 ); + uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); + Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; + RrPriorityAttribute rrpa; + n.setAttribute( rrpa, lvl ); } } diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 34649ae05..bad58eef8 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -26,14 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -/** Attribute true for quantifiers that are axioms */ -struct AxiomAttributeId {}; -typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; - -/** Attribute true for quantifiers that are conjecture */ -struct ConjectureAttributeId {}; -typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; - /** Attribute priority for rewrite rules */ //struct RrPriorityAttributeId {}; //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0d85eae83..7ec503016 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -976,3 +976,66 @@ Node TermDb::getRewriteRule( Node q ) { return Node::null(); } } + + +void TermDb::computeAttributes( Node q ) { + if( q.getNumChildren()==3 ){ + for( unsigned i=0; i::iterator it = d_qattr_conjecture.find( q ); + if( it==d_qattr_conjecture.end() ){ + return false; + }else{ + return it->second; + } +} + +bool TermDb::isQAttrAxiom( Node q ) { + std::map< Node, bool >::iterator it = d_qattr_axiom.find( q ); + if( it==d_qattr_axiom.end() ){ + return false; + }else{ + return it->second; + } +} + +int TermDb::getQAttrQuantInstLevel( Node q ) { + std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q ); + if( it==d_qattr_qinstLevel.end() ){ + return -1; + }else{ + return it->second; + } +} + +int TermDb::getQAttrRewriteRulePriority( Node q ) { + std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q ); + if( it==d_qattr_rr_priority.end() ){ + return -1; + }else{ + return it->second; + } +} diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 91ad0135b..e9234bdfe 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -25,6 +25,14 @@ namespace CVC4 { namespace theory { +/** Attribute true for quantifiers that are axioms */ +struct AxiomAttributeId {}; +typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; + +/** Attribute true for quantifiers that are conjecture */ +struct ConjectureAttributeId {}; +typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; + /** Attribute true for nodes that should not be used for matching */ struct NoMatchAttributeId {}; /** use the special for boolean flag */ @@ -285,6 +293,24 @@ public: //general queries concerning quantified formulas wrt modules /** get the rewrite rule associated with the quanfied formula */ static Node getRewriteRule( Node q ); +//attributes +private: + std::map< Node, bool > d_qattr_conjecture; + std::map< Node, bool > d_qattr_axiom; + std::map< Node, int > d_qattr_rr_priority; + std::map< Node, int > d_qattr_qinstLevel; + //record attributes + void computeAttributes( Node q ); +public: + /** is conjecture */ + bool isQAttrConjecture( Node q ); + /** is axiom */ + bool isQAttrAxiom( Node q ); + /** get instantiation level */ + int getQAttrQuantInstLevel( Node q ); + /** get rewrite rule priority */ + int getQAttrRewriteRulePriority( Node q ); + };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 18546b09c..e71489fc5 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -42,7 +42,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); - out.handleUserAttribute( "inst-level", this ); + out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); } diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 7fc69c539..5d86c29c0 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -96,13 +96,21 @@ struct QuantifierInstNoPatternTypeRule { } };/* struct QuantifierInstNoPatternTypeRule */ +struct QuantifierInstAttributeTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::INST_ATTRIBUTE ); + return nodeManager->instPatternType(); + } +};/* struct QuantifierInstAttributeTypeRule */ + struct QuantifierInstPatternListTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::INST_PATTERN_LIST ); if( check ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN ){ + if( n[i].getKind()!=kind::INST_PATTERN && n[i].getKind()!=kind::INST_NO_PATTERN && n[i].getKind()!=kind::INST_ATTRIBUTE ){ throw TypeCheckingExceptionPrivate(n, "argument of inst pattern list is not inst pattern"); } } @@ -148,7 +156,6 @@ public: } };/* class RewriteRuleTypeRule */ - class RRRewriteTypeRule { public: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5bf285ae2..d81db8b8d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -286,6 +286,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){ Assert( f.getKind()==FORALL ); //make instantiation constants for f d_term_db->makeInstantiationConstantsFor( f ); + d_term_db->computeAttributes( f ); //register with quantifier relevance if( d_quant_rel ){ d_quant_rel->registerQuantifier( f ); @@ -464,10 +465,9 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) { if( n.hasAttribute(InstLevelAttribute()) ){ - unsigned ml = options::instMaxLevel(); - if( f.hasAttribute(QuantInstLevelAttribute()) ){ - ml = f.getAttribute(QuantInstLevelAttribute()); - } + int fml = d_term_db->getQAttrQuantInstLevel( f ); + unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + if( n.getAttribute(InstLevelAttribute())>ml ){ Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;