From 83be77ff113cbc0357796fb8121091eed2c95ab1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 19:51:06 -0500 Subject: Improvements and fixes for symmetry detection and breaking (#2459) This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do: - Alpha equivalence to recognize symmetries between quantified formulas, - A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol, - Symmetry breaking for maximal subterms instead of variables. --- src/preprocessing/passes/symmetry_breaker.cpp | 71 ++- src/preprocessing/passes/symmetry_detect.cpp | 712 +++++++++++++++++++------- src/preprocessing/passes/symmetry_detect.h | 109 ++-- src/theory/quantifiers/term_util.cpp | 6 +- test/regress/Makefile.tests | 5 + test/regress/regress1/sym/q-constant.smt2 | 17 + test/regress/regress1/sym/q-function.smt2 | 14 + test/regress/regress1/sym/qf-function.smt2 | 13 + test/regress/regress1/sym/sb-wrong.smt2 | 10 + test/regress/regress1/sym/sym-setAB.smt2 | 12 + 10 files changed, 719 insertions(+), 250 deletions(-) create mode 100644 test/regress/regress1/sym/q-constant.smt2 create mode 100644 test/regress/regress1/sym/q-function.smt2 create mode 100644 test/regress/regress1/sym/qf-function.smt2 create mode 100644 test/regress/regress1/sym/sb-wrong.smt2 create mode 100644 test/regress/regress1/sym/sym-setAB.smt2 diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp index c32057d5f..1e4b9853d 100644 --- a/src/preprocessing/passes/symmetry_breaker.cpp +++ b/src/preprocessing/passes/symmetry_breaker.cpp @@ -16,6 +16,7 @@ #include "preprocessing/passes/symmetry_detect.h" using namespace std; +using namespace CVC4::kind; namespace CVC4 { namespace preprocessing { @@ -31,8 +32,12 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts if (part.size() >= 2) { Kind kd = getOrderKind(part[0]); - - if (kd != kind::EQUAL) + if (kd == UNDEFINED_KIND) + { + // no symmetry breaking possible + continue; + } + if (kd != EQUAL) { for (unsigned int i = 0; i < part.size() - 1; ++i) { @@ -50,12 +55,11 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts { for (unsigned int j = i + 2; j < part.size(); ++j) { - // Generate consecutive constraints v_i = v_j => v_i = v_{j-1} for all 0 - // <= i < j-1 < j < part.size() - Node constraint = nm->mkNode( - kind::IMPLIES, - nm->mkNode(kd, part[i], part[j]), - nm->mkNode(kd, part[i], part[j - 1])); + // Generate consecutive constraints v_i = v_j => v_i = v_{j-1}, + // for all 0 <= i < j-1 < j < part.size() + Node constraint = nm->mkNode(IMPLIES, + nm->mkNode(kd, part[i], part[j]), + nm->mkNode(kd, part[i], part[j - 1])); constraints.push_back(constraint); Trace("sym-bk") << "[sym-bk] Generate a symmetry breaking constraint: " @@ -74,15 +78,14 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts if(prev_seg_start_index >= 0) { rhs = nm->mkNode( - kind::OR, + OR, rhs, - nm->mkNode(kd, part[i-1], part[prev_seg_start_index])); + nm->mkNode(kd, part[i - 1], part[prev_seg_start_index])); } // Generate length order constraints // v_i = v_j => (v_{i} = v_{i-1} OR v_{i-1} = x_{(i-1)-(j-i)}) // for all 1 <= i < j < part.size() and (i-1)-(j-i) >= 0 - Node constraint = - nm->mkNode(kind::IMPLIES, lhs, rhs); + Node constraint = nm->mkNode(IMPLIES, lhs, rhs); constraints.push_back(constraint); Trace("sym-bk") << "[sym-bk] Generate a symmetry breaking constraint: " @@ -101,23 +104,29 @@ Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts { return constraints[0]; } - return nm->mkNode(kind::AND, constraints); + return nm->mkNode(AND, constraints); } Kind SymmetryBreaker::getOrderKind(Node node) { - if (node.getType().isInteger() || node.getType().isReal()) + TypeNode tn = node.getType(); + if (tn.isBoolean()) + { + return IMPLIES; + } + else if (tn.isReal()) { - return kind::LEQ; + return LEQ; } - else if (node.getType().isBitVector()) + else if (tn.isBitVector()) { - return kind::BITVECTOR_ULE; + return BITVECTOR_ULE; } - else + if (tn.isFirstClass()) { - return kind::EQUAL; + return EQUAL; } + return UNDEFINED_KIND; } SymBreakerPass::SymBreakerPass(PreprocessingPassContext* preprocContext) @@ -128,27 +137,37 @@ PreprocessingPassResult SymBreakerPass::applyInternal( { Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl; // detect symmetries - std::vector> part; + std::vector> sterms; symbreak::SymmetryDetect symd; - symd.getPartition(part, assertionsToPreprocess->ref()); - if (Trace.isOn("sym-break-pass")) + symd.computeTerms(sterms, assertionsToPreprocess->ref()); + if (Trace.isOn("sym-break-pass") || Trace.isOn("sb-constraint")) { - Trace("sym-break-pass") << "Detected symmetry partition:" << std::endl; - for (const std::vector& p : part) + if (sterms.empty()) { - Trace("sym-break-pass") << " " << p << std::endl; + Trace("sym-break-pass") << "Detected no symmetric terms." << std::endl; + } + else + { + Trace("sb-constraint") << "; found symmetry" << std::endl; + Trace("sym-break-pass") << "Detected symmetric terms:" << std::endl; + for (const std::vector& p : sterms) + { + Trace("sym-break-pass") << " " << p << std::endl; + } } } // construct the symmetry breaking constraint Trace("sym-break-pass") << "Construct symmetry breaking constraint..." << std::endl; SymmetryBreaker symb; - Node sbConstraint = symb.generateSymBkConstraints(part); + Node sbConstraint = symb.generateSymBkConstraints(sterms); // add symmetry breaking constraint to the set of assertions Trace("sym-break-pass") << "...got: " << sbConstraint << std::endl; // if not true if (!sbConstraint.isConst()) { + Trace("sb-constraint") << "(symmetry-break " << sbConstraint << ")" + << std::endl; // add to assertions assertionsToPreprocess->push_back(sbConstraint); } diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp index a1273b1d9..24db144e4 100644 --- a/src/preprocessing/passes/symmetry_detect.cpp +++ b/src/preprocessing/passes/symmetry_detect.cpp @@ -13,10 +13,13 @@ **/ #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 { @@ -91,6 +94,25 @@ void Partition::printPartition(const char* c, Partition p) } } +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 >::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 > p : d_subvar_to_vars) @@ -98,12 +120,30 @@ void Partition::normalize() std::sort(p.second.begin(), p.second.end()); } } +void Partition::getVariables(std::vector& vars) +{ + for (const std::pair& p : d_var_to_subvar) + { + vars.push_back(p.first); + } +} + +void Partition::getSubstitution(std::vector& vars, + std::vector& subs) +{ + for (const std::pair& p : d_var_to_subvar) + { + vars.push_back(p.first); + subs.push_back(p.second); + } +} void PartitionMerger::initialize(Kind k, const std::vector& partitions, const std::vector& 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) { @@ -136,7 +176,8 @@ void PartitionMerger::initialize(Kind k, bool PartitionMerger::merge(std::vector& partitions, unsigned base_index, - std::unordered_set& active_indices) + std::unordered_set& active_indices, + std::vector& merged_indices) { Assert(base_index < partitions.size()); d_master_base_index = base_index; @@ -185,7 +226,18 @@ bool PartitionMerger::merge(std::vector& partitions, 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; @@ -219,7 +271,9 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, 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]; @@ -229,6 +283,7 @@ bool PartitionMerger::mergeNewVar(unsigned 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& svs = p.d_subvar_to_vars.begin()->second; bool include_success = true; @@ -286,7 +341,8 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, 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--; @@ -312,7 +368,7 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, // 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); @@ -332,10 +388,9 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, 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, @@ -369,70 +424,10 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, 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) +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 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]; + d_trueNode = NodeManager::currentNM()->mkConst(true); + d_falseNode = NodeManager::currentNM()->mkConst(false); } Partition SymmetryDetect::detect(const vector& assertions) @@ -471,15 +466,12 @@ Node SymmetryDetect::getSymBreakVariable(TypeNode tn, unsigned index) 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]; @@ -499,11 +491,12 @@ Node SymmetryDetect::getSymBreakVariableInc(TypeNode tn, return getSymBreakVariable(tn, new_index); } -void SymmetryDetect::getPartition(vector >& parts, - const vector& assertions) +void SymmetryDetect::compute(std::vector >& part, + const std::vector& assertions) { Partition p = detect(assertions); + std::vector > parts; for (map >::const_iterator subvar_to_vars_it = p.d_subvar_to_vars.begin(); subvar_to_vars_it != p.d_subvar_to_vars.end(); @@ -512,6 +505,98 @@ void SymmetryDetect::getPartition(vector >& parts, parts.push_back(subvar_to_vars_it->second); } } +void SymmetryDetect::computeTerms(std::vector >& sterms, + const std::vector& assertions) +{ + Partition p = detect(assertions); + + for (const std::pair > 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& 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 vars; + std::vector subs; + for (const Node& v : sp.second) + { + vars.push_back(v); + subs.push_back(sv); + } + std::vector& tsym = d_tsyms[tsymId]; + // map terms in this symmetry to their final form + std::vector tsym_indices; + std::vector 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 > t_to_st; + computeAlphaEqTerms(tsym_indices, tsym_terms, t_to_st); + Node tshUse; + for (const std::pair >& 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 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 d_variables; + /** The mapping from a node to its children */ + std::map d_children; +}; Partition SymmetryDetect::findPartitions(Node node) { @@ -535,14 +620,11 @@ Partition SymmetryDetect::findPartitions(Node node) // If node is a variable if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE) { - vector 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; } @@ -567,14 +649,18 @@ Partition SymmetryDetect::findPartitions(Node node) isAssocComm = theory::quantifiers::TermUtil::isComm(k); } - // Children of node - vector children; - // Partitions of children - vector 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 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()); @@ -585,14 +671,14 @@ Partition SymmetryDetect::findPartitions(Node node) } Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl; + // Partitions of children + std::vector partitions; // Create partitions for children std::unordered_set active_indices; - for (vector::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")) { @@ -609,15 +695,21 @@ Partition SymmetryDetect::findPartitions(Node node) if (isAssocComm) { - // map substituted terms to indices in partitions - std::map > sterm_to_indices; + // get the list of indices and terms + std::vector indices; + std::vector 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 > sterm_to_indices; + computeAlphaEqTerms(indices, sterms, sterm_to_indices); for (const std::pair >& sti : sterm_to_indices) { @@ -632,42 +724,26 @@ Partition SymmetryDetect::findPartitions(Node node) Trace("sym-dt-debug") << std::endl; } // merge children, remove active indices - processPartitions(k, partitions, sti.second, active_indices); + std::vector fixedSVar; + std::vector 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 all_vars; - std::map type_index; - std::vector 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 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 f_vars; - std::vector f_subs; // add to overall list of variables for (const pair >& 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) { @@ -676,67 +752,140 @@ Partition SymmetryDetect::findPartitions(Node node) 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 type_index; + type_index.clear(); + // the indices we need to reconstruct + std::map 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 subvars; + std::vector 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::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 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 pvars; + std::vector psubs; + if (!rcons_indices.empty()) + { + p.getSubstitution(pvars, psubs); + } + + // Reconstruct the substituted node + p.d_term = node; + std::vector 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; @@ -746,7 +895,7 @@ Partition SymmetryDetect::findPartitions(Node node) } else { - if (node.getMetaKind() == kind::metakind::PARAMETERIZED) + if (node.getMetaKind() == metakind::PARAMETERIZED && !operatorChild) { schildren.insert(schildren.begin(), node.getOperator()); } @@ -757,6 +906,7 @@ Partition SymmetryDetect::findPartitions(Node node) << 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); @@ -802,13 +952,54 @@ void SymmetryDetect::collectChildren(Node node, vector& children) } while (!visit.empty()); } +void SymmetryDetect::computeAlphaEqTerms( + const std::vector& indices, + const std::vector& sterms, + std::map >& sterm_to_indices) +{ + Assert(indices.size() == sterms.size()); + // also store quantified formulas, since these may be alpha-equivalent + std::vector 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 d_value; /** children of this node */ std::map d_children; /** clear the children */ @@ -823,11 +1014,8 @@ class NodeTrie { if (index == args.size()) { - if (d_value == -1) - { - d_value = static_cast(value); - } - return d_value; + d_value.push_back(value); + return d_value[0]; } return d_children[args[index]].add(value, args, index + 1); } @@ -837,15 +1025,125 @@ void SymmetryDetect::processPartitions( Kind k, std::vector& partitions, const std::vector& indices, - std::unordered_set& active_indices) + std::unordered_set& active_indices, + std::vector& fixedSVar, + std::vector& 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 svarTrie; + std::map > > svarEqc; + + for (unsigned j = 0, size = indices.size(); j < size; j++) + { + unsigned index = indices[j]; + Partition& p = partitions[index]; + for (const std::pair > 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 > > sve : + svarEqc) + { + if (Trace.isOn("sym-dt-debug")) + { + Trace("sym-dt-debug") << "For " << sve.first << " : "; + for (const std::pair > 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 >& 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 @@ -907,10 +1205,26 @@ void SymmetryDetect::processPartitions( } 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); } + // 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( @@ -925,7 +1239,8 @@ 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 << " "; @@ -938,12 +1253,27 @@ void SymmetryDetect::mergePartitions( 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 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 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 vars; + partitions[index].getVariables(vars); + storeTermSymmetry(symTerms, vars); + Trace("sym-dt-debug") << " ......recurse" << std::endl; std::vector rem_indices; for (unsigned ii : indices) { @@ -958,6 +1288,30 @@ void SymmetryDetect::mergePartitions( } } +void SymmetryDetect::storeTermSymmetry(const std::vector& symTerms, + const std::vector& 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 diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h index 9a5f83868..67e40da00 100644 --- a/src/preprocessing/passes/symmetry_detect.h +++ b/src/preprocessing/passes/symmetry_detect.h @@ -21,6 +21,7 @@ #include #include #include "expr/node.h" +#include "theory/quantifiers/term_canonize.h" namespace CVC4 { namespace preprocessing { @@ -65,10 +66,18 @@ class Partition * { w-> { x, y } } */ std::map > 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& vars); + /** get substitution */ + void getSubstitution(std::vector& vars, std::vector& subs); }; /** partition merger @@ -128,7 +137,8 @@ class PartitionMerger */ bool merge(std::vector& partitions, unsigned base_index, - std::unordered_set& active_indices); + std::unordered_set& active_indices, + std::vector& merged_indices); private: /** the kind of the node we are consdiering */ @@ -176,49 +186,16 @@ class PartitionMerger 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. - * */ + * 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(true); - d_falseNode = NodeManager::currentNM()->mkConst(false); - } + /** constructor */ + SymmetryDetect(); /** * Destructor @@ -226,11 +203,22 @@ class SymmetryDetect ~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 >& parts, const std::vector& assertions); + void compute(std::vector >& part, + const std::vector& 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 >& sterms, + const std::vector& assertions); private: /** (canonical) symmetry breaking variables for each type */ @@ -253,6 +241,9 @@ class SymmetryDetect Node d_trueNode; Node d_falseNode; + /** term canonizer (for quantified formulas) */ + theory::quantifiers::TermCanonize d_tcanon; + /** Cache for partitions */ std::map d_term_partition; @@ -275,6 +266,22 @@ class SymmetryDetect * */ void collectChildren(Node node, std::vector& 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& indices, + const std::vector& sterms, + std::map >& sterm_to_indices); /** process partitions * * This method is called when we have detected symmetries for the children @@ -295,7 +302,9 @@ class SymmetryDetect void processPartitions(Kind k, std::vector& partitions, const std::vector& indices, - std::unordered_set& active_indices); + std::unordered_set& active_indices, + std::vector& fixedSVar, + std::vector& fixedVar); /** merge partitions * * This method merges groups of partitions occurring in indices using the @@ -307,7 +316,21 @@ class SymmetryDetect std::vector& partitions, const std::vector& indices, std::unordered_set& active_indices); + //-------------------for symmetry breaking terms + /** symmetry breaking id counter */ + unsigned d_tsym_id_counter; + /** list of term symmetries */ + std::map > d_tsyms; + /** list of term symmetries */ + std::map > d_tsym_to_vars; + /** variables to ids */ + std::map > d_var_to_tsym_ids; + /** store term symmetry */ + void storeTermSymmetry(const std::vector& symTerms, + const std::vector& vars); + //-------------------end for symmetry breaking terms }; + } // namespace symbreak } // namespace passes } // namespace preprocessing diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index d2b7688ec..f8e8ed5ad 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -659,14 +659,16 @@ bool TermUtil::isAssoc( Kind k ) { || 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; + || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT + || k == SEP_STAR; } bool TermUtil::isComm( Kind k ) { 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; + || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION + || k == SEP_STAR; } bool TermUtil::isNonAdditive( Kind k ) { diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b4f920ca4..a1cba3b55 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1618,6 +1618,10 @@ REG1_TESTS = \ regress1/sygus/unbdd_inv_gen_ex7.sy \ regress1/sygus/unbdd_inv_gen_winf1.sy \ regress1/sygus/univ_2-long-repeat.sy \ + regress1/sym/qf-function.smt2 \ + regress1/sym/q-constant.smt2 \ + regress1/sym/q-function.smt2 \ + regress1/sym/sb-wrong.smt2 \ regress1/sym/sym1.smt2 \ regress1/sym/sym2.smt2 \ regress1/sym/sym3.smt2 \ @@ -1625,6 +1629,7 @@ REG1_TESTS = \ regress1/sym/sym5.smt2 \ regress1/sym/sym6.smt2 \ regress1/sym/sym7-uf.smt2 \ + regress1/sym/sym-setAB.smt2 \ regress1/test12.cvc \ regress1/trim.cvc \ regress1/uf2.smt2 \ diff --git a/test/regress/regress1/sym/q-constant.smt2 b/test/regress/regress1/sym/q-constant.smt2 new file mode 100644 index 000000000..b8fee6c8d --- /dev/null +++ b/test/regress/regress1/sym/q-constant.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) +(declare-fun R (Int Int) Bool) + +(assert (or (forall ((x Int)) (R x a)) (forall ((x Int)) (R x b)))) +(assert (not (R c a))) +(assert (not (R c b))) + +(check-sat) diff --git a/test/regress/regress1/sym/q-function.smt2 b/test/regress/regress1/sym/q-function.smt2 new file mode 100644 index 000000000..3e303106e --- /dev/null +++ b/test/regress/regress1/sym/q-function.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun P (Int) Bool) +(declare-fun Q (Int) Bool) + +(assert (or (forall ((x Int)) (P x)) (forall ((x Int)) (Q x)))) +(assert (not (P a))) +(assert (not (Q a))) +(check-sat) diff --git a/test/regress/regress1/sym/qf-function.smt2 b/test/regress/regress1/sym/qf-function.smt2 new file mode 100644 index 000000000..697f9e1f0 --- /dev/null +++ b/test/regress/regress1/sym/qf-function.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic QF_UFLIA) +(set-info :status sat) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun P (Int) Int) +(declare-fun Q (Int) Int) + +(assert (or (= (f a) 0) (= (g a) 0))) + +(check-sat) diff --git a/test/regress/regress1/sym/sb-wrong.smt2 b/test/regress/regress1/sym/sb-wrong.smt2 new file mode 100644 index 000000000..5f5e6bb34 --- /dev/null +++ b/test/regress/regress1/sym/sb-wrong.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic QF_UFLIA) +(set-info :status sat) +(declare-fun f (Int) Int) +(declare-fun c () Int) +(declare-fun d () Int) +(assert +(or (= c (f d)) (= d (f d))) +) +(check-sat) diff --git a/test/regress/regress1/sym/sym-setAB.smt2 b/test/regress/regress1/sym/sym-setAB.smt2 new file mode 100644 index 000000000..9d613c3b6 --- /dev/null +++ b/test/regress/regress1/sym/sym-setAB.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --symmetry-breaker-exp +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun C () (Set Int)) + +(assert (and (member x A) (member x B) (member x C))) +(assert (member y C)) +(check-sat) -- cgit v1.2.3