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

diff --git a/src/Makefile.am b/src/Makefile.am
index d82c0945d2e5cb4db94baa564b1f4a780b338372..a04b86bee69cc5d1668fb820ee23cb2ec501baf7 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -332,6 +332,8 @@ libcvc4_la_SOURCES = \
        theory/quantifiers/conjecture_generator.cpp \
        theory/quantifiers/ce_guided_instantiation.h \
        theory/quantifiers/ce_guided_instantiation.cpp \
+       theory/quantifiers/fun_def_process.h \
+       theory/quantifiers/fun_def_process.cpp \
        theory/quantifiers/options_handlers.h \
        theory/arith/theory_arith_type_rules.h \
        theory/arith/type_enumerator.h \

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 0a3773d0871aa5fd30e7095bd103dcf3e334e115..35566be45cb01b5f3c5bf9bf8bbb78761c73df01 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1298,21 +1298,40 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
         PARSER_STATE->warning(ss.str());
       }
       // do nothing
-    } else if(attr==":axiom" || attr==":conjecture" || attr==":sygus" || attr==":synthesis") {
+    } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || attr==":sygus" || attr==":synthesis") {
       if(hasValue) {
         std::stringstream ss;
         ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
         PARSER_STATE->warning(ss.str());
       }
-      std::string attr_name = attr;
-      attr_name.erase( attr_name.begin() );
-      //will set the attribute on auxiliary var (preserves attribute on formula through rewriting)
-      Type t = EXPR_MANAGER->booleanType();
-      Expr avar = PARSER_STATE->mkVar(attr_name, t);
-      retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
-      Command* c = new SetUserAttributeCommand( attr_name, avar );
-      c->setMuted(true);
-      PARSER_STATE->preemptCommand(c);
+      bool success = true;
+      if( attr==":fun-def" ){
+        if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){
+          success = false;
+        }else{
+          for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){
+            if( expr[0][i].getKind()!=kind::BOUND_VARIABLE ){
+              success = false;
+            }
+          }
+        }
+        if( !success ){
+          std::stringstream ss;
+          ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to variables.";
+          PARSER_STATE->warning(ss.str());
+        }
+      }
+      if( success ){
+        std::string attr_name = attr;
+        attr_name.erase( attr_name.begin() );
+        //will set the attribute on auxiliary var (preserves attribute on formula through rewriting)
+        Type t = EXPR_MANAGER->booleanType();
+        Expr avar = PARSER_STATE->mkVar(attr_name, t);
+        retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar);
+        Command* c = new SetUserAttributeCommand( attr_name, avar );
+        c->setMuted(true);
+        PARSER_STATE->preemptCommand(c);
+      }
     } else {
       PARSER_STATE->attributeNotSupported(attr);
     }

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
new file mode 100644 (file)
index 0000000..c9dbb8d
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file fun_def_process.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Kshitij Bansal
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sort inference module
+ **
+ ** This class implements pre-process steps for well-defined functions
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/fun_def_process.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+
+void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
+
+}

diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
new file mode 100644 (file)
index 0000000..c2d8aeb
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file fun_def_process.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Pre-process steps for well-defined functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
+#define __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//find finite models for well-defined functions
+class FunDefFmf {
+public:
+  FunDefFmf(){}
+  ~FunDefFmf(){}
+
+  void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+};
+
+
+}
+}
+}
+
+#endif

diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 4284c8145ac050ec598fc5db62e7e2ec4e829226..02536eb9924fec8038ec4413478e5d07926a05f3 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -220,7 +220,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     d_patTerms[0][f].clear();
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
-    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+    if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){
+      Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
+      Assert( bd.getKind()==EQUAL || bd.getKind()==IFF );
+      Assert( bd[0].getKind()==APPLY_UF );
+      patTermsF.push_back( bd[0] );
+    }else{
+      Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true );
+    }
     Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
     Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)patTermsF.size(); i++ ){

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index dc2102ffae20b22f70b8c188a9d96cf84117dd76..730da88396cef01405a08e09ea91cf1c079667fb 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -72,6 +72,9 @@ option multiTriggerWhenSingle --multi-trigger-when-single bool :default true
 option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
  selection mode for triggers
 
+option quantFunWellDefined --quant-fun-wd bool :default false
+ assume that function defined by quantifiers are well defined
+ 
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 48608cb4ed690dab3786042a57ad3ac536df978b..ef5b71f9d1095bd27e9c9e44be3d8b46d0b0df61 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -33,6 +33,10 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n, s
     Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
     ConjectureAttribute ca;
     n.setAttribute( ca, true );
+  }else if( attr=="fun-def" ){
+    Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
+    FunDefAttribute fda;
+    n.setAttribute( fda, true );
   }else if( attr=="sygus" ){
     Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
     SygusAttribute ca;

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9c1eeb9b472d5910d43ab3662e534527b8f1b13a..3a9353de9e317132e3808ac878200c191bee5d47 100644 (file)
--- 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() ){

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 25ef9c81c4ff2423c734af6b830cf6ba67621f0c..13dfa657ca27e34b5e67f1101cc1090cce92a28c 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -34,6 +34,10 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
 struct ConjectureAttributeId {};
 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
   
+/** Attribute true for function definition quantifiers */
+struct FunDefAttributeId {};
+typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
+
 /** Attribute true for quantifiers that are SyGus conjectures */
 struct SygusAttributeId {};
 typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
@@ -317,6 +321,7 @@ public: //general queries concerning quantified formulas wrt modules
 private:
   std::map< Node, bool > d_qattr_conjecture;
   std::map< Node, bool > d_qattr_axiom;
+  std::map< Node, bool > d_qattr_fundef;
   std::map< Node, bool > d_qattr_sygus;
   std::map< Node, bool > d_qattr_synthesis;
   std::map< Node, int > d_qattr_rr_priority;
@@ -328,6 +333,8 @@ public:
   bool isQAttrConjecture( Node q );
   /** is axiom */
   bool isQAttrAxiom( Node q );
+  /** is function definition */
+  bool isQAttrFunDef( Node q );
   /** is sygus conjecture */
   bool isQAttrSygus( Node q );
   /** is synthesis conjecture */

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index f7c4c745f81d153957627d9107d0192042d96461..6dac8a72d0c1cfffb75f2e8079a2483da3736f15 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -42,6 +42,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   d_baseDecLevel = -1;
   out.handleUserAttribute( "axiom", this );
   out.handleUserAttribute( "conjecture", this );
+  out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
   out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );