Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.

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 );
   }
 }