diff options
Diffstat (limited to 'src')
23 files changed, 188 insertions, 2371 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5b07a7ca6..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 @@ -517,8 +513,6 @@ libcvc4_add_sources( theory/quantifiers/instantiate.h theory/quantifiers/lazy_trie.cpp theory/quantifiers/lazy_trie.h - theory/quantifiers/local_theory_ext.cpp - theory/quantifiers/local_theory_ext.h theory/quantifiers/quant_conflict_find.cpp theory/quantifiers/quant_conflict_find.h theory/quantifiers/quant_epr.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 926eacaae..e104101ef 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1935,15 +1935,6 @@ header = "options/quantifiers_options.h" help = "do instantiation based on local theory extensions" [[option]] - name = "ltePartialInst" - category = "regular" - long = "lte-partial-inst" - type = "bool" - default = "false" - read_only = true - help = "partially instantiate local theory quantifiers" - -[[option]] name = "lteRestrictInstClosure" category = "regular" long = "lte-restrict-inst-closure" 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 @@ -384,14 +384,6 @@ header = "options/smt_options.h" 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" short = "i" diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c0484e52b..d1fbfe969 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1841,7 +1841,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } else if (isBuiltinOperator) { - Trace("ajr-temp") << "mkTerm builtin operator" << std::endl; if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args 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<vector<Node>>& parts) -{ - vector<Node> constraints; - NodeManager* nm = NodeManager::currentNM(); - - for (const vector<Node>& 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<std::vector<Node>> 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<Node>& 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 <map> -#include <string> -#include <vector> -#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<bool>(true); - d_falseNode = NodeManager::currentNM()->mkConst<bool>(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<std::vector<Node> >& 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<int>(k); ++i) - { - result *= (n - i + 1); - result /= i; - } - return result; -} - -/** mk associative node - * - * This returns (a normal form for) the term <k>( children ), where - * k is an associative operator. We return a right-associative - * chain, since some operators (e.g. set union) require this. - */ -Node mkAssociativeNode(Kind k, std::vector<Node>& children) -{ - Assert(!children.empty()); - NodeManager* nm = NodeManager::currentNM(); - // sort and make right-associative chain - bool isComm = theory::quantifiers::TermUtil::isComm(k); - if (isComm) - { - std::sort(children.begin(), children.end()); - } - Node sn; - for (const Node& sc : children) - { - Assert(!sc.isNull()); - if (sn.isNull()) - { - sn = sc; - } - else - { - Assert(!isComm || sc.getType().isComparableTo(sn.getType())); - sn = nm->mkNode(k, sc, sn); - } - } - return sn; -} - -void Partition::printPartition(const char* c, Partition p) -{ - for (map<Node, vector<Node> >::iterator sub_vars_it = - p.d_subvar_to_vars.begin(); - sub_vars_it != p.d_subvar_to_vars.end(); - ++sub_vars_it) - { - Trace(c) << "[sym-dt] Partition: " << sub_vars_it->first << " -> {"; - - for (vector<Node>::iterator part_it = (sub_vars_it->second).begin(); - part_it != (sub_vars_it->second).end(); - ++part_it) - { - Trace(c) << " " << *part_it; - } - Trace(c) << " }" << endl; - } -} - -void Partition::addVariable(Node sv, Node v) -{ - d_subvar_to_vars[sv].push_back(v); - Assert(d_var_to_subvar.find(v) == d_var_to_subvar.end()); - d_var_to_subvar[v] = sv; -} - -void Partition::removeVariable(Node sv) -{ - std::map<Node, std::vector<Node> >::iterator its = d_subvar_to_vars.find(sv); - Assert(its != d_subvar_to_vars.end()); - for (const Node& v : its->second) - { - Assert(d_var_to_subvar.find(v) != d_var_to_subvar.end()); - d_var_to_subvar.erase(v); - } - d_subvar_to_vars.erase(sv); -} - -void Partition::normalize() -{ - for (std::pair<const Node, std::vector<Node> > p : d_subvar_to_vars) - { - std::sort(p.second.begin(), p.second.end()); - } -} -void Partition::getVariables(std::vector<Node>& vars) -{ - for (const std::pair<const Node, Node>& p : d_var_to_subvar) - { - vars.push_back(p.first); - } -} - -void Partition::getSubstitution(std::vector<Node>& vars, - std::vector<Node>& subs) -{ - for (const std::pair<const Node, Node>& p : d_var_to_subvar) - { - vars.push_back(p.first); - subs.push_back(p.second); - } -} - -void PartitionMerger::initialize(Kind k, - const std::vector<Partition>& partitions, - const std::vector<unsigned>& indices) -{ - d_kind = k; - Trace("sym-dt-debug") << "Initialize partition merger..." << std::endl; - Trace("sym-dt-debug") << "Count variable occurrences..." << std::endl; - for (unsigned index : indices) - { - d_indices.push_back(index); - const Partition& p = partitions[index]; - const std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second; - for (const Node& v : svs) - { - if (d_occurs_count.find(v) == d_occurs_count.end()) - { - d_occurs_count[v] = 1; - } - else - { - d_occurs_count[v]++; - } - d_occurs_by[index][v] = d_occurs_count[v] - 1; - } - } - if (Trace.isOn("sym-dt-debug")) - { - Trace("sym-dt-debug") << " variable occurrences: " << std::endl; - for (const std::pair<const Node, unsigned>& o : d_occurs_count) - { - Trace("sym-dt-debug") - << " " << o.first << " -> " << o.second << std::endl; - } - } -} - -bool PartitionMerger::merge(std::vector<Partition>& partitions, - unsigned base_index, - std::unordered_set<unsigned>& active_indices, - std::vector<unsigned>& 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<Node>& svs = p.d_subvar_to_vars.begin()->second; - Trace("sym-dt-debug") << " try basis: " << svs << std::endl; - // try to merge variables one-by-one - d_base_indices.clear(); - d_base_indices.insert(base_index); - d_base_vars.clear(); - d_base_vars.insert(svs.begin(), svs.end()); - d_num_new_indices_needed = d_base_vars.size(); - bool merged = false; - bool success = false; - unsigned base_choose = d_base_vars.size() - 1; - unsigned base_occurs_req = d_base_vars.size(); - do - { - Trace("sym-dt-debug") << " base variables must occur " << base_occurs_req - << " times." << std::endl; - // check if all the base_vars occur at least the required number of times - bool var_ok = true; - for (const Node& v : d_base_vars) - { - if (d_occurs_count[v] < base_occurs_req) - { - Trace("sym-dt-debug") << "...failed variable " << v << std::endl; - var_ok = false; - break; - } - } - if (!var_ok) - { - // cannot merge due to a base variable - break; - } - // try to find a new variable to merge - Trace("sym-dt-debug") << " must find " << d_num_new_indices_needed - << " new indices to merge." << std::endl; - std::vector<unsigned> new_indices; - Node merge_var; - d_merge_var_tried.clear(); - if (mergeNewVar(0, new_indices, merge_var, 0, partitions, active_indices)) - { - 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<unsigned>& new_indices, - Node& merge_var, - unsigned num_merge_var_max, - std::vector<Partition>& partitions, - std::unordered_set<unsigned>& active_indices) -{ - Assert(new_indices.size() < d_num_new_indices_needed); - if (curr_index == d_indices.size()) - { - return false; - } - Trace("sym-dt-debug2") << "merge " << curr_index << " / " << d_indices.size() - << ", 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<Node>& svs = p.d_subvar_to_vars.begin()->second; - bool include_success = true; - Node curr_merge_var; - for (const Node& v : svs) - { - if (d_base_vars.find(v) == d_base_vars.end() && v != merge_var) - { - if (merge_var.isNull() && curr_merge_var.isNull()) - { - curr_merge_var = v; - } - else - { - // cannot include - Trace("sym-dt-debug2") << "...cannot include (new-var)\n"; - include_success = false; - curr_merge_var = Node::null(); - break; - } - } - } - if (!curr_merge_var.isNull()) - { - // compute the maximum number of indices we can include for v - Assert(d_occurs_by[index].find(curr_merge_var) - != d_occurs_by[index].end()); - Assert(d_occurs_count.find(curr_merge_var) != d_occurs_count.end()); - unsigned num_v_max = - d_occurs_count[curr_merge_var] - d_occurs_by[index][curr_merge_var]; - if (num_v_max >= d_num_new_indices_needed) - { - // have we already tried this merge_var? - if (d_merge_var_tried.find(curr_merge_var) != d_merge_var_tried.end()) - { - include_success = false; - Trace("sym-dt-debug2") - << "...cannot include (already tried new merge var " - << curr_merge_var << ")\n"; - } - else - { - Trace("sym-dt-debug2") - << "set merge var : " << curr_merge_var << std::endl; - d_merge_var_tried.insert(curr_merge_var); - num_merge_var_max = num_v_max; - merge_var = curr_merge_var; - } - } - else - { - Trace("sym-dt-debug2") - << "...cannot include (not enough room for new merge var " - << num_v_max << "<" << d_num_new_indices_needed << ")\n"; - include_success = false; - } - } - else if (!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<Node> children; - children.push_back(p.d_term); - std::vector<Node> schildren; - schildren.push_back(p.d_sterm); - // can now include in the base - d_base_vars.insert(merge_var); - Trace("sym-dt-debug") << "found symmetry : { "; - for (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<bool>(true); - d_falseNode = NodeManager::currentNM()->mkConst<bool>(false); -} - -Partition SymmetryDetect::detect(const vector<Node>& assertions) -{ - Node an; - if (assertions.empty()) - { - an = d_trueNode; - } - else if (assertions.size() == 1) - { - an = assertions[0]; - } - else - { - an = NodeManager::currentNM()->mkNode(kind::AND, assertions); - } - Partition p = findPartitions(an); - Trace("sym-dt") << endl - << "------------------------------ The Final Partition " - "------------------------------" - << endl; - if(Trace.isOn("sym-dt")) - { - Partition::printPartition("sym-dt", p); - } - return p; -} - -Node SymmetryDetect::getSymBreakVariable(TypeNode tn, unsigned index) -{ - std::map<TypeNode, std::vector<Node> >::iterator it = d_sb_vars.find(tn); - if (it == d_sb_vars.end()) - { - // initialize the variables for type tn - d_sb_vars[tn].clear(); - it = d_sb_vars.find(tn); - } - 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<TypeNode, unsigned>& index) -{ - // ensure we use a new index for this variable - unsigned new_index = 0; - std::map<TypeNode, unsigned>::iterator itt = index.find(tn); - if (itt != index.end()) - { - new_index = itt->second; - } - index[tn] = new_index + 1; - return getSymBreakVariable(tn, new_index); -} - -void SymmetryDetect::compute(std::vector<std::vector<Node> >& part, - const std::vector<Node>& assertions) -{ - Partition p = detect(assertions); - - std::vector<std::vector<Node> > parts; - for (map<Node, vector<Node> >::const_iterator subvar_to_vars_it = - p.d_subvar_to_vars.begin(); - subvar_to_vars_it != p.d_subvar_to_vars.end(); - ++subvar_to_vars_it) - { - parts.push_back(subvar_to_vars_it->second); - } -} -void SymmetryDetect::computeTerms(std::vector<std::vector<Node> >& sterms, - const std::vector<Node>& assertions) -{ - Partition p = detect(assertions); - - for (const std::pair<const Node, std::vector<Node> > sp : p.d_subvar_to_vars) - { - if (sp.second.size() > 1) - { - // A naive method would do sterms.push_back(sp.second), that is, say that - // the variables themselves are symmetric terms. However, the following - // code finds some subterms of assertions that are symmetric under this - // set in the variable partition. For example, for the input: - // f(x)+f(y) >= 0 - // naively {x, y} are reported as symmetric terms, but below ensures we - // say {f(x), f(y)} are reported as symmetric terms instead. - Node sv = sp.first; - Trace("sym-dt-tsym-cons") - << "Construct term symmetry from " << sp.second << "..." << std::endl; - // choose an arbitrary term symmetry - std::vector<unsigned>& tsids = d_var_to_tsym_ids[sp.second[0]]; - if (tsids.empty()) - { - // no (ground) term symmetries, just use naive - sterms.push_back(sp.second); - } - else - { - unsigned tsymId = tsids[tsids.size() - 1]; - Trace("sym-dt-tsym-cons") << "...use tsym id " << tsymId << std::endl; - // get the substitution - std::vector<Node> vars; - std::vector<Node> subs; - for (const Node& v : sp.second) - { - vars.push_back(v); - subs.push_back(sv); - } - std::vector<Node>& tsym = d_tsyms[tsymId]; - // map terms in this symmetry to their final form - std::vector<unsigned> tsym_indices; - std::vector<Node> tsym_terms; - for (unsigned j = 0, size = tsym.size(); j < size; j++) - { - Node tst = tsym[j]; - Node tsts = tst.substitute( - vars.begin(), vars.end(), subs.begin(), subs.end()); - tsym_indices.push_back(j); - tsym_terms.push_back(tsts); - } - // take into account alpha-equivalence - std::map<Node, std::vector<unsigned> > t_to_st; - computeAlphaEqTerms(tsym_indices, tsym_terms, t_to_st); - Node tshUse; - for (const std::pair<const Node, std::vector<unsigned> >& tsh : t_to_st) - { - Trace("sym-dt-tsym-cons-debug") - << " " << tsh.first << " -> #" << tsh.second.size() << std::endl; - if (tsh.second.size() > 1) - { - tshUse = tsh.first; - break; - } - } - if (!tshUse.isNull()) - { - std::vector<Node> tsymCons; - for (unsigned j : t_to_st[tshUse]) - { - tsymCons.push_back(tsym[j]); - } - Trace("sym-dt-tsym-cons") << "...got " << tsymCons << std::endl; - sterms.push_back(tsymCons); - } - } - } - } -} - -/** - * We build the partition trie indexed by - * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a - * partition trie are the new regions of a partition - */ -class PartitionTrie -{ - public: - /** Variables at the leave */ - std::vector<Node> d_variables; - /** The mapping from a node to its children */ - std::map<Node, PartitionTrie> d_children; -}; - -Partition SymmetryDetect::findPartitions(Node node) -{ - Trace("sym-dt-debug") - << "------------------------------------------------------------" << endl; - Trace("sym-dt-debug") << "[sym-dt] findPartitions gets a term: " << node - << endl; - map<Node, Partition>::iterator partition = d_term_partition.find(node); - - // Return its partition from cache if we have processed the node before - if (partition != d_term_partition.end()) - { - Trace("sym-dt-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<Node> children; - bool operatorChild = false; - if (node.getKind() == APPLY_UF) - { - // compute for the operator - children.push_back(node.getOperator()); - operatorChild = true; - } - if (!isAssocComm) - { - children.insert(children.end(), node.begin(), node.end()); - } - else - { - collectChildren(node, children); - } - Trace("sym-dt-debug") << "[sym-dt] children: " << children << endl; - - // Partitions of children - std::vector<Partition> partitions; - // Create partitions for children - std::unordered_set<unsigned> active_indices; - for (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<unsigned> indices; - std::vector<Node> 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<Node, std::vector<unsigned> > sterm_to_indices; - computeAlphaEqTerms(indices, sterms, sterm_to_indices); - - for (const std::pair<Node, std::vector<unsigned> >& sti : sterm_to_indices) - { - 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<Node> fixedSVar; - std::vector<Node> fixedVar; - processPartitions( - k, partitions, sti.second, active_indices, fixedSVar, fixedVar); - } - } - // initially set substituted term to node - p.d_sterm = node; - // for all active indices - vector<Node> all_vars; - 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<const Node, vector<Node> >& 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<TypeNode, unsigned> type_index; - type_index.clear(); - // the indices we need to reconstruct - std::map<unsigned, bool> rcons_indices; - // Build the partition trie - std::sort(all_vars.begin(), all_vars.end()); - // for each variable - for (const Node& n : all_vars) - { - Trace("sym-dt-debug") << "[sym-dt] Add a variable {" << n - << "} to the partition trie, #partitions = " - << active_indices.size() << "..." << endl; - std::vector<Node> subvars; - std::vector<unsigned> useVarInd; - Node useVar; - for (unsigned i : active_indices) - { - Partition& pa = partitions[i]; - std::map<Node, Node>::iterator var_sub_it = pa.d_var_to_subvar.find(n); - if (var_sub_it != pa.d_var_to_subvar.end()) - { - 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<Node> pvars; - std::vector<Node> psubs; - if (!rcons_indices.empty()) - { - p.getSubstitution(pvars, psubs); - } - - // Reconstruct the substituted node - p.d_term = node; - std::vector<Node> schildren; - if (!isAssocComm) - { - 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<Node>& 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<Node> visit; - visit.push_back(node); - unordered_set<Node, NodeHashFunction> 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<unsigned>& indices, - const std::vector<Node>& sterms, - std::map<Node, std::vector<unsigned> >& sterm_to_indices) -{ - Assert(indices.size() == sterms.size()); - // also store quantified formulas, since these may be alpha-equivalent - std::vector<unsigned> quant_sterms; - for (unsigned j = 0, size = indices.size(); j < size; j++) - { - Node st = sterms[j]; - Assert(!st.isNull()); - if (st.getKind() == FORALL) - { - quant_sterms.push_back(j); - } - else - { - sterm_to_indices[st].push_back(indices[j]); - } - } - // process the quantified formulas - if (quant_sterms.size() == 1) - { - // only one quantified formula, won't be alpha equivalent - unsigned j = quant_sterms[0]; - sterm_to_indices[sterms[j]].push_back(indices[j]); - } - else if (!quant_sterms.empty()) - { - theory::quantifiers::AlphaEquivalenceDb aedb(&d_tcanon); - for (unsigned j : quant_sterms) - { - // project via alpha equivalence - Node st = sterms[j]; - Node st_ae = aedb.addTerm(st); - sterm_to_indices[st_ae].push_back(indices[j]); - } - } -} - -/** A basic trie for storing vectors of arguments */ -class NodeTrie -{ - public: - NodeTrie() {} - /** value at this node*/ - std::vector<unsigned> d_value; - /** children of this node */ - std::map<Node, NodeTrie> d_children; - /** clear the children */ - void clear() { d_children.clear(); } - /** - * Return true iff we've added the suffix of the vector of arguments starting - * at index before. - */ - unsigned add(unsigned value, - const std::vector<Node>& args, - unsigned index = 0) - { - 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<Partition>& partitions, - const std::vector<unsigned>& indices, - std::unordered_set<unsigned>& active_indices, - std::vector<Node>& fixedSVar, - std::vector<Node>& fixedVar) -{ - Assert(!indices.empty()); - unsigned first_index = indices[0]; - if (Trace.isOn("sym-dt-debug")) - { - Trace("sym-dt-debug") << "[sym-dt] process partitions for "; - for (unsigned i : indices) - { - Trace("sym-dt-debug") << i << " "; - } - Trace("sym-dt-debug") << std::endl; - } - unsigned num_sb_vars = partitions[first_index].d_subvar_to_vars.size(); - if (num_sb_vars == 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<Node, NodeTrie> svarTrie; - std::map<Node, std::map<unsigned, std::vector<unsigned> > > svarEqc; - - for (unsigned j = 0, size = indices.size(); j < size; j++) - { - unsigned index = indices[j]; - Partition& p = partitions[index]; - for (const std::pair<const Node, std::vector<Node> > ps : - p.d_subvar_to_vars) - { - Node sv = ps.first; - unsigned res = svarTrie[sv].add(index, ps.second); - svarEqc[sv][res].push_back(index); - } - } - Trace("sym-dt-debug") - << "...multiple symmetry breaking variables, regroup and drop" - << std::endl; - unsigned minGroups = indices.size(); - Node svarMin; - for (const std::pair<const Node, - std::map<unsigned, std::vector<unsigned> > > sve : - svarEqc) - { - if (Trace.isOn("sym-dt-debug")) - { - Trace("sym-dt-debug") << "For " << sve.first << " : "; - for (const std::pair<const unsigned, std::vector<unsigned> > svee : - sve.second) - { - Trace("sym-dt-debug") << "{ "; - for (unsigned i : svee.second) - { - Trace("sym-dt-debug") << i << " "; - } - Trace("sym-dt-debug") << "}"; - } - } - unsigned ngroups = sve.second.size(); - Trace("sym-dt-debug") << ", #groups=" << ngroups << std::endl; - if (ngroups < minGroups) - { - minGroups = ngroups; - svarMin = sve.first; - if (minGroups == 1) - { - break; - } - } - } - if (minGroups == indices.size()) - { - // can only handle symmetries that are classified by { n } - Trace("sym-dt-debug") << "...failed to merge (multiple symmetry breaking " - "vars with no groups)" - << std::endl; - return; - } - // recursive call for each group - for (const std::pair<unsigned, std::vector<unsigned> >& svee : - svarEqc[svarMin]) - { - Assert(!svee.second.empty()); - unsigned firstIndex = svee.second[0]; - unsigned nfvars = 0; - Trace("sym-dt-debug") << "Recurse, fixing " << svarMin << " -> { "; - // add the list of fixed variables - for (const Node& v : partitions[firstIndex].d_subvar_to_vars[svarMin]) - { - Trace("sym-dt-debug") << v << " "; - fixedSVar.push_back(svarMin); - fixedVar.push_back(v); - nfvars++; - } - Trace("sym-dt-debug") << "}" << std::endl; - - // remove it from each of the partitions to process - for (unsigned pindex : svee.second) - { - partitions[pindex].removeVariable(svarMin); - } - - // recursive call - processPartitions( - k, partitions, svee.second, active_indices, fixedSVar, fixedVar); - - // remove the list of fixed variables - for (unsigned 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<unsigned, std::vector<unsigned> > 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<const unsigned, std::vector<unsigned> >& 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<unsigned> nvis; - for (unsigned index : nvi.second) - { - Partition& p = partitions[index]; - std::vector<Node>& svs = p.d_subvar_to_vars.begin()->second; - unsigned aindex = ntrie.add(index, svs); - if (aindex == index) - { - nvis.insert(index); - } - else if (theory::quantifiers::TermUtil::isNonAdditive(k)) - { - Trace("sym-dt-debug") - << "Drop duplicate child : " << index << std::endl; - Assert(active_indices.find(index) != active_indices.end()); - active_indices.erase(index); - } - else - { - nvis.erase(aindex); - } - } - std::vector<unsigned> check_indices; - check_indices.insert(check_indices.end(), nvis.begin(), nvis.end()); - // 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<Partition>& partitions, - const std::vector<unsigned>& indices, - std::unordered_set<unsigned>& 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<unsigned> 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<Node> symTerms; - // include the term from the base index - symTerms.push_back(mterm); - for (unsigned mi : merged_indices) - { - Node st = partitions[mi].d_term; - symTerms.push_back(st); - } - Trace("sym-dt-debug") << " ......merged " << symTerms << std::endl; - std::vector<Node> vars; - partitions[index].getVariables(vars); - storeTermSymmetry(symTerms, vars); - Trace("sym-dt-debug") << " ......recurse" << std::endl; - std::vector<unsigned> rem_indices; - for (unsigned ii : indices) - { - 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<Node>& symTerms, - const std::vector<Node>& vars) -{ - Trace("sym-dt-tsym") << "*** Term symmetry : " << symTerms << std::endl; - Trace("sym-dt-tsym") << "*** Over variables : " << vars << std::endl; - // cannot have free variable - if (expr::hasFreeVar(symTerms[0])) - { - Trace("sym-dt-tsym") << "...free variable, do not allocate." << std::endl; - return; - } - - unsigned tid = d_tsym_id_counter; - Trace("sym-dt-tsym") << "...allocate id " << tid << std::endl; - d_tsym_id_counter = d_tsym_id_counter + 1; - // allocate the term symmetry - d_tsyms[tid] = symTerms; - d_tsym_to_vars[tid] = vars; - for (const Node& v : vars) - { - d_var_to_tsym_ids[v].push_back(tid); - } -} - -} // namespace symbreak -} // namespace passes -} // namespace preprocessing -} // 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 <map> -#include <string> -#include <vector> -#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<Node, Node> d_var_to_subvar; - - /** - * Mapping between the symmetry breaking variables and variables, e.g. - * { w-> { x, y } } - */ - std::map<Node, std::vector<Node> > d_subvar_to_vars; - /** Add variable v to d_subvar_to_vars[sv]. */ - void addVariable(Node sv, Node v); - /** Remove variable sv from the domain of d_subvar_to_vars. */ - void removeVariable(Node sv); - /** Sorts the ranges of d_subvar_to_vars. */ - void normalize(); - /** Print a partition */ - static void printPartition(const char* c, Partition p); - /** get variables */ - void getVariables(std::vector<Node>& vars); - /** get substitution */ - void getSubstitution(std::vector<Node>& vars, std::vector<Node>& subs); -}; - -/** partition merger - * - * This class is used to identify sets of children of commutative operators k - * that are identical up to a set of automorphisms. - * - * This class is used when we have detected symmetries for the children - * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative - * operator. For each i=1,...n, partitions[i] represents symmetries (in the - * form of a partition) computed for the child t_i. - * - * The vector d_indices of this class stores a list ( i_1...i_m ) such that - * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent - * for each j=1...m, where * is application of substitution. - * - * In detail, we say that - * partition[j1] = { w -> X_1 }, - * ..., - * partition[jp] = { w -> X_p } - * are mergeable if s=|X_1|=...=|X_p|, and all subsets of - * X* = ( union_{k=1...p} X_k ) of size s are equal to exactly one of - * X_1 ... X_p. - */ -class PartitionMerger -{ - public: - PartitionMerger() - : d_kind(kind::UNDEFINED_KIND), - d_master_base_index(0), - d_num_new_indices_needed(0) - { - } - /** initialize this class - * - * We will be trying to merge the given partitions that occur at the given - * indices. k is the kind of the operator that partitions are children of. - */ - void initialize(Kind k, - const std::vector<Partition>& partitions, - const std::vector<unsigned>& indices); - /** merge - * - * This method tries to "merge" partitions occurring at the indices d_indices - * of the vector partitions. - * - * Assuming the setting described above, if there exists a mergeable set of - * partitions with indices (j_m1...j_mp), we remove {j_m1...j_mp} \ { j_m1 } - * from active_indices, and update partition[j1] := { w -> X* }. - * - * The base_index is an index from d_indices that serves as a basis for - * detecting this symmetry. In particular, we start by assuming that - * p=1, and j_m1 is base_index. We proceed by trying to find sets of indices - * that add exactly one variable to X* at a time. We return - * true if p>1, that is, at least one partition was merged with the - * base_index. - */ - bool merge(std::vector<Partition>& partitions, - unsigned base_index, - std::unordered_set<unsigned>& active_indices, - std::vector<unsigned>& merged_indices); - - private: - /** the kind of the node we are consdiering */ - Kind d_kind; - /** indices we are considering */ - std::vector<unsigned> d_indices; - /** count the number of times each variable occurs */ - std::map<Node, unsigned> d_occurs_count; - /** the number of times each variable occurs up to the given index */ - std::map<unsigned, std::map<Node, unsigned> > d_occurs_by; - /** current master base index */ - unsigned d_master_base_index; - /** the indices that occur in the current symmetry (the list (j1...jp)) */ - std::unordered_set<unsigned> d_base_indices; - /** the free variables that occur in the current symmetry (the set X*)*/ - std::unordered_set<Node, NodeHashFunction> d_base_vars; - /** the number of indices we need to add to extended X* by one variable */ - unsigned d_num_new_indices_needed; - /** the variables we have currently tried to add to X* */ - std::unordered_set<Node, NodeHashFunction> d_merge_var_tried; - /** merge new variable - * - * This is a recursive helper for the merge function. This function attempts - * to construct a set of indices {j1...jp} of partitions and a variable - * "merge_var" such that partitions[ji] is of the form { w -> X_ji }, where - * merge_var in X_ji and ( X_ji \ { merge_var } ) is a subset of the base - * variables X*. We require that p = d_num_new_indices_needed, where - * d_num_new_indices_needed is - * |d_base_vars| choose (|X_ji|-1) - * that is, n!/((n-k)!*k!) where n=|d_base_vars| and k=|X_ji|-1. - * - * curr_index : the index of d_indices we are currently considering whether - * to add to new_indices, - * new_indices : the currently considered indices {j1...jp}, - * merge_var : the variable we are currently trying to add to X*, - * new_merge_var_max : the maximum number of times that merge_var might - * appear in remainding indices, i.e. d_indices[curr_index]...d_indices.end(), - * which is used as an optimization for recognizing quickly when this method - * will fail. - */ - bool mergeNewVar(unsigned curr_index, - std::vector<unsigned>& new_indices, - Node& merge_var, - unsigned num_merge_var_max, - std::vector<Partition>& partitions, - std::unordered_set<unsigned>& active_indices); -}; - -/** - * 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<std::vector<Node> >& part, - const std::vector<Node>& assertions); - - /** Get the final partition after symmetry detection. - * - * If a vector in sterms contains two terms t and s, - * then assertions and assertions { t -> s, s -> t } are - * equisatisfiable. - * */ - void computeTerms(std::vector<std::vector<Node> >& sterms, - const std::vector<Node>& assertions); - - private: - /** (canonical) symmetry breaking variables for each type */ - std::map<TypeNode, std::vector<Node> > 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<TypeNode, unsigned>& 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<Node, Partition> 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<Node>& 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<Node>& children); - - /** Compute alpha equivalent terms - * - * This is used for determining pairs of terms in sterms that are - * alpha-equivalent. In detail, this constructs sterm_to_indices such that if - * sterm_to_indices[t] contains an index i, then there exists a k such that - * indices[k] = i and sterms[k] is alpha-equivalent to t, and sterm_to_indices - * contains indices[k] for each k=1,...,indicies.size()-1. For example, - * computeAlphaEqTerms( { 0, 3, 7 }, { Q(a), forall x. P(x), forall y. P(y) } - * may construct sterm_to_indices such that - * sterm_to_indices[Q(a)] -> { 0 } - * sterm_to_indices[forall x. P(x)] -> { 3, 7 } - */ - void computeAlphaEqTerms( - const std::vector<unsigned>& indices, - const std::vector<Node>& sterms, - std::map<Node, std::vector<unsigned> >& sterm_to_indices); - /** process partitions - * - * This method is called when we have detected symmetries for the children - * of a term t of the form <k>( t_1, ..., t_n ), where k is a commutative - * operator. The vector indices stores a list ( i_1...i_m ) such that - * ( t_i_j * partition[i_j].d_var_to_subvar ) is syntactically equivalent - * for each j=1...m, where * is application of substitution. In particular, - * ( t_i_j * partition[i_j].d_var_to_subvar ) is equal to - * partitions[i_j].d_sterm for each j=1...m. - * - * This function calls mergePartitions on subsets of these indices for which - * it is possible to "merge" (see PartitionMerger). In particular, we consider - * subsets of indices whose corresponding partitions are of the form - * { w -> { x1...xn } } - * for each n. This means that partitions like { w -> { x1 } } and - * { w -> { x1 x2 } } are considered separately when merging. - */ - void processPartitions(Kind k, - std::vector<Partition>& partitions, - const std::vector<unsigned>& indices, - std::unordered_set<unsigned>& active_indices, - std::vector<Node>& fixedSVar, - std::vector<Node>& 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<Partition>& partitions, - const std::vector<unsigned>& indices, - std::unordered_set<unsigned>& active_indices); - //-------------------for symmetry breaking terms - /** symmetry breaking id counter */ - unsigned d_tsym_id_counter; - /** list of term symmetries */ - std::map<unsigned, std::vector<Node> > d_tsyms; - /** list of term symmetries */ - std::map<unsigned, std::vector<Node> > d_tsym_to_vars; - /** variables to ids */ - std::map<Node, std::vector<unsigned> > d_var_to_tsym_ids; - /** store term symmetry */ - void storeTermSymmetry(const std::vector<Node>& symTerms, - const std::vector<Node>& vars); - //-------------------end for symmetry breaking terms -}; - -} // namespace symbreak -} // namespace passes -} // namespace preprocessing -} // 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<MipLibTrick>); registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>); registerPassInfo("ackermann", callCtor<Ackermann>); - registerPassInfo("sym-break", callCtor<SymBreakerPass>); registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>); registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>); registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>); diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index c8284762c..21636650d 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -69,7 +69,7 @@ ProofRule CnfProof::getProofRule(ClauseId clause) { Node CnfProof::getAssertionForClause(ClauseId clause) { ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); - Assert(it != d_clauseToAssertion.end()); + Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull()); return (*it).second; } @@ -135,8 +135,15 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { // case we keep the first assertion. For example asserting a /\ b // and then b /\ c where b is an atom, would assert b twice (note // that since b is top level, it is not cached by the CnfStream) - if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) + // + // Note: If the current assertion associated with the clause is null, we + // update it because it means that it was previously added the clause without + // associating it with an assertion. + const auto& it = d_clauseToAssertion.find(clause); + if (it != d_clauseToAssertion.end() && (*it).second != Node::null()) + { return; + } d_clauseToAssertion.insert (clause, expr); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 6690f12db..aa5bb92d9 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -160,8 +160,19 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // If we were called with something other than a theory atom (or // Boolean variable), we get a SatLiteral that is definitionally // equal to it. + // + // We are setting the current assertion to be null. This is because `toCNF` + // may add clauses to the SAT solver and we look up the current assertion + // in that case. Setting it to null ensures that the assertion stack is + // non-empty and that we are not associating a bogus assertion with the + // clause. This should be ok because we use the mapping back to assertions + // for clauses from input assertions only. + PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); }); + lit = toCNF(n, false); + PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); }); + // Store backward-mappings // These may already exist d_literalToNodeMap.insert_safe(lit, n); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5b5504cc5..27d06e104 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/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b82b958af..bccb33f1d 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -66,12 +66,14 @@ Node OpArgIndex::getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& a } } return Node::null(); - }else{ - std::vector< TNode > args2; + } + std::vector<TNode> args2; + if (d_op_terms[0].getMetaKind() == kind::metakind::PARAMETERIZED) + { args2.push_back( d_ops[0] ); - args2.insert( args2.end(), args.begin(), args.end() ); - return NodeManager::currentNM()->mkNode( d_op_terms[0].getKind(), args2 ); } + args2.insert(args2.end(), args.begin(), args.end()); + return NodeManager::currentNM()->mkNode(d_op_terms[0].getKind(), args2); } void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ) { diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp deleted file mode 100644 index a3de5ced9..000000000 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ /dev/null @@ -1,270 +0,0 @@ -/********************* */ -/*! \file local_theory_ext.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, 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 Implementation of local theory ext utilities - **/ - -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/first_order_model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - - -LtePartialInst::LtePartialInst( QuantifiersEngine * qe, context::Context* c ) : -QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){ - -} - -/** add quantifier */ -void LtePartialInst::checkOwnership(Node q) -{ - if( !q.getAttribute(LtePartialInstAttribute()) ){ - if( d_do_inst.find( q )!=d_do_inst.end() ){ - if( d_do_inst[q] ){ - d_lte_asserts.push_back( q ); - d_quantEngine->setOwner( q, this ); - } - }else{ - d_vars[q].clear(); - d_pat_var_order[q].clear(); - //check if this quantified formula is eligible for partial instantiation - std::map< Node, bool > vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars[q[0][i]] = false; - } - getEligibleInstVars( q[1], vars ); - - //instantiate only if we would force ground instances - std::map< Node, int > var_order; - bool doInst = true; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - if( vars[q[0][i]] ){ - d_vars[q].push_back( q[0][i] ); - var_order[q[0][i]] = i; - }else{ - Trace("lte-partial-inst-debug") << "...do not consider, variable " << q[0][i] << " was not found in correct position in body." << std::endl; - doInst = false; - break; - } - } - if( doInst ){ - //also needs patterns - if( q.getNumChildren()==3 && q[2].getNumChildren()==1 ){ - for( unsigned i=0; i<q[2][0].getNumChildren(); i++ ){ - Node pat = q[2][0][i]; - if( pat.getKind()==APPLY_UF ){ - for( unsigned j=0; j<pat.getNumChildren(); j++ ){ - if( !addVariableToPatternList( pat[j], d_pat_var_order[q], var_order ) ){ - doInst = false; - } - } - }else if( !addVariableToPatternList( pat, d_pat_var_order[q], var_order ) ){ - doInst = false; - } - if( !doInst ){ - Trace("lte-partial-inst-debug") << "...do not consider, cannot resolve pattern : " << pat << std::endl; - break; - } - } - }else{ - Trace("lte-partial-inst-debug") << "...do not consider (must have exactly one pattern)." << std::endl; - } - } - - - Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl; - d_do_inst[q] = doInst; - if( doInst ){ - d_lte_asserts.push_back( q ); - d_needsCheck = true; - d_quantEngine->setOwner( q, this ); - } - } - } -} - -bool LtePartialInst::addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ) { - std::map< Node, int >::iterator it = var_order.find( v ); - if( it==var_order.end() ){ - return false; - }else if( std::find( pat_var_order.begin(), pat_var_order.end(), it->second )!=pat_var_order.end() ){ - return false; - }else{ - pat_var_order.push_back( it->second ); - return true; - } -} - -void LtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) { - if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( vars.find( n[i] )!=vars.end() ){ - vars[n[i]] = true; - } - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getEligibleInstVars( n[i], vars ); - } -} - -/* whether this module needs to check this round */ -bool LtePartialInst::needsCheck( Theory::Effort e ) { - return e>=Theory::EFFORT_FULL && d_needsCheck; -} -/* Call during quantifier engine's check */ -void LtePartialInst::check(Theory::Effort e, QEffort quant_e) -{ - //flush lemmas ASAP (they are a reduction) - if (quant_e == QEFFORT_CONFLICT && d_needsCheck) - { - std::vector< Node > lemmas; - getInstantiations( lemmas ); - //add lemmas to quantifiers engine - for( unsigned i=0; i<lemmas.size(); i++ ){ - d_quantEngine->addLemma( lemmas[i], false ); - } - d_needsCheck = false; - } -} - - -void LtePartialInst::reset() { - d_reps.clear(); - eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tn = r.getType(); - d_reps[tn].push_back( r ); - ++eqcs_i; - } -} - - -/** get instantiations */ -void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { - Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; - reset(); - for( unsigned i=0; i<d_lte_asserts.size(); i++ ){ - Node q = d_lte_asserts[i]; - Assert(d_do_inst.find(q) != d_do_inst.end() && d_do_inst[q]); - if( d_inst.find( q )==d_inst.end() ){ - Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl; - d_inst[q] = true; - Assert(!d_vars[q].empty()); - //make bound list - Node bvl; - std::vector< Node > bvs; - for( unsigned j=0; j<q[0].getNumChildren(); j++ ){ - if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){ - bvs.push_back( q[0][j] ); - } - } - if( !bvs.empty() ){ - bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); - } - std::vector< Node > conj; - std::vector< Node > terms; - std::vector< TypeNode > types; - for( unsigned j=0; j<d_vars[q].size(); j++ ){ - types.push_back( d_vars[q][j].getType() ); - terms.push_back( Node::null() ); - } - - getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, NULL, 0, 0, 0 ); - Assert(!conj.empty()); - lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); - d_wasInvoked = true; - } - } -} - -void LtePartialInst::getPartialInstantiations(std::vector<Node>& conj, - Node q, - Node bvl, - std::vector<Node>& vars, - std::vector<Node>& terms, - std::vector<TypeNode>& types, - TNodeTrie* curr, - unsigned pindex, - unsigned paindex, - unsigned iindex) -{ - if( iindex==vars.size() ){ - Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( bvl.isNull() ){ - conj.push_back( body ); - Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; - }else{ - Node nq; - if( q.getNumChildren()==3 ){ - Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); - }else{ - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - } - Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; - LtePartialInstAttribute ltpia; - nq.setAttribute(ltpia,true); - conj.push_back( nq ); - } - }else{ - Assert(pindex < q[2][0].getNumChildren()); - Node pat = q[2][0][pindex]; - Assert(pat.getNumChildren() == 0 || paindex <= pat.getNumChildren()); - if( pat.getKind()==APPLY_UF ){ - Assert(paindex <= pat.getNumChildren()); - if( paindex==pat.getNumChildren() ){ - getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex ); - }else{ - if( !curr ){ - Assert(paindex == 0); - //start traversing term index for the operator - curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() ); - } - for (std::pair<const TNode, TNodeTrie>& t : curr->d_data) - { - terms[d_pat_var_order[q][iindex]] = t.first; - getPartialInstantiations(conj, - q, - bvl, - vars, - terms, - types, - &t.second, - pindex, - paindex + 1, - iindex + 1); - } - } - }else{ - std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] ); - if( it!=d_reps.end() ){ - Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[iindex] << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - terms[d_pat_var_order[q][iindex]] = it->second[i]; - getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex+1 ); - } - }else{ - Trace("lte-partial-inst-debug") << "No reps found of type " << types[iindex] << std::endl; - } - } - } -} diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h deleted file mode 100644 index d39ea3cfe..000000000 --- a/src/theory/quantifiers/local_theory_ext.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file local_theory_ext.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** 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 local theory extensions util - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__LOCAL_THEORY_EXT_H -#define CVC4__THEORY__LOCAL_THEORY_EXT_H - -#include "context/cdo.h" -#include "expr/attribute.h" -#include "expr/node_trie.h" -#include "theory/quantifiers/quant_util.h" - -namespace CVC4 { -namespace theory { - -/** Attribute true for quantifiers that do not need to be partially instantiated - */ -struct LtePartialInstAttributeId -{ -}; -typedef expr::Attribute<LtePartialInstAttributeId, bool> - LtePartialInstAttribute; - -namespace quantifiers { - -class LtePartialInst : public QuantifiersModule { -private: - // was this module invoked - bool d_wasInvoked; - // needs check - bool d_needsCheck; - //representatives per type - std::map< TypeNode, std::vector< Node > > d_reps; - // should we instantiate quantifier - std::map< Node, bool > d_do_inst; - // have we instantiated quantifier - std::map< Node, bool > d_inst; - std::map< Node, std::vector< Node > > d_vars; - std::map< Node, std::vector< int > > d_pat_var_order; - /** list of relevant quantifiers asserted in the current context */ - std::vector< Node > d_lte_asserts; - /** reset */ - void reset(); - /** get instantiations */ - void getInstantiations( std::vector< Node >& lemmas ); - void getPartialInstantiations(std::vector<Node>& conj, - Node q, - Node bvl, - std::vector<Node>& vars, - std::vector<Node>& inst, - std::vector<TypeNode>& types, - TNodeTrie* curr, - unsigned pindex, - unsigned paindex, - unsigned iindex); - /** get eligible inst variables */ - void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); - - bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ); -public: - LtePartialInst( QuantifiersEngine * qe, context::Context* c ); - /** determine whether this quantified formula will be reduced */ - void checkOwnership(Node q) override; - /** was invoked */ - bool wasInvoked() { return d_wasInvoked; } - - /* whether this module needs to check this round */ - bool needsCheck(Theory::Effort e) override; - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* check complete */ - bool checkComplete() override { return !d_wasInvoked; } - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "LtePartialInst"; } -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6a54e8393..187c765d1 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1792,7 +1792,6 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg } } Assert(!qvl1.empty()); - Assert(!qvl2.empty() || !qvsh.empty()); //check for literals that only contain shared variables std::vector<Node> qlitsh; std::vector<Node> qlit2; diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index a0e25b756..50831fdac 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -346,7 +346,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, d_conjuncts[2].push_back(cr); std::unordered_set<Node, NodeHashFunction> fvs; expr::getFreeVariables(cr, fvs); - d_all_vars.insert(d_all_vars.end(), fvs.begin(), fvs.end()); + d_all_vars.insert(fvs.begin(), fvs.end()); if (singleInvocation) { // replace with single invocation formulation diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 0a4af3185..cdc56d1f0 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -201,7 +201,7 @@ class SingleInvocationPartition std::vector<Node> d_si_vars; /** every free variable of conjuncts[2] */ - std::vector<Node> d_all_vars; + std::unordered_set<Node, NodeHashFunction> d_all_vars; /** map from functions to first-order variables that anti-skolemized them */ std::map<Node, Node> d_func_fo_var; /** map from first-order variables to the function it anti-skolemized */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ed4a79808..4339ee75f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_strategy_enumerative.h" -#include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -52,7 +51,6 @@ class QuantifiersEnginePrivate d_qcf(nullptr), d_sg_gen(nullptr), d_synth_e(nullptr), - d_lte_part_inst(nullptr), d_fs(nullptr), d_i_cbqi(nullptr), d_qsplit(nullptr), @@ -79,8 +77,6 @@ class QuantifiersEnginePrivate std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; /** ceg instantiation */ std::unique_ptr<quantifiers::SynthEngine> d_synth_e; - /** lte partial instantiation */ - std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst; /** full saturation */ std::unique_ptr<quantifiers::InstStrategyEnum> d_fs; /** counterexample-based quantifier instantiation */ @@ -142,11 +138,6 @@ class QuantifiersEnginePrivate // finite model finder has special ways of building the model needsBuilder = true; } - if (options::ltePartialInst()) - { - d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); - modules.push_back(d_lte_part_inst.get()); - } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { d_qsplit.reset(new quantifiers::QuantDSplit(qe, c)); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 765c2b4c8..b3f1e23d7 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -81,6 +81,11 @@ struct RewriteStackElement { NodeBuilder<> d_builder; }; +RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n) +{ + return RewriteResponse(REWRITE_DONE, n); +} + Node Rewriter::rewrite(TNode node) { if (node.getNumChildren() == 0) { @@ -88,8 +93,35 @@ Node Rewriter::rewrite(TNode node) { // eagerly for the sake of efficiency here. return node; } - Rewriter& rewriter = getInstance(); - return rewriter.rewriteTo(theoryOf(node), node); + return getInstance().rewriteTo(theoryOf(node), node); +} + +void Rewriter::registerPreRewrite( + Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn) +{ + Assert(k != kind::EQUAL) << "Register pre-rewrites for EQUAL with registerPreRewriteEqual."; + d_preRewriters[k] = fn; +} + +void Rewriter::registerPostRewrite( + Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn) +{ + Assert(k != kind::EQUAL) << "Register post-rewrites for EQUAL with registerPostRewriteEqual."; + d_postRewriters[k] = fn; +} + +void Rewriter::registerPreRewriteEqual( + theory::TheoryId tid, + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn) +{ + d_preRewritersEqual[tid] = fn; +} + +void Rewriter::registerPostRewriteEqual( + theory::TheoryId tid, + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn) +{ + d_postRewritersEqual[tid] = fn; } Rewriter& Rewriter::getInstance() @@ -153,8 +185,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { for(;;) { // Perform the pre-rewrite RewriteResponse response = - d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite( - rewriteStackTop.d_node); + preRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); // Put the rewritten node to the top of the stack rewriteStackTop.d_node = response.d_node; TheoryId newTheory = theoryOf(rewriteStackTop.d_node); @@ -225,8 +256,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { for(;;) { // Do the post-rewrite RewriteResponse response = - d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite( - rewriteStackTop.d_node); + postRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); // We continue with the response we got TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() @@ -290,6 +320,30 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Unreachable(); }/* Rewriter::rewriteTo() */ +RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, TNode n) +{ + Kind k = n.getKind(); + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn = + (k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k]; + if (fn == nullptr) + { + return d_theoryRewriters[theoryId]->preRewrite(n); + } + return fn(&d_re, n); +} + +RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n) +{ + Kind k = n.getKind(); + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn = + (k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k]; + if (fn == nullptr) + { + return d_theoryRewriters[theoryId]->postRewrite(n); + } + return fn(&d_re, n); +} + void Rewriter::clearCaches() { Rewriter& rewriter = getInstance(); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index e55ca5d1c..f7298e1fb 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -28,6 +28,23 @@ namespace theory { class RewriterInitializer; /** + * The rewrite environment holds everything that the individual rewrites have + * access to. + */ +class RewriteEnvironment +{ +}; + +/** + * The identity rewrite just returns the original node. + * + * @param re The rewrite environment + * @param n The node to rewrite + * @return The original node + */ +RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n); + +/** * The main rewriter class. */ class Rewriter { @@ -45,6 +62,44 @@ class Rewriter { */ static void clearCaches(); + /** + * Register a prerewrite for a given kind. + * + * @param k The kind to register a rewrite for. + * @param fn The function that performs the rewrite. + */ + void registerPreRewrite( + Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn); + + /** + * Register a postrewrite for a given kind. + * + * @param k The kind to register a rewrite for. + * @param fn The function that performs the rewrite. + */ + void registerPostRewrite( + Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn); + + /** + * Register a prerewrite for equalities belonging to a given theory. + * + * @param tid The theory to register a rewrite for. + * @param fn The function that performs the rewrite. + */ + void registerPreRewriteEqual( + theory::TheoryId tid, + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn); + + /** + * Register a postrewrite for equalities belonging to a given theory. + * + * @param tid The theory to register a rewrite for. + * @param fn The function that performs the rewrite. + */ + void registerPostRewriteEqual( + theory::TheoryId tid, + std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn); + private: /** * Get the (singleton) instance of the rewriter. @@ -71,10 +126,10 @@ class Rewriter { Node rewriteTo(theory::TheoryId theoryId, Node node); /** Calls the pre-rewriter for the given theory */ - RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); + RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n); /** Calls the post-rewriter for the given theory */ - RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); + RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n); /** * Calls the equality-rewriter for the given theory. @@ -88,6 +143,27 @@ class Rewriter { unsigned long d_iterationCount = 0; + /** Rewriter table for prewrites. Maps kinds to rewriter function. */ + std::function<RewriteResponse(RewriteEnvironment*, TNode)> + d_preRewriters[kind::LAST_KIND]; + /** Rewriter table for postrewrites. Maps kinds to rewriter function. */ + std::function<RewriteResponse(RewriteEnvironment*, TNode)> + d_postRewriters[kind::LAST_KIND]; + /** + * Rewriter table for prerewrites of equalities. Maps theory to rewriter + * function. + */ + std::function<RewriteResponse(RewriteEnvironment*, TNode)> + d_preRewritersEqual[theory::THEORY_LAST]; + /** + * Rewriter table for postrewrites of equalities. Maps theory to rewriter + * function. + */ + std::function<RewriteResponse(RewriteEnvironment*, TNode)> + d_postRewritersEqual[theory::THEORY_LAST]; + + RewriteEnvironment d_re; + #ifdef CVC4_ASSERTIONS std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack = nullptr; diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index e1be6355b..1bb03e253 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -64,6 +64,19 @@ ${post_rewrite_set_cache} Rewriter::Rewriter() { ${rewrite_init} + +for (size_t i = 0; i < kind::LAST_KIND; ++i) +{ + d_preRewriters[i] = nullptr; + d_postRewriters[i] = nullptr; +} + +for (size_t i = 0; i < theory::THEORY_LAST; ++i) +{ + d_preRewritersEqual[i] = nullptr; + d_postRewritersEqual[i] = nullptr; + d_theoryRewriters[i]->registerRewrites(this); +} } void Rewriter::clearCachesInternal() { diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index e7dc782bb..311ab9020 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -24,6 +24,8 @@ namespace CVC4 { namespace theory { +class Rewriter; + /** * Theory rewriters signal whether more rewriting is needed (or not) * by using a member of this enumeration. See RewriteResponse, below. @@ -64,6 +66,13 @@ class TheoryRewriter virtual ~TheoryRewriter() = default; /** + * Registers the rewrites of a given theory with the rewriter. + * + * @param rewriter The rewriter to register the rewrites with. + */ + virtual void registerRewrites(Rewriter* rewriter) {} + + /** * Performs a pre-rewrite step. * * @param node The node to rewrite |