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;
}
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)
{
}
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 */
#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
~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
* (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
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 */
projects / cvc5.git / commitdiff