diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-17 17:35:56 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-17 17:35:56 -0600 |
commit | b0d7ac44fb7be5c56cd0c743114e792a985bb3b7 (patch) | |
tree | 4d5e8de3b66de4af0fe225d594edd78726b8bb1d /src/theory/quantifiers/quantifiers_attributes.cpp | |
parent | c603a047ac534ed4caafb128b5d333e05e1fd191 (diff) |
Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 8c6b30124..040eadc9f 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -24,7 +24,7 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value ){ +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( attr=="axiom" ){ Trace("quant-attr-debug") << "Set axiom " << n << std::endl; @@ -58,5 +58,13 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; RrPriorityAttribute rrpa; n.setAttribute( rrpa, lvl ); + }else if( attr=="quant-elim" ){ + Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; + QuantElimAttribute qea; + n.setAttribute( qea, true ); + }else if( attr=="quant-elim-partial" ){ + Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl; + QuantElimPartialAttribute qepa; + n.setAttribute( qepa, true ); } } |