**/
#include "preprocessing/passes/symmetry_detect.h"
+#include "expr/node_algorithm.h"
+#include "theory/quantifiers/alpha_equivalence.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
using namespace std;
+using namespace CVC4::kind;
namespace CVC4 {
namespace preprocessing {
}
}
+void Partition::addVariable(Node sv, Node v)
+{
+ d_subvar_to_vars[sv].push_back(v);
+ Assert(d_var_to_subvar.find(v) == d_var_to_subvar.end());
+ d_var_to_subvar[v] = sv;
+}
+
+void Partition::removeVariable(Node sv)
+{
+ std::map<Node, std::vector<Node> >::iterator its = d_subvar_to_vars.find(sv);
+ Assert(its != d_subvar_to_vars.end());
+ for (const Node& v : its->second)
+ {
+ Assert(d_var_to_subvar.find(v) != d_var_to_subvar.end());
+ d_var_to_subvar.erase(v);
+ }
+ d_subvar_to_vars.erase(sv);
+}
+
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 Partition::getVariables(std::vector<Node>& vars)
+{
+ for (const std::pair<const Node, Node>& p : d_var_to_subvar)
+ {
+ vars.push_back(p.first);
+ }
+}
+
+void Partition::getSubstitution(std::vector<Node>& vars,
+ std::vector<Node>& subs)
+{
+ for (const std::pair<const Node, Node>& p : d_var_to_subvar)
+ {
+ vars.push_back(p.first);
+ subs.push_back(p.second);
+ }
+}
void PartitionMerger::initialize(Kind k,
const std::vector<Partition>& partitions,
const std::vector<unsigned>& indices)
{
d_kind = k;
+ Trace("sym-dt-debug") << "Initialize partition merger..." << std::endl;
Trace("sym-dt-debug") << "Count variable occurrences..." << std::endl;
for (unsigned index : indices)
{
bool PartitionMerger::merge(std::vector<Partition>& partitions,
unsigned base_index,
- std::unordered_set<unsigned>& active_indices)
+ std::unordered_set<unsigned>& active_indices,
+ std::vector<unsigned>& merged_indices)
{
Assert(base_index < partitions.size());
d_master_base_index = base_index;
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;
+ if (Trace.isOn("sym-dt-debug"))
+ {
+ Trace("sym-dt-debug")
+ << " ...merged: " << merge_var << " from indices [ ";
+ for (unsigned ni : new_indices)
+ {
+ Trace("sym-dt-debug") << ni << " ";
+ }
+ Trace("sym-dt-debug") << "]" << std::endl;
+ }
+ merged_indices.insert(
+ merged_indices.end(), new_indices.begin(), new_indices.end());
Assert(!merge_var.isNull());
merged = true;
success = true;
return false;
}
Trace("sym-dt-debug2") << "merge " << curr_index << " / " << d_indices.size()
- << std::endl;
+ << ", merge var : " << merge_var
+ << ", upper bound for #occ of merge_var : "
+ << num_merge_var_max << std::endl;
// try to include this index
unsigned index = d_indices[curr_index];
Assert(active_indices.find(index) != active_indices.end());
// check whether it can merge
Partition& p = partitions[index];
+ Trace("sym-dt-debug2") << "current term is " << p.d_term << std::endl;
Assert(p.d_subvar_to_vars.size() == 1);
std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second;
bool include_success = true;
include_success = false;
}
}
- else if (!include_success && !merge_var.isNull())
+ else if (!merge_var.isNull()
+ && p.d_var_to_subvar.find(merge_var) != p.d_var_to_subvar.end())
{
// decrement
num_merge_var_max--;
// can now include in the base
d_base_vars.insert(merge_var);
Trace("sym-dt-debug") << "found symmetry : { ";
- for (const unsigned& i : new_indices)
+ for (unsigned i : new_indices)
{
Assert(d_base_indices.find(i) == d_base_indices.end());
d_base_indices.insert(i);
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;
+ p.addVariable(sb_v, merge_var);
return true;
}
if (mergeNewVar(curr_index + 1,
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)
+SymmetryDetect::SymmetryDetect() : d_tsym_id_counter(1)
{
- 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];
+ d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+ d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
}
Partition SymmetryDetect::detect(const vector<Node>& assertions)
d_sb_vars[tn].clear();
it = d_sb_vars.find(tn);
}
+ NodeManager* nm = NodeManager::currentNM();
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);
+ Node fresh_var = nm->mkBoundVar(ss.str(), tn);
it->second.push_back(fresh_var);
}
return it->second[index];
return getSymBreakVariable(tn, new_index);
}
-void SymmetryDetect::getPartition(vector<vector<Node> >& parts,
- const vector<Node>& assertions)
+void SymmetryDetect::compute(std::vector<std::vector<Node> >& part,
+ const std::vector<Node>& assertions)
{
Partition p = detect(assertions);
+ std::vector<std::vector<Node> > parts;
for (map<Node, vector<Node> >::const_iterator subvar_to_vars_it =
p.d_subvar_to_vars.begin();
subvar_to_vars_it != p.d_subvar_to_vars.end();
parts.push_back(subvar_to_vars_it->second);
}
}
+void SymmetryDetect::computeTerms(std::vector<std::vector<Node> >& sterms,
+ const std::vector<Node>& assertions)
+{
+ Partition p = detect(assertions);
+
+ for (const std::pair<const Node, std::vector<Node> > sp : p.d_subvar_to_vars)
+ {
+ if (sp.second.size() > 1)
+ {
+ // A naive method would do sterms.push_back(sp.second), that is, say that
+ // the variables themselves are symmetric terms. However, the following
+ // code finds some subterms of assertions that are symmetric under this
+ // set in the variable partition. For example, for the input:
+ // f(x)+f(y) >= 0
+ // naively {x, y} are reported as symmetric terms, but below ensures we
+ // say {f(x), f(y)} are reported as symmetric terms instead.
+ Node sv = sp.first;
+ Trace("sym-dt-tsym-cons")
+ << "Construct term symmetry from " << sp.second << "..." << std::endl;
+ // choose an arbitrary term symmetry
+ std::vector<unsigned>& tsids = d_var_to_tsym_ids[sp.second[0]];
+ if (tsids.empty())
+ {
+ // no (ground) term symmetries, just use naive
+ sterms.push_back(sp.second);
+ }
+ else
+ {
+ unsigned tsymId = tsids[tsids.size() - 1];
+ Trace("sym-dt-tsym-cons") << "...use tsym id " << tsymId << std::endl;
+ // get the substitution
+ std::vector<Node> vars;
+ std::vector<Node> subs;
+ for (const Node& v : sp.second)
+ {
+ vars.push_back(v);
+ subs.push_back(sv);
+ }
+ std::vector<Node>& tsym = d_tsyms[tsymId];
+ // map terms in this symmetry to their final form
+ std::vector<unsigned> tsym_indices;
+ std::vector<Node> tsym_terms;
+ for (unsigned j = 0, size = tsym.size(); j < size; j++)
+ {
+ Node tst = tsym[j];
+ Node tsts = tst.substitute(
+ vars.begin(), vars.end(), subs.begin(), subs.end());
+ tsym_indices.push_back(j);
+ tsym_terms.push_back(tsts);
+ }
+ // take into account alpha-equivalence
+ std::map<Node, std::vector<unsigned> > t_to_st;
+ computeAlphaEqTerms(tsym_indices, tsym_terms, t_to_st);
+ Node tshUse;
+ for (const std::pair<const Node, std::vector<unsigned> >& tsh : t_to_st)
+ {
+ Trace("sym-dt-tsym-cons-debug")
+ << " " << tsh.first << " -> #" << tsh.second.size() << std::endl;
+ if (tsh.second.size() > 1)
+ {
+ tshUse = tsh.first;
+ break;
+ }
+ }
+ if (!tshUse.isNull())
+ {
+ std::vector<Node> tsymCons;
+ for (unsigned j : t_to_st[tshUse])
+ {
+ tsymCons.push_back(tsym[j]);
+ }
+ Trace("sym-dt-tsym-cons") << "...got " << tsymCons << std::endl;
+ sterms.push_back(tsymCons);
+ }
+ }
+ }
+ }
+}
+
+/**
+ * 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 are 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;
+};
Partition SymmetryDetect::findPartitions(Node node)
{
// If node is a variable
if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE)
{
- vector<Node> vars;
TypeNode type = node.getType();
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;
+ p.addVariable(fresh_var, node);
d_term_partition[node] = p;
return p;
}
isAssocComm = theory::quantifiers::TermUtil::isComm(k);
}
- // Children of node
- vector<Node> children;
- // Partitions of children
- vector<Partition> partitions;
-
// Get all children of node
Trace("sym-dt-debug") << "[sym-dt] collectChildren for: " << node
- << " with operator " << node.getKind() << endl;
+ << " with kind " << node.getKind() << endl;
+ // Children of node
+ std::vector<Node> children;
+ bool operatorChild = false;
+ if (node.getKind() == APPLY_UF)
+ {
+ // compute for the operator
+ children.push_back(node.getOperator());
+ operatorChild = true;
+ }
if (!isAssocComm)
{
children.insert(children.end(), node.begin(), node.end());
}
Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl;
+ // Partitions of children
+ std::vector<Partition> partitions;
// Create partitions for children
std::unordered_set<unsigned> active_indices;
- for (vector<Node>::iterator children_it = children.begin();
- children_it != children.end();
- ++children_it)
+ for (const Node& c : children)
{
active_indices.insert(partitions.size());
- partitions.push_back(findPartitions(*children_it));
+ partitions.push_back(findPartitions(c));
}
if (Trace.isOn("sym-dt-debug"))
{
if (isAssocComm)
{
- // map substituted terms to indices in partitions
- std::map<Node, std::vector<unsigned> > sterm_to_indices;
+ // get the list of indices and terms
+ std::vector<unsigned> indices;
+ std::vector<Node> sterms;
for (unsigned j = 0, size = partitions.size(); j < size; j++)
{
- if (!partitions[j].d_sterm.isNull())
+ Node st = partitions[j].d_sterm;
+ if (!st.isNull())
{
- sterm_to_indices[partitions[j].d_sterm].push_back(j);
+ indices.push_back(j);
+ sterms.push_back(st);
}
}
+ // now, compute terms to indices
+ std::map<Node, std::vector<unsigned> > sterm_to_indices;
+ computeAlphaEqTerms(indices, sterms, sterm_to_indices);
for (const std::pair<Node, std::vector<unsigned> >& sti : sterm_to_indices)
{
Trace("sym-dt-debug") << std::endl;
}
// merge children, remove active indices
- processPartitions(k, partitions, sti.second, active_indices);
+ std::vector<Node> fixedSVar;
+ std::vector<Node> fixedVar;
+ processPartitions(
+ k, partitions, sti.second, active_indices, fixedSVar, fixedVar);
}
}
// 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)
- {
- 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)
+ for (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)
{
- 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);
+ << "...process " << pas.first << " -> " << pas.second << std::endl;
// add all vars to partition trie classifier
for (const Node& c : pas.second)
{
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;
- }
}
- // reconstruct the partition
- for (unsigned j = 0, size = f_vars.size(); j < size; j++)
+ Trace("sym-dt-debug") << "...term : " << pa.d_sterm << std::endl;
+ }
+
+ PartitionTrie pt;
+ std::map<TypeNode, unsigned> type_index;
+ type_index.clear();
+ // the indices we need to reconstruct
+ std::map<unsigned, bool> rcons_indices;
+ // Build the partition trie
+ std::sort(all_vars.begin(), all_vars.end());
+ // for each variable
+ for (const Node& n : all_vars)
+ {
+ Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << n
+ << "} to the partition trie, #partitions = "
+ << active_indices.size() << "..." << endl;
+ std::vector<Node> subvars;
+ std::vector<unsigned> useVarInd;
+ Node useVar;
+ for (unsigned i : active_indices)
{
- Node v = f_vars[j];
- Node new_v = f_subs[j];
- if (new_v != v)
+ Partition& pa = partitions[i];
+ std::map<Node, Node>::iterator var_sub_it = pa.d_var_to_subvar.find(n);
+ if (var_sub_it != pa.d_var_to_subvar.end())
{
- 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);
+ Node v = var_sub_it->second;
+ subvars.push_back(v);
+ if (useVar.isNull() || v == useVar)
+ {
+ useVar = v;
+ useVarInd.push_back(i);
+ }
+ else
+ {
+ // will need to reconstruct the child
+ rcons_indices[i] = true;
+ }
+ }
+ else
+ {
+ subvars.push_back(Node::null());
}
}
- 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)
+ // all variables should occur in at least one child
+ Assert(!useVar.isNull());
+ Trace("sym-dt-debug")
+ << "[sym-dt] Symmetry breaking variables for the variable " << n << ": "
+ << subvars << endl;
+ // add to the trie
+ PartitionTrie* curr = &pt;
+ for (const Node& c : subvars)
+ {
+ curr = &(curr->d_children[c]);
+ }
+ curr->d_variables.push_back(n);
+
+ // allocate the necessary variable
+ bool usingUseVar = false;
+ if (curr->d_variables.size() > 1)
+ {
+ // must use the previous
+ Node an = curr->d_variables[0];
+ useVar = p.d_var_to_subvar[an];
+ Trace("sym-dt-debug") << "...use var from " << an << "." << std::endl;
+ }
+ else if (useVar.isNull()
+ || p.d_subvar_to_vars.find(useVar) != p.d_subvar_to_vars.end())
{
- Assert(!pa.d_sterm.isNull());
- schildren.push_back(pa.d_sterm);
+ Trace("sym-dt-debug") << "...allocate new var." << std::endl;
+ // must allocate new
+ TypeNode ntn = n.getType();
+ do
+ {
+ useVar = getSymBreakVariableInc(ntn, type_index);
+ } while (p.d_subvar_to_vars.find(useVar) != p.d_subvar_to_vars.end());
}
else
{
- Assert(i < schildren.size());
- schildren[i] = pa.d_sterm;
+ Trace("sym-dt-debug") << "...reuse var." << std::endl;
+ usingUseVar = true;
+ }
+ if (!usingUseVar)
+ {
+ // can't use the useVar, indicate indices for reconstruction
+ for (unsigned ui : useVarInd)
+ {
+ rcons_indices[ui] = true;
+ }
}
- Trace("sym-dt-debug") << "...got : " << pa.d_sterm << std::endl;
- active_partitions.push_back(pa);
+ Trace("sym-dt-debug") << "[sym-dt] Map : " << n << " -> " << useVar
+ << std::endl;
+ p.addVariable(useVar, n);
}
- 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)
+ std::vector<Node> pvars;
+ std::vector<Node> psubs;
+ if (!rcons_indices.empty())
+ {
+ p.getSubstitution(pvars, psubs);
+ }
+
+ // Reconstruct the substituted node
+ p.d_term = node;
+ std::vector<Node> schildren;
+ if (!isAssocComm)
{
- Node an = pt.addNode(n, active_partitions);
- // if this is a new node, allocate
- if (an == n)
+ Assert(active_indices.size() == children.size());
+ // order matters, and there is no chance we merged children
+ schildren.resize(children.size());
+ }
+ for (unsigned i : active_indices)
+ {
+ Partition& pa = partitions[i];
+ Node sterm = pa.d_sterm;
+ Assert(!sterm.isNull());
+ if (rcons_indices.find(i) != rcons_indices.end())
+ {
+ // must reconstruct via a substitution
+ Trace("sym-dt-debug2") << " reconstruct index " << i << std::endl;
+ sterm = pa.d_term.substitute(
+ pvars.begin(), pvars.end(), psubs.begin(), psubs.end());
+ }
+ if (isAssocComm)
+ {
+ schildren.push_back(sterm);
+ }
+ else
{
- Node new_v = getSymBreakVariableInc(n.getType(), type_index);
- var_to_svar[n] = new_v;
+ Assert(i < schildren.size());
+ schildren[i] = sterm;
}
}
- // 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;
}
else
{
- if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+ if (node.getMetaKind() == metakind::PARAMETERIZED && !operatorChild)
{
schildren.insert(schildren.begin(), node.getOperator());
}
<< node.getType() << std::endl;
Assert(p.d_sterm.getType() == node.getType());
+ // normalize: ensures that variable lists are sorted
p.normalize();
d_term_partition[node] = p;
Partition::printPartition("sym-dt-debug", p);
} while (!visit.empty());
}
+void SymmetryDetect::computeAlphaEqTerms(
+ const std::vector<unsigned>& indices,
+ const std::vector<Node>& sterms,
+ std::map<Node, std::vector<unsigned> >& sterm_to_indices)
+{
+ Assert(indices.size() == sterms.size());
+ // also store quantified formulas, since these may be alpha-equivalent
+ std::vector<unsigned> quant_sterms;
+ for (unsigned j = 0, size = indices.size(); j < size; j++)
+ {
+ Node st = sterms[j];
+ Assert(!st.isNull());
+ if (st.getKind() == FORALL)
+ {
+ quant_sterms.push_back(j);
+ }
+ else
+ {
+ sterm_to_indices[st].push_back(indices[j]);
+ }
+ }
+ // process the quantified formulas
+ if (quant_sterms.size() == 1)
+ {
+ // only one quantified formula, won't be alpha equivalent
+ unsigned j = quant_sterms[0];
+ sterm_to_indices[sterms[j]].push_back(indices[j]);
+ }
+ else if (!quant_sterms.empty())
+ {
+ theory::quantifiers::AlphaEquivalenceDb aedb(&d_tcanon);
+ for (unsigned j : quant_sterms)
+ {
+ // project via alpha equivalence
+ Node st = sterms[j];
+ Node st_ae = aedb.addTerm(st);
+ sterm_to_indices[st_ae].push_back(indices[j]);
+ }
+ }
+}
+
/** A basic trie for storing vectors of arguments */
class NodeTrie
{
public:
- NodeTrie() : d_value(-1) {}
- /** value of this node, -1 if unset */
- int d_value;
+ NodeTrie() {}
+ /** value at this node*/
+ std::vector<unsigned> d_value;
/** children of this node */
std::map<Node, NodeTrie> d_children;
/** clear the children */
{
if (index == args.size())
{
- if (d_value == -1)
- {
- d_value = static_cast<int>(value);
- }
- return d_value;
+ d_value.push_back(value);
+ return d_value[0];
}
return d_children[args[index]].add(value, args, index + 1);
}
Kind k,
std::vector<Partition>& partitions,
const std::vector<unsigned>& indices,
- std::unordered_set<unsigned>& active_indices)
+ std::unordered_set<unsigned>& active_indices,
+ std::vector<Node>& fixedSVar,
+ std::vector<Node>& fixedVar)
{
Assert(!indices.empty());
unsigned first_index = indices[0];
-
+ if (Trace.isOn("sym-dt-debug"))
+ {
+ Trace("sym-dt-debug") << "[sym-dt] process partitions for ";
+ for (unsigned i : indices)
+ {
+ Trace("sym-dt-debug") << i << " ";
+ }
+ Trace("sym-dt-debug") << std::endl;
+ }
unsigned num_sb_vars = partitions[first_index].d_subvar_to_vars.size();
- if (num_sb_vars != 1)
+ if (num_sb_vars == 0)
{
- // can only handle symmetries that are classified by { n }
+ // no need to merge
+ Trace("sym-dt-debug") << "...trivial (no sym vars)" << std::endl;
+ return;
+ }
+ if (num_sb_vars > 1)
+ {
+ // see if we can drop, e.g. {x}{A}, {x}{B} ---> {A}, {B}
+
+ std::map<Node, NodeTrie> svarTrie;
+ std::map<Node, std::map<unsigned, std::vector<unsigned> > > svarEqc;
+
+ for (unsigned j = 0, size = indices.size(); j < size; j++)
+ {
+ unsigned index = indices[j];
+ Partition& p = partitions[index];
+ for (const std::pair<const Node, std::vector<Node> > ps :
+ p.d_subvar_to_vars)
+ {
+ Node sv = ps.first;
+ unsigned res = svarTrie[sv].add(index, ps.second);
+ svarEqc[sv][res].push_back(index);
+ }
+ }
+ Trace("sym-dt-debug")
+ << "...multiple symmetry breaking variables, regroup and drop"
+ << std::endl;
+ unsigned minGroups = indices.size();
+ Node svarMin;
+ for (const std::pair<const Node,
+ std::map<unsigned, std::vector<unsigned> > > sve :
+ svarEqc)
+ {
+ if (Trace.isOn("sym-dt-debug"))
+ {
+ Trace("sym-dt-debug") << "For " << sve.first << " : ";
+ for (const std::pair<const unsigned, std::vector<unsigned> > svee :
+ sve.second)
+ {
+ Trace("sym-dt-debug") << "{ ";
+ for (unsigned i : svee.second)
+ {
+ Trace("sym-dt-debug") << i << " ";
+ }
+ Trace("sym-dt-debug") << "}";
+ }
+ }
+ unsigned ngroups = sve.second.size();
+ Trace("sym-dt-debug") << ", #groups=" << ngroups << std::endl;
+ if (ngroups < minGroups)
+ {
+ minGroups = ngroups;
+ svarMin = sve.first;
+ if (minGroups == 1)
+ {
+ break;
+ }
+ }
+ }
+ if (minGroups == indices.size())
+ {
+ // can only handle symmetries that are classified by { n }
+ Trace("sym-dt-debug") << "...failed to merge (multiple symmetry breaking "
+ "vars with no groups)"
+ << std::endl;
+ return;
+ }
+ // recursive call for each group
+ for (const std::pair<unsigned, std::vector<unsigned> >& svee :
+ svarEqc[svarMin])
+ {
+ Assert(!svee.second.empty());
+ unsigned firstIndex = svee.second[0];
+ unsigned nfvars = 0;
+ Trace("sym-dt-debug") << "Recurse, fixing " << svarMin << " -> { ";
+ // add the list of fixed variables
+ for (const Node& v : partitions[firstIndex].d_subvar_to_vars[svarMin])
+ {
+ Trace("sym-dt-debug") << v << " ";
+ fixedSVar.push_back(svarMin);
+ fixedVar.push_back(v);
+ nfvars++;
+ }
+ Trace("sym-dt-debug") << "}" << std::endl;
+
+ // remove it from each of the partitions to process
+ for (unsigned pindex : svee.second)
+ {
+ partitions[pindex].removeVariable(svarMin);
+ }
+
+ // recursive call
+ processPartitions(
+ k, partitions, svee.second, active_indices, fixedSVar, fixedVar);
+
+ // remove the list of fixed variables
+ for (unsigned k = 0; k < nfvars; k++)
+ {
+ fixedVar.pop_back();
+ fixedSVar.pop_back();
+ }
+ }
return;
}
// separate by number of variables
}
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);
}
+ // now, re-add the fixed variables
+ if (!fixedVar.empty())
+ {
+ for (unsigned j = 0, size = indices.size(); j < size; j++)
+ {
+ unsigned index = indices[j];
+ // if still active
+ if (active_indices.find(index) != active_indices.end())
+ {
+ for (unsigned i = 0, size = fixedSVar.size(); i < size; i++)
+ {
+ // add variable
+ partitions[index].addVariable(fixedSVar[i], fixedVar[i]);
+ }
+ }
+ }
+ }
}
void SymmetryDetect::mergePartitions(
}
if (Trace.isOn("sym-dt-debug"))
{
- Trace("sym-dt-debug") << " merge indices ";
+ Trace("sym-dt-debug") << "--- mergePartitions..." << std::endl;
+ Trace("sym-dt-debug") << " indices ";
for (unsigned i : indices)
{
Trace("sym-dt-debug") << i << " ";
PartitionMerger pm;
pm.initialize(k, partitions, indices);
- // TODO (#2198): process indices for distinct types separately
for (unsigned index : indices)
{
- if (pm.merge(partitions, index, active_indices))
+ Node mterm = partitions[index].d_term;
+ std::vector<unsigned> merged_indices;
+ if (pm.merge(partitions, index, active_indices, merged_indices))
{
- Trace("sym-dt-debug") << " ......we merged, recurse" << std::endl;
+ // get the symmetric terms, these will be used when doing symmetry
+ // breaking
+ std::vector<Node> symTerms;
+ // include the term from the base index
+ symTerms.push_back(mterm);
+ for (unsigned mi : merged_indices)
+ {
+ Node st = partitions[mi].d_term;
+ symTerms.push_back(st);
+ }
+ Trace("sym-dt-debug") << " ......merged " << symTerms << std::endl;
+ std::vector<Node> vars;
+ partitions[index].getVariables(vars);
+ storeTermSymmetry(symTerms, vars);
+ Trace("sym-dt-debug") << " ......recurse" << std::endl;
std::vector<unsigned> rem_indices;
for (unsigned ii : indices)
{
}
}
+void SymmetryDetect::storeTermSymmetry(const std::vector<Node>& symTerms,
+ const std::vector<Node>& vars)
+{
+ Trace("sym-dt-tsym") << "*** Term symmetry : " << symTerms << std::endl;
+ Trace("sym-dt-tsym") << "*** Over variables : " << vars << std::endl;
+ // cannot have free variable
+ if (expr::hasFreeVar(symTerms[0]))
+ {
+ Trace("sym-dt-tsym") << "...free variable, do not allocate." << std::endl;
+ return;
+ }
+
+ unsigned tid = d_tsym_id_counter;
+ Trace("sym-dt-tsym") << "...allocate id " << tid << std::endl;
+ d_tsym_id_counter = d_tsym_id_counter + 1;
+ // allocate the term symmetry
+ d_tsyms[tid] = symTerms;
+ d_tsym_to_vars[tid] = vars;
+ for (const Node& v : vars)
+ {
+ d_var_to_tsym_ids[v].push_back(tid);
+ }
+}
+
} // namespace symbreak
} // namespace passes
} // namespace preprocessing
#include <string>
#include <vector>
#include "expr/node.h"
+#include "theory/quantifiers/term_canonize.h"
namespace CVC4 {
namespace preprocessing {
* { w-> { x, y } }
*/
std::map<Node, std::vector<Node> > d_subvar_to_vars;
- /** sorts the ranges of d_subvar_to_vars. */
+ /** Add variable v to d_subvar_to_vars[sv]. */
+ void addVariable(Node sv, Node v);
+ /** Remove variable sv from the domain of d_subvar_to_vars. */
+ void removeVariable(Node sv);
+ /** Sorts the ranges of d_subvar_to_vars. */
void normalize();
/** Print a partition */
static void printPartition(const char* c, Partition p);
+ /** get variables */
+ void getVariables(std::vector<Node>& vars);
+ /** get substitution */
+ void getSubstitution(std::vector<Node>& vars, std::vector<Node>& subs);
};
/** partition merger
*/
bool merge(std::vector<Partition>& partitions,
unsigned base_index,
- std::unordered_set<unsigned>& active_indices);
+ std::unordered_set<unsigned>& active_indices,
+ std::vector<unsigned>& merged_indices);
private:
/** the kind of the node we are consdiering */
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.
- * */
+ * This is the class to detect symmetries between variables or terms relative
+ * to a set of input assertions.
+ */
class SymmetryDetect
{
public:
- /**
- * Constructor
- * */
- SymmetryDetect()
- {
- d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
- d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
- }
+ /** constructor */
+ SymmetryDetect();
/**
* Destructor
~SymmetryDetect() {}
/** Get the final partition after symmetry detection.
- * If a vector in parts contains two variables x and y,
+ *
+ * If a vector in sterms contains two variables x and y,
* then assertions and assertions { x -> y, y -> x } are
* equisatisfiable.
* */
- void getPartition(std::vector<std::vector<Node> >& parts, const std::vector<Node>& assertions);
+ void compute(std::vector<std::vector<Node> >& part,
+ const std::vector<Node>& assertions);
+
+ /** Get the final partition after symmetry detection.
+ *
+ * If a vector in sterms contains two terms t and s,
+ * then assertions and assertions { t -> s, s -> t } are
+ * equisatisfiable.
+ * */
+ void computeTerms(std::vector<std::vector<Node> >& sterms,
+ const std::vector<Node>& assertions);
private:
/** (canonical) symmetry breaking variables for each type */
Node d_trueNode;
Node d_falseNode;
+ /** term canonizer (for quantified formulas) */
+ theory::quantifiers::TermCanonize d_tcanon;
+
/** Cache for partitions */
std::map<Node, Partition> d_term_partition;
* */
void collectChildren(Node node, std::vector<Node>& children);
+ /** Compute alpha equivalent terms
+ *
+ * This is used for determining pairs of terms in sterms that are
+ * alpha-equivalent. In detail, this constructs sterm_to_indices such that if
+ * sterm_to_indices[t] contains an index i, then there exists a k such that
+ * indices[k] = i and sterms[k] is alpha-equivalent to t, and sterm_to_indices
+ * contains indices[k] for each k=1,...,indicies.size()-1. For example,
+ * computeAlphaEqTerms( { 0, 3, 7 }, { Q(a), forall x. P(x), forall y. P(y) }
+ * may construct sterm_to_indices such that
+ * sterm_to_indices[Q(a)] -> { 0 }
+ * sterm_to_indices[forall x. P(x)] -> { 3, 7 }
+ */
+ void computeAlphaEqTerms(
+ const std::vector<unsigned>& indices,
+ const std::vector<Node>& sterms,
+ std::map<Node, std::vector<unsigned> >& sterm_to_indices);
/** process partitions
*
* This method is called when we have detected symmetries for the children
void processPartitions(Kind k,
std::vector<Partition>& partitions,
const std::vector<unsigned>& indices,
- std::unordered_set<unsigned>& active_indices);
+ std::unordered_set<unsigned>& active_indices,
+ std::vector<Node>& fixedSVar,
+ std::vector<Node>& fixedVar);
/** merge partitions
*
* This method merges groups of partitions occurring in indices using the
std::vector<Partition>& partitions,
const std::vector<unsigned>& indices,
std::unordered_set<unsigned>& active_indices);
+ //-------------------for symmetry breaking terms
+ /** symmetry breaking id counter */
+ unsigned d_tsym_id_counter;
+ /** list of term symmetries */
+ std::map<unsigned, std::vector<Node> > d_tsyms;
+ /** list of term symmetries */
+ std::map<unsigned, std::vector<Node> > d_tsym_to_vars;
+ /** variables to ids */
+ std::map<Node, std::vector<unsigned> > d_var_to_tsym_ids;
+ /** store term symmetry */
+ void storeTermSymmetry(const std::vector<Node>& symTerms,
+ const std::vector<Node>& vars);
+ //-------------------end for symmetry breaking terms
};
+
} // namespace symbreak
} // namespace passes
} // namespace preprocessing
projects / cvc5.git / commitdiff