diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 41 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 |
11 files changed, 68 insertions, 26 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 71b05cec5..3260f7122 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -74,6 +74,8 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de when to apply instantiation option instMaxLevel --inst-max-level=N int :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) +option instLevelInputOnly --inst-level-input-only bool :default true + only input terms are assigned instantiation level zero option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index a5de6ffa9..b41987923 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -22,7 +23,8 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){ +void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector<Node> 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; @@ -32,14 +34,22 @@ 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 if( attr=="inst-level" ){ + Assert( node_values.size()==1 ); + uint64_t lvl = node_values[0].getConst<Rational>().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<Rational>().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<n.getNumChildren(); i++ ){ - setUserAttribute( attr, n[i] ); + setUserAttribute( attr, n[i], node_values, str_value ); } } } diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index cf9620a07..34649ae05 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -44,7 +44,7 @@ struct QuantifiersAttributes * This function will apply a custom set of attributes to all top-level universal * quantifiers contained in n */ - static void setUserAttribute( const std::string& attr, Node n ); + static void setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value ); }; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d6b336dfa..504ecd667 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -55,6 +55,13 @@ typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribu struct BoundIntLitAttributeId {}; typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute; +//for quantifier instantiation level +struct QuantInstLevelAttributeId {}; +typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute; + +//rewrite-rule priority +struct RrPriorityAttributeId {}; +typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute; class QuantifiersEngine; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 4ba3c499d..4e8a0a411 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -42,6 +42,8 @@ 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( "rr-priority", this ); } TheoryQuantifiers::~TheoryQuantifiers() { @@ -193,6 +195,6 @@ bool TheoryQuantifiers::restart(){ } } -void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){ - QuantifiersAttributes::setUserAttribute( attr, n ); +void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ + QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index ffd3c4c59..6febc8417 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -69,7 +69,7 @@ public: void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } bool flipDecision(); - void setUserAttribute( const std::string& attr, Node n ); + void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value); eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; } private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f80f65723..eb5dbaef0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -404,7 +404,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } } } - setInstantiationLevelAttr( body, f[1], maxInstLevel+1, terms ); + setInstantiationLevelAttr( body, f[1], maxInstLevel+1 ); } Trace("inst-debug") << "*** Lemma is " << lem << std::endl; ++(d_statistics.d_instantiations); @@ -415,22 +415,31 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } } -void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms ){ +void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){ + Trace("inst-level-debug") << "IL : " << n << " " << qn << " " << level << std::endl; //if not from the vector of terms we instantiatied - if( std::find( inst_terms.begin(), inst_terms.end(), n )==inst_terms.end() ){ + if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){ //if this is a new term, without an instantiation level - if( n!=qn && !n.hasAttribute(InstLevelAttribute()) ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ InstLevelAttribute ila; n.setAttribute(ila,level); + Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl; } - Assert( qn.getKind()!=BOUND_VARIABLE ); Assert( n.getNumChildren()==qn.getNumChildren() ); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationLevelAttr( n[i], qn[i], level, inst_terms ); + setInstantiationLevelAttr( n[i], qn[i], level ); } } } +void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } +} + Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ if( n.getKind()==INST_CONSTANT ){ Debug("check-inst") << "Substitute inst constant : " << n << std::endl; @@ -579,11 +588,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo if( options::instMaxLevel()!=-1 ){ for( unsigned i=0; i<terms.size(); i++ ){ - if( terms[i].hasAttribute(InstLevelAttribute()) && - (int)terms[i].getAttribute(InstLevelAttribute())>options::instMaxLevel() ){ - Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl; - return false; + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + unsigned ml = options::instMaxLevel(); + if( f.hasAttribute(QuantInstLevelAttribute()) ){ + ml = f.getAttribute(QuantInstLevelAttribute()); + } + if( terms[i].getAttribute(InstLevelAttribute())>ml ){ + Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; + return false; + } + }else{ + if( options::instLevelInputOnly() ){ + Trace("inst-add-debug") << "Term " << terms[i] << " does not have an instantiation level." << std::endl; + return false; + } } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f74c478ae..5315a1de8 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -205,7 +205,7 @@ private: /** instantiate f with arguments terms */ bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ - void setInstantiationLevelAttr( Node n, Node qn, uint64_t level, std::vector< Node >& inst_terms ); + static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ void flushLemmas(); public: @@ -235,6 +235,8 @@ public: bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } /** get number of waiting lemmas */ int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); } + /** set instantiation level attr */ + static void setInstantiationLevelAttr( Node n, uint64_t level ); public: /** get number of quantifiers */ int getNumQuantifiers() { return (int)d_quants.size(); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 7bfc7051f..ac3d018fb 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -678,7 +678,7 @@ public: * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! n :attr) */ - virtual void setUserAttribute(const std::string& attr, Node n) { + virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) { Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface", identify().c_str()); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index eb1da84b2..1b0270b94 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1668,11 +1668,11 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) } -void TheoryEngine::setUserAttribute(const std::string& attr, Node n) { +void TheoryEngine::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) { Trace("te-attr") << "set user attribute " << attr << " " << n << endl; if( d_attr_handle.find( attr )!=d_attr_handle.end() ){ for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){ - d_attr_handle[attr][i]->setUserAttribute(attr, n); + d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value); } } else { //unhandled exception? diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e6684d56e..eec4f1168 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -820,7 +820,7 @@ public: * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! n :attr) */ - void setUserAttribute(const std::string& attr, Node n); + void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value); /** * Handle user attribute. |