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

1 files changed, 105 insertions, 51 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a679ccfa8..284cae2e0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1787,69 +1787,107 @@ bool TermDb::isSygusConjectureAnnotation( Node ipl ){
   return false;
 }
 
+bool TermDb::isQuantElimAnnotation( Node ipl ) {
+  if( !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        Node avar = ipl[i][0];
+        if( avar.getAttribute(QuantElimAttribute()) ){
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 void TermDb::computeAttributes( Node q ) {
+  computeQuantAttributes( q, d_qattr[q] );
+  if( !d_qattr[q].d_rr.isNull() ){
+    if( d_quantEngine->getRewriteEngine()==NULL ){
+      Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
+    }
+    //set rewrite engine as owner
+    d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+  }
+  if( d_qattr[q].isFunDef() ){
+    Node f = d_qattr[q].d_fundef_f;
+    if( d_fun_defs.find( f )!=d_fun_defs.end() ){
+      Message() << "Cannot define function " << f << " more than once." << std::endl;
+      exit( 1 );
+    }
+    d_fun_defs[f] = true;
+    d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+  }
+  if( d_qattr[q].d_sygus ){
+    if( d_quantEngine->getCegInstantiation()==NULL ){
+      Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+    }
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+  }
+  if( d_qattr[q].d_synthesis ){
+    if( d_quantEngine->getCegInstantiation()==NULL ){
+      Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
+    }
+    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+  }
+}
+
+void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
   Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
   if( q.getNumChildren()==3 ){
+    qa.d_ipl = q[2];
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
       Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
       if( q[2][i].getKind()==INST_ATTRIBUTE ){
         Node avar = q[2][i][0];
         if( avar.getAttribute(AxiomAttribute()) ){
           Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
-          d_qattr_axiom[q] = true;
+          qa.d_axiom = true;
         }
         if( avar.getAttribute(ConjectureAttribute()) ){
           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
-          d_qattr_conjecture[q] = true;
+          qa.d_conjecture = true;
         }
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
-          d_qattr_fundef[q] = true;
           //get operator directly from pattern
-          Node f = q[2][i][0].getOperator();
-          if( d_fun_defs.find( f )!=d_fun_defs.end() ){
-            Message() << "Cannot define function " << f << " more than once." << std::endl;
-            exit( 0 );
-          }
-          d_fun_defs[f] = true;
-          d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
+          qa.d_fundef_f = q[2][i][0].getOperator();
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //not necessarily nested existential
           //Assert( q[1].getKind()==NOT );
           //Assert( q[1][0].getKind()==FORALL );
-
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
-          d_qattr_sygus[q] = true;
-          if( d_quantEngine->getCegInstantiation()==NULL ){
-            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
-          }
-          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+          qa.d_sygus = true;
         }
         if( avar.getAttribute(SynthesisAttribute()) ){
           Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
-          d_qattr_synthesis[q] = true;
-          if( d_quantEngine->getCegInstantiation()==NULL ){
-            Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
-          }
-          d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+          qa.d_synthesis = true;
         }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
-          d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
-          Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
+          qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
+          Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
         }
         if( avar.hasAttribute(RrPriorityAttribute()) ){
-          d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
-          Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
+          qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
+          Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
         }
+        if( avar.getAttribute(QuantElimAttribute()) ){
+          Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
+          qa.d_quant_elim = true;
+          //don't set owner, should happen naturally
+        } 
+        if( avar.getAttribute(QuantElimPartialAttribute()) ){
+          Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
+          qa.d_quant_elim = true;
+          qa.d_quant_elim_partial = true;
+          //don't set owner, should happen naturally
+        } 
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
           Assert( i==0 );
-          if( d_quantEngine->getRewriteEngine()==NULL ){
-            Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
-          }
-          //set rewrite engine as owner
-          d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+          qa.d_rr = avar;
         }
       }
     }
@@ -1857,69 +1895,85 @@ void TermDb::computeAttributes( Node q ) {
 }
 
 bool TermDb::isQAttrConjecture( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_conjecture.find( q );
-  if( it==d_qattr_conjecture.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_conjecture;
   }
 }
 
 bool TermDb::isQAttrAxiom( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_axiom.find( q );
-  if( it==d_qattr_axiom.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_axiom;
   }
 }
 
 bool TermDb::isQAttrFunDef( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_fundef.find( q );
-  if( it==d_qattr_fundef.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.isFunDef();
   }
 }
 
 bool TermDb::isQAttrSygus( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
-  if( it==d_qattr_sygus.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_sygus;
   }
 }
 
 bool TermDb::isQAttrSynthesis( Node q ) {
-  std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
-  if( it==d_qattr_synthesis.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return false;
   }else{
-    return it->second;
+    return it->second.d_synthesis;
   }
 }
 
 int TermDb::getQAttrQuantInstLevel( Node q ) {
-  std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
-  if( it==d_qattr_qinstLevel.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return -1;
   }else{
-    return it->second;
+    return it->second.d_qinstLevel;
   }
 }
 
 int TermDb::getQAttrRewriteRulePriority( Node q ) {
-  std::map< Node, int >::iterator it = d_qattr_rr_priority.find( q );
-  if( it==d_qattr_rr_priority.end() ){
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
     return -1;
   }else{
-    return it->second;
+    return it->second.d_rr_priority;
   }
 }
 
+bool TermDb::isQAttrQuantElim( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
+    return false;
+  }else{
+    return it->second.d_quant_elim;
+  }
+}
 
+bool TermDb::isQAttrQuantElimPartial( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
+    return false;
+  }else{
+    return it->second.d_quant_elim_partial;
+  }
+}
 
 TermDbSygus::TermDbSygus(){
   d_true = NodeManager::currentNM()->mkConst( true );