From eaebc10c50ca44644edd430ed3f555092a0fb27a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 3 Apr 2018 20:29:26 -0500 Subject: [PATCH] Option to turn arbitrary input into sygus (#1704) Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver. --- src/Makefile.am | 2 + src/options/quantifiers_options.toml | 9 + src/smt/smt_engine.cpp | 42 +++- src/theory/quantifiers/quantifiers_rewriter.h | 12 + .../sygus/ce_guided_single_inv.cpp | 17 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 69 ++++-- .../quantifiers/sygus/sygus_grammar_cons.h | 9 +- src/theory/quantifiers/sygus_inference.cpp | 216 ++++++++++++++++++ src/theory/quantifiers/sygus_inference.h | 49 ++++ test/regress/Makefile.tests | 1 + .../quantifiers/sygus-infer-nested.smt2 | 5 + 11 files changed, 409 insertions(+), 22 deletions(-) create mode 100644 src/theory/quantifiers/sygus_inference.cpp create mode 100644 src/theory/quantifiers/sygus_inference.h create mode 100644 test/regress/regress1/quantifiers/sygus-infer-nested.smt2 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 @@ -878,6 +878,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" 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& 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(preGrammarType.toType()) + .getDatatype() + .isSygus()) + { + tn = preGrammarType; }else{ // check which arguments are irrelevant std::unordered_set 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; jmkBoundVar( 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 argTypes = f.getType().getArgTypes(); + // make default variable list if none was specified by input + std::vector 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 @@ -83,12 +83,19 @@ public: * fun is for naming */ 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& 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 qvars; + std::map > qtvars; + std::vector free_functions; + + std::vector visit; + std::unordered_set visited; + + // add top-level conjuncts to eassertions + std::vector assertions_proc = assertions; + std::vector 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 processed_assertions; + for (const Node& as : eassertions) + { + // substitution for this assertion + std::vector vars; + std::vector subs; + std::map 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 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 +#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& assertions); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c3d02bbd6..4fb9065c6 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1266,6 +1266,7 @@ REG1_TESTS = \ regress1/quantifiers/smtlibe99bbe.smt2 \ regress1/quantifiers/smtlibf957ea.smt2 \ regress1/quantifiers/stream-x2014-09-18-unsat.smt2 \ + regress1/quantifiers/sygus-infer-nested.smt2 \ regress1/quantifiers/symmetric_unsat_7.smt2 \ regress1/quantifiers/z3.620661-no-fv-trigger.smt2 \ regress1/rels/addr_book_1.cvc \ diff --git a/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 new file mode 100644 index 000000000..a1e449fa3 --- /dev/null +++ b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --sygus-inference --no-check-models +(set-logic LIA) +(set-info :status sat) +(assert (forall ((x Int) (y Int)) (or (<= x (+ y 1)) (exists ((z Int)) (and (> z y) (< z x)))))) +(check-sat) -- 2.30.2