Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9c1eeb9b4..3a9353de9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1015,6 +1015,10 @@ void TermDb::computeAttributes( Node q ) {
           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
           d_qattr_conjecture[q] = true;
         }
+        if( avar.getAttribute(FunDefAttribute()) ){
+          Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
+          d_qattr_fundef[q] = true;
+        }
         if( avar.getAttribute(SygusAttribute()) ){
           //should be nested existential
           Assert( q[1].getKind()==NOT );
@@ -1074,6 +1078,15 @@ bool TermDb::isQAttrAxiom( Node q ) {
   }
 }
 
+bool TermDb::isQAttrFunDef( Node q ) {
+  std::map< Node, bool >::iterator it = d_qattr_fundef.find( q );
+  if( it==d_qattr_fundef.end() ){
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
 bool TermDb::isQAttrSygus( Node q ) {
   std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
   if( it==d_qattr_sygus.end() ){