namespace CVC4 {
namespace preprocessing {
namespace passes {
+namespace symbreak {
-SymmetryDetect::Partition SymmetryDetect::detect(const vector<Node>& assertions)
+/** returns n choose k, that is, n!/(k! * (n-k)!) */
+unsigned nChoosek(unsigned n, unsigned k)
{
- Partition p =
- findPartitions(NodeManager::currentNM()->mkNode(kind::AND, assertions));
+ if (k > n) return 0;
+ if (k * 2 > n) k = n - k;
+ if (k == 0) return 1;
+
+ int result = n;
+ for (int i = 2; i <= static_cast<int>(k); ++i)
+ {
+ result *= (n - i + 1);
+ result /= i;
+ }
+ return result;
+}
+
+/** mk associative node
+ *
+ * This returns (a normal form for) the term <k>( children ), where
+ * k is an associative operator. We return a right-associative
+ * chain, since some operators (e.g. set union) require this.
+ */
+Node mkAssociativeNode(Kind k, std::vector<Node>& children)
+{
+ Assert(!children.empty());
+ NodeManager* nm = NodeManager::currentNM();
+ // sort and make right-associative chain
+ bool isComm = theory::quantifiers::TermUtil::isComm(k);
+ if (isComm)
+ {
+ std::sort(children.begin(), children.end());
+ }
+ Node sn;
+ for (const Node& sc : children)
+ {
+ Assert(!sc.isNull());
+ if (sn.isNull())
+ {
+ sn = sc;
+ }
+ else
+ {
+ Assert(!isComm || sc.getType().isComparableTo(sn.getType()));
+ sn = nm->mkNode(k, sc, sn);
+ }
+ }
+ return sn;
+}
+
+void Partition::printPartition(const char* c, Partition p)
+{
+ for (map<Node, vector<Node> >::iterator sub_vars_it =
+ p.d_subvar_to_vars.begin();
+ sub_vars_it != p.d_subvar_to_vars.end();
+ ++sub_vars_it)
+ {
+ Trace(c) << "[sym-dt] Partition: " << sub_vars_it->first << " -> {";
+
+ for (vector<Node>::iterator part_it = (sub_vars_it->second).begin();
+ part_it != (sub_vars_it->second).end();
+ ++part_it)
+ {
+ Trace(c) << " " << *part_it;
+ }
+ Trace(c) << " }" << endl;
+ }
+}
+
+void Partition::normalize()
+{
+ for (std::pair<const Node, std::vector<Node> > p : d_subvar_to_vars)
+ {
+ std::sort(p.second.begin(), p.second.end());
+ }
+}
+
+void PartitionMerger::initialize(Kind k,
+ const std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices)
+{
+ d_kind = k;
+ Trace("sym-dt-debug") << "Count variable occurrences..." << std::endl;
+ for (unsigned index : indices)
+ {
+ d_indices.push_back(index);
+ const Partition& p = partitions[index];
+ const std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+ for (const Node& v : svs)
+ {
+ if (d_occurs_count.find(v) == d_occurs_count.end())
+ {
+ d_occurs_count[v] = 1;
+ }
+ else
+ {
+ d_occurs_count[v]++;
+ }
+ d_occurs_by[index][v] = d_occurs_count[v] - 1;
+ }
+ }
+ if (Trace.isOn("sym-dt-debug"))
+ {
+ Trace("sym-dt-debug") << " variable occurrences: " << std::endl;
+ for (const std::pair<const Node, unsigned>& o : d_occurs_count)
+ {
+ Trace("sym-dt-debug")
+ << " " << o.first << " -> " << o.second << std::endl;
+ }
+ }
+}
+
+bool PartitionMerger::merge(std::vector<Partition>& partitions,
+ unsigned base_index,
+ std::unordered_set<unsigned>& active_indices)
+{
+ Assert(base_index < partitions.size());
+ d_master_base_index = base_index;
+ Partition& p = partitions[base_index];
+ Trace("sym-dt-debug") << " try basis index " << base_index
+ << " (#vars = " << p.d_subvar_to_vars.size() << ")"
+ << std::endl;
+ Assert(p.d_subvar_to_vars.size() == 1);
+ std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+ Trace("sym-dt-debug") << " try basis: " << svs << std::endl;
+ // try to merge variables one-by-one
+ d_base_indices.clear();
+ d_base_indices.insert(base_index);
+ d_base_vars.clear();
+ d_base_vars.insert(svs.begin(), svs.end());
+ d_num_new_indices_needed = d_base_vars.size();
+ bool merged = false;
+ bool success = false;
+ unsigned base_choose = d_base_vars.size() - 1;
+ unsigned base_occurs_req = d_base_vars.size();
+ do
+ {
+ Trace("sym-dt-debug") << " base variables must occur " << base_occurs_req
+ << " times." << std::endl;
+ // check if all the base_vars occur at least the required number of times
+ bool var_ok = true;
+ for (const Node& v : d_base_vars)
+ {
+ if (d_occurs_count[v] < base_occurs_req)
+ {
+ Trace("sym-dt-debug") << "...failed variable " << v << std::endl;
+ var_ok = false;
+ break;
+ }
+ }
+ if (!var_ok)
+ {
+ // cannot merge due to a base variable
+ break;
+ }
+ // try to find a new variable to merge
+ Trace("sym-dt-debug") << " must find " << d_num_new_indices_needed
+ << " new indices to merge." << std::endl;
+ std::vector<unsigned> new_indices;
+ Node merge_var;
+ d_merge_var_tried.clear();
+ if (mergeNewVar(0, new_indices, merge_var, 0, partitions, active_indices))
+ {
+ Trace("sym-dt-debug") << " ...merged: " << merge_var << std::endl;
+ Assert(!merge_var.isNull());
+ merged = true;
+ success = true;
+ // update the number of new indicies needed
+ if (base_choose > 0)
+ {
+ d_num_new_indices_needed +=
+ nChoosek(d_base_vars.size(), base_choose - 1);
+ // TODO (#2198): update base_occurs_req
+ }
+ }
+ else
+ {
+ Trace("sym-dt-debug") << " ...failed to merge" << std::endl;
+ success = false;
+ }
+ } while (success);
+ return merged;
+}
+
+bool PartitionMerger::mergeNewVar(unsigned curr_index,
+ std::vector<unsigned>& new_indices,
+ Node& merge_var,
+ unsigned num_merge_var_max,
+ std::vector<Partition>& partitions,
+ std::unordered_set<unsigned>& active_indices)
+{
+ Assert(new_indices.size() < d_num_new_indices_needed);
+ if (curr_index == d_indices.size())
+ {
+ return false;
+ }
+ Trace("sym-dt-debug2") << "merge " << curr_index << " / " << d_indices.size()
+ << std::endl;
+ // try to include this index
+ unsigned index = d_indices[curr_index];
+
+ // if not already included
+ if (d_base_indices.find(index) == d_base_indices.end())
+ {
+ Assert(active_indices.find(index) != active_indices.end());
+ // check whether it can merge
+ Partition& p = partitions[index];
+ Assert(p.d_subvar_to_vars.size() == 1);
+ std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+ bool include_success = true;
+ Node curr_merge_var;
+ for (const Node& v : svs)
+ {
+ if (d_base_vars.find(v) == d_base_vars.end() && v != merge_var)
+ {
+ if (merge_var.isNull() && curr_merge_var.isNull())
+ {
+ curr_merge_var = v;
+ }
+ else
+ {
+ // cannot include
+ Trace("sym-dt-debug2") << "...cannot include (new-var)\n";
+ include_success = false;
+ curr_merge_var = Node::null();
+ break;
+ }
+ }
+ }
+ if (!curr_merge_var.isNull())
+ {
+ // compute the maximum number of indices we can include for v
+ Assert(d_occurs_by[index].find(curr_merge_var)
+ != d_occurs_by[index].end());
+ Assert(d_occurs_count.find(curr_merge_var) != d_occurs_count.end());
+ unsigned num_v_max =
+ d_occurs_count[curr_merge_var] - d_occurs_by[index][curr_merge_var];
+ if (num_v_max >= d_num_new_indices_needed)
+ {
+ // have we already tried this merge_var?
+ if (d_merge_var_tried.find(curr_merge_var) != d_merge_var_tried.end())
+ {
+ include_success = false;
+ Trace("sym-dt-debug2")
+ << "...cannot include (already tried new merge var "
+ << curr_merge_var << ")\n";
+ }
+ else
+ {
+ Trace("sym-dt-debug2")
+ << "set merge var : " << curr_merge_var << std::endl;
+ d_merge_var_tried.insert(curr_merge_var);
+ num_merge_var_max = num_v_max;
+ merge_var = curr_merge_var;
+ }
+ }
+ else
+ {
+ Trace("sym-dt-debug2")
+ << "...cannot include (not enough room for new merge var "
+ << num_v_max << "<" << d_num_new_indices_needed << ")\n";
+ include_success = false;
+ }
+ }
+ else if (!include_success && !merge_var.isNull())
+ {
+ // decrement
+ num_merge_var_max--;
+ if (num_merge_var_max < d_num_new_indices_needed - new_indices.size())
+ {
+ Trace("sym-dt-debug2") << "...fail (out of merge var)\n";
+ return false;
+ }
+ }
+
+ if (include_success)
+ {
+ // try with the index included
+ new_indices.push_back(index);
+
+ // do we have enough now?
+ if (new_indices.size() == d_num_new_indices_needed)
+ {
+ std::vector<Node> children;
+ children.push_back(p.d_term);
+ std::vector<Node> schildren;
+ schildren.push_back(p.d_sterm);
+ // can now include in the base
+ d_base_vars.insert(merge_var);
+ Trace("sym-dt-debug") << "found symmetry : { ";
+ for (const unsigned& i : new_indices)
+ {
+ Assert(d_base_indices.find(i) == d_base_indices.end());
+ d_base_indices.insert(i);
+ Trace("sym-dt-debug") << i << " ";
+ const Partition& p = partitions[i];
+ children.push_back(p.d_term);
+ schildren.push_back(p.d_sterm);
+ Assert(active_indices.find(i) != active_indices.end());
+ active_indices.erase(i);
+ }
+ Trace("sym-dt-debug") << "}" << std::endl;
+ Trace("sym-dt-debug") << "Reconstruct master partition "
+ << d_master_base_index << std::endl;
+ Partition& p = partitions[d_master_base_index];
+ // reconstruct the master partition
+ p.d_term = mkAssociativeNode(d_kind, children);
+ p.d_sterm = mkAssociativeNode(d_kind, schildren);
+ Assert(p.d_subvar_to_vars.size() == 1);
+ Node sb_v = p.d_subvar_to_vars.begin()->first;
+ p.d_subvar_to_vars[sb_v].push_back(merge_var);
+ Trace("sym-dt-debug") << "- set var to svar: " << merge_var << " -> "
+ << sb_v << std::endl;
+ p.d_var_to_subvar[merge_var] = sb_v;
+ return true;
+ }
+ if (mergeNewVar(curr_index + 1,
+ new_indices,
+ merge_var,
+ num_merge_var_max,
+ partitions,
+ active_indices))
+ {
+ return true;
+ }
+ new_indices.pop_back();
+ // if we included with the merge var, no use trying not including
+ if (curr_merge_var.isNull() && !merge_var.isNull())
+ {
+ Trace("sym-dt-debug2") << "...fail (failed merge var)\n";
+ return false;
+ }
+ }
+ }
+ // TODO (#2198):
+ // if we haven't yet chosen a merge variable, we may not have enough elements
+ // left in d_indices.
+
+ // try with it not included
+ return mergeNewVar(curr_index + 1,
+ new_indices,
+ merge_var,
+ num_merge_var_max,
+ partitions,
+ active_indices);
+}
+
+void PartitionTrie::getNewPartition(Partition& part,
+ PartitionTrie& pt,
+ std::map<Node, Node>& var_to_svar)
+{
+ if (!pt.d_variables.empty())
+ {
+ Assert(var_to_svar.find(pt.d_variables[0]) != var_to_svar.end());
+ Node svar = var_to_svar[pt.d_variables[0]];
+ Trace("sym-dt-debug")
+ << "[sym-dt] A partition from leaves of the partition trie:{";
+ for (const Node& v : pt.d_variables)
+ {
+ Trace("sym-dt-debug") << " " << v;
+ part.d_var_to_subvar[v] = svar;
+ part.d_subvar_to_vars[svar].push_back(v);
+ }
+ Trace("sym-dt-debug") << " }" << endl;
+ }
+ else
+ {
+ for (map<Node, PartitionTrie>::iterator part_it = pt.d_children.begin();
+ part_it != pt.d_children.end();
+ ++part_it)
+ {
+ getNewPartition(part, part_it->second, var_to_svar);
+ }
+ }
+}
+
+Node PartitionTrie::addNode(Node target_var, vector<Partition>& partitions)
+{
+ Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << target_var
+ << "} to the partition trie, #partitions = "
+ << partitions.size() << "..." << endl;
+ Assert(!partitions.empty());
+ vector<Node> subvars;
+
+ for (vector<Partition>::iterator part_it = partitions.begin();
+ part_it != partitions.end();
+ ++part_it)
+ {
+ map<Node, Node>::iterator var_sub_it =
+ (*part_it).d_var_to_subvar.find(target_var);
+
+ if (var_sub_it != (*part_it).d_var_to_subvar.end())
+ {
+ subvars.push_back(var_sub_it->second);
+ }
+ else
+ {
+ subvars.push_back(Node::null());
+ }
+ }
+
+ Trace("sym-dt-debug")
+ << "[sym-dt] Symmetry breaking variables for the variable " << target_var
+ << ": " << subvars << endl;
+ PartitionTrie* curr = this;
+ for (const Node& c : subvars)
+ {
+ curr = &(curr->d_children[c]);
+ }
+ curr->d_variables.push_back(target_var);
+ return curr->d_variables[0];
+}
+
+Partition SymmetryDetect::detect(const vector<Node>& assertions)
+{
+ Node an;
+ if (assertions.empty())
+ {
+ an = d_trueNode;
+ }
+ else if (assertions.size() == 1)
+ {
+ an = assertions[0];
+ }
+ else
+ {
+ an = NodeManager::currentNM()->mkNode(kind::AND, assertions);
+ }
+ Partition p = findPartitions(an);
Trace("sym-dt") << endl
<< "------------------------------ The Final Partition "
"------------------------------"
<< endl;
if(Trace.isOn("sym-dt"))
{
- printPartition(p);
+ Partition::printPartition("sym-dt", p);
}
return p;
}
+Node SymmetryDetect::getSymBreakVariable(TypeNode tn, unsigned index)
+{
+ std::map<TypeNode, std::vector<Node> >::iterator it = d_sb_vars.find(tn);
+ if (it == d_sb_vars.end())
+ {
+ // initialize the variables for type tn
+ d_sb_vars[tn].clear();
+ it = d_sb_vars.find(tn);
+ }
+ while (it->second.size() <= index)
+ {
+ std::stringstream ss;
+ ss << "_sym_bk_" << tn << "_" << (it->second.size() + 1);
+ Node fresh_var =
+ NodeManager::currentNM()->mkSkolem(ss.str(),
+ tn,
+ "symmetry breaking variable",
+ NodeManager::SKOLEM_EXACT_NAME);
+ it->second.push_back(fresh_var);
+ }
+ return it->second[index];
+}
+
+Node SymmetryDetect::getSymBreakVariableInc(TypeNode tn,
+ std::map<TypeNode, unsigned>& index)
+{
+ // ensure we use a new index for this variable
+ unsigned new_index = 0;
+ std::map<TypeNode, unsigned>::iterator itt = index.find(tn);
+ if (itt != index.end())
+ {
+ new_index = itt->second;
+ }
+ index[tn] = new_index + 1;
+ return getSymBreakVariable(tn, new_index);
+}
+
void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
const vector<Node>& assertions)
{
}
}
-SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node)
+Partition SymmetryDetect::findPartitions(Node node)
{
- Trace("sym-dt")
- << "------------------------------------------------------------"
- << endl;
- Trace("sym-dt") << "[sym-dt] findPartitions gets a term: " << node << endl;
+ Trace("sym-dt-debug")
+ << "------------------------------------------------------------" << endl;
+ Trace("sym-dt-debug") << "[sym-dt] findPartitions gets a term: " << node
+ << endl;
map<Node, Partition>::iterator partition = d_term_partition.find(node);
// Return its partition from cache if we have processed the node before
if (partition != d_term_partition.end())
{
- Trace("sym-dt") << "[sym-dt] We have seen the node " << node
- << " before, thus we return its partition from cache."
- << endl;
+ Trace("sym-dt-debug") << "[sym-dt] We have seen the node " << node
+ << " before, thus we return its partition from cache."
+ << endl;
return partition->second;
}
{
vector<Node> vars;
TypeNode type = node.getType();
- Node fresh_var = NodeManager::currentNM()->mkSkolem("sym_bk", type);
-
+ Node fresh_var = getSymBreakVariable(type, 0);
vars.push_back(node);
p.d_term = node;
+ p.d_sterm = fresh_var;
p.d_subvar_to_vars[fresh_var] = vars;
p.d_var_to_subvar[node] = fresh_var;
d_term_partition[node] = p;
return p;
}
// If node is a constant
- else if (node.isConst())
+ else if (node.getNumChildren() == 0)
{
p.d_term = node;
+ p.d_sterm = node;
d_term_partition[node] = p;
return p;
}
+ NodeManager* nm = NodeManager::currentNM();
+
+ Kind k = node.getKind();
+ bool isAssocComm = false;
+ // EQUAL is a special case here: we consider EQUAL to be associative,
+ // and handle the type polymorphism specially.
+ bool isAssoc = k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k);
+ // for now, only consider commutative operators that are also associative
+ if (isAssoc)
+ {
+ isAssocComm = theory::quantifiers::TermUtil::isComm(k);
+ }
// Children of node
vector<Node> children;
vector<Partition> partitions;
// Get all children of node
- Trace("sym-dt") << "[sym-dt] collectChildren for: " << node
- << " with operator " << node.getKind() << endl;
- collectChildren(node, children);
- Trace("sym-dt") << "[sym-dt] children: " << children
- << endl;
+ Trace("sym-dt-debug") << "[sym-dt] collectChildren for: " << node
+ << " with operator " << node.getKind() << endl;
+ if (!isAssocComm)
+ {
+ children.insert(children.end(), node.begin(), node.end());
+ }
+ else
+ {
+ collectChildren(node, children);
+ }
+ Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl;
// Create partitions for children
+ std::unordered_set<unsigned> active_indices;
for (vector<Node>::iterator children_it = children.begin();
children_it != children.end();
++children_it)
{
+ active_indices.insert(partitions.size());
partitions.push_back(findPartitions(*children_it));
}
-
- Trace("sym-dt") << "----------------------------- Start processing "
- "partitions -------------------------------"
- << endl;
-
- PartitionTrie pt;
- unordered_set<Node, NodeHashFunction> vars;
-
- if (theory::quantifiers::TermUtil::isComm(node.getKind()))
- {
- // Start processing the singleton partitions and collect variables
- processSingletonPartitions(partitions, vars);
- }
- else
+ if (Trace.isOn("sym-dt-debug"))
{
- // Get all the variables from the partitions
- getVariables(partitions, vars);
- }
-
- // Build the partition trie
- for (unordered_set<Node, NodeHashFunction>::iterator vars_it = vars.begin();
- vars_it != vars.end();
- ++vars_it)
- {
- pt.addNode(*vars_it, partitions);
+ Trace("sym-dt-debug") << "----------------------------- Start processing "
+ "partitions for "
+ << node << " -------------------------------" << endl;
+ for (unsigned j = 0, size = partitions.size(); j < size; j++)
+ {
+ Trace("sym-dt-debug") << "[" << j << "]: " << partitions[j].d_term
+ << " --> " << partitions[j].d_sterm << std::endl;
+ }
+ Trace("sym-dt-debug") << "-----------------------------" << std::endl;
}
- // Get the new partition
- pt.getNewPartition(p, pt);
-
- // Reconstruct the node
- Trace("sym-dt") << "[sym-dt] Reconstructing node: " << node << endl;
- p.d_term = node;
- d_term_partition[node] = p;
- printPartition(p);
- return p;
-}
-
-void SymmetryDetect::matches(vector<Partition>& partitions,
- map<Node, Node>& subvar_to_var,
- map<Node, Node>& subvar_to_expr)
-{
- Trace("sym-dt")
- << "[sym-dt] Start testing if singleton partitions can be merged!"
- << endl;
-
- if (!subvar_to_expr.empty())
+ if (isAssocComm)
{
- // Replacement variables
- vector<Node> repls;
- // Variables that have been merged
- unordered_set<Node, NodeHashFunction> merged;
- // Put the variable in repls
- repls.push_back((subvar_to_expr.begin())->first);
-
- for (map<Node, Node>::iterator expr_it1 = subvar_to_expr.begin();
- expr_it1 != subvar_to_expr.end();
- ++expr_it1)
+ // map substituted terms to indices in partitions
+ std::map<Node, std::vector<unsigned> > sterm_to_indices;
+ for (unsigned j = 0, size = partitions.size(); j < size; j++)
{
- // Skip expr_it1->first, if it has been merged
- if (merged.find(expr_it1->first) != merged.end())
+ if (!partitions[j].d_sterm.isNull())
{
- continue;
+ sterm_to_indices[partitions[j].d_sterm].push_back(j);
}
+ }
- Partition p;
- vector<Node> subs;
- vector<Node> part;
- Node fst_var = subvar_to_var.find(expr_it1->first)->second;
-
- part.push_back(fst_var);
- subs.push_back(fst_var);
- merged.insert(expr_it1->first);
- p.d_var_to_subvar[fst_var] = expr_it1->first;
- Node sub_expr1 =
- (expr_it1->second)
- .substitute(subs.begin(), subs.end(), repls.begin(), repls.end());
-
- for (map<Node, Node>::iterator expr_it2 = subvar_to_expr.begin();
- expr_it2 != subvar_to_expr.end();
- ++expr_it2)
+ for (const std::pair<Node, std::vector<unsigned> >& sti : sterm_to_indices)
+ {
+ Node cterm = sti.first;
+ if (Trace.isOn("sym-dt-debug"))
{
- if (merged.find(expr_it2->first) != merged.end())
- {
- continue;
- }
- if ((expr_it1->second).getType() != (expr_it2->second).getType())
+ Trace("sym-dt-debug") << " indices[" << cterm << "] = ";
+ for (unsigned i : sti.second)
{
- continue;
- }
- vector<Node> subs2;
- Node snd_var = subvar_to_var.find(expr_it2->first)->second;
-
- subs2.push_back(snd_var);
- Node sub_expr2 =
- (expr_it2->second)
- .substitute(
- subs2.begin(), subs2.end(), repls.begin(), repls.end());
- Trace("sym-dt") << "[sym-dt] Testing if " << sub_expr1
- << " is equivalent to " << sub_expr2 << endl;
-
- if (sub_expr1 == sub_expr2)
- {
- Trace("sym-dt") << "[sym-dt] Merge variable " << fst_var
- << " with variable " << snd_var << endl;
- merged.insert(expr_it2->first);
- part.push_back(snd_var);
- p.d_var_to_subvar[snd_var] = expr_it1->first;
+ Trace("sym-dt-debug") << i << " ";
}
+ Trace("sym-dt-debug") << std::endl;
}
- p.d_subvar_to_vars[expr_it1->first] = part;
- Trace("sym-dt") << "[sym-dt] Add a new partition after merging: " << endl;
- printPartition(p);
- partitions.push_back(p);
+ // merge children, remove active indices
+ processPartitions(k, partitions, sti.second, active_indices);
}
}
-}
-
-void SymmetryDetect::processSingletonPartitions(
- vector<Partition>& partitions, unordered_set<Node, NodeHashFunction>& vars)
-{
- Trace("sym-dt") << "[sym-dt] Start post-processing partitions with size = "
- << partitions.size() << endl;
-
- // Mapping between the substitution variable to the actual variable
- map<Node, Node> subvar_to_var;
- // Mapping between the substitution variable to the actual expression
- map<Node, Node> subvar_to_expr;
- // Partitions that have 2 or more variables
- vector<Partition> new_partitions;
-
- // Collect singleton partitions: subvar_to_expr, subvar_to_var, and variables
- for (vector<Partition>::const_iterator part_it = partitions.begin();
- part_it != partitions.end();
- ++part_it)
+ // initially set substituted term to node
+ p.d_sterm = node;
+ // for all active indices
+ vector<Node> all_vars;
+ std::map<TypeNode, unsigned> type_index;
+ std::vector<Node> schildren;
+ if (!isAssocComm)
{
- if ((*part_it).d_var_to_subvar.size() == 1)
+ Assert(active_indices.size() == children.size());
+ // order matters, and there is no chance we merged children
+ schildren.resize(children.size());
+ }
+ std::vector<Partition> active_partitions;
+ for (const unsigned& i : active_indices)
+ {
+ Trace("sym-dt-debug") << "Reconstruct partition for active index : " << i
+ << std::endl;
+ Partition& pa = partitions[i];
+ // ensure the variables of pa are fresh
+ std::vector<Node> f_vars;
+ std::vector<Node> f_subs;
+ // add to overall list of variables
+ for (const pair<const Node, vector<Node> >& pas : pa.d_subvar_to_vars)
{
- vars.insert(((*part_it).d_var_to_subvar.begin())->first);
- subvar_to_expr[((*part_it).d_var_to_subvar.begin())->second] =
- (*part_it).d_term;
- subvar_to_var[((*part_it).d_var_to_subvar.begin())->second] =
- ((*part_it).d_var_to_subvar.begin())->first;
+ Node v = pas.first;
+ Trace("sym-dt-debug")
+ << "...process " << v << " -> " << pas.second << std::endl;
+ Assert(!v.isNull());
+ TypeNode tnv = v.getType();
+ // ensure we use a new index for this variable
+ Node new_v = getSymBreakVariableInc(tnv, type_index);
+ f_vars.push_back(v);
+ f_subs.push_back(new_v);
+ // add all vars to partition trie classifier
+ for (const Node& c : pas.second)
+ {
+ if (std::find(all_vars.begin(), all_vars.end(), c) == all_vars.end())
+ {
+ all_vars.push_back(c);
+ }
+ }
+ for (const Node& x : pas.second)
+ {
+ Assert(x.getType() == new_v.getType());
+ pa.d_var_to_subvar[x] = new_v;
+ Trace("sym-dt-debug")
+ << "...set var to svar: " << x << " -> " << new_v << std::endl;
+ }
}
- else if ((*part_it).d_var_to_subvar.size() >= 2)
+ // reconstruct the partition
+ for (unsigned j = 0, size = f_vars.size(); j < size; j++)
{
- for (const pair<Node, Node>& var_to_subvar : (*part_it).d_var_to_subvar)
+ Node v = f_vars[j];
+ Node new_v = f_subs[j];
+ if (new_v != v)
{
- vars.insert(var_to_subvar.first);
+ pa.d_subvar_to_vars[new_v].insert(pa.d_subvar_to_vars[new_v].end(),
+ pa.d_subvar_to_vars[v].begin(),
+ pa.d_subvar_to_vars[v].end());
+ pa.d_subvar_to_vars.erase(v);
}
- // Only add partitions that have more than 1 variable
- new_partitions.push_back(*part_it);
}
+ Assert(f_vars.size() == f_subs.size());
+ Assert(!pa.d_sterm.isNull());
+ pa.d_sterm = pa.d_sterm.substitute(
+ f_vars.begin(), f_vars.end(), f_subs.begin(), f_subs.end());
+ if (isAssocComm)
+ {
+ Assert(!pa.d_sterm.isNull());
+ schildren.push_back(pa.d_sterm);
+ }
+ else
+ {
+ Assert(i < schildren.size());
+ schildren[i] = pa.d_sterm;
+ }
+ Trace("sym-dt-debug") << "...got : " << pa.d_sterm << std::endl;
+ active_partitions.push_back(pa);
}
- // Save all partitions that have more than 1 variable
- partitions = new_partitions;
+ PartitionTrie pt;
+ std::map<Node, Node> var_to_svar;
+ type_index.clear();
+ // Build the partition trie
+ std::sort(all_vars.begin(), all_vars.end());
+ for (const Node& n : all_vars)
+ {
+ Node an = pt.addNode(n, active_partitions);
+ // if this is a new node, allocate
+ if (an == n)
+ {
+ Node new_v = getSymBreakVariableInc(n.getType(), type_index);
+ var_to_svar[n] = new_v;
+ }
+ }
- // Do matches on singleton terms
- if (!subvar_to_var.empty())
+ // Get the new partition
+ pt.getNewPartition(p, pt, var_to_svar);
+
+ // Reconstruct the node
+ p.d_term = node;
+ Assert(!p.d_sterm.isNull());
+ Trace("sym-dt-debug") << "[sym-dt] Reconstructing node: " << node
+ << ", #children = " << schildren.size() << "/"
+ << children.size() << endl;
+ if (isAssocComm)
+ {
+ p.d_sterm = mkAssociativeNode(k, schildren);
+ }
+ else
{
- matches(partitions, subvar_to_var, subvar_to_expr);
+ if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ schildren.insert(schildren.begin(), node.getOperator());
+ }
+ p.d_sterm = nm->mkNode(k, schildren);
}
+ Trace("sym-dt-debug") << "...return sterm: " << p.d_sterm << std::endl;
+ Trace("sym-dt-debug") << ".....types: " << p.d_sterm.getType() << " "
+ << node.getType() << std::endl;
+ Assert(p.d_sterm.getType() == node.getType());
+
+ p.normalize();
+ d_term_partition[node] = p;
+ Partition::printPartition("sym-dt-debug", p);
+ return p;
}
void SymmetryDetect::collectChildren(Node node, vector<Node>& children)
{
Kind k = node.getKind();
+ Assert((k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k))
+ && theory::quantifiers::TermUtil::isComm(k));
- if(!theory::quantifiers::TermUtil::isAssoc(k))
- {
- children.insert(children.end(), node.begin(), node.end());
- return;
- }
+ // must track the type of the children we are collecting
+ // this is to avoid having vectors of children with different type, like
+ // (= (= x 0) (= y "abc"))
+ TypeNode ctn = node[0].getType();
Node cur;
vector<Node> visit;
if (visited.find(cur) == visited.end())
{
visited.insert(cur);
- if (cur.getKind() == k)
+ if (cur.getNumChildren() > 0 && cur.getKind() == k
+ && cur[0].getType() == ctn)
{
for (const Node& cn : cur)
{
} while (!visit.empty());
}
-void SymmetryDetect::PartitionTrie::getNewPartition(Partition& part,
- PartitionTrie& pt)
+/** A basic trie for storing vectors of arguments */
+class NodeTrie
{
- if (!pt.d_variables.empty())
+ public:
+ NodeTrie() : d_value(-1) {}
+ /** value of this node, -1 if unset */
+ int d_value;
+ /** children of this node */
+ std::map<Node, NodeTrie> d_children;
+ /** clear the children */
+ void clear() { d_children.clear(); }
+ /**
+ * Return true iff we've added the suffix of the vector of arguments starting
+ * at index before.
+ */
+ unsigned add(unsigned value,
+ const std::vector<Node>& args,
+ unsigned index = 0)
{
- vector<Node> vars;
- Node fresh_var = NodeManager::currentNM()->mkSkolem(
- "sym_bk", pt.d_variables[0].getType());
- Trace("sym-dt")
- << "[sym-dt] A partition from leaves of the partition trie:{";
-
- for (vector<Node>::iterator var_it = pt.d_variables.begin();
- var_it != pt.d_variables.end();
- ++var_it)
+ if (index == args.size())
{
- Trace("sym-dt") << " " << *var_it;
- vars.push_back(*var_it);
- part.d_var_to_subvar[*var_it] = fresh_var;
- }
- Trace("sym-dt") << " }" << endl;
- part.d_subvar_to_vars[fresh_var] = vars;
- }
- else
- {
- for (map<Node, PartitionTrie>::iterator part_it = pt.d_children.begin();
- part_it != pt.d_children.end();
- ++part_it)
- {
- getNewPartition(part, part_it->second);
+ if (d_value == -1)
+ {
+ d_value = static_cast<int>(value);
+ }
+ return d_value;
}
+ return d_children[args[index]].add(value, args, index + 1);
}
-}
+};
-void SymmetryDetect::getVariables(vector<Partition>& partitions,
- unordered_set<Node, NodeHashFunction>& vars)
+void SymmetryDetect::processPartitions(
+ Kind k,
+ std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices,
+ std::unordered_set<unsigned>& active_indices)
{
- for (vector<Partition>::iterator part_it = partitions.begin();
- part_it != partitions.end();
- ++part_it)
+ Assert(!indices.empty());
+ unsigned first_index = indices[0];
+
+ unsigned num_sb_vars = partitions[first_index].d_subvar_to_vars.size();
+ if (num_sb_vars != 1)
{
- for (map<Node, vector<Node> >::iterator sub_var_it =
- (*part_it).d_subvar_to_vars.begin();
- sub_var_it != (*part_it).d_subvar_to_vars.end();
- ++sub_var_it)
- {
- vars.insert((sub_var_it->second).begin(), (sub_var_it->second).end());
- }
+ // can only handle symmetries that are classified by { n }
+ return;
}
-}
-
-void SymmetryDetect::PartitionTrie::addNode(Node target_var,
- vector<Partition>& partitions)
-{
- Trace("sym-dt") << "[sym-dt] Add a variable {" << target_var
- << "} to the partition trie..." << endl;
- vector<Node> subvars;
-
- for (vector<Partition>::iterator part_it = partitions.begin();
- part_it != partitions.end();
- ++part_it)
+ // separate by number of variables
+ // for each n, nv_indices[n] contains the indices of partitions of the form
+ // { w1 -> { x1, ..., xn } }
+ std::map<unsigned, std::vector<unsigned> > nv_indices;
+ for (unsigned j = 0, size = indices.size(); j < size; j++)
{
- map<Node, Node>::iterator var_sub_it =
- (*part_it).d_var_to_subvar.find(target_var);
-
- if (var_sub_it != (*part_it).d_var_to_subvar.end())
+ unsigned index = indices[j];
+ Assert(partitions[index].d_subvar_to_vars.size() == 1);
+ unsigned num_vars = partitions[index].d_var_to_subvar.size();
+ nv_indices[num_vars].push_back(index);
+ }
+ for (const std::pair<const unsigned, std::vector<unsigned> >& nvi :
+ nv_indices)
+ {
+ if (nvi.second.size() <= 1)
{
- for (map<Node, vector<Node> >::iterator sub_vars_it =
- (*part_it).d_subvar_to_vars.begin();
- sub_vars_it != (*part_it).d_subvar_to_vars.end();
- ++sub_vars_it)
+ // no symmetries
+ continue;
+ }
+ unsigned num_vars = nvi.first;
+ if (Trace.isOn("sym-dt-debug"))
+ {
+ Trace("sym-dt-debug") << " nv_indices[" << num_vars << "] = ";
+ for (unsigned i : nvi.second)
{
- if (var_sub_it->second == sub_vars_it->first)
- {
- subvars.push_back(var_sub_it->second);
- }
- else
- {
- subvars.push_back(Node::null());
- }
+ Trace("sym-dt-debug") << i << " ";
}
+ Trace("sym-dt-debug") << std::endl;
}
- else
+ Trace("sym-dt-debug") << "Check for duplicates..." << std::endl;
+ // drop duplicates
+ // this ensures we don't double count equivalent children that were not
+ // syntactically identical e.g. (or (= x y) (= y x))
+ NodeTrie ntrie;
+ // non-duplicate indices
+ std::unordered_set<unsigned> nvis;
+ for (unsigned index : nvi.second)
{
- subvars.resize(subvars.size()+(*part_it).d_subvar_to_vars.size());
+ Partition& p = partitions[index];
+ std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
+ unsigned aindex = ntrie.add(index, svs);
+ if (aindex == index)
+ {
+ nvis.insert(index);
+ }
+ else if (theory::quantifiers::TermUtil::isNonAdditive(k))
+ {
+ Trace("sym-dt-debug")
+ << "Drop duplicate child : " << index << std::endl;
+ Assert(active_indices.find(index) != active_indices.end());
+ active_indices.erase(index);
+ }
+ else
+ {
+ nvis.erase(aindex);
+ }
}
+ std::vector<unsigned> check_indices;
+ check_indices.insert(check_indices.end(), nvis.begin(), nvis.end());
+ Trace("sym-dt-debug") << "Merge..." << std::endl;
+ // now, try to merge these partitions
+ mergePartitions(k, partitions, check_indices, active_indices);
}
-
- Trace("sym-dt") << "[sym-dt] Substitution variables for the variable "
- << target_var << ": " << subvars << endl;
- addNode(target_var, subvars);
}
-void SymmetryDetect::PartitionTrie::addNode(Node target_var,
- vector<Node>& subvars)
+void SymmetryDetect::mergePartitions(
+ Kind k,
+ std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices,
+ std::unordered_set<unsigned>& active_indices)
{
- if (subvars.empty())
+ if (indices.size() <= 1)
{
- d_variables.push_back(target_var);
+ return;
}
- else
+ if (Trace.isOn("sym-dt-debug"))
{
- vector<Node> new_subs;
- map<Node, PartitionTrie>::iterator children_it =
- d_children.find(subvars[0]);
-
- if (subvars.begin() + 1 < subvars.end())
- {
- new_subs.insert(new_subs.begin(), subvars.begin() + 1, subvars.end());
- }
- if (children_it != d_children.end())
+ Trace("sym-dt-debug") << " merge indices ";
+ for (unsigned i : indices)
{
- (children_it->second).addNode(target_var, new_subs);
- }
- else
- {
- PartitionTrie pt;
-
- pt.addNode(target_var, new_subs);
- d_children[subvars[0]] = pt;
+ Trace("sym-dt-debug") << i << " ";
}
+ Trace("sym-dt-debug") << std::endl;
}
-}
+ Assert(!indices.empty());
-void SymmetryDetect::printPartition(Partition p)
-{
- for (map<Node, vector<Node> >::iterator sub_vars_it =
- p.d_subvar_to_vars.begin();
- sub_vars_it != p.d_subvar_to_vars.end();
- ++sub_vars_it)
- {
- Trace("sym-dt") << "[sym-dt] Partition: " << sub_vars_it->first << " -> {";
+ // initialize partition merger class
+ PartitionMerger pm;
+ pm.initialize(k, partitions, indices);
- for (vector<Node>::iterator part_it = (sub_vars_it->second).begin();
- part_it != (sub_vars_it->second).end();
- ++part_it)
+ // TODO (#2198): process indices for distinct types separately
+ for (unsigned index : indices)
+ {
+ if (pm.merge(partitions, index, active_indices))
{
- Trace("sym-dt") << " " << *part_it;
+ Trace("sym-dt-debug") << " ......we merged, recurse" << std::endl;
+ std::vector<unsigned> rem_indices;
+ for (unsigned ii : indices)
+ {
+ if (ii != index && active_indices.find(ii) != active_indices.end())
+ {
+ rem_indices.push_back(ii);
+ }
+ }
+ mergePartitions(k, partitions, rem_indices, active_indices);
+ return;
}
- Trace("sym-dt") << " }" << endl;
}
}
+
+} // namespace symbreak
} // namespace passes
} // namespace preprocessing
} // namespace CVC4
namespace CVC4 {
namespace preprocessing {
namespace passes {
+namespace symbreak {
+
+/**
+ * This class stores a "partition", which is a way of representing a
+ * class of symmetries.
+ *
+ * For example, when finding symmetries for a term like x+y = 0, we
+ * construct a partition { w -> { x, y } } that indicates that automorphisms
+ * over { x, y } do not affect the satisfiability of this term. In this
+ * example, we have the following assignments to the members of this class:
+ * d_term : x+y=0
+ * d_sterm : w+w=0
+ * d_var_to_subvar : { x -> w, y -> w }
+ * d_subvar_to_vars : { w -> { x, y } }
+ * We often identify a partition with its d_subvar_to_vars field.
+ *
+ * We call w a "symmetry breaking variable".
+ */
+class Partition
+{
+ public:
+ /** The term for which the partition was computed for. */
+ Node d_term;
+ /** Substituted term corresponding to the partition
+ *
+ * This is equal to d_term * d_var_to_subvar, where * is application of
+ * substitution.
+ */
+ Node d_sterm;
+ /**
+ * Mapping between the variable and the symmetry breaking variable e.g.
+ * { x -> w, y -> w }.
+ */
+ std::map<Node, Node> d_var_to_subvar;
+
+ /**
+ * Mapping between the symmetry breaking variables and variables, e.g.
+ * { w-> { x, y } }
+ */
+ std::map<Node, std::vector<Node> > d_subvar_to_vars;
+ /** sorts the ranges of d_subvar_to_vars. */
+ void normalize();
+ /** Print a partition */
+ static void printPartition(const char* c, Partition p);
+};
+
+/** partition merger
+ *
+ * This class is used to identify sets of children of commutative operators k
+ * that are identical up to a set of automorphisms.
+ *
+ * This class is used when we have detected symmetries for the children
+ * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative
+ * operator. For each i=1,...n, partitions[i] represents symmetries (in the
+ * form of a partition) computed for the child t_i.
+ *
+ * The vector d_indices of this class stores a list ( i_1...i_m ) such that
+ * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent
+ * for each j=1...m, where * is application of substitution.
+ *
+ * In detail, we say that
+ * partition[j1] = { w -> X_1 },
+ * ...,
+ * partition[jp] = { w -> X_p }
+ * are mergeable if s=|X_1|=...=|X_p|, and all subsets of
+ * X* = ( union_{k=1...p} X_k ) of size s are equal to exactly one of
+ * X_1 ... X_p.
+ */
+class PartitionMerger
+{
+ public:
+ PartitionMerger()
+ : d_kind(kind::UNDEFINED_KIND),
+ d_master_base_index(0),
+ d_num_new_indices_needed(0)
+ {
+ }
+ /** initialize this class
+ *
+ * We will be trying to merge the given partitions that occur at the given
+ * indices. k is the kind of the operator that partitions are children of.
+ */
+ void initialize(Kind k,
+ const std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices);
+ /** merge
+ *
+ * This method tries to "merge" partitions occurring at the indices d_indices
+ * of the vector partitions.
+ *
+ * Assuming the setting described above, if there exists a mergeable set of
+ * partitions with indices (j_m1...j_mp), we remove {j_m1...j_mp} \ { j_m1 }
+ * from active_indices, and update partition[j1] := { w -> X* }.
+ *
+ * The base_index is an index from d_indices that serves as a basis for
+ * detecting this symmetry. In particular, we start by assuming that
+ * p=1, and j_m1 is base_index. We proceed by trying to find sets of indices
+ * that add exactly one variable to X* at a time. We return
+ * true if p>1, that is, at least one partition was merged with the
+ * base_index.
+ */
+ bool merge(std::vector<Partition>& partitions,
+ unsigned base_index,
+ std::unordered_set<unsigned>& active_indices);
+
+ private:
+ /** the kind of the node we are consdiering */
+ Kind d_kind;
+ /** indices we are considering */
+ std::vector<unsigned> d_indices;
+ /** count the number of times each variable occurs */
+ std::map<Node, unsigned> d_occurs_count;
+ /** the number of times each variable occurs up to the given index */
+ std::map<unsigned, std::map<Node, unsigned> > d_occurs_by;
+ /** current master base index */
+ unsigned d_master_base_index;
+ /** the indices that occur in the current symmetry (the list (j1...jp)) */
+ std::unordered_set<unsigned> d_base_indices;
+ /** the free variables that occur in the current symmetry (the set X*)*/
+ std::unordered_set<Node, NodeHashFunction> d_base_vars;
+ /** the number of indices we need to add to extended X* by one variable */
+ unsigned d_num_new_indices_needed;
+ /** the variables we have currently tried to add to X* */
+ std::unordered_set<Node, NodeHashFunction> d_merge_var_tried;
+ /** merge new variable
+ *
+ * This is a recursive helper for the merge function. This function attempts
+ * to construct a set of indices {j1...jp} of partitions and a variable
+ * "merge_var" such that partitions[ji] is of the form { w -> X_ji }, where
+ * merge_var in X_ji and ( X_ji \ { merge_var } ) is a subset of the base
+ * variables X*. We require that p = d_num_new_indices_needed, where
+ * d_num_new_indices_needed is
+ * |d_base_vars| choose (|X_ji|-1)
+ * that is, n!/((n-k)!*k!) where n=|d_base_vars| and k=|X_ji|-1.
+ *
+ * curr_index : the index of d_indices we are currently considering whether
+ * to add to new_indices,
+ * new_indices : the currently considered indices {j1...jp},
+ * merge_var : the variable we are currently trying to add to X*,
+ * new_merge_var_max : the maximum number of times that merge_var might
+ * appear in remainding indices, i.e. d_indices[curr_index]...d_indices.end(),
+ * which is used as an optimization for recognizing quickly when this method
+ * will fail.
+ */
+ bool mergeNewVar(unsigned curr_index,
+ std::vector<unsigned>& new_indices,
+ Node& merge_var,
+ unsigned num_merge_var_max,
+ std::vector<Partition>& partitions,
+ std::unordered_set<unsigned>& active_indices);
+};
+/**
+ * We build the partition trie indexed by
+ * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a
+ * partition trie is the new regions of a partition
+ */
+class PartitionTrie
+{
+ public:
+ /** Variables at the leave */
+ std::vector<Node> d_variables;
+
+ /** The mapping from a node to its children */
+ std::map<Node, PartitionTrie> d_children;
+
+ /** Add variable v to the trie, indexed by
+ * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */
+ Node addNode(Node v, std::vector<Partition>& parts);
+
+ /** Get all the new regions of a partition and store in part
+ *
+ * This constructs a new partition, part, where each set in this partition
+ * corresponds to one leaf in the PartitionTrie pt.
+ * var_to_svar: map from variables to symmetry variables to use in part.
+ */
+ void getNewPartition(Partition& part,
+ PartitionTrie& pt,
+ std::map<Node, Node>& var_to_svar);
+};
/**
* This is the class to detect symmetries from input based on terms equality.
void getPartition(std::vector<std::vector<Node> >& parts, const std::vector<Node>& assertions);
private:
+ /** (canonical) symmetry breaking variables for each type */
+ std::map<TypeNode, std::vector<Node> > d_sb_vars;
/**
- * This is the class to store the partition,
- * where d_term store the term corresponding to the partition,
- * d_var_to_subvar is the mapping from the variable to the substitution
- * variable, and d_subvar_to_vars is the mapping from the substitution
- * variable to a list of variables forming a region of a partition.
+ * Get the index^th symmetry breaking variable for type tn in the above
+ * vector. These are fresh variables of type tn which are used for
+ * constructing a canonical form for terms considered by this class, and
+ * are used in the domains of partitions (Partition::d_subvar_to_vars).
+ * This variable is created by this method if it does not already exist.
*/
- class Partition
- {
- public:
- /** Term corresponding to the partition, e.g., x + y = 0 */
- Node d_term;
- /** Mapping between the variable and the substitution variable x -> w, y -> w,
- * z -> w */
- std::map<Node, Node> d_var_to_subvar;
-
- /** Mapping between the substitution variable and variables w-> { x, y, z } */
- std::map<Node, std::vector<Node> > d_subvar_to_vars;
- };
-
+ Node getSymBreakVariable(TypeNode tn, unsigned index);
/**
- * We build the partition trie indexed by
- * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a
- * partition trie is the new regions of a partition
+ * Get the index[tn]^th symmetry breaking variable for type tn using the
+ * above function and increment index[tn].
*/
- class PartitionTrie
- {
- public:
- /** Variables at the leave */
- std::vector<Node> d_variables;
-
- /** The mapping from a node to its children */
- std::map<Node, PartitionTrie> d_children;
-
- /** Add variable v to the trie, indexed by
- * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */
- void addNode(Node v, std::vector<Partition>& parts);
- void addNode(Node v, std::vector<Node>& subs);
-
- /** Get all the new regions of a partition and store in part */
- void getNewPartition(Partition& part, PartitionTrie& pt);
- };
-
+ Node getSymBreakVariableInc(TypeNode tn, std::map<TypeNode, unsigned>& index);
/** True and false constant nodes */
Node d_trueNode;
Partition detect(const std::vector<Node>& assertions);
/** Find symmetries in node */
- SymmetryDetect::Partition findPartitions(Node node);
+ Partition findPartitions(Node node);
/** Collect children of a node
* If the kind of node is associative, we will chain its children together.
* */
void collectChildren(Node node, std::vector<Node>& children);
- /** Print a partition */
- void printPartition(Partition p);
-
- /** Retrieve all variables from partitions and put in vars */
- void getVariables(std::vector<Partition>& partitions,
- std::unordered_set<Node, NodeHashFunction>& vars);
-
- /** Process singleton partitions and add all variables to vars
- * It collects all partitions with more than 1 variable and save it in
- * partitions first. And then it collects the substitution variable to
- * variable and to term mappings respectively from partitions with 1
- * variable and invokes matches function on the mappings to check
- * if any subset of the variables can be merged. If yes, they will be merged
- * and put in partitions. The remaining ones after the merge check will be
- * put in the partitions as well.
- * */
- void processSingletonPartitions(std::vector<Partition>& partitions,
- std::unordered_set<Node, NodeHashFunction>& vars);
-
- /** Do matches on singleton partitions
- * This function checks if any subset of the expressions corresponding to
- * substitution variables are equivalent under variables substitution.
- * If the expressions are equivalent, we will merge the variables corresponding
- * to the same substitution variables and put them in partitions.
- * For example, suppose we have subvar_to_var: {w1 -> u, w2 -> x, w3 -> y,
- * w4 -> z} and subvar_to_expr: {w1 -> u>2, w2 -> x>0, w3 -> y>0, w4 -> z>1}.
- * Since [x/w]>0 is equivalent [y/w]>0 but not equivalent to [z/w]>1 and [u/w]>2,
- * and [u/w]>2 is not equivalent to [z/w]>1, we would merge x and y and put
- * w5->{x, y} and also w1->{u}, w4->{z} in partitions.
- * */
- void matches(std::vector<Partition>& partitions,
- std::map<Node, Node>& subvar_to_var,
- std::map<Node, Node>& subvar_to_expr);
+ /** process partitions
+ *
+ * This method is called when we have detected symmetries for the children
+ * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative
+ * operator. The vector indices stores a list ( i_1...i_m ) such that
+ * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent
+ * for each j=1...m, where * is application of substitution. In particular,
+ * ( t_i_j * partition[i_j].d_var_to_subvar ) is equal to
+ * partitions[i_j].d_sterm for each j=1...m.
+ *
+ * This function calls mergePartitions on subsets of these indices for which
+ * it is possible to "merge" (see PartitionMerger). In particular, we consider
+ * subsets of indices whose corresponding partitions are of the form
+ * { w -> { x1...xn } }
+ * for each n. This means that partitions like { w -> { x1 } } and
+ * { w -> { x1 x2 } } are considered separately when merging.
+ */
+ void processPartitions(Kind k,
+ std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices,
+ std::unordered_set<unsigned>& active_indices);
+ /** merge partitions
+ *
+ * This method merges groups of partitions occurring in indices using the
+ * PartitionMerger class. Each merge updates one partition in partitions (the
+ * master index of the merge) and removes a set of indices from active_indices
+ * (the slave indices).
+ */
+ void mergePartitions(Kind k,
+ std::vector<Partition>& partitions,
+ const std::vector<unsigned>& indices,
+ std::unordered_set<unsigned>& active_indices);
};
+} // namespace symbreak
} // namespace passes
} // namespace preprocessing
} // namespace CVC4
projects / cvc5.git / commitdiff