diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 9 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 42 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 17 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 69 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_inference.cpp | 216 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_inference.h | 49 |
9 files changed, 403 insertions, 22 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index b1d7febbb..8aa06e82f 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -483,6 +483,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_unif_strat.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ + theory/quantifiers/sygus_inference.cpp \ + theory/quantifiers/sygus_inference.h \ theory/quantifiers/sygus_sampler.cpp \ theory/quantifiers/sygus_sampler.h \ theory/quantifiers/symmetry_breaking.cpp \ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index f877143a2..4a098f9fc 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -879,6 +879,15 @@ header = "options/quantifiers_options.h" ### Synthesis options [[option]] + name = "sygusInference" + category = "regular" + long = "sygus-inference" + type = "bool" + default = "false" + read_only = false + help = "attempt to preprocess arbitrary inputs to sygus conjectures" + +[[option]] name = "ceGuidedInst" category = "regular" long = "cegqi" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a329541e5..2f6832089 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -93,12 +93,13 @@ #include "theory/bv/bvintropow2.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus_inference.h" #include "theory/quantifiers/term_util.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" @@ -1366,6 +1367,14 @@ void SmtEngine::setDefaults() { */ } + // sygus inference may require datatypes + if (options::sygusInference()) + { + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableTheory(THEORY_DATATYPES); + d_logic.lock(); + } + if ((options::checkModels() || options::checkSynthSol()) && !options::produceAssertions()) { @@ -1882,6 +1891,23 @@ void SmtEngine::setDefaults() { } //apply counterexample guided instantiation options + // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst + if (options::sygusInference()) + { + if (!options::ceGuidedInst.wasSetByUser()) + { + options::ceGuidedInst.set(true); + } + // optimization: apply preskolemization, makes it succeed more often + if (!options::preSkolemQuant.wasSetByUser()) + { + options::preSkolemQuant.set(true); + } + if (!options::preSkolemQuantNested.wasSetByUser()) + { + options::preSkolemQuantNested.set(true); + } + } if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){ if( !options::ceGuidedInst.wasSetByUser() ){ options::ceGuidedInst.set( true ); @@ -4235,9 +4261,19 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - // global negation of the formula - if (options::globalNegate()) + if (options::sygusInference()) + { + // try recast as sygus + quantifiers::SygusInference si; + if (si.simplify(d_assertions.ref())) + { + Trace("smt-proc") << "...converted to sygus conjecture." << std::endl; + d_smt.d_globalNegation = !d_smt.d_globalNegation; + } + } + else if (options::globalNegate()) { + // global negation of the formula quantifiers::GlobalNegate gn; gn.simplify(d_assertions.ref()); d_smt.d_globalNegation = !d_smt.d_globalNegation; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 149380b84..2fbcc2641 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -100,6 +100,18 @@ public: static Node rewriteRewriteRule( Node r ); static bool containsQuantifiers( Node n ); static bool isPrenexNormalForm( Node n ); + /** preprocess + * + * This returns the result of applying simple quantifiers-specific + * preprocessing to n, including but not limited to: + * - rewrite rule elimination, + * - pre-skolemization, + * - aggressive prenexing. + * The argument isInst is set to true if n is an instance of a previously + * registered quantified formula. If this flag is true, we do not apply + * certain steps like pre-skolemization since we know they will have no + * effect. + */ static Node preprocess( Node n, bool isInst = false ); static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 3e48c11b2..0979e8b4e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -118,14 +118,20 @@ void CegConjectureSingleInv::initialize( Node q ) { d_simp_quant = q; Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl; // infer single invocation-ness + + // get the variables std::vector< Node > progs; std::map< Node, std::vector< Node > > prog_vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - Node sf = q[0][i]; + for (const Node& sf : q[0]) + { progs.push_back( sf ); - Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute()); - for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){ - prog_vars[sf].push_back( sfvl[j] ); + Node sfvl = CegGrammarConstructor::getSygusVarList(sf); + if (!sfvl.isNull()) + { + for (const Node& sfv : sfvl) + { + prog_vars[sf].push_back(sfv); + } } } // compute single invocation partition @@ -270,6 +276,7 @@ void CegConjectureSingleInv::initialize( Node q ) { Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; Assert( !templ.isNull() ); // subsitute the template arguments + Assert(prog_templ_vars.size() == prog_vars[prog].size()); templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); Trace("cegqi-inv") << " template : " << templ << std::endl; d_templ[prog] = templ; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 08b0dc837..322d49af6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -99,25 +99,45 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, collectTerms( q[1], extra_cons ); } + NodeManager* nm = NodeManager::currentNM(); + std::vector< Node > qchildren; std::map< Node, Node > synth_fun_vars; std::vector< Node > ebvl; Node qbody_subs = q[1]; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ Node sf = q[0][i]; - // v encodes the syntactic restrictions (via an inductive datatype) on sf - // from the input + // if non-null, v encodes the syntactic restrictions (via an inductive + // datatype) on sf from the input. Node v = sf.getAttribute(SygusSynthGrammarAttribute()); - Assert(!v.isNull()); - Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute()); + TypeNode preGrammarType; + if (!v.isNull()) + { + preGrammarType = v.getType(); + } + else + { + // otherwise, the grammar is the default for the range of the function + preGrammarType = sf.getType(); + if (preGrammarType.isFunction()) + { + preGrammarType = preGrammarType.getRangeType(); + } + } + Node sfvl = getSygusVarList(sf); // sfvl may be null for constant synthesis functions Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl; + // the actual sygus datatype we will use (normalized below) TypeNode tn; std::stringstream ss; ss << sf; - if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){ - tn = v.getType(); + if (preGrammarType.isDatatype() + && static_cast<DatatypeType>(preGrammarType.toType()) + .getDatatype() + .isSygus()) + { + tn = preGrammarType; }else{ // check which arguments are irrelevant std::unordered_set<unsigned> arg_irrelevant; @@ -135,8 +155,9 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, // make the default grammar tn = mkSygusDefaultType( - v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant); + preGrammarType, sfvl, ss.str(), extra_cons, term_irrelevant); } + // normalize type SygusGrammarNorm sygus_norm(d_qe); tn = sygus_norm.normalizeSygusType(tn, sfvl); @@ -158,18 +179,19 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::vector< Node > largs; for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){ schildren.push_back( sfvl[j] ); - largs.push_back( NodeManager::currentNM()->mkBoundVar( sfvl[j].getType() ) ); + largs.push_back(nm->mkBoundVar(sfvl[j].getType())); } std::vector< Node > subsfn_children; subsfn_children.push_back( sf ); subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() ); - Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children ); + Node subsfn = nm->mkNode(kind::APPLY_UF, subsfn_children); TNode subsf = subsfn; Trace("cegqi-debug") << " substitute arg : " << templ_arg << " -> " << subsf << std::endl; templ = templ.substitute( templ_arg, subsf ); // substitute lambda arguments templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() ); - Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ ); + Node subsn = + nm->mkNode(kind::LAMBDA, nm->mkNode(BOUND_VAR_LIST, largs), templ); TNode var = sf; TNode subs = subsn; Trace("cegqi-debug") << " substitute : " << var << " -> " << subs << std::endl; @@ -194,12 +216,12 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, // ev is the first-order variable corresponding to this synth fun std::stringstream ssf; ssf << "f" << sf; - Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn ); + Node ev = nm->mkBoundVar(ssf.str(), tn); ebvl.push_back( ev ); synth_fun_vars[sf] = ev; Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; } - qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) ); + qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl)); if( qbody_subs!=q[1] ){ Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl; qbody_subs = Rewriter::rewrite( qbody_subs ); @@ -209,7 +231,7 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, if( q.getNumChildren()==3 ){ qchildren.push_back( q[2] ); } - return NodeManager::currentNM()->mkNode( kind::FORALL, qchildren ); + return nm->mkNode(kind::FORALL, qchildren); } Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){ @@ -707,6 +729,27 @@ TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); } +Node CegGrammarConstructor::getSygusVarList(Node f) +{ + Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute()); + if (sfvl.isNull() && f.getType().isFunction()) + { + NodeManager* nm = NodeManager::currentNM(); + std::vector<TypeNode> argTypes = f.getType().getArgTypes(); + // make default variable list if none was specified by input + std::vector<Node> bvs; + for (unsigned j = 0, size = argTypes.size(); j < size; j++) + { + std::stringstream ss; + ss << "arg" << j; + bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j])); + } + sfvl = nm->mkNode(BOUND_VAR_LIST, bvs); + f.setAttribute(SygusSynthFunVarListAttribute(), sfvl); + } + return sfvl; +} + }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index d8a77848b..16f4672b0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -84,11 +84,18 @@ public: */ static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); /** + * Returns the sygus variable list for function-to-synthesize variable f. + * These are the names of the arguments of f, which should be included in the + * grammar for f. This returns either the variable list set explicitly via the + * attribute SygusSynthFunVarListAttribute, or a fresh variable list of the + * proper type otherwise. It will return null if f is not a function. + */ + static Node getSygusVarList(Node f); + /** * Returns true iff there are syntax restrictions on the * functions-to-synthesize of sygus conjecture q. */ static bool hasSyntaxRestrictions(Node q); - private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp new file mode 100644 index 000000000..a2bc9357d --- /dev/null +++ b/src/theory/quantifiers/sygus_inference.cpp @@ -0,0 +1,216 @@ +/********************* */ +/*! \file sygus_inference.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_inference + **/ + +#include "theory/quantifiers/sygus_inference.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusInference::SygusInference() {} + +bool SygusInference::simplify(std::vector<Node>& assertions) +{ + Trace("sygus-infer") << "Sygus inference : " << std::endl; + + if (assertions.empty()) + { + Trace("sygus-infer") << "...fail: empty assertions." << std::endl; + return false; + } + + NodeManager* nm = NodeManager::currentNM(); + + // collect free variables in all assertions + std::vector<Node> qvars; + std::map<TypeNode, std::vector<Node> > qtvars; + std::vector<Node> free_functions; + + std::vector<TNode> visit; + std::unordered_set<TNode, TNodeHashFunction> visited; + + // add top-level conjuncts to eassertions + std::vector<Node> assertions_proc = assertions; + std::vector<Node> eassertions; + unsigned index = 0; + while (index < assertions_proc.size()) + { + Node ca = assertions_proc[index]; + if (ca.getKind() == AND) + { + for (const Node& ai : ca) + { + assertions_proc.push_back(ai); + } + } + else + { + eassertions.push_back(ca); + } + } + + // process eassertions + std::vector<Node> processed_assertions; + for (const Node& as : eassertions) + { + // substitution for this assertion + std::vector<Node> vars; + std::vector<Node> subs; + std::map<TypeNode, unsigned> type_count; + Node pas = as; + // rewrite + pas = Rewriter::rewrite(pas); + Trace("sygus-infer") << " " << pas << std::endl; + if (pas.getKind() == FORALL) + { + // preprocess the quantified formula + pas = quantifiers::QuantifiersRewriter::preprocess(pas); + Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; + + pas = pas[1]; + // infer prefix + for (const Node& v : pas[0]) + { + TypeNode tnv = v.getType(); + unsigned vnum = type_count[tnv]; + type_count[tnv]++; + if (vnum < qtvars[tnv].size()) + { + vars.push_back(v); + subs.push_back(qtvars[tnv][vnum]); + } + else + { + Assert(vnum == qtvars[tnv].size()); + qtvars[tnv].push_back(v); + qvars.push_back(v); + } + } + if (!vars.empty()) + { + pas = + pas.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + } + } + Trace("sygus-infer-debug") << " ...substituted to " << pas << std::endl; + + // collect free functions, ensure no quantified formulas + TNode cur = pas; + // compute free variables + visit.push_back(cur); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() == APPLY_UF) + { + Node op = cur.getOperator(); + if (std::find(free_functions.begin(), free_functions.end(), op) + == free_functions.end()) + { + free_functions.push_back(op); + } + } + else if (cur.getKind() == FORALL) + { + Trace("sygus-infer") + << "...fail: non-top-level quantifier." << std::endl; + return false; + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + processed_assertions.push_back(pas); + } + + // if no free function symbols, there is no use changing into SyGuS + if (free_functions.empty()) + { + Trace("sygus-infer") << "...fail: no free function symbols." << std::endl; + return false; + } + + // conjunction of the assertions + Node body; + if (processed_assertions.size() == 1) + { + body = processed_assertions[0]; + } + else + { + body = nm->mkNode(AND, processed_assertions); + } + + // for each free function symbol, make a bound variable of the same type + std::vector<Node> ff_vars; + for (const Node& ff : free_functions) + { + Node ffv = nm->mkBoundVar(ff.getType()); + ff_vars.push_back(ffv); + } + // substitute free functions -> variables + body = body.substitute(free_functions.begin(), + free_functions.end(), + ff_vars.begin(), + ff_vars.end()); + + // quantify the body + if (!qvars.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); + body = nm->mkNode(EXISTS, bvl, body.negate()); + } + + // sygus attribute to mark the conjecture as a sygus conjecture + Node sygusVar = nm->mkBoundVar("sygus", nm->booleanType()); + SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); + + Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars); + + body = nm->mkNode(FORALL, fbvl, body, instAttrList); + + Trace("sygus-infer") << "...return : " << body << std::endl; + + // replace all assertions except the first with true + Node truen = nm->mkConst(true); + for (unsigned i = 0, size = assertions.size(); i < size; i++) + { + if (i == 0) + { + assertions[i] = body; + } + else + { + assertions[i] = truen; + } + } + return true; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h new file mode 100644 index 000000000..a61cebcc0 --- /dev/null +++ b/src/theory/quantifiers/sygus_inference.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file sygus_inference.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_inference + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H + +#include <vector> +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** SygusInference + * + * A preprocessing utility to turn a set of (quantified) assertions into a + * single SyGuS conjecture. + */ +class SygusInference +{ + public: + SygusInference(); + ~SygusInference() {} + /** simplify assertions + * + * Either replaces assertions with the negation of an equivalent SyGuS + * conjecture and returns true, or otherwise returns false. + */ + bool simplify(std::vector<Node>& assertions); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H */ |