diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-11 11:28:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-11 11:28:01 -0700 |
commit | 6ae63e11bf6b8cfa50e29e9ace43056c75d605fc (patch) | |
tree | 78cdaa30ca6cc8408409441e880052879f0e14ea | |
parent | 9beba49c7de90529a1a0507b59b35c7f063f880c (diff) | |
parent | 82ddf4c77bf234d08feaa884d9ead245abcead81 (diff) |
Merge branch 'master' into emptyStrRewrites
21 files changed, 565 insertions, 170 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 435407fea..62a7a7ea0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -280,7 +280,7 @@ if(ENABLE_COVERAGE) # into a timeout. As a consequence, the coverage report is not generated. To # prevent this we always return with exit code 0 after the ctest command has # finished. - setup_target_for_coverage_lcov( + setup_target_for_coverage_gcovr_html( NAME coverage EXECUTABLE ctest -j${CTEST_NTHREADS} -LE "example" diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 037a1beb2..8bedd4979 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<Type>& cargs, + const std::string& cname, + const std::vector<Type>& cargs, std::shared_ptr<SygusPrintCallback> spc, int weight) { @@ -1316,7 +1316,7 @@ void DatatypeConstructorArg::toStream(std::ostream& out) const else if (d_selector.isNull()) { string typeName = d_name.substr(d_name.find('\0') + 1); - out << (typeName == "") ? "[self]" : typeName; + out << ((typeName == "") ? "[self]" : typeName); return; } else 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<Type>& cargs, + const std::string& cname, + const std::vector<Type>& cargs, std::shared_ptr<SygusPrintCallback> spc = nullptr, int weight = -1); diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cbc380f43..2e5252529 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -994,7 +994,7 @@ header = "options/quantifiers_options.h" [[option]] name = "sygusUnifCondIndNoRepeatSol" category = "regular" - long = "sygus-unif-cond-indpendent-no-repeat-sol" + long = "sygus-unif-cond-independent-no-repeat-sol" type = "bool" default = "true" help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis" @@ -1317,6 +1317,30 @@ header = "options/quantifiers_options.h" 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" long = "sygus-expr-miner-check-timeout=N" 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 @@ -296,22 +296,6 @@ header = "options/smt_options.h" 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" long = "simp-with-care" 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<SynthRrComputedAttributeId, bool> - 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<Node>& assertions = assertionsToPreprocess->ref(); + if (assertions.empty()) + { + return PreprocessingPassResult::NO_CONFLICT; + } - // compute the variables we will be sampling - std::vector<Node> 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<theory::quantifiers::CandidateRewriteDatabaseGen> crdg; std::unordered_map<TNode, bool, TNodeHashFunction> visited; std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it; std::vector<TNode> 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<Node> terms; + // all variables (free constants) appearing in the input + std::vector<Node> 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<TypeNode, std::vector<Node> > tvars; + std::vector<TypeNode> allVarTypes; + std::vector<Node> allVars; + unsigned varCounter = 0; + // standard constants for each type (e.g. true, false for Bool) + std::map<TypeNode, std::vector<Node> > 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<Node> 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<Node, Node> term_to_cterm; + std::map<Node, Node> cterm_to_term; + std::vector<Node> cterms; + // canonical terms for each type + std::map<TypeNode, std::vector<Node> > 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<Node, Node>::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<theory::quantifiers::CandidateRewriteDatabaseGen>( - 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<Type> unres; + std::vector<Datatype> datatypes; + // make unresolved types for each canonical term + std::map<Node, TypeNode> 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<Type> 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<Type> argListTmp = argList; + argList.clear(); + std::map<Type, bool> 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<Type> 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<DatatypeType> types = nm->toExprManager()->mkMutualDatatypeTypes( + datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + Trace("srs-input") << "...finished." << std::endl; + Assert(types.size() == unres.size()); + std::map<Node, DatatypeType> 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<TypeNode, TypeNode> tlGrammarTypes; + for (std::pair<const TypeNode, std::vector<Node> >& 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<Type> 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<Node> synthConj; + unsigned fCounter = 1; + theory::SygusSynthGrammarAttribute ssg; + for (std::pair<const TypeNode, TypeNode> 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..0a4859971 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1115,22 +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()) - { - options::cbqiMidpoint.set(true); - } - if (options::sygusRepairConst()) - { - if (!options::cbqi.wasSetByUser()) - { - options::cbqi.set(true); - } - } } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) @@ -1212,10 +1196,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 +1794,37 @@ 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); } + // must use Ferrante/Rackoff for real arithmetic + if (!options::cbqiMidpoint.wasSetByUser()) + { + options::cbqiMidpoint.set(true); + } + if (options::sygusRepairConst()) + { + if (!options::cbqi.wasSetByUser()) + { + options::cbqi.set(true); + } + } + // setting unif requirements + if (options::sygusUnifBooleanHeuristicDt() + && !options::sygusUnifCondIndependent()) + { + options::sygusUnifCondIndependent.set(true); + } + if (options::sygusUnifCondIndependent() && !options::sygusUnif()) + { + options::sygusUnif.set(true); + } + } + if (options::sygusInference()) + { // optimization: apply preskolemization, makes it succeed more often if (!options::preSkolemQuant.wasSetByUser()) { @@ -1850,6 +1862,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 +3210,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<SmtEngine>& 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<SmtEngine>& 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<SmtEngine>& 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.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 2e7f0cc02..06f041d93 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -198,6 +198,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, Node lem = nm->mkNode( OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); lems.push_back(lem); + addedEvalLemmas = true; Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index c32a1390c..972d07af7 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -71,6 +71,13 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf void initialize(const std::vector<Node>& es, const std::map<Node, Node>& e_to_cond, const std::map<Node, std::vector<Node>>& strategy_lemmas); + + /* + * Do not hide the zero-argument version of initialize() inherited from the + * base class + */ + using DecisionStrategy::initialize; + /** get the current set of enumerators for strategy point e * * Index 0 adds the set of return value enumerators to es, index 1 adds the @@ -88,8 +95,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf * registerEvalPtAtSize on the output channel of d_qe. */ void registerEvalPts(const std::vector<Node>& eis, Node e); - /** Retrieves active guard for enumerator */ - Node getActiveGuardForEnumerator(Node e); private: /** reference to quantifier engine */ @@ -102,9 +107,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<Node, Node> 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<DatatypeType>(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<unsigned> 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<Node>& 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<Type>& unres); - // make the builtin constants for type type that should be included in a sygus grammar - static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& 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..8e41b6b07 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -158,12 +158,14 @@ 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())); - // if it is a builtin operator, convert to total version if necessary - if (exp_sop_n.getKind() == kind::BUILTIN) + Node exp_sop_n = sygus_op; + if (exp_sop_n.isConst()) { - Kind ok = NodeManager::operatorToKind(sygus_op); + // If it is a builtin operator, convert to total version if necessary. + // First, get the kind for the operator. + Kind ok = NodeManager::operatorToKind(exp_sop_n); + Trace("sygus-grammar-normalize-debug") + << "...builtin kind is " << ok << std::endl; Kind nk = getEliminateKind(ok); if (nk != ok) { @@ -174,6 +176,12 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, } else { + // 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. + exp_sop_n = Node::fromExpr( + smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); exp_sop_n = Rewriter::rewrite(exp_sop_n); Trace("sygus-grammar-normalize-debug") << ".....operator (post-rewrite) is " << exp_sop_n << std::endl; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 26ff9188f..fb25e1348 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1778,18 +1778,21 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef Node conc = nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); conc = Rewriter::rewrite(conc); + conc = conc.negate(); bool do_infer = false; - if (conc.getKind() == EQUAL) + bool pol = conc.getKind() != NOT; + Node lit = pol ? conc : conc[0]; + if (lit.getKind() == EQUAL) { - do_infer = !areDisequal(conc[0], conc[1]); + do_infer = pol ? !areEqual(lit[0], lit[1]) + : !areDisequal(lit[0], lit[1]); } else { - do_infer = !areEqual(conc, d_false); + do_infer = !areEqual(lit, pol ? d_true : d_false); } if (do_infer) { - conc = conc.negate(); std::vector<Node> exp_c; exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 6c653bf05..236c3906c 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -740,6 +740,12 @@ private: /** initialize */ void initialize(const std::vector<Node>& vars); + /* + * Do not hide the zero-argument version of initialize() inherited from the + * base class + */ + using DecisionStrategyFmf::initialize; + private: /** * User-context-dependent node corresponding to the sum of the lengths of diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bfcd640b9..902ddf0f9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1548,6 +1548,7 @@ set(regress_1_tests regress1/strings/strings-lt-simple.smt2 regress1/strings/strip-endpt-sound.smt2 regress1/strings/substr001.smt2 + regress1/strings/timeout-no-resp.smt2 regress1/strings/type002.smt2 regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index fc080f0e0..91f33721a 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1545,6 +1545,7 @@ REG1_TESTS = \ regress1/strings/strings-lt-simple.smt2 \ regress1/strings/strip-endpt-sound.smt2 \ regress1/strings/substr001.smt2 \ + regress1/strings/timeout-no-resp.smt2 \ regress1/strings/type002.smt2 \ regress1/strings/type003.smt2 \ regress1/strings/username_checker_min.smt2 \ diff --git a/test/regress/regress1/strings/timeout-no-resp.smt2 b/test/regress/regress1/strings/timeout-no-resp.smt2 new file mode 100644 index 000000000..65608da62 --- /dev/null +++ b/test/regress/regress1/strings/timeout-no-resp.smt2 @@ -0,0 +1,7 @@ +(set-logic SLIA) +(set-info :status sat) +(set-option :strings-exp true) +(declare-const x String) +(declare-const y String) +(assert (not (= (str.replace "A" (str.replace x "A" y) x) (str.replace "A" x (str.replace x y x))))) +(check-sat)
\ No newline at end of file |