From: Andrew Reynolds Date: Thu, 11 Oct 2018 01:44:02 +0000 (-0500) Subject: Synthesize rewrite rules from inputs (#2608) X-Git-Tag: cvc5-1.0.0~4438 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d70b721f43157e01bc6166a822df79250df632a;p=cvc5.git Synthesize rewrite rules from inputs (#2608) --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 037a1beb2..66caedf8e 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -173,8 +173,8 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ } void Datatype::addSygusConstructor(Expr op, - std::string& cname, - std::vector& cargs, + const std::string& cname, + const std::vector& cargs, std::shared_ptr spc, int weight) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 3fbb7e17b..615ad0e10 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -691,8 +691,8 @@ public: * constructors. */ void addSygusConstructor(Expr op, - std::string& cname, - std::vector& cargs, + const std::string& cname, + const std::vector& cargs, std::shared_ptr spc = nullptr, int weight = -1); diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cbc380f43..c844a197d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1316,6 +1316,30 @@ header = "options/quantifiers_options.h" default = "false" help = "use satisfiability check to verify correctness of candidate rewrites" +[[option]] + name = "sygusRewSynthInput" + category = "regular" + long = "sygus-rr-synth-input" + type = "bool" + default = "false" + help = "synthesize rewrite rules based on the input formula" + +[[option]] + name = "sygusRewSynthInputNVars" + category = "regular" + long = "sygus-rr-synth-input-nvars=N" + type = "int" + default = "3" + help = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input" + +[[option]] + name = "sygusRewSynthInputUseBool" + category = "regular" + long = "sygus-rr-synth-input-use-bool" + type = "bool" + default = "false" + help = "synthesize Boolean rewrite rules based on the input formula" + [[option]] name = "sygusExprMinerCheckTimeout" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 93e892943..8af1000ba 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -295,22 +295,6 @@ header = "options/smt_options.h" default = "false" help = "use aggressive extended rewriter as a preprocessing pass" -[[option]] - name = "synthRrPrep" - category = "regular" - long = "synth-rr-prep" - type = "bool" - default = "false" - help = "synthesize and output rewrite rules during preprocessing" - -[[option]] - name = "synthRrPrepExtRew" - category = "regular" - long = "synth-rr-prep-ext-rew" - type = "bool" - default = "false" - help = "use the extended rewriter for synthRrPrep" - [[option]] name = "simplifyWithCareEnabled" category = "regular" diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 2ff525285..14dea3908 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -18,143 +18,433 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "printer/sygus_print_callback.h" #include "theory/quantifiers/candidate_rewrite_database.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/term_canonize.h" +#include "theory/quantifiers/term_util.h" using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace preprocessing { namespace passes { -// Attribute for whether we have computed rewrite rules for a given term. -// Notice that this currently must be a global attribute, since if -// we've computed rewrites for a term, we should not compute rewrites for the -// same term in a subcall to another SmtEngine (for instance, when using -// "exact" equivalence checking). -struct SynthRrComputedAttributeId -{ -}; -typedef expr::Attribute - SynthRrComputedAttribute; - SynthRewRulesPass::SynthRewRulesPass(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "synth-rr"){}; PreprocessingPassResult SynthRewRulesPass::applyInternal( AssertionPipeline* assertionsToPreprocess) { - Trace("synth-rr-pass") << "Synthesize rewrite rules from assertions..." - << std::endl; + Trace("srs-input") << "Synthesize rewrite rules from assertions..." + << std::endl; std::vector& assertions = assertionsToPreprocess->ref(); + if (assertions.empty()) + { + return PreprocessingPassResult::NO_CONFLICT; + } - // compute the variables we will be sampling - std::vector vars; - unsigned nsamples = options::sygusSamples(); - - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - - // attribute to mark processed terms - SynthRrComputedAttribute srrca; + NodeManager* nm = NodeManager::currentNM(); // initialize the candidate rewrite - std::unique_ptr crdg; std::unordered_map visited; std::unordered_map::iterator it; std::vector visit; - // two passes: the first collects the variables, the second registers the - // terms - for (unsigned r = 0; r < 2; r++) + // Get all usable terms from the input. A term is usable if it does not + // contain a quantified subterm + std::vector terms; + // all variables (free constants) appearing in the input + std::vector vars; + + // We will generate a fixed number of variables per type. These are the + // variables that appear as free variables in the rewrites we generate. + unsigned nvars = options::sygusRewSynthInputNVars(); + // must have at least one variable per type + nvars = nvars < 1 ? 1 : nvars; + std::map > tvars; + std::vector allVarTypes; + std::vector allVars; + unsigned varCounter = 0; + // standard constants for each type (e.g. true, false for Bool) + std::map > consts; + + TNode cur; + Trace("srs-input") << "Collect terms in assertions..." << std::endl; + for (const Node& a : assertions) { - visited.clear(); - visit.clear(); - TNode cur; - for (const Node& a : assertions) + Trace("srs-input-debug") << "Assertion : " << a << std::endl; + visit.push_back(a); + do { - visit.push_back(a); - do + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - // if already processed, ignore - if (cur.getAttribute(SynthRrComputedAttribute())) + Trace("srs-input-debug") << "...preprocess " << cur << std::endl; + visited[cur] = false; + Kind k = cur.getKind(); + bool isQuant = k == FORALL || k == EXISTS || k == LAMBDA || k == CHOICE; + // we recurse on this node if it is not a quantified formula + if (!isQuant) { - Trace("synth-rr-pass-debug") - << "...already processed " << cur << std::endl; + visit.push_back(cur); + for (const Node& cc : cur) + { + visit.push_back(cc); + } } - else if (it == visited.end()) + } + else if (!it->second) + { + Trace("srs-input-debug") << "...postprocess " << cur << std::endl; + // check if all of the children are valid + // this ensures we do not register terms that have e.g. quantified + // formulas as subterms + bool childrenValid = true; + for (const Node& cc : cur) { - Trace("synth-rr-pass-debug") << "...preprocess " << cur << std::endl; - visited[cur] = false; - Kind k = cur.getKind(); - bool isQuant = k == kind::FORALL || k == kind::EXISTS - || k == kind::LAMBDA || k == kind::CHOICE; - // we recurse on this node if it is not a quantified formula - if (!isQuant) + Assert(visited.find(cc) != visited.end()); + if (!visited[cc]) { - visit.push_back(cur); - for (const Node& cc : cur) - { - visit.push_back(cc); - } + childrenValid = false; } } - else if (!it->second) + if (childrenValid) { - Trace("synth-rr-pass-debug") << "...postprocess " << cur << std::endl; - // check if all of the children are valid - // this ensures we do not register terms that have e.g. quantified - // formulas as subterms - bool childrenValid = true; - for (const Node& cc : cur) + Trace("srs-input-debug") << "...children are valid" << std::endl; + Trace("srs-input-debug") << "Add term " << cur << std::endl; + if (cur.isVar()) { - Assert(visited.find(cc) != visited.end()); - if (!visited[cc]) - { - childrenValid = false; - } + vars.push_back(cur); } - if (childrenValid) + // register type information + TypeNode tn = cur.getType(); + if (tvars.find(tn) == tvars.end()) { - Trace("synth-rr-pass-debug") - << "...children are valid, check rewrites..." << std::endl; - if (r == 0) + // Only make one Boolean variable unless option is set. This ensures + // we do not compute purely Boolean rewrites by default. + unsigned useNVars = + (options::sygusRewSynthInputUseBool() || !tn.isBoolean()) + ? nvars + : 1; + for (unsigned i = 0; i < useNVars; i++) { - if (cur.isVar()) + // We must have a good name for these variables, these are + // the ones output in rewrite rules. We choose + // a,b,c,...,y,z,x1,x2,... + std::stringstream ssv; + if (varCounter < 26) { - vars.push_back(cur); + ssv << String::convertUnsignedIntToChar(varCounter + 32); } + else + { + ssv << "x" << (varCounter - 26); + } + varCounter++; + Node v = nm->mkBoundVar(ssv.str(), tn); + tvars[tn].push_back(v); + allVars.push_back(v); + allVarTypes.push_back(tn); } - else - { - Trace("synth-rr-pass-debug") << "Add term " << cur << std::endl; - // mark as processed - cur.setAttribute(srrca, true); - bool ret = crdg->addTerm(cur, *nodeManagerOptions.getOut()); - Trace("synth-rr-pass-debug") << "...return " << ret << std::endl; - // if we want only rewrites of minimal size terms, we would set - // childrenValid to false if ret is false here. - } + // also add the standard constants for this type + theory::quantifiers::CegGrammarConstructor::mkSygusConstantsForType( + tn, consts[tn]); + visit.insert(visit.end(), consts[tn].begin(), consts[tn].end()); } - visited[cur] = childrenValid; + terms.push_back(cur); } - } while (!visit.empty()); + visited[cur] = childrenValid; + } + } while (!visit.empty()); + } + Trace("srs-input") << "...finished." << std::endl; + + Trace("srs-input") << "Convert subterms to free variable form..." + << std::endl; + // Replace all free variables with bound variables. This ensures that + // we can perform term canonization on subterms. + std::vector vsubs; + for (const Node& v : vars) + { + TypeNode tnv = v.getType(); + Node vs = nm->mkBoundVar(tnv); + vsubs.push_back(vs); + } + if (!vars.empty()) + { + for (unsigned i = 0, nterms = terms.size(); i < nterms; i++) + { + terms[i] = terms[i].substitute( + vars.begin(), vars.end(), vsubs.begin(), vsubs.end()); } - if (r == 0) + } + Trace("srs-input") << "...finished." << std::endl; + + Trace("srs-input") << "Process " << terms.size() << " subterms..." + << std::endl; + // We've collected all terms in the input. We construct a sygus grammar in + // following which generates terms that correspond to abstractions of the + // terms in the input. + + // We map terms to a canonical (ordered variable) form. This ensures that + // we don't generate distinct grammar types for distinct alpha-equivalent + // terms, which would produce grammars of identical shape. + std::map term_to_cterm; + std::map cterm_to_term; + std::vector cterms; + // canonical terms for each type + std::map > t_cterms; + theory::quantifiers::TermCanonize tcanon; + for (unsigned i = 0, nterms = terms.size(); i < nterms; i++) + { + Node n = terms[i]; + Node cn = tcanon.getCanonicalTerm(n); + term_to_cterm[n] = cn; + Trace("srs-input-debug") << "Canon : " << n << " -> " << cn << std::endl; + std::map::iterator itc = cterm_to_term.find(cn); + if (itc == cterm_to_term.end()) { - Trace("synth-rr-pass-debug") - << "Initialize with " << nsamples - << " samples and variables : " << vars << std::endl; - crdg = std::unique_ptr( - new theory::quantifiers::CandidateRewriteDatabaseGen(vars, nsamples)); + cterm_to_term[cn] = n; + cterms.push_back(cn); + t_cterms[cn.getType()].push_back(cn); } } + Trace("srs-input") << "...finished." << std::endl; + // the sygus variable list + Node sygusVarList = nm->mkNode(BOUND_VAR_LIST, allVars); + Expr sygusVarListE = sygusVarList.toExpr(); + Trace("srs-input") << "Have " << cterms.size() << " canonical subterms." + << std::endl; + + Trace("srs-input") << "Construct unresolved types..." << std::endl; + // each canonical subterm corresponds to a grammar type + std::set unres; + std::vector datatypes; + // make unresolved types for each canonical term + std::map cterm_to_utype; + for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++) + { + Node ct = cterms[i]; + std::stringstream ss; + ss << "T" << i; + std::string tname = ss.str(); + TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER); + cterm_to_utype[ct] = tnu; + unres.insert(tnu.toType()); + datatypes.push_back(Datatype(tname)); + } + Trace("srs-input") << "...finished." << std::endl; + + Trace("srs-input") << "Construct datatypes..." << std::endl; + for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++) + { + Node ct = cterms[i]; + Node t = cterm_to_term[ct]; + + // add the variables for the type + TypeNode ctt = ct.getType(); + Assert(tvars.find(ctt) != tvars.end()); + std::vector argList; + for (const Node& v : tvars[ctt]) + { + std::stringstream ssc; + ssc << "C_" << i << "_" << v; + datatypes[i].addSygusConstructor(v.toExpr(), ssc.str(), argList); + } + // add the constructor for the operator if it is not a variable + if (ct.getKind() != BOUND_VARIABLE) + { + Assert(!ct.isVar()); + Node op = ct.hasOperator() ? ct.getOperator() : ct; + // iterate over the original term + for (const Node& tc : t) + { + // map its arguments back to canonical + Assert(term_to_cterm.find(tc) != term_to_cterm.end()); + Node ctc = term_to_cterm[tc]; + Assert(cterm_to_utype.find(ctc) != cterm_to_utype.end()); + // get the type + argList.push_back(cterm_to_utype[ctc].toType()); + } + // check if we should chain + bool do_chain = false; + if (argList.size() > 2) + { + Kind k = NodeManager::operatorToKind(op); + do_chain = theory::quantifiers::TermUtil::isAssoc(k) + && theory::quantifiers::TermUtil::isComm(k); + // eliminate duplicate child types + std::vector argListTmp = argList; + argList.clear(); + std::map hasArgType; + for (unsigned j = 0, size = argListTmp.size(); j < size; j++) + { + Type t = argListTmp[j]; + if (hasArgType.find(t) == hasArgType.end()) + { + hasArgType[t] = true; + argList.push_back(t); + } + } + } + if (do_chain) + { + // we make one type per child + // the operator of each constructor is a no-op + Node tbv = nm->mkBoundVar(ctt); + Expr lambdaOp = + nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, tbv), tbv).toExpr(); + std::vector argListc; + // the following construction admits any number of repeated factors, + // so for instance, t1+t2+t3, we generate the grammar: + // T_{t1+t2+t3} -> + // +( T_{t1+t2+t3}, T_{t1+t2+t3} ) | T_{t1} | T_{t2} | T_{t3} + // where we write T_t to denote "the type that abstracts term t". + // Notice this construction allows to abstract subsets of the factors + // of t1+t2+t3. This is particularly helpful for terms t1+...+tn for + // large n, where we would like to consider binary applications of +. + for (unsigned j = 0, size = argList.size(); j < size; j++) + { + argListc.clear(); + argListc.push_back(argList[j]); + std::stringstream sscs; + sscs << "C_factor_" << i << "_" << j; + // ID function is not printed and does not count towards weight + datatypes[i].addSygusConstructor( + lambdaOp, + sscs.str(), + argListc, + printer::SygusEmptyPrintCallback::getEmptyPC(), + 0); + } + // recursive apply + Type recType = cterm_to_utype[ct].toType(); + argListc.clear(); + argListc.push_back(recType); + argListc.push_back(recType); + std::stringstream ssc; + ssc << "C_" << i << "_rec_" << op; + datatypes[i].addSygusConstructor(op.toExpr(), ssc.str(), argListc); + } + else + { + std::stringstream ssc; + ssc << "C_" << i << "_" << op; + datatypes[i].addSygusConstructor(op.toExpr(), ssc.str(), argList); + } + } + datatypes[i].setSygus(ctt.toType(), sygusVarListE, false, false); + } + Trace("srs-input") << "...finished." << std::endl; + + Trace("srs-input") << "Make mutual datatype types for subterms..." + << std::endl; + std::vector types = nm->toExprManager()->mkMutualDatatypeTypes( + datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + Trace("srs-input") << "...finished." << std::endl; + Assert(types.size() == unres.size()); + std::map subtermTypes; + for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++) + { + subtermTypes[cterms[i]] = types[i]; + } + + Trace("srs-input") << "Construct the top-level types..." << std::endl; + // we now are ready to create the "top-level" types + std::map tlGrammarTypes; + for (std::pair >& tcp : t_cterms) + { + TypeNode t = tcp.first; + std::stringstream ss; + ss << "T_" << t; + Datatype dttl(ss.str()); + Node tbv = nm->mkBoundVar(t); + // the operator of each constructor is a no-op + Expr lambdaOp = + nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, tbv), tbv).toExpr(); + Trace("srs-input") << " We have " << tcp.second.size() + << " subterms of type " << t << std::endl; + for (unsigned i = 0, size = tcp.second.size(); i < size; i++) + { + Node n = tcp.second[i]; + // add constructor that encodes abstractions of this subterm + std::vector argList; + Assert(subtermTypes.find(n) != subtermTypes.end()); + argList.push_back(subtermTypes[n]); + std::stringstream ssc; + ssc << "Ctl_" << i; + // the no-op should not be printed, hence we pass an empty callback + dttl.addSygusConstructor(lambdaOp, + ssc.str(), + argList, + printer::SygusEmptyPrintCallback::getEmptyPC(), + 0); + Trace("srs-input-debug") + << "Grammar for subterm " << n << " is: " << std::endl; + Trace("srs-input-debug") << subtermTypes[n].getDatatype() << std::endl; + } + // set that this is a sygus datatype + dttl.setSygus(t.toType(), sygusVarListE, false, false); + DatatypeType tlt = nm->toExprManager()->mkDatatypeType( + dttl, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + tlGrammarTypes[t] = TypeNode::fromType(tlt); + Trace("srs-input") << "Grammar is: " << std::endl; + Trace("srs-input") << tlt.getDatatype() << std::endl; + } + Trace("srs-input") << "...finished." << std::endl; + + // sygus attribute to mark the conjecture as a sygus conjecture + Trace("srs-input") << "Make sygus conjecture..." << std::endl; + Node iaVar = nm->mkSkolem("sygus", nm->booleanType()); + // the attribute to mark the conjecture as being a sygus conjecture + theory::SygusAttribute ca; + iaVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, iaVar); + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); + // we are "synthesizing" functions for each type of subterm + std::vector synthConj; + unsigned fCounter = 1; + theory::SygusSynthGrammarAttribute ssg; + for (std::pair ttp : tlGrammarTypes) + { + Node gvar = nm->mkBoundVar("sfproxy", ttp.second); + TypeNode ft = nm->mkFunctionType(allVarTypes, ttp.first); + // likewise, it is helpful if these have good names, we choose f1, f2, ... + std::stringstream ssf; + ssf << "f" << fCounter; + fCounter++; + Node sfun = nm->mkBoundVar(ssf.str(), ft); + // this marks that the grammar used for solutions for sfun is the type of + // gvar, which is the sygus datatype type constructed above. + sfun.setAttribute(ssg, gvar); + Node fvarBvl = nm->mkNode(BOUND_VAR_LIST, sfun); + + Node body = nm->mkConst(false); + body = nm->mkNode(FORALL, fvarBvl, body, instAttrList); + synthConj.push_back(body); + } + Node trueNode = nm->mkConst(true); + Node res = + synthConj.empty() + ? trueNode + : (synthConj.size() == 1 ? synthConj[0] : nm->mkNode(AND, synthConj)); + + Trace("srs-input") << "got : " << res << std::endl; + Trace("srs-input") << "...finished." << std::endl; + + assertionsToPreprocess->replace(0, res); + for (unsigned i = 1, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, trueNode); + } - Trace("synth-rr-pass") << "...finished " << std::endl; return PreprocessingPassResult::NO_CONFLICT; } - } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index cf0b491fb..2b05bbf00 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -24,12 +24,41 @@ namespace preprocessing { namespace passes { /** - * This class computes candidate rewrite rules of the form t1 = t2, where - * t1 and t2 are subterms of assertionsToPreprocess. It prints - * "candidate-rewrite" messages on the output stream of options. + * This class rewrites the input assertions into a sygus conjecture over a + * grammar whose terms are "abstractions" of the subterms of + * assertionsToPreprocess. In detail, assume our input was + * bvadd( bvlshr( bvadd( a, 4 ), 1 ), b ) = 1 + * This class constructs this grammar: + * A -> T1 | T2 | T3 | T4 | Tv + * T1 -> bvadd( T2, Tv ) | x | y + * T2 -> bvlshr( T3, T4 ) | x | y + * T3 -> bvadd( Tv, T5 ) | x | y + * T4 -> 1 | x | y + * T5 -> 4 | x | y + * Tv -> x | y + * Notice that this grammar generates all subterms of the input where leaves + * are replaced by the variables x and/or y. The number of variable constructors + * (x and y in this example) used in this construction is configurable via + * sygus-rr-synth-input-nvars. The default for this value is 3, the + * justification is that this covers most of the interesting rewrites while + * not being too inefficient. * - * In contrast to other preprocessing passes, this pass does not modify - * the set of assertions. + * Also notice that currently, this grammar construction admits terms that + * do not necessarily match any in the input. For example, the above grammar + * admits bvlshr( x, x ), which is not matchable with a subterm of the input. + * + * Notice that Booleans are treated specially unless the option + * --sygus-rr-synth-input-bool is enabled, since we do not by default want to + * generate purely propositional rewrites. In particular, we allocate only + * one Boolean variable (to ensure that no sygus type is non-empty). + * + * It then rewrites the input into the negated sygus conjecture + * forall x : ( BV_n x BV_n ) -> BV_n. false + * where x has the sygus grammar restriction A from above. This conjecture can + * then be processed using --sygus-rr-synth in the standard way, which will + * cause candidate rewrites to be printed on the output stream. If multiple + * types are present, then we generate a conjunction of multiple synthesis + * conjectures, which we enumerate terms for in parallel. */ class SynthRewRulesPass : public PreprocessingPass { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c9aef9828..1bde3975e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1115,10 +1115,6 @@ void SmtEngine::setDefaults() { if (options::inputLanguage() == language::input::LANG_SYGUS) { is_sygus = true; - if (!options::ceGuidedInst.wasSetByUser()) - { - options::ceGuidedInst.set(true); - } // must use Ferrante/Rackoff for real arithmetic if (!options::cbqiMidpoint.wasSetByUser()) { @@ -1212,10 +1208,13 @@ void SmtEngine::setDefaults() { } // sygus inference may require datatypes - if (options::sygusInference()) + if (options::sygusInference() || options::sygusRewSynthInput()) { d_logic = d_logic.getUnlockedCopy(); + // sygus requires arithmetic, datatypes and quantifiers + d_logic.enableTheory(THEORY_ARITH); d_logic.enableTheory(THEORY_DATATYPES); + d_logic.enableTheory(THEORY_QUANTIFIERS); d_logic.lock(); // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; @@ -1807,12 +1806,15 @@ void SmtEngine::setDefaults() { //apply counterexample guided instantiation options // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst - if (options::sygusInference()) + if (is_sygus) { if (!options::ceGuidedInst.wasSetByUser()) { options::ceGuidedInst.set(true); } + } + if (options::sygusInference()) + { // optimization: apply preskolemization, makes it succeed more often if (!options::preSkolemQuant.wasSetByUser()) { @@ -1850,6 +1852,19 @@ void SmtEngine::setDefaults() { options::sygusRewSynth.set(true); options::sygusRewVerify.set(true); } + if (options::sygusRewSynthInput()) + { + // If we are using synthesis rewrite rules from input, we use + // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for + // details on this technique. + options::sygusRewSynth.set(true); + // we should not use the extended rewriter, since we are interested + // in rewrites that are not in the main rewriter + if (!options::sygusExtRew.wasSetByUser()) + { + options::sygusExtRew.set(false); + } + } if (options::sygusRewSynth() || options::sygusRewVerify()) { // rewrite rule synthesis implies that sygus stream must be true @@ -3185,7 +3200,7 @@ void SmtEnginePrivate::processAssertions() { d_passes["pseudo-boolean-processor"]->apply(&d_assertions); } - if (options::synthRrPrep()) + if (options::sygusRewSynthInput()) { // do candidate rewrite rule synthesis d_passes["synth-rr"]->apply(&d_assertions); diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index fe6764297..4469f0fe9 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -244,14 +244,21 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; return ret; } - Kind ok = getOperatorKindForSygusBuiltin(op); - if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND) + Kind ok = NodeManager::operatorToKind(op); + if (ok != UNDEFINED_KIND) + { + ret = NodeManager::currentNM()->mkNode(ok, schildren); + Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; + return ret; + } + Kind tok = getOperatorKindForSygusBuiltin(op); + if (schildren.size() == 1 && tok == kind::UNDEFINED_KIND) { ret = schildren[0]; } else { - ret = NodeManager::currentNM()->mkNode(ok, schildren); + ret = NodeManager::currentNM()->mkNode(tok, schildren); } Trace("dt-sygus-util") << "...return " << ret << std::endl; return ret; diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 908bef92c..2d2e9ce30 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -276,11 +276,7 @@ CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) { - ExtendedRewriter* er = nullptr; - if (options::synthRrPrepExtRew()) - { - er = &d_ext_rewrite; - } + ExtendedRewriter* er = &d_ext_rewrite; Node nr; if (er == nullptr) { diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 0e8542826..67aa8688c 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -77,7 +77,8 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, // check is ground. Node squery = convertToSkolem(query); NodeManager* nm = NodeManager::currentNM(); - if (options::sygusExprMinerCheckTimeout.wasSetByUser()) + if (options::sygusExprMinerCheckTimeout.wasSetByUser() + || options::sygusRewSynthInput()) { // To support a separate timeout for the subsolver, we need to create // a separate ExprManager with its own options. This requires that @@ -89,6 +90,7 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, checker.reset(new SmtEngine(&em)); checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); + checker->setOption("sygus-rr-synth-input", false); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); } @@ -96,8 +98,9 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, { std::stringstream msg; msg << "Unable to export " << squery - << " but exporting expressions is required for " - "--sygus-rr-synth-check-timeout."; + << " but exporting expressions is " + "required for an expression " + "miner check."; throw OptionException(msg.str()); } needExport = true; diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index c32a1390c..448150d06 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -88,8 +88,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf * registerEvalPtAtSize on the output channel of d_qe. */ void registerEvalPts(const std::vector& eis, Node e); - /** Retrieves active guard for enumerator */ - Node getActiveGuardForEnumerator(Node e); private: /** reference to quantifier engine */ @@ -102,9 +100,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf bool d_initialized; /** null node */ Node d_null; - /** map from condition enumerators to active guards (in case they are - * enumerated indepedently of the return values) */ - std::map d_enum_to_active_guard; /** information per initialized type */ class StrategyPtInfo { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index eadbf766a..47c701cf6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -126,21 +126,18 @@ Node CegGrammarConstructor::process(Node q, 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 (preGrammarType.isDatatype() - && static_cast(preGrammarType.toType()) - .getDatatype() - .isSygus()) + Node sfvl; + if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus()) { + sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList()); tn = preGrammarType; }else{ + sfvl = getSygusVarList(sf); // check which arguments are irrelevant std::unordered_set arg_irrelevant; d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); @@ -156,6 +153,9 @@ Node CegGrammarConstructor::process(Node q, tn = mkSygusDefaultType( preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv); } + // sfvl may be null for constant synthesis functions + Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " + << sfvl << std::endl; // normalize type SygusGrammarNorm sygus_norm(d_qe); @@ -367,6 +367,10 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, ops.push_back(nm->mkConst(true)); ops.push_back(nm->mkConst(false)); } + else if (type.isString()) + { + ops.push_back(nm->mkConst(String(""))); + } // TODO #1178 : add other missing types } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 022031bef..0c5b67656 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -108,6 +108,12 @@ public: * functions-to-synthesize of sygus conjecture q. */ static bool hasSyntaxRestrictions(Node q); + /** + * Make the builtin constants for type "type" that should be included in a + * sygus grammar, add them to vector ops. + */ + static void mkSygusConstantsForType(TypeNode type, std::vector& ops); + private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; @@ -124,8 +130,6 @@ public: //---------------- grammar construction // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set& unres); - // make the builtin constants for type type that should be included in a sygus grammar - static void mkSygusConstantsForType(TypeNode type, std::vector& ops); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); /** helper function for function mkSygusDefaultType diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index b014a30c6..b5dea4c38 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -158,12 +158,21 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, Node sygus_op = Node::fromExpr(cons.getSygusOp()); Trace("sygus-grammar-normalize-debug") << ".....operator is " << sygus_op << std::endl; - Node exp_sop_n = Node::fromExpr( - smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); + Node exp_sop_n = sygus_op; + // Only expand definitions if the operator is not constant, since calling + // expandDefinitions on them should be a no-op. This check ensures we don't + // try to expand e.g. bitvector extract operators, whose type is undefined, + // and thus should not be passed to expandDefinitions. + if (!sygus_op.isConst()) + { + exp_sop_n = Node::fromExpr( + smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); + } + // get the kind for the operator. + Kind ok = NodeManager::operatorToKind(exp_sop_n); // if it is a builtin operator, convert to total version if necessary - if (exp_sop_n.getKind() == kind::BUILTIN) + if (ok != UNDEFINED_KIND) { - Kind ok = NodeManager::operatorToKind(sygus_op); Kind nk = getEliminateKind(ok); if (nk != ok) {