From 55323fd7283d758caf31e637be237d2416b86167 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 28 Oct 2014 14:28:31 +0100 Subject: [PATCH] Initial infrastructure for function definition quantifiers, internal parsing format for Smt2. --- src/Makefile.am | 2 + src/parser/smt2/Smt2.g | 39 +++++++++++----- src/theory/quantifiers/fun_def_process.cpp | 31 +++++++++++++ src/theory/quantifiers/fun_def_process.h | 45 +++++++++++++++++++ .../quantifiers/inst_strategy_e_matching.cpp | 9 +++- src/theory/quantifiers/options | 3 ++ .../quantifiers/quantifiers_attributes.cpp | 4 ++ src/theory/quantifiers/term_database.cpp | 13 ++++++ src/theory/quantifiers/term_database.h | 7 +++ src/theory/quantifiers/theory_quantifiers.cpp | 1 + 10 files changed, 143 insertions(+), 11 deletions(-) create mode 100644 src/theory/quantifiers/fun_def_process.cpp create mode 100644 src/theory/quantifiers/fun_def_process.h 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; iwarning(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 + +#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 +#include +#include +#include +#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 ); -- 2.30.2