diff options
| -rw-r--r-- | src/theory/quantifiers/ce_guided_conjecture.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_conjecture.h | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.h | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_grammar_cons.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_process_conj.cpp | 751 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_process_conj.h | 293 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/inv-unused.sy | 13 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/process-10-vars-2fun.sy | 28 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/process-10-vars.sy | 24 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/process-arg-invariance.sy | 18 |
12 files changed, 1115 insertions, 59 deletions
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 7110f1037..c89b6b2b4 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -61,8 +61,8 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; d_quant = q; - // simplify the quantified formula based on the process utility - d_simp_quant = d_ceg_proc->simplify(d_quant); + // pre-simplify the quantified formula based on the process utility + d_simp_quant = d_ceg_proc->preSimplify(d_quant); std::map< Node, Node > templates; std::map< Node, Node > templates_arg; @@ -82,6 +82,11 @@ void CegConjecture::assign( Node q ) { } } + // post-simplify the quantified formula based on the process utility + d_simp_quant = d_ceg_proc->postSimplify(d_simp_quant); + + // finished simplifying the quantified formula at this point + // convert to deep embedding and finalize single invocation here d_embed_quant = d_ceg_gc->process(d_simp_quant, templates, templates_arg); Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl; diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index 90627699f..0f000bba5 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -114,6 +114,8 @@ public: /** get program by examples utility */ CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); } + /** get utility for static preprocessing and analysis of conjectures */ + CegConjectureProcess* getProcess() { return d_ceg_proc.get(); } /** get the symmetry breaking predicate for type */ Node getSymmetryBreakingPredicate( Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index ca0190dc0..d69c94944 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -26,8 +26,6 @@ namespace theory { namespace quantifiers { class CegConjecture; -class CegConjecturePbe; -class CegEntailmentInfer; /** CegConjecturePbe * @@ -60,15 +58,15 @@ class CegEntailmentInfer; * Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...). * * Notice that each enumerator is associated with a single -* function-to-synthesize, -* but a function-to-sythesize may be mapped to multiple enumerators. -* Some public functions of this class expect an enumerator as input, which we -* map to a function-to-synthesize via TermDatabaseSygus::getSynthFunFor(e). +* function-to-synthesize, but a function-to-sythesize may be mapped to multiple +* enumerators. Some public functions of this class expect an enumerator as +* input, which we map to a function-to-synthesize via +* TermDatabaseSygus::getSynthFunFor(e). * * An enumerator is initially "active" but may become inactive if the enumeration * exhausts all possible values in the datatype corresponding to syntactic -* restrictions -* for it. The search may continue unless all enumerators become inactive. +* restrictions for it. The search may continue unless all enumerators become +* inactive. * * (4) During search, the extension of quantifier-free datatypes procedure for * SyGuS datatypes may ask this class whether current candidates can be @@ -95,9 +93,7 @@ class CegEntailmentInfer; * solution based on the high-level strategy (stored in d_c_info). * * This class is not designed to work in incremental mode, since there is no way -* to -* specify incremental problems in SyguS. -* +* to specify incremental problems in SyguS. */ class CegConjecturePbe { public: @@ -163,8 +159,8 @@ class CegConjecturePbe { * tn is a sygus datatype that encodes a subsignature of the integers. * * This returns either: - * - A SyGuS term whose analog is equivalent to bvr up to examples, in the - * above example, + * - A SyGuS term whose analog is equivalent to bvr up to examples + * In the above example, * it may return a term t of the form Plus( One(), x() ), such that this * function was previously called with t as input. * - e, indicating that no previous terms are equivalent to e up to examples. @@ -191,10 +187,7 @@ class CegConjecturePbe { /** true and false nodes */ Node d_true; Node d_false; - /** parent conjecture - * This is the data structure that contains global information about the - * conjecture. - */ + /** A reference to the conjecture that owns this class. */ CegConjecture* d_parent; /** is this a PBE conjecture for any function? */ bool d_is_pbe; diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index f6b2ab07a..68926eb34 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -19,6 +19,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus_process_conj.h" #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -101,7 +102,7 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, }else{ // check which arguments are irrelevant std::unordered_set<unsigned> arg_irrelevant; - // TODO (#1210) : get arg irrelevant based on conjecture-specific analysis + d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant); std::unordered_set<Node, NodeHashFunction> term_irrelevant; // convert to term for (std::unordered_set<unsigned>::iterator ita = arg_irrelevant.begin(); diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus_process_conj.cpp index 600c09a58..06ce99007 100644 --- a/src/theory/quantifiers/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus_process_conj.cpp @@ -27,11 +27,546 @@ namespace CVC4 { namespace theory { namespace quantifiers { +void CegConjectureProcessFun::init(Node f) +{ + d_synth_fun = f; + Assert(f.getType().isFunction()); + + // initialize the arguments + std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> + type_to_init_deq_id; + std::vector<Type> argTypes = + static_cast<FunctionType>(f.getType().toType()).getArgTypes(); + for (unsigned j = 0; j < argTypes.size(); j++) + { + TypeNode atn = TypeNode::fromType(argTypes[j]); + std::stringstream ss; + ss << "a" << j; + Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn); + d_arg_vars.push_back(k); + d_arg_var_num[k] = j; + d_arg_props.push_back(CegConjectureProcessArg()); + } +} + +bool CegConjectureProcessFun::checkMatch( + Node cn, Node n, std::unordered_map<unsigned, Node>& n_arg_map) +{ + std::vector<Node> vars; + std::vector<Node> subs; + for (std::unordered_map<unsigned, Node>::iterator it = n_arg_map.begin(); + it != n_arg_map.end(); + ++it) + { + Assert(it->first < d_arg_vars.size()); + Assert( + it->second.getType().isComparableTo(d_arg_vars[it->first].getType())); + vars.push_back(d_arg_vars[it->first]); + subs.push_back(it->second); + } + Node cn_subs = + cn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + cn_subs = Rewriter::rewrite(cn_subs); + Assert(Rewriter::rewrite(n) == n); + return cn_subs == n; +} + +bool CegConjectureProcessFun::isArgVar(Node n, unsigned& arg_index) +{ + if (n.isVar()) + { + std::unordered_map<Node, unsigned, NodeHashFunction>::iterator ita = + d_arg_var_num.find(n); + if (ita != d_arg_var_num.end()) + { + arg_index = ita->second; + return true; + } + } + return false; +} + +Node CegConjectureProcessFun::inferDefinition( + Node n, + std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars) +{ + std::unordered_map<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::stack<TNode> visit; + TNode cur; + visit.push(n); + do + { + cur = visit.top(); + visit.pop(); + it = visited.find(cur); + if (it == visited.end()) + { + // if it is ground, we can use it + if (free_vars[cur].empty()) + { + visited[cur] = cur; + } + else + { + // if it is term used by another argument, use it + std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt = + term_to_arg_carry.find(cur); + if (itt != term_to_arg_carry.end()) + { + visited[cur] = d_arg_vars[itt->second]; + } + else if (cur.getNumChildren() > 0) + { + // try constructing children + visited[cur] = Node::null(); + visit.push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.push(cur[i]); + } + } + else + { + return Node::null(); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + it = visited.find(cur[i]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur[i] != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +unsigned CegConjectureProcessFun::assignRelevantDef(Node def, + std::vector<unsigned>& args) +{ + unsigned id = 0; + if (def.isNull()) + { + // prefer one that already has a definition, if one exists + for (unsigned j = 0; j < args.size(); j++) + { + unsigned i = args[j]; + if (!d_arg_props[i].d_template.isNull()) + { + id = j; + break; + } + } + } + unsigned rid = args[id]; + // for merging previously equivalent definitions + std::unordered_map<Node, unsigned, NodeHashFunction> prev_defs; + for (unsigned j = 0; j < args.size(); j++) + { + unsigned i = args[j]; + Trace("sygus-process-arg-deps") << " ...processed arg #" << i; + if (!d_arg_props[i].d_template.isNull()) + { + if (d_arg_props[i].d_template == def) + { + // definition was consistent + } + else + { + Node t = d_arg_props[i].d_template; + std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt = + prev_defs.find(t); + if (itt != prev_defs.end()) + { + // merge previously equivalent definitions + d_arg_props[i].d_template = d_arg_vars[itt->second]; + Trace("sygus-process-arg-deps") + << " (merged equivalent def from argument "; + Trace("sygus-process-arg-deps") << itt->second << ")." << std::endl; + } + else + { + // store this as previous + prev_defs[t] = i; + // now must be relevant + d_arg_props[i].d_relevant = true; + Trace("sygus-process-arg-deps") + << " (marked relevant, overwrite definition)." << std::endl; + } + } + } + else + { + if (def.isNull()) + { + if (i != rid) + { + // marked as relevant, but template can be set equal to master + d_arg_props[i].d_template = d_arg_vars[rid]; + Trace("sygus-process-arg-deps") << " (new definition, map to master " + << d_arg_vars[rid] << ")." + << std::endl; + } + else + { + d_arg_props[i].d_relevant = true; + Trace("sygus-process-arg-deps") << " (marked relevant)." << std::endl; + } + } + else + { + // has new definition + d_arg_props[i].d_template = def; + Trace("sygus-process-arg-deps") << " (new definition " << def << ")." + << std::endl; + } + } + } + return rid; +} + +void CegConjectureProcessFun::processTerms( + std::vector<Node>& ns, + std::vector<Node>& ks, + Node nf, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars) +{ + Assert(ns.size() == ks.size()); + Trace("sygus-process-arg-deps") << "Process " << ns.size() + << " applications of " << d_synth_fun << "..." + << std::endl; + + // get the relevant variables + // relevant variables are those that appear in the body of the conjunction + std::unordered_set<Node, NodeHashFunction> rlv_vars; + Assert(free_vars.find(nf) != free_vars.end()); + rlv_vars = free_vars[nf]; + + // get the single occurrence variables + // single occurrence variables are those that appear in only one position, + // as an argument to the function-to-synthesize. + std::unordered_map<Node, bool, NodeHashFunction> single_occ_variables; + for (unsigned index = 0; index < ns.size(); index++) + { + Node n = ns[index]; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + Node nn = n[i]; + if (nn.isVar()) + { + std::unordered_map<Node, bool, NodeHashFunction>::iterator its = + single_occ_variables.find(nn); + if (its == single_occ_variables.end()) + { + // only irrelevant variables + single_occ_variables[nn] = rlv_vars.find(nn) == rlv_vars.end(); + } + else + { + single_occ_variables[nn] = false; + } + } + else + { + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>::iterator itf = free_vars.find(nn); + Assert(itf != free_vars.end()); + for (std::unordered_set<Node, NodeHashFunction>::iterator itfv = + itf->second.begin(); + itfv != itf->second.end(); + ++itfv) + { + single_occ_variables[*itfv] = false; + } + } + } + } + + // update constant argument information + for (unsigned index = 0; index < ns.size(); index++) + { + Node n = ns[index]; + Trace("sygus-process-arg-deps") + << " Analyze argument information for application #" << index << ": " + << n << std::endl; + + // in the following, we say an argument a "carries" a term t if + // the function to synthesize would use argument a to construct + // the term t in its definition. + + // map that assumes all arguments carry their respective term + std::unordered_map<unsigned, Node> n_arg_map; + // terms to the argument that is carrying it. + // the arguments in the range of this map must be marked as relevant. + std::unordered_map<Node, unsigned, NodeHashFunction> term_to_arg_carry; + // map of terms to (unprocessed) arguments where it occurs + std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction> + term_to_args; + + // initialize + for (unsigned a = 0; a < n.getNumChildren(); a++) + { + n_arg_map[a] = n[a]; + } + + for (unsigned a = 0; a < n.getNumChildren(); a++) + { + bool processed = false; + if (d_arg_props[a].d_relevant) + { + // we can assume all relevant arguments carry their terms + processed = true; + Trace("sygus-process-arg-deps") << " ...processed arg #" << a + << " (already relevant)." << std::endl; + if (term_to_arg_carry.find(n[a]) == term_to_arg_carry.end()) + { + Trace("sygus-process-arg-deps") << " carry " << n[a] + << " by argument #" << a << std::endl; + term_to_arg_carry[n[a]] = a; + } + } + else + { + // first, check if single occurrence variable + // check if an irrelevant variable + if (n[a].isVar() && synth_fv.find(n[a]) != synth_fv.end()) + { + Assert(single_occ_variables.find(n[a]) != single_occ_variables.end()); + // may be able to make this more precise? + // check if a single-occurrence variable + if (single_occ_variables[n[a]]) + { + // if we do not already have a template definition, or the + // template is a single occurrence variable + if (d_arg_props[a].d_template.isNull() + || d_arg_props[a].d_var_single_occ) + { + processed = true; + Trace("sygus-process-arg-deps") << " ...processed arg #" << a; + Trace("sygus-process-arg-deps") + << " (single occurrence variable "; + Trace("sygus-process-arg-deps") << n[a] << ")." << std::endl; + d_arg_props[a].d_var_single_occ = true; + d_arg_props[a].d_template = n[a]; + } + } + } + if (!processed && !d_arg_props[a].d_template.isNull() + && !d_arg_props[a].d_var_single_occ) + { + // argument already has a definition, see if it is maintained + if (checkMatch(d_arg_props[a].d_template, n[a], n_arg_map)) + { + processed = true; + Trace("sygus-process-arg-deps") << " ...processed arg #" << a; + Trace("sygus-process-arg-deps") << " (consistent definition " + << n[a]; + Trace("sygus-process-arg-deps") + << " with " << d_arg_props[a].d_template << ")." << std::endl; + } + } + } + if (!processed) + { + // otherwise, add it to the list of arguments for this term + term_to_args[n[a]].push_back(a); + } + } + + Trace("sygus-process-arg-deps") << " Look at argument terms..." + << std::endl; + + // list of all arguments + std::vector<Node> arg_list; + // now look at the terms for unprocessed arguments + for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: + iterator it = term_to_args.begin(); + it != term_to_args.end(); + ++it) + { + Node nn = it->first; + arg_list.push_back(nn); + if (Trace.isOn("sygus-process-arg-deps")) + { + Trace("sygus-process-arg-deps") << " argument " << nn; + Trace("sygus-process-arg-deps") << " (" << it->second.size() + << " positions)"; + // check the status of this term + if (nn.isVar() && synth_fv.find(nn) != synth_fv.end()) + { + // is it relevant? + if (rlv_vars.find(nn) != rlv_vars.end()) + { + Trace("sygus-process-arg-deps") << " is a relevant variable." + << std::endl; + } + else + { + Trace("sygus-process-arg-deps") << " is an irrelevant variable." + << std::endl; + } + } + else + { + // this can be more precise + Trace("sygus-process-arg-deps") << " is a relevant term." + << std::endl; + } + } + } + + unsigned arg_list_counter = 0; + // sort arg_list by term size? + + while (arg_list_counter < arg_list.size()) + { + Node infer_def_t; + do + { + infer_def_t = Node::null(); + // see if we can infer a definition + for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: + iterator it = term_to_args.begin(); + it != term_to_args.end(); + ++it) + { + Node def = inferDefinition(it->first, term_to_arg_carry, free_vars); + if (!def.isNull()) + { + Trace("sygus-process-arg-deps") << " *** Inferred definition " + << def << " for " << it->first + << std::endl; + // assign to each argument + assignRelevantDef(def, it->second); + // term_to_arg_carry[it->first] = rid; + infer_def_t = it->first; + break; + } + } + if (!infer_def_t.isNull()) + { + term_to_args.erase(infer_def_t); + } + } while (!infer_def_t.isNull()); + + // decide to make an argument relevant + bool success = false; + while (arg_list_counter < arg_list.size() && !success) + { + Node curr = arg_list[arg_list_counter]; + std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>:: + iterator it = term_to_args.find(curr); + if (it != term_to_args.end()) + { + Trace("sygus-process-arg-deps") << " *** Decide relevant " << curr + << std::endl; + // assign relevant to each + Node null_def; + unsigned rid = assignRelevantDef(null_def, it->second); + term_to_arg_carry[curr] = rid; + Trace("sygus-process-arg-deps") + << " carry " << curr << " by argument #" << rid << std::endl; + term_to_args.erase(curr); + success = true; + } + arg_list_counter++; + } + } + } +} + +bool CegConjectureProcessFun::isArgRelevant(unsigned i) +{ + return d_arg_props[i].d_relevant; +} + +void CegConjectureProcessFun::getIrrelevantArgs( + std::unordered_set<unsigned>& args) +{ + for (unsigned i = 0; i < d_arg_vars.size(); i++) + { + if (!d_arg_props[i].d_relevant) + { + args.insert(i); + } + } +} + CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {} CegConjectureProcess::~CegConjectureProcess() {} -Node CegConjectureProcess::simplify(Node q) +Node CegConjectureProcess::preSimplify(Node q) +{ + Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl; + return q; +} + +Node CegConjectureProcess::postSimplify(Node q) { - Trace("sygus-process") << "Simplify conjecture : " << q << std::endl; + Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl; + Assert(q.getKind() == FORALL); + + // initialize the information about each function to synthesize + for (unsigned i = 0; i < q[0].getNumChildren(); i++) + { + Node f = q[0][i]; + if (f.getType().isFunction()) + { + d_sf_info[f].init(f); + } + } + + // get the base on the conjecture + Node base = q[1]; + std::unordered_set<Node, NodeHashFunction> synth_fv; + if (base.getKind() == NOT && base[0].getKind() == FORALL) + { + for (unsigned j = 0; j < base[0][0].getNumChildren(); j++) + { + synth_fv.insert(base[0][0][j]); + } + base = base[0][1]; + } + std::vector<Node> conjuncts; + getComponentVector(AND, base, conjuncts); + + // process the conjunctions + for (std::map<Node, CegConjectureProcessFun>::iterator it = d_sf_info.begin(); + it != d_sf_info.end(); + ++it) + { + Node f = it->first; + for (unsigned i = 0; i < conjuncts.size(); i++) + { + processConjunct(conjuncts[i], f, synth_fv); + } + } return q; } @@ -47,44 +582,193 @@ void CegConjectureProcess::initialize(Node n, std::vector<Node>& candidates) Trace("sygus-process") << " " << candidates[i] << std::endl; } } - Node base; - if (n.getKind() == NOT && n[0].getKind() == FORALL) +} + +bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) +{ + std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f); + if (its != d_sf_info.end()) { - base = n[0][1]; + return its->second.isArgRelevant(i); } - else + Assert(false); + return true; +} + +bool CegConjectureProcess::getIrrelevantArgs(Node f, + std::unordered_set<unsigned>& args) +{ + std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f); + if (its != d_sf_info.end()) { - base = n; + its->second.getIrrelevantArgs(args); + return true; } + return false; +} + +void CegConjectureProcess::processConjunct( + Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv) +{ + Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl; + Trace("sygus-process-arg-deps") << " " << n << " for synth fun " << f + << "..." << std::endl; - std::vector<Node> conj; - if (base.getKind() == AND) + // first, flatten the conjunct + // make a copy of free variables since we may add new ones + std::unordered_set<Node, NodeHashFunction> synth_fv_n = synth_fv; + std::unordered_map<Node, Node, NodeHashFunction> defs; + Node nf = flatten(n, f, synth_fv_n, defs); + + Trace("sygus-process-arg-deps") << "Flattened to: " << std::endl; + Trace("sygus-process-arg-deps") << " " << nf << std::endl; + + // get free variables in nf + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction> + free_vars; + getFreeVariables(nf, synth_fv_n, free_vars); + // get free variables in each application + std::vector<Node> ns; + std::vector<Node> ks; + for (std::unordered_map<Node, Node, NodeHashFunction>::iterator it = + defs.begin(); + it != defs.end(); + ++it) { - for (unsigned i = 0; i < base.getNumChildren(); i++) - { - conj.push_back(base[i]); - } + getFreeVariables(it->second, synth_fv_n, free_vars); + ns.push_back(it->second); + ks.push_back(it->first); } - else + + // process the applications of synthesis functions + if (!ns.empty()) { - conj.push_back(base); + std::map<Node, CegConjectureProcessFun>::iterator its = d_sf_info.find(f); + if (its != d_sf_info.end()) + { + its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars); + } } +} - // initialize the information for synth funs - for (unsigned i = 0; i < candidates.size(); i++) +Node CegConjectureProcess::CegConjectureProcess::flatten( + Node n, + Node f, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, Node, NodeHashFunction>& defs) +{ + std::unordered_map<Node, Node, NodeHashFunction> visited; + std::unordered_map<Node, Node, NodeHashFunction>::iterator it; + std::stack<Node> visit; + Node cur; + visit.push(n); + do { - Node e = candidates[i]; - // d_sf_info[e].d_arg_independent - } + cur = visit.top(); + visit.pop(); + it = visited.find(cur); - // process the conjunctions - for (unsigned i = 0; i < conj.size(); i++) + if (it == visited.end()) + { + visited[cur] = Node::null(); + visit.push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.push(cur[i]); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + it = visited.find(cur[i]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur[i] != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); + } + // is it the function to synthesize? + if (cur.getKind() == APPLY_UF && cur.getOperator() == f) + { + // if so, flatten + Node k = NodeManager::currentNM()->mkBoundVar("vf", cur.getType()); + defs[k] = ret; + ret = k; + synth_fv.insert(k); + } + // post-rewrite + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +void CegConjectureProcess::getFreeVariables( + Node n, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars) +{ + // first must compute free variables in each subterm of n, + // as well as contains_synth_fun + std::unordered_map<Node, bool, NodeHashFunction> visited; + std::unordered_map<Node, bool, NodeHashFunction>::iterator it; + std::stack<Node> visit; + Node cur; + visit.push(n); + do { - processConjunct(conj[i]); - } + cur = visit.top(); + visit.pop(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited[cur] = false; + visit.push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.push(cur[i]); + } + } + else if (!it->second) + { + free_vars[cur].clear(); + if (synth_fv.find(cur) != synth_fv.end()) + { + // it is a free variable + free_vars[cur].insert(cur); + } + else + { + // otherwise, carry the free variables from the children + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + free_vars[cur].insert(free_vars[cur[i]].begin(), + free_vars[cur[i]].end()); + } + } + visited[cur] = true; + } + } while (!visit.empty()); } -void CegConjectureProcess::processConjunct(Node c) {} Node CegConjectureProcess::getSymmetryBreakingPredicate( Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth) { @@ -92,6 +776,23 @@ Node CegConjectureProcess::getSymmetryBreakingPredicate( } void CegConjectureProcess::debugPrint(const char* c) {} +void CegConjectureProcess::getComponentVector(Kind k, + Node n, + std::vector<Node>& args) +{ + if (n.getKind() == k) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + args.push_back(n[i]); + } + } + else + { + args.push_back(n); + } +} + } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus_process_conj.h index 4637ae551..f5966c55f 100644 --- a/src/theory/quantifiers/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus_process_conj.h @@ -15,26 +15,242 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PPROCESS_CONJ_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESSS_CONJ_H +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H + +#include <map> +#include <unordered_map> +#include <unordered_set> +#include <vector> #include "expr/node.h" +#include "expr/type_node.h" #include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { +/** This file contains techniques that compute + * argument relevancy for synthesis functions + * + * Let F be a synthesis conjecture of the form: + * exists f. forall X. P( f, X ) + * + * The classes below compute whether certain arguments of + * the function-to-synthesize f are irrelevant. + * Assume that f is a binary function, where possible solutions + * to the above conjecture are of the form: + * f -> (lambda (xy) t[x,y]) + * We say e.g. that the 2nd argument of f is irrelevant if we + * can determine: + * F has a solution + * if and only if + * F has a solution of the form f -> (lambda (xy) t[x] ) + * We conclude that arguments are irrelevant using the following + * techniques. + * + * + * (1) Argument invariance: + * + * Let s[z] be a term whose free variables are contained in { z }. + * If all occurrences of f-applications in F are of the form: + * f(t, s[t]) + * then: + * f = (lambda (xy) r[x,y]) + * is a solution to F only if: + * f = (lambda (xy) r[x,s[x]]) + * is as well. + * Hence the second argument of f is not relevant. + * + * + * (2) Variable irrelevance: + * + * If F is equivalent to: + * exists f. forall w z u1...un. C1 ^...^Cm, + * where for i=1...m, Ci is of the form: + * ( w1 = f(tm1[z], u1) ^ + * ... ^ + * wn = f(tmn[z], un) ) => Pm(w1...wn, z) + * then the second argument of f is irrelevant. + * We call u1...un single occurrence variables + * (in Ci). + * + * + * TODO (#1210) others, generalize (2)? + * + */ + +/** This structure stores information regarding + * an argument of a function to synthesize. + * + * It is used to store whether the argument + * position in the function to synthesize is + * relevant. + */ +class CegConjectureProcessArg +{ + public: + CegConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} + /** template definition + * This is the term s[z] described + * under "Argument Invariance" above. + */ + Node d_template; + /** single occurrence + * Whether we are trying to show this argument + * is irrelevant by "Variable irrelevance" + * described above. + */ + bool d_var_single_occ; + /** whether this argument is relevant + * An argument is marked as relevant if: + * (A) it is explicitly marked as relevant + * due to a function application containing + * a relevant term at this argument position, or + * (B) if it is given conflicting template definitions. + */ + bool d_relevant; +}; + /** This structure stores information regarding conjecture-specific -* analysis of a function to synthesize. +* analysis of a single function to synthesize within +* a conjecture to synthesize. +* +* It maintains information about each of the function to +* synthesize's arguments. */ -struct CegSynthFunProcessInfo +struct CegConjectureProcessFun { public: - CegSynthFunProcessInfo() {} - ~CegSynthFunProcessInfo() {} - /** the set of arguments that this synth-fun is independent of */ - std::map<unsigned, bool> d_arg_independent; + CegConjectureProcessFun() {} + ~CegConjectureProcessFun() {} + /** initialize this class for function f */ + void init(Node f); + /** process terms + * + * This is called once per conjunction in + * the synthesis conjecture. + * + * ns are the f-applications to process, + * ks are the variables we introduced to flatten them, + * nf is the flattened form of our conjecture to process, + * free_vars maps all subterms of n and nf to the set + * of variables (in set synth_fv) they contain. + * + * This updates information regarding which arguments + * of the function-to-synthesize are relevant. + */ + void processTerms( + std::vector<Node>& ns, + std::vector<Node>& ks, + Node nf, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars); + /** is the i^th argument of the function-to-synthesize of this class relevant? + */ + bool isArgRelevant(unsigned i); + /** get irrelevant arguments for the function-to-synthesize of this class */ + void getIrrelevantArgs(std::unordered_set<unsigned>& args); + + private: + /** the synth fun associated with this */ + Node d_synth_fun; + /** properties of each argument */ + std::vector<CegConjectureProcessArg> d_arg_props; + /** variables for each argument type of f + * + * These are used to express templates for argument + * invariance, in the data member + * CegConjectureProcessArg::d_template. + */ + std::vector<Node> d_arg_vars; + /** map from d_arg_vars to the argument # + * they represent. + */ + std::unordered_map<Node, unsigned, NodeHashFunction> d_arg_var_num; + /** check match + * This function returns true iff we can infer: + * cn * { x -> n_arg_map[d_arg_var_num[x]] | x in d_arg_vars } = n + * In other words, cn and n are equivalent + * via the substitution mapping argument variables to terms + * specified by n_arg_map. The rewriter is used for inferring + * this equivalence. + * + * For example, if n_arg_map contains { 1 -> t, 2 -> s }, then + * checkMatch( x1+x2, t+s, n_arg_map ) returns true, + * checkMatch( x1+1, t+1, n_arg_map ) returns true, + * checkMatch( 0, 0, n_arg_map ) returns true, + * checkMatch( x1+1, s, n_arg_map ) returns false. + */ + bool checkMatch(Node cn, + Node n, + std::unordered_map<unsigned, Node>& n_arg_map); + /** infer definition + * + * In the following, we say a term is a "template + * definition" if its free variables are a subset of d_arg_vars. + * + * If this function returns a non-null node ret, then + * checkMatch( ret, n, term_to_arg_carry^-1 ) returns true. + * and ret is a template definition. + * + * The free variables for all subterms of n are stored in + * free_vars. The map term_to_arg_carry is injective. + * + * For example, if term_to_arg_carry contains { t -> 1, s -> 2 } and + * free_vars is { t -> {y}, r -> {y}, s -> {}, q -> {}, ... -> {} }, then + * inferDefinition( 0, term_to_arg_carry, free_vars ) + * returns 0 + * inferDefinition( t, term_to_arg_carry, free_vars ) + * returns x1 + * inferDefinition( t+s+q, term_to_arg_carry, free_vars ) + * returns x1+x2+q + * inferDefinition( t+r, term_to_arg_carry, free_vars ) + * returns null + * + * Notice that multiple definitions are possible, e.g. above: + * inferDefinition( s, term_to_arg_carry, free_vars ) + * may return either s or x2 + * TODO (#1210) : try multiple definitions? + */ + Node inferDefinition( + Node n, + std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars); + /** Assign relevant definition + * + * If def is non-null, + * this function assigns def as a template definition + * for the argument positions in args. + * This is called when there exists a term of the form + * f( t1....tn ) + * in the synthesis conjecture that we are processing, + * where t_i = def * sigma for all i \in args, + * for some substitution sigma, where def is a template + * definition. + * + * If def is null, then there exists a term of the form + * f( t1....tn ) + * where t_i = s for for all i \in args, and s is not + * a template definition. In this case, at least one + * argument in args must be marked as a relevant + * argument position. + * + * Returns a value rid such that: + * (1) rid occurs in args, + * (2) if def is null, then argument rid was marked + * relevant by this call. + */ + unsigned assignRelevantDef(Node def, std::vector<unsigned>& args); + /** returns true if n is in d_arg_vars, updates arg_index + * to its position in d_arg_vars. + */ + bool isArgVar(Node n, unsigned& arg_index); }; /** Ceg Conjecture Process @@ -63,8 +279,20 @@ class CegConjectureProcess ~CegConjectureProcess(); /** simplify the synthesis conjecture q * Returns a formula that is equivalent to q. + * This simplification pass is called before all others + * in CegConjecture::assign. + * + * This function is intended for simplifications that + * impact whether or not the synthesis conjecture is + * single-invocation. */ - Node simplify(Node q); + Node preSimplify(Node q); + /** simplify the synthesis conjecture q + * Returns a formula that is equivalent to q. + * This simplification pass is called after all others + * in CegConjecture::assign. + */ + Node postSimplify(Node q); /** initialize * * n is the "base instantiation" of the deep-embedding version of @@ -72,6 +300,12 @@ class CegConjectureProcess * (see CegConjecture::d_base_inst) */ void initialize(Node n, std::vector<Node>& candidates); + /** is the i^th argument of the function-to-synthesize f relevant? */ + bool isArgRelevant(Node f, unsigned i); + /** get irrelevant arguments for function-to-synthesize f + * returns true if f is a function-to-synthesize. + */ + bool getIrrelevantArgs(Node f, std::unordered_set<unsigned>& args); /** get symmetry breaking predicate * * Returns a formula that restricts the enumerative search space (for a given @@ -82,14 +316,47 @@ class CegConjectureProcess Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); /** print out debug information about this conjecture */ void debugPrint(const char* c); - private: - /** process conjunct */ - void processConjunct(Node c); + /** process conjunct + * + * This sets up initial information about functions to synthesize + * where n is a conjunct of the synthesis conjecture, and synth_fv + * is the set of (inner) universal variables in the synthesis + * conjecture. + */ + void processConjunct(Node n, + Node f, + std::unordered_set<Node, NodeHashFunction>& synth_fv); + /** flatten + * + * Flattens all applications of f in term n. + * This may add new variables to synth_fv, which + * are introduced at all positions of functions + * to synthesize in a bottom-up fashion. For each + * variable k introduced for a function application + * f(t), we add ( k -> f(t) ) to defs and ( f -> k ) + * to fun_to_defs. + */ + Node flatten(Node n, + Node f, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, Node, NodeHashFunction>& defs); + /** get free variables + * Constructs a map of all free variables that occur in n + * from synth_fv and stores them in the map free_vars. + */ + void getFreeVariables( + Node n, + std::unordered_set<Node, NodeHashFunction>& synth_fv, + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction>& free_vars); /** for each synth-fun, information that is specific to this conjecture */ - std::map<Node, CegSynthFunProcessInfo> d_sf_info; + std::map<Node, CegConjectureProcessFun> d_sf_info; /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** get component vector */ + void getComponentVector(Kind k, Node n, std::vector<Node>& args); }; } /* namespace CVC4::theory::quantifiers */ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 3c118a007..b40ee845f 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -67,6 +67,9 @@ TESTS = commutative.sy \ triv-type-mismatch-si.sy \ nia-max-square-ns.sy \ strings-concat-3-args.sy \ + process-10-vars.sy \ + process-10-vars-2fun.sy \ + inv-unused.sy \ ccp16.lus.sy diff --git a/test/regress/regress0/sygus/inv-unused.sy b/test/regress/regress0/sygus/inv-unused.sy new file mode 100644 index 000000000..91ba95d39 --- /dev/null +++ b/test/regress/regress0/sygus/inv-unused.sy @@ -0,0 +1,13 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0)) +(inv-constraint inv-f pre-f trans-f post-f) +; invariant does not depend on arguments y and b +(check-synth) diff --git a/test/regress/regress0/sygus/process-10-vars-2fun.sy b/test/regress/regress0/sygus/process-10-vars-2fun.sy new file mode 100644 index 000000000..00340030f --- /dev/null +++ b/test/regress/regress0/sygus/process-10-vars-2fun.sy @@ -0,0 +1,28 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; EXPECT: unsat +(set-logic LIA) + +(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) + +(synth-fun g ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) + +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var x3 Int) +(declare-var x4 Int) +(declare-var x5 Int) +(declare-var x6 Int) +(declare-var x7 Int) +(declare-var x8 Int) +(declare-var x9 Int) +(declare-var x10 Int) + +; should be able to determine that arguments 1...6, 8...10 are irrelevant for f +; and arguments 1...3, 5...10 are irrelevant for g + +(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7))) + +(constraint (>= (g x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x4 x4 x4))) + +(check-synth) + diff --git a/test/regress/regress0/sygus/process-10-vars.sy b/test/regress/regress0/sygus/process-10-vars.sy new file mode 100644 index 000000000..523abd70d --- /dev/null +++ b/test/regress/regress0/sygus/process-10-vars.sy @@ -0,0 +1,24 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; EXPECT: unsat +(set-logic LIA) + +(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) + + +(declare-var x1 Int) +(declare-var x2 Int) +(declare-var x3 Int) +(declare-var x4 Int) +(declare-var x5 Int) +(declare-var x6 Int) +(declare-var x7 Int) +(declare-var x8 Int) +(declare-var x9 Int) +(declare-var x10 Int) + +; should be able to determine that arguments 1...6, 8...10 are irrelevant for f + +(constraint (>= (f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) (+ x7 x7 x7))) + +(check-synth) + diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am index 17b8e8872..190cf0f9f 100644 --- a/test/regress/regress1/sygus/Makefile.am +++ b/test/regress/regress1/sygus/Makefile.am @@ -27,7 +27,8 @@ TESTS = \ icfp_easy_mt_ite.sy \ three.sy \ nia-max-square.sy \ - MPwL_d1s3.sy + MPwL_d1s3.sy \ + process-arg-invariance.sy EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/sygus/process-arg-invariance.sy b/test/regress/regress1/sygus/process-arg-invariance.sy new file mode 100644 index 000000000..3c18b6c75 --- /dev/null +++ b/test/regress/regress1/sygus/process-arg-invariance.sy @@ -0,0 +1,18 @@ +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar +; EXPECT: unsat +(set-logic LIA) + +(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int) + + +(declare-var x Int) +(declare-var y Int) + +; should be able to determine that only 3 arguments +; (one of 5...9, one of 1 or 4, one of 2 or 3) is relevant for f + +(constraint (> (f (+ x x) (+ x 1) (+ x 1) (+ x x) x x x x x 0) (+ x x x))) +(constraint (<= (f x x x x x x x x x 0) (+ x x x))) + +(check-synth) + |