summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am2
-rw-r--r--src/parser/smt2/Smt2.g39
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp31
-rw-r--r--src/theory/quantifiers/fun_def_process.h45
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp9
-rw-r--r--src/theory/quantifiers/options3
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp13
-rw-r--r--src/theory/quantifiers/term_database.h7
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp1
10 files changed, 143 insertions, 11 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index d82c0945d..a04b86bee 100644
--- 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 0a3773d08..35566be45 100644
--- 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
index 000000000..c9dbb8d4b
--- /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
index 000000000..c2d8aeb65
--- /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 4284c8145..02536eb99 100644
--- 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 dc2102ffa..730da8839 100644
--- 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 48608cb4e..ef5b71f9d 100644
--- 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 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() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 25ef9c81c..13dfa657c 100644
--- 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 f7c4c745f..6dac8a72d 100644
--- 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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback