From 8a56e62da0a8940f0ae1ee9575398e5f21660097 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Mar 2020 13:01:42 -0500 Subject: [PATCH] Remove experimental symmetry breaker (#4005) This never impacted performance positively. Fixes #3997 and fixes #4015. There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique. --- src/CMakeLists.txt | 4 - src/options/smt_options.toml | 8 - src/preprocessing/passes/symmetry_breaker.cpp | 182 --- src/preprocessing/passes/symmetry_breaker.h | 109 -- src/preprocessing/passes/symmetry_detect.cpp | 1319 ----------------- src/preprocessing/passes/symmetry_detect.h | 339 ----- .../preprocessing_pass_registry.cpp | 3 - src/smt/smt_engine.cpp | 6 - test/regress/regress1/sym/q-constant.smt2 | 1 - test/regress/regress1/sym/q-function.smt2 | 1 - test/regress/regress1/sym/qf-function.smt2 | 1 - test/regress/regress1/sym/sb-wrong.smt2 | 1 - test/regress/regress1/sym/sym-setAB.smt2 | 1 - test/regress/regress1/sym/sym1.smt2 | 1 - test/regress/regress1/sym/sym2.smt2 | 1 - test/regress/regress1/sym/sym3.smt2 | 1 - test/regress/regress1/sym/sym4.smt2 | 1 - test/regress/regress1/sym/sym5.smt2 | 1 - test/regress/regress1/sym/sym6.smt2 | 1 - test/regress/regress1/sym/sym7-uf.smt2 | 1 - 20 files changed, 1982 deletions(-) delete mode 100644 src/preprocessing/passes/symmetry_breaker.cpp delete mode 100644 src/preprocessing/passes/symmetry_breaker.h delete mode 100644 src/preprocessing/passes/symmetry_detect.cpp delete mode 100644 src/preprocessing/passes/symmetry_detect.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0908b5b68..bb2b95960 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -92,10 +92,6 @@ libcvc4_add_sources( preprocessing/passes/static_learning.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h - preprocessing/passes/symmetry_breaker.cpp - preprocessing/passes/symmetry_breaker.h - preprocessing/passes/symmetry_detect.cpp - preprocessing/passes/symmetry_detect.h preprocessing/passes/synth_rew_rules.cpp preprocessing/passes/synth_rew_rules.h preprocessing/passes/theory_preprocess.cpp diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 676e01484..67829ede8 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -383,14 +383,6 @@ header = "options/smt_options.h" default = "false" help = "calculate sort inference of input problem, convert the input based on monotonic sorts" -[[option]] - name = "symmetryBreakerExp" - category = "regular" - long = "symmetry-breaker-exp" - type = "bool" - default = "false" - help = "generate symmetry breaking constraints after symmetry detection" - [[option]] name = "incrementalSolving" category = "common" diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp deleted file mode 100644 index eb83fd229..000000000 --- a/src/preprocessing/passes/symmetry_breaker.cpp +++ /dev/null @@ -1,182 +0,0 @@ -/********************* */ -/*! \file symmetry_breaker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Paul Meng, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Symmetry breaker module - **/ - -#include "preprocessing/passes/symmetry_breaker.h" - -#include "preprocessing/passes/symmetry_detect.h" - -using namespace std; -using namespace CVC4::kind; - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -Node SymmetryBreaker::generateSymBkConstraints(const vector>& parts) -{ - vector constraints; - NodeManager* nm = NodeManager::currentNM(); - - for (const vector& part : parts) - { - if (part.size() >= 2) - { - Kind kd = getOrderKind(part[0]); - if (kd == UNDEFINED_KIND) - { - // no symmetry breaking possible - continue; - } - if (kd != EQUAL) - { - for (unsigned int i = 0; i < part.size() - 1; ++i) - { - // Generate less than or equal to constraints: part[i] <= part[i+1] - Node constraint = nm->mkNode(kd, part[i], part[i + 1]); - constraints.push_back(constraint); - Trace("sym-bk") - << "[sym-bk] Generate a symmetry breaking constraint: " - << constraint << endl; - } - } - else if (part.size() >= 3) - { - for (unsigned int i = 0; i < part.size(); ++i) - { - 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(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: " - << constraint << endl; - } - if (i >= 1) - { - for (unsigned int j = i + 1; j < part.size(); ++j) - { - Node lhs = nm->mkNode(kd, part[i], part[j]); - Node rhs = nm->mkNode(kd, part[i], part[i - 1]); - int prev_seg_start_index = 2*i - j - 1; - - // Since prev_seg_len is always less than i - 1, we just need to make - // sure prev_seg_len is greater than or equal to 0 - if(prev_seg_start_index >= 0) - { - rhs = nm->mkNode( - OR, - rhs, - 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(IMPLIES, lhs, rhs); - constraints.push_back(constraint); - Trace("sym-bk") - << "[sym-bk] Generate a symmetry breaking constraint: " - << constraint << endl; - } - } - } - } - } - } - if(constraints.empty()) - { - return d_trueNode; - } - else if(constraints.size() == 1) - { - return constraints[0]; - } - return nm->mkNode(AND, constraints); -} - -Kind SymmetryBreaker::getOrderKind(Node node) -{ - TypeNode tn = node.getType(); - if (tn.isBoolean()) - { - return IMPLIES; - } - else if (tn.isReal()) - { - return LEQ; - } - else if (tn.isBitVector()) - { - return BITVECTOR_ULE; - } - if (tn.isFirstClass()) - { - return EQUAL; - } - return UNDEFINED_KIND; -} - -SymBreakerPass::SymBreakerPass(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "sym-break"){}; - -PreprocessingPassResult SymBreakerPass::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - Trace("sym-break-pass") << "Apply symmetry breaker pass..." << std::endl; - // detect symmetries - std::vector> sterms; - symbreak::SymmetryDetect symd; - symd.computeTerms(sterms, assertionsToPreprocess->ref()); - if (Trace.isOn("sym-break-pass") || Trace.isOn("sb-constraint")) - { - if (sterms.empty()) - { - 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(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); - } - - return PreprocessingPassResult::NO_CONFLICT; -} - - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h deleted file mode 100644 index 6bb10ebb8..000000000 --- a/src/preprocessing/passes/symmetry_breaker.h +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file symmetry_breaker.h - ** \verbatim - ** Top contributors (to current version): - ** Paul Meng, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Symmetry breaker for theories - **/ - -#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ -#define CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ - -#include -#include -#include -#include "expr/node.h" - -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -/** - * Given a vector of partitions {{v_{11}, ... , v_{1n}}, {v_{m1}, ... , v_{mk}}}, - * the symmetry breaker will generate symmetry breaking constraints for each - * partition {v_{i1}, ... , v_{ij}} depending on the type of variables - * in each partition. - * - * For a partition of integer, real and bit-vectors variables {v1, ..., vn}, - * we generate ordered constraints: {v1 <= v2, ..., v{n-1} <= vn}. - * For a partition of variables of other types {v1, ..., vn}, we generate - * the following two kinds of constraints. - * - * 1. Consecutive constraints ensure that equivalence classes over v_1...v_n are - * in consecutive segments - * v_i = v_j => v_i = v_{j-1} for all 0 <= i < j-1 < j < n - * 2. Length order constraints ensure that the length of segments occur in - * descending order - * 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 - * */ - -class SymmetryBreaker -{ - public: - /** - * Constructor - * */ - SymmetryBreaker() - { - d_trueNode = NodeManager::currentNM()->mkConst(true); - d_falseNode = NodeManager::currentNM()->mkConst(false); - } - - /** - * Destructor - * */ - ~SymmetryBreaker() {} - - /** - * This is to generate symmetry breaking constraints for partitions in parts. - * Since parts are symmetries of the original assertions C, - * the symmetry breaking constraints SB for parts returned by this function - * conjuncted with the original assertions SB ^ C is equisatisfiable to C. - * */ - Node generateSymBkConstraints(const std::vector >& parts); - - private: - - /** True and false constant nodes */ - Node d_trueNode; - Node d_falseNode; - - /** - * Get the order kind depending on the type of node. - * For example, if node is a integer or real, this function would return - * the operator less than or equal to (<=) so that we can use it to build - * ordered constraints. - * */ - Kind getOrderKind(Node node); -}; - -/** - * This class detects symmetries in the input assertions in the form of a - * partition (see symmetry_detect.h), and subsequently adds symmetry breaking - * constraints that correspond to this partition, using the above class. - */ -class SymBreakerPass : public PreprocessingPass -{ - public: - SymBreakerPass(PreprocessingPassContext* preprocContext); - - protected: - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; -}; - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 - -#endif /* CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */ diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp deleted file mode 100644 index d0327263b..000000000 --- a/src/preprocessing/passes/symmetry_detect.cpp +++ /dev/null @@ -1,1319 +0,0 @@ -/********************* */ -/*! \file symmetry_detect.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Symmetry detection module - **/ - -#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 { -namespace passes { -namespace symbreak { - -/** returns n choose k, that is, n!/(k! * (n-k)!) */ -unsigned nChoosek(unsigned n, unsigned k) -{ - 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::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) - { - 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) - { - 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, - std::vector& merged_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)) - { - 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; - // 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() - << ", 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]; - - // 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]; - 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; - 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 (!merge_var.isNull() - && p.d_var_to_subvar.find(merge_var) != p.d_var_to_subvar.end()) - { - // 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 (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& p2 = partitions[i]; - children.push_back(p2.d_term); - schildren.push_back(p2.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& p3 = partitions[d_master_base_index]; - // reconstruct the master partition - p3.d_term = mkAssociativeNode(d_kind, children); - p3.d_sterm = mkAssociativeNode(d_kind, schildren); - Assert(p3.d_subvar_to_vars.size() == 1); - Node sb_v = p3.d_subvar_to_vars.begin()->first; - Trace("sym-dt-debug") << "- set var to svar: " << merge_var << " -> " - << sb_v << std::endl; - p3.addVariable(sb_v, merge_var); - 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); -} - -SymmetryDetect::SymmetryDetect() : d_tsym_id_counter(1) -{ - d_trueNode = NodeManager::currentNM()->mkConst(true); - d_falseNode = NodeManager::currentNM()->mkConst(false); -} - -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")) - { - 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); - } - NodeManager* nm = NodeManager::currentNM(); - while (it->second.size() <= index) - { - std::stringstream ss; - ss << "_sym_bk_" << tn << "_" << (it->second.size() + 1); - Node fresh_var = nm->mkBoundVar(ss.str(), tn); - 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::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(); - ++subvar_to_vars_it) - { - 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) -{ - 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-debug") << "[sym-dt] We have seen the node " << node - << " before, thus we return its partition from cache." - << endl; - return partition->second; - } - - // The new partition for node - Partition p; - // If node is a variable - if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE) - { - TypeNode type = node.getType(); - Node fresh_var = getSymBreakVariable(type, 0); - p.d_term = node; - p.d_sterm = fresh_var; - p.addVariable(fresh_var, node); - d_term_partition[node] = p; - return p; - } - // If node is a constant - 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); - } - - // Get all children of node - Trace("sym-dt-debug") << "[sym-dt] collectChildren for: " << node - << " 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()); - } - else - { - collectChildren(node, children); - } - 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 (const Node& c : children) - { - active_indices.insert(partitions.size()); - partitions.push_back(findPartitions(c)); - } - if (Trace.isOn("sym-dt-debug")) - { - 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; - } - - if (isAssocComm) - { - // get the list of indices and terms - std::vector indices; - std::vector sterms; - for (unsigned j = 0, size = partitions.size(); j < size; j++) - { - Node st = partitions[j].d_sterm; - if (!st.isNull()) - { - 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) - { - Node cterm = sti.first; - if (Trace.isOn("sym-dt-debug")) - { - Trace("sym-dt-debug") << " indices[" << cterm << "] = "; - for (unsigned i : sti.second) - { - Trace("sym-dt-debug") << i << " "; - } - Trace("sym-dt-debug") << std::endl; - } - // merge children, remove 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; - for (unsigned i : active_indices) - { - Trace("sym-dt-debug") << "Reconstruct partition for active index : " << i - << std::endl; - Partition& pa = partitions[i]; - // add to overall list of variables - for (const pair >& pas : pa.d_subvar_to_vars) - { - Trace("sym-dt-debug") - << "...process " << pas.first << " -> " << pas.second << std::endl; - // 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); - } - } - } - 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) - { - 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()) - { - 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()); - } - } - // 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()) - { - 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 - { - 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") << "[sym-dt] Map : " << n << " -> " << useVar - << std::endl; - p.addVariable(useVar, n); - } - - 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) - { - 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 - { - Assert(i < schildren.size()); - schildren[i] = sterm; - } - } - - Trace("sym-dt-debug") << "[sym-dt] Reconstructing node: " << node - << ", #children = " << schildren.size() << "/" - << children.size() << endl; - if (isAssocComm) - { - p.d_sterm = mkAssociativeNode(k, schildren); - } - else - { - if (node.getMetaKind() == metakind::PARAMETERIZED && !operatorChild) - { - 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()); - - // normalize: ensures that variable lists are sorted - 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)); - - // 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; - visit.push_back(node); - unordered_set visited; - - do - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur.getNumChildren() > 0 && cur.getKind() == k - && cur[0].getType() == ctn) - { - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else - { - children.push_back(cur); - } - } - } 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() {} - /** value at this node*/ - std::vector 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) - { - if (index == args.size()) - { - d_value.push_back(value); - return d_value[0]; - } - return d_children[args[index]].add(value, args, index + 1); - } -}; - -void SymmetryDetect::processPartitions( - Kind k, - std::vector& partitions, - const std::vector& 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 == 0) - { - // 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 i = 0; i < nfvars; i++) - { - fixedVar.pop_back(); - fixedSVar.pop_back(); - } - } - return; - } - // 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++) - { - 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) - { - // 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) - { - Trace("sym-dt-debug") << i << " "; - } - Trace("sym-dt-debug") << std::endl; - } - 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) - { - 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()); - // 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, size2 = fixedSVar.size(); i < size2; i++) - { - // add variable - partitions[index].addVariable(fixedSVar[i], fixedVar[i]); - } - } - } - } -} - -void SymmetryDetect::mergePartitions( - Kind k, - std::vector& partitions, - const std::vector& indices, - std::unordered_set& active_indices) -{ - if (indices.size() <= 1) - { - return; - } - if (Trace.isOn("sym-dt-debug")) - { - Trace("sym-dt-debug") << "--- mergePartitions..." << std::endl; - Trace("sym-dt-debug") << " indices "; - for (unsigned i : indices) - { - Trace("sym-dt-debug") << i << " "; - } - Trace("sym-dt-debug") << std::endl; - } - Assert(!indices.empty()); - - // initialize partition merger class - PartitionMerger pm; - pm.initialize(k, partitions, indices); - - for (unsigned index : indices) - { - Node mterm = partitions[index].d_term; - std::vector merged_indices; - if (pm.merge(partitions, index, active_indices, merged_indices)) - { - // 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) - { - if (ii != index && active_indices.find(ii) != active_indices.end()) - { - rem_indices.push_back(ii); - } - } - mergePartitions(k, partitions, rem_indices, active_indices); - return; - } - } -} - -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 -} // namespace CVC4 diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h deleted file mode 100644 index deb1accd7..000000000 --- a/src/preprocessing/passes/symmetry_detect.h +++ /dev/null @@ -1,339 +0,0 @@ -/********************* */ -/*! \file symmetry_detect.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Symmetry detection for theories - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H -#define CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H - -#include -#include -#include -#include "expr/node.h" -#include "expr/term_canonize.h" - -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; - /** 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 - * - * 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, - std::vector& merged_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); -}; - -/** - * This is the class to detect symmetries between variables or terms relative - * to a set of input assertions. - */ -class SymmetryDetect -{ - public: - /** constructor */ - SymmetryDetect(); - - /** - * Destructor - * */ - ~SymmetryDetect() {} - - /** Get the final partition after symmetry detection. - * - * If a vector in sterms contains two variables x and y, - * then assertions and assertions { x -> y, y -> x } are - * equisatisfiable. - * */ - 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 */ - std::map > d_sb_vars; - /** - * 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. - */ - Node getSymBreakVariable(TypeNode tn, unsigned index); - /** - * Get the index[tn]^th symmetry breaking variable for type tn using the - * above function and increment index[tn]. - */ - Node getSymBreakVariableInc(TypeNode tn, std::map& index); - - /** True and false constant nodes */ - Node d_trueNode; - Node d_falseNode; - - /** term canonizer (for quantified formulas) */ - expr::TermCanonize d_tcanon; - - /** Cache for partitions */ - std::map d_term_partition; - - /** detect - * - * Called on the input assertions, where assertions are interpreted as a - * conjunction. This computes a partition P of the variables in assertions - * such that for each set S in P, then all automorphisms for S applied to - * assertions result in an equisatisfiable formula. - */ - Partition detect(const std::vector& assertions); - - /** Find symmetries in node */ - Partition findPartitions(Node node); - - /** Collect children of a node - * If the kind of node is associative, we will chain its children together. - * We might need optimizations here, such as rewriting the input to negation - * normal form. - * */ - 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 - * 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, - std::vector& fixedSVar, - std::vector& fixedVar); - /** 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); - //-------------------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 -} // namespace CVC4 - -#endif diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 9272bbb5a..e264c17e5 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -50,8 +50,6 @@ #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" #include "preprocessing/passes/sygus_inference.h" -#include "preprocessing/passes/symmetry_breaker.h" -#include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" #include "preprocessing/passes/theory_preprocess.h" #include "preprocessing/passes/unconstrained_simplifier.h" @@ -143,7 +141,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("miplib-trick", callCtor); registerPassInfo("non-clausal-simp", callCtor); registerPassInfo("ackermann", callCtor); - registerPassInfo("sym-break", callCtor); registerPassInfo("ext-rew-pre", callCtor); registerPassInfo("theory-preprocess", callCtor); registerPassInfo("quantifier-macros", callCtor); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bfb126e9e..e4e582b6e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3454,12 +3454,6 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); - if (options::symmetryBreakerExp() && !options::incrementalSolving()) - { - // apply symmetry breaking if not in incremental mode - d_passes["sym-break"]->apply(&d_assertions); - } - if(options::doStaticLearning()) { d_passes["static-learning"]->apply(&d_assertions); } diff --git a/test/regress/regress1/sym/q-constant.smt2 b/test/regress/regress1/sym/q-constant.smt2 index b8fee6c8d..8649df2c7 100644 --- a/test/regress/regress1/sym/q-constant.smt2 +++ b/test/regress/regress1/sym/q-constant.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status unsat) (declare-fun f (Int) Int) diff --git a/test/regress/regress1/sym/q-function.smt2 b/test/regress/regress1/sym/q-function.smt2 index 3e303106e..6ab835e00 100644 --- a/test/regress/regress1/sym/q-function.smt2 +++ b/test/regress/regress1/sym/q-function.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status unsat) (declare-fun f (Int) Int) diff --git a/test/regress/regress1/sym/qf-function.smt2 b/test/regress/regress1/sym/qf-function.smt2 index 697f9e1f0..d2933d26f 100644 --- a/test/regress/regress1/sym/qf-function.smt2 +++ b/test/regress/regress1/sym/qf-function.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic QF_UFLIA) (set-info :status sat) (declare-fun f (Int) Int) diff --git a/test/regress/regress1/sym/sb-wrong.smt2 b/test/regress/regress1/sym/sb-wrong.smt2 index 5f5e6bb34..80c7ea550 100644 --- a/test/regress/regress1/sym/sb-wrong.smt2 +++ b/test/regress/regress1/sym/sb-wrong.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic QF_UFLIA) (set-info :status sat) (declare-fun f (Int) Int) diff --git a/test/regress/regress1/sym/sym-setAB.smt2 b/test/regress/regress1/sym/sym-setAB.smt2 index 9d613c3b6..0fdf90bfb 100644 --- a/test/regress/regress1/sym/sym-setAB.smt2 +++ b/test/regress/regress1/sym/sym-setAB.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym1.smt2 b/test/regress/regress1/sym/sym1.smt2 index c063f8b8f..987b6c1f4 100644 --- a/test/regress/regress1/sym/sym1.smt2 +++ b/test/regress/regress1/sym/sym1.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2 index e2e62cbb6..ec812dbb7 100644 --- a/test/regress/regress1/sym/sym2.smt2 +++ b/test/regress/regress1/sym/sym2.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2 index c6b87adeb..50ba55c42 100644 --- a/test/regress/regress1/sym/sym3.smt2 +++ b/test/regress/regress1/sym/sym3.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2 index 1cbd6f5b2..a69a23160 100644 --- a/test/regress/regress1/sym/sym4.smt2 +++ b/test/regress/regress1/sym/sym4.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-info :smt-lib-version 2.6) (set-logic QF_LIA) (set-info :category "crafted") diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 index 6b16d9d35..c13497acd 100644 --- a/test/regress/regress1/sym/sym5.smt2 +++ b/test/regress/regress1/sym/sym5.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status unsat) (declare-fun A () (Set Int)) diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2 index 10218ebc9..1161db24f 100644 --- a/test/regress/regress1/sym/sym6.smt2 +++ b/test/regress/regress1/sym/sym6.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-fun x () Int) diff --git a/test/regress/regress1/sym/sym7-uf.smt2 b/test/regress/regress1/sym/sym7-uf.smt2 index ee91240d3..8a343303e 100644 --- a/test/regress/regress1/sym/sym7-uf.smt2 +++ b/test/regress/regress1/sym/sym7-uf.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --symmetry-breaker-exp (set-logic ALL) (set-info :status sat) (declare-sort U 0) -- 2.30.2