From: Andrew Reynolds Date: Mon, 23 Jul 2018 22:39:12 +0000 (-0500) Subject: Generalize symmetry detection for 1 symmetry variable mapped to n input variables... X-Git-Tag: cvc5-1.0.0~4874 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3471e731b8538a906e37f8aeb4b0301598b34eff;p=cvc5.git Generalize symmetry detection for 1 symmetry variable mapped to n input variables (#1888) --- diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp index e1b6b4274..c32057d5f 100644 --- a/src/preprocessing/passes/symmetry_breaker.cpp +++ b/src/preprocessing/passes/symmetry_breaker.cpp @@ -129,7 +129,7 @@ PreprocessingPassResult SymBreakerPass::applyInternal( Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl; // detect symmetries std::vector> part; - SymmetryDetect symd; + symbreak::SymmetryDetect symd; symd.getPartition(part, assertionsToPreprocess->ref()); if (Trace.isOn("sym-break-pass")) { diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp index 683bec6ac..a1273b1d9 100644 --- a/src/preprocessing/passes/symmetry_detect.cpp +++ b/src/preprocessing/passes/symmetry_detect.cpp @@ -21,22 +21,484 @@ using namespace std; namespace CVC4 { namespace preprocessing { namespace passes { +namespace symbreak { -SymmetryDetect::Partition SymmetryDetect::detect(const vector& 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(k); ++i) + { + result *= (n - i + 1); + result /= i; + } + return result; +} + +/** mk associative node + * + * This returns (a normal form for) the term ( 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& 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 >::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::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 > p : d_subvar_to_vars) + { + std::sort(p.second.begin(), p.second.end()); + } +} + +void PartitionMerger::initialize(Kind k, + const std::vector& partitions, + const std::vector& 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& 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& o : d_occurs_count) + { + Trace("sym-dt-debug") + << " " << o.first << " -> " << o.second << std::endl; + } + } +} + +bool PartitionMerger::merge(std::vector& partitions, + unsigned base_index, + std::unordered_set& 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& 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 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& new_indices, + Node& merge_var, + unsigned num_merge_var_max, + std::vector& partitions, + std::unordered_set& 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& 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 children; + children.push_back(p.d_term); + std::vector 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& 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::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& partitions) +{ + Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << target_var + << "} to the partition trie, #partitions = " + << partitions.size() << "..." << endl; + Assert(!partitions.empty()); + vector subvars; + + for (vector::iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + map::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& 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 >::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& index) +{ + // ensure we use a new index for this variable + unsigned new_index = 0; + std::map::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 >& parts, const vector& assertions) { @@ -51,20 +513,20 @@ void SymmetryDetect::getPartition(vector >& parts, } } -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::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; } @@ -75,22 +537,35 @@ SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node) { vector 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 children; @@ -98,193 +573,206 @@ SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node) vector 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 active_indices; for (vector::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 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::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& partitions, - map& subvar_to_var, - map& 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 repls; - // Variables that have been merged - unordered_set merged; - // Put the variable in repls - repls.push_back((subvar_to_expr.begin())->first); - - for (map::iterator expr_it1 = subvar_to_expr.begin(); - expr_it1 != subvar_to_expr.end(); - ++expr_it1) + // map substituted terms to indices in partitions + std::map > 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 subs; - vector 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::iterator expr_it2 = subvar_to_expr.begin(); - expr_it2 != subvar_to_expr.end(); - ++expr_it2) + for (const std::pair >& 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 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& partitions, unordered_set& 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 subvar_to_var; - // Mapping between the substitution variable to the actual expression - map subvar_to_expr; - // Partitions that have 2 or more variables - vector new_partitions; - - // Collect singleton partitions: subvar_to_expr, subvar_to_var, and variables - for (vector::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 all_vars; + std::map type_index; + std::vector 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 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 f_vars; + std::vector f_subs; + // add to overall list of variables + for (const pair >& 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& 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 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& 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 visit; @@ -298,7 +786,8 @@ void SymmetryDetect::collectChildren(Node node, vector& children) 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) { @@ -313,147 +802,163 @@ void SymmetryDetect::collectChildren(Node node, vector& children) } 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 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& args, + unsigned index = 0) { - vector 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::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::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(value); + } + return d_value; } + return d_children[args[index]].add(value, args, index + 1); } -} +}; -void SymmetryDetect::getVariables(vector& partitions, - unordered_set& vars) +void SymmetryDetect::processPartitions( + Kind k, + std::vector& partitions, + const std::vector& indices, + std::unordered_set& active_indices) { - for (vector::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 >::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& partitions) -{ - Trace("sym-dt") << "[sym-dt] Add a variable {" << target_var - << "} to the partition trie..." << endl; - vector subvars; - - for (vector::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 > nv_indices; + for (unsigned j = 0, size = indices.size(); j < size; j++) { - map::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 >& nvi : + nv_indices) + { + if (nvi.second.size() <= 1) { - for (map >::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 nvis; + for (unsigned index : nvi.second) { - subvars.resize(subvars.size()+(*part_it).d_subvar_to_vars.size()); + Partition& p = partitions[index]; + std::vector& 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 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& subvars) +void SymmetryDetect::mergePartitions( + Kind k, + std::vector& partitions, + const std::vector& indices, + std::unordered_set& active_indices) { - if (subvars.empty()) + if (indices.size() <= 1) { - d_variables.push_back(target_var); + return; } - else + if (Trace.isOn("sym-dt-debug")) { - vector new_subs; - map::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 >::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::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 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 diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h index 758169611..9a5f83868 100644 --- a/src/preprocessing/passes/symmetry_detect.h +++ b/src/preprocessing/passes/symmetry_detect.h @@ -25,6 +25,185 @@ 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 d_var_to_subvar; + + /** + * Mapping between the symmetry breaking variables and variables, e.g. + * { w-> { x, y } } + */ + std::map > 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 ( 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& partitions, + const std::vector& 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& partitions, + unsigned base_index, + std::unordered_set& active_indices); + + private: + /** the kind of the node we are consdiering */ + Kind d_kind; + /** indices we are considering */ + std::vector d_indices; + /** count the number of times each variable occurs */ + std::map d_occurs_count; + /** the number of times each variable occurs up to the given index */ + std::map > 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 d_base_indices; + /** the free variables that occur in the current symmetry (the set X*)*/ + std::unordered_set 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 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& new_indices, + Node& merge_var, + unsigned num_merge_var_max, + std::vector& partitions, + std::unordered_set& 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 d_variables; + + /** The mapping from a node to its children */ + std::map 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& 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& var_to_svar); +}; /** * This is the class to detect symmetries from input based on terms equality. @@ -54,49 +233,21 @@ class SymmetryDetect void getPartition(std::vector >& parts, const std::vector& assertions); private: + /** (canonical) symmetry breaking variables for each type */ + std::map > 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 d_var_to_subvar; - - /** Mapping between the substitution variable and variables w-> { x, y, z } */ - std::map > 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 d_variables; - - /** The mapping from a node to its children */ - std::map 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& parts); - void addNode(Node v, std::vector& 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& index); /** True and false constant nodes */ Node d_trueNode; @@ -115,7 +266,7 @@ class SymmetryDetect Partition detect(const std::vector& 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. @@ -124,40 +275,40 @@ class SymmetryDetect * */ void collectChildren(Node node, std::vector& children); - /** Print a partition */ - void printPartition(Partition p); - - /** Retrieve all variables from partitions and put in vars */ - void getVariables(std::vector& partitions, - std::unordered_set& 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& partitions, - std::unordered_set& 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& partitions, - std::map& subvar_to_var, - std::map& subvar_to_expr); + /** process partitions + * + * This method is called when we have detected symmetries for the children + * of a term t of the form ( 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& partitions, + const std::vector& indices, + std::unordered_set& 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& partitions, + const std::vector& indices, + std::unordered_set& active_indices); }; +} // namespace symbreak } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 958fec175..71256e3d8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4330,9 +4330,9 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); - if (options::symmetryBreakerExp()) + if (options::symmetryBreakerExp() && !options::incrementalSolving()) { - // apply symmetry breaking + // apply symmetry breaking if not in incremental mode d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions); } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 5bf284dff..cf06dfa45 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -817,18 +817,18 @@ bool TermUtil::isNegate(Kind k) } bool TermUtil::isAssoc( Kind k ) { - return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS - || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR - || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT - || k == STRING_CONCAT || k == UNION || k == INTERSECTION || k == JOIN - || k == PRODUCT; + return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR + || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT + || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR + || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT + || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT; } bool TermUtil::isComm( Kind k ) { - return k == EQUAL || k == PLUS || k == MULT || k == AND || k == OR || k == XOR - || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND - || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR - || k == UNION || k == INTERSECTION; + return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND + || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT + || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR + || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION; } bool TermUtil::isNonAdditive( Kind k ) {