diff options
author | PaulMeng <baolmeng@gmail.com> | 2018-04-20 10:15:00 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-20 10:15:00 -0500 |
commit | adc22697d4c44c54993aa2048dcbd705cbebd466 (patch) | |
tree | 1a4ebb511ac135bc54d35524fc7d6975dfb750b8 /src | |
parent | b384376e687f53bea69b4fdaa11898a52e0f471f (diff) |
Symmetry detection module (#1749)
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 2 | ||||
-rw-r--r-- | src/options/smt_options.toml | 8 | ||||
-rw-r--r-- | src/preprocessing/passes/symmetry_detect.cpp | 459 | ||||
-rw-r--r-- | src/preprocessing/passes/symmetry_detect.h | 165 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 14 |
6 files changed, 651 insertions, 5 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index f89a8426e..04d6e24b7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -68,6 +68,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ preprocessing/passes/pseudo_boolean_processor.h \ + preprocessing/passes/symmetry_detect.cpp \ + preprocessing/passes/symmetry_detect.h \ preprocessing/preprocessing_pass.cpp \ preprocessing/preprocessing_pass.h \ preprocessing/preprocessing_pass_context.cpp \ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index a9093b894..e7a385a42 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -342,6 +342,14 @@ header = "options/smt_options.h" type = "bool" default = "false" help = "calculate sort inference of input problem, convert the input based on monotonic sorts" + +[[option]] + name = "symmetryDetect" + category = "regular" + long = "symmetry-detect" + type = "bool" + default = "false" + help = "compute symmetries in the input as a preprocessing pass" [[option]] name = "incrementalSolving" diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp new file mode 100644 index 000000000..d39b8d14e --- /dev/null +++ b/src/preprocessing/passes/symmetry_detect.cpp @@ -0,0 +1,459 @@ +/********************* */ +/*! \file symmetry_detect.cpp + ** \verbatim + ** Top contributors (to current version): + ** Paul Meng, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace std; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +SymmetryDetect::Partition SymmetryDetect::detect(const vector<Node>& assertions) +{ + Partition p = + findPartitions(NodeManager::currentNM()->mkNode(kind::AND, assertions)); + Trace("sym-dt") << endl + << "------------------------------ The Final Partition " + "------------------------------" + << endl; + if(Trace.isOn("sym-dt")) + { + printPartition(p); + } + return p; +} + +void SymmetryDetect::getPartition(vector<vector<Node> >& parts, + const vector<Node>& assertions) +{ + Partition p = detect(assertions); + + 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); + } +} + +SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node) +{ + Trace("sym-dt") + << "------------------------------------------------------------" + << endl; + Trace("sym-dt") << "[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") << "[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) + { + vector<Node> vars; + TypeNode type = node.getType(); + Node fresh_var = NodeManager::currentNM()->mkSkolem("sym_bk", type); + + vars.push_back(node); + p.d_term = node; + p.d_subvar_to_vars[fresh_var] = vars; + p.d_var_to_subvar[node] = fresh_var; + d_term_partition[node] = p; + return p; + } + // If node is a constant + else if (node.isConst()) + { + p.d_term = node; + d_term_partition[node] = p; + return p; + } + + // Children of node + vector<Node> children; + // Partitions of children + vector<Partition> partitions; + + // Get all children of node + Trace("sym-dt") << "[sym-dt] collectChildren for: " << node + << " with operator " << node.getKind() << endl; + collectChildren(node, children); + Trace("sym-dt") << "[sym-dt] children: " << children + << endl; + + // Create partitions for children + for (vector<Node>::iterator children_it = children.begin(); + children_it != children.end(); + ++children_it) + { + partitions.push_back(findPartitions(*children_it)); + } + + Trace("sym-dt") << "----------------------------- Start processing " + "partitions -------------------------------" + << endl; + + PartitionTrie pt; + unordered_set<Node, NodeHashFunction> vars; + + if (theory::quantifiers::TermUtil::isComm(node.getKind())) + { + // Start processing the singleton partitions and collect variables + processSingletonPartitions(partitions, vars); + } + else + { + // Get all the variables from the partitions + getVariables(partitions, vars); + } + + // Build the partition trie + for (unordered_set<Node, NodeHashFunction>::iterator vars_it = vars.begin(); + vars_it != vars.end(); + ++vars_it) + { + pt.addNode(*vars_it, partitions); + } + + // Get the new partition + pt.getNewPartition(p, pt); + + // Reconstruct the node + Trace("sym-dt") << "[sym-dt] Reconstructing node: " << node << endl; + p.d_term = node; + d_term_partition[node] = p; + printPartition(p); + return p; +} + +void SymmetryDetect::matches(vector<Partition>& partitions, + map<Node, Node>& subvar_to_var, + map<Node, Node>& subvar_to_expr) +{ + Trace("sym-dt") + << "[sym-dt] Start testing if singleton partitions can be merged!" + << endl; + + if (!subvar_to_expr.empty()) + { + // Replacement variables + vector<Node> repls; + // Variables that have been merged + unordered_set<Node, NodeHashFunction> merged; + // Put the variable in repls + repls.push_back((subvar_to_expr.begin())->first); + + for (map<Node, Node>::iterator expr_it1 = subvar_to_expr.begin(); + expr_it1 != subvar_to_expr.end(); + ++expr_it1) + { + // Skip expr_it1->first, if it has been merged + if (merged.find(expr_it1->first) != merged.end()) + { + continue; + } + + Partition p; + vector<Node> subs; + vector<Node> part; + Node fst_var = subvar_to_var.find(expr_it1->first)->second; + + part.push_back(fst_var); + subs.push_back(fst_var); + merged.insert(expr_it1->first); + p.d_var_to_subvar[fst_var] = expr_it1->first; + Node sub_expr1 = + (expr_it1->second) + .substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + + for (map<Node, Node>::iterator expr_it2 = subvar_to_expr.begin(); + expr_it2 != subvar_to_expr.end(); + ++expr_it2) + { + if (merged.find(expr_it2->first) != merged.end()) + { + continue; + } + if ((expr_it1->second).getType() != (expr_it2->second).getType()) + { + continue; + } + vector<Node> subs2; + Node snd_var = subvar_to_var.find(expr_it2->first)->second; + + subs2.push_back(snd_var); + Node sub_expr2 = + (expr_it2->second) + .substitute( + subs2.begin(), subs2.end(), repls.begin(), repls.end()); + Trace("sym-dt") << "[sym-dt] Testing if " << sub_expr1 + << " is equivalent to " << sub_expr2 << endl; + + if (sub_expr1 == sub_expr2) + { + Trace("sym-dt") << "[sym-dt] Merge variable " << fst_var + << " with variable " << snd_var << endl; + merged.insert(expr_it2->first); + part.push_back(snd_var); + p.d_var_to_subvar[snd_var] = expr_it1->first; + } + } + p.d_subvar_to_vars[expr_it1->first] = part; + Trace("sym-dt") << "[sym-dt] Add a new partition after merging: " << endl; + printPartition(p); + partitions.push_back(p); + } + } +} + +void SymmetryDetect::processSingletonPartitions( + vector<Partition>& partitions, unordered_set<Node, NodeHashFunction>& vars) +{ + Trace("sym-dt") << "[sym-dt] Start post-processing partitions with size = " + << partitions.size() << endl; + + // Mapping between the substitution variable to the actual variable + map<Node, Node> subvar_to_var; + // Mapping between the substitution variable to the actual expression + map<Node, Node> subvar_to_expr; + // Partitions that have 2 or more variables + vector<Partition> new_partitions; + + // Collect singleton partitions: subvar_to_expr, subvar_to_var, and variables + for (vector<Partition>::const_iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + if ((*part_it).d_var_to_subvar.size() == 1) + { + vars.insert(((*part_it).d_var_to_subvar.begin())->first); + subvar_to_expr[((*part_it).d_var_to_subvar.begin())->second] = + (*part_it).d_term; + subvar_to_var[((*part_it).d_var_to_subvar.begin())->second] = + ((*part_it).d_var_to_subvar.begin())->first; + } + else if ((*part_it).d_var_to_subvar.size() >= 2) + { + for (const pair<Node, Node>& var_to_subvar : (*part_it).d_var_to_subvar) + { + vars.insert(var_to_subvar.first); + } + // Only add partitions that have more than 1 variable + new_partitions.push_back(*part_it); + } + } + + // Save all partitions that have more than 1 variable + partitions = new_partitions; + + // Do matches on singleton terms + if (!subvar_to_var.empty()) + { + matches(partitions, subvar_to_var, subvar_to_expr); + } +} + +void SymmetryDetect::collectChildren(Node node, vector<Node>& children) +{ + Kind k = node.getKind(); + + if(!theory::quantifiers::TermUtil::isAssoc(k)) + { + children.insert(children.end(), node.begin(), node.end()); + return; + } + + 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.getKind() == k) + { + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + else + { + children.push_back(cur); + } + } + } while (!visit.empty()); +} + +void SymmetryDetect::PartitionTrie::getNewPartition(Partition& part, + PartitionTrie& pt) +{ + if (!pt.d_variables.empty()) + { + vector<Node> vars; + Node fresh_var = NodeManager::currentNM()->mkSkolem( + "sym_bk", pt.d_variables[0].getType()); + Trace("sym-dt") + << "[sym-dt] A partition from leaves of the partition trie:{"; + + for (vector<Node>::iterator var_it = pt.d_variables.begin(); + var_it != pt.d_variables.end(); + ++var_it) + { + Trace("sym-dt") << " " << *var_it; + vars.push_back(*var_it); + part.d_var_to_subvar[*var_it] = fresh_var; + } + Trace("sym-dt") << " }" << endl; + part.d_subvar_to_vars[fresh_var] = vars; + } + else + { + for (map<Node, PartitionTrie>::iterator part_it = pt.d_children.begin(); + part_it != pt.d_children.end(); + ++part_it) + { + getNewPartition(part, part_it->second); + } + } +} + +void SymmetryDetect::getVariables(vector<Partition>& partitions, + unordered_set<Node, NodeHashFunction>& vars) +{ + for (vector<Partition>::iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + for (map<Node, vector<Node> >::iterator sub_var_it = + (*part_it).d_subvar_to_vars.begin(); + sub_var_it != (*part_it).d_subvar_to_vars.end(); + ++sub_var_it) + { + vars.insert((sub_var_it->second).begin(), (sub_var_it->second).end()); + } + } +} + +void SymmetryDetect::PartitionTrie::addNode(Node target_var, + vector<Partition>& partitions) +{ + Trace("sym-dt") << "[sym-dt] Add a variable {" << target_var + << "} to the partition trie..." << endl; + vector<Node> subvars; + + for (vector<Partition>::iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + map<Node, Node>::iterator var_sub_it = + (*part_it).d_var_to_subvar.find(target_var); + + if (var_sub_it != (*part_it).d_var_to_subvar.end()) + { + for (map<Node, vector<Node> >::iterator sub_vars_it = + (*part_it).d_subvar_to_vars.begin(); + sub_vars_it != (*part_it).d_subvar_to_vars.end(); + ++sub_vars_it) + { + if (var_sub_it->second == sub_vars_it->first) + { + subvars.push_back(var_sub_it->second); + } + else + { + subvars.push_back(Node::null()); + } + } + } + else + { + subvars.resize(subvars.size()+(*part_it).d_subvar_to_vars.size()); + } + } + + Trace("sym-dt") << "[sym-dt] Substitution variables for the variable " + << target_var << ": " << subvars << endl; + addNode(target_var, subvars); +} + +void SymmetryDetect::PartitionTrie::addNode(Node target_var, + vector<Node>& subvars) +{ + if (subvars.empty()) + { + d_variables.push_back(target_var); + } + else + { + vector<Node> new_subs; + map<Node, PartitionTrie>::iterator children_it = + d_children.find(subvars[0]); + + if (subvars.begin() + 1 < subvars.end()) + { + new_subs.insert(new_subs.begin(), subvars.begin() + 1, subvars.end()); + } + if (children_it != d_children.end()) + { + (children_it->second).addNode(target_var, new_subs); + } + else + { + PartitionTrie pt; + + pt.addNode(target_var, new_subs); + d_children[subvars[0]] = pt; + } + } +} + +void SymmetryDetect::printPartition(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("sym-dt") << "[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("sym-dt") << " " << *part_it; + } + Trace("sym-dt") << " }" << endl; + } +} +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h new file mode 100644 index 000000000..3741eff3e --- /dev/null +++ b/src/preprocessing/passes/symmetry_detect.h @@ -0,0 +1,165 @@ +/********************* */ +/*! \file symmetry_detect.h + ** \verbatim + ** Top contributors (to current version): + ** Paul Meng, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * This is the class to detect symmetries from input based on terms equality. + * */ +class SymmetryDetect +{ + public: + /** + * Constructor + * */ + SymmetryDetect() + { + d_trueNode = NodeManager::currentNM()->mkConst<bool>(true); + d_falseNode = NodeManager::currentNM()->mkConst<bool>(false); + } + + /** + * Destructor + * */ + ~SymmetryDetect() {} + + /** Get the final partition after symmetry detection. + * If a vector in parts contains two variables x and y, + * then assertions and assertions { x -> y, y -> x } are + * equisatisfiable. + * */ + void getPartition(std::vector<std::vector<Node> >& parts, const std::vector<Node>& assertions); + + private: + /** + * This is the class to store the partition, + * where d_term store the term corresponding to the partition, + * d_var_to_subvar is the mapping from the variable to the substitution + * variable, and d_subvar_to_vars is the mapping from the substitution + * variable to a list of variables forming a region of a partition. + */ + class Partition + { + public: + /** Term corresponding to the partition, e.g., x + y = 0 */ + Node d_term; + /** Mapping between the variable and the substitution variable x -> w, y -> w, + * z -> w */ + std::map<Node, Node> d_var_to_subvar; + + /** Mapping between the substitution variable and variables w-> { x, y, z } */ + std::map<Node, std::vector<Node> > d_subvar_to_vars; + }; + + /** + * We build the partition trie indexed by + * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. The leaves of a + * partition trie is the new regions of a partition + */ + class PartitionTrie + { + public: + /** Variables at the leave */ + std::vector<Node> d_variables; + + /** The mapping from a node to its children */ + std::map<Node, PartitionTrie> d_children; + + /** Add variable v to the trie, indexed by + * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */ + void addNode(Node v, std::vector<Partition>& parts); + void addNode(Node v, std::vector<Node>& subs); + + /** Get all the new regions of a partition and store in part */ + void getNewPartition(Partition& part, PartitionTrie& pt); + }; + + + /** True and false constant nodes */ + Node d_trueNode; + Node d_falseNode; + + /** 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 */ + SymmetryDetect::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); + + /** Print a partition */ + void printPartition(Partition p); + + /** Retrieve all variables from partitions and put in vars */ + void getVariables(std::vector<Partition>& partitions, + std::unordered_set<Node, NodeHashFunction>& vars); + + /** Process singleton partitions and add all variables to vars + * It collects all partitions with more than 1 variable and save it in + * partitions first. And then it collects the substitution variable to + * variable and to term mappings respectively from partitions with 1 + * variable and invokes matches function on the mappings to check + * if any subset of the variables can be merged. If yes, they will be merged + * and put in partitions. The remaining ones after the merge check will be + * put in the partitions as well. + * */ + void processSingletonPartitions(std::vector<Partition>& partitions, + std::unordered_set<Node, NodeHashFunction>& vars); + + /** Do matches on singleton partitions + * This function checks if any subset of the expressions corresponding to + * substitution variables are equivalent under variables substitution. + * If the expressions are equivalent, we will merge the variables corresponding + * to the same substitution variables and put them in partitions. + * For example, suppose we have subvar_to_var: {w1 -> u, w2 -> x, w3 -> y, + * w4 -> z} and subvar_to_expr: {w1 -> u>2, w2 -> x>0, w3 -> y>0, w4 -> z>1}. + * Since [x/w]>0 is equivalent [y/w]>0 but not equivalent to [z/w]>1 and [u/w]>2, + * and [u/w]>2 is not equivalent to [z/w]>1, we would merge x and y and put + * w5->{x, y} and also w1->{u}, w4->{z} in partitions. + * */ + void matches(std::vector<Partition>& partitions, + std::map<Node, Node>& subvar_to_var, + std::map<Node, Node>& subvar_to_expr); +}; +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 65d3697b7..a65d55859 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -71,6 +71,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/pseudo_boolean_processor.h" +#include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -4283,6 +4284,13 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl; dumpAssertions("post-simplify", d_assertions); + if (options::symmetryDetect()) + { + SymmetryDetect symd; + vector<vector<Node>> part; + symd.getPartition(part, d_assertions.ref()); + } + dumpAssertions("pre-static-learning", d_assertions); if(options::doStaticLearning()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl; diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index b3915bd5d..76d95bf5e 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -811,14 +811,18 @@ Node TermUtil::mkNegate(Kind notk, Node n) } bool TermUtil::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || - k==STRING_CONCAT; + return k == PLUS || k == MULT || k == AND || k == OR || k == BITVECTOR_PLUS + || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR + || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT + || k == STRING_CONCAT || k == UNION || k == INTERSECTION || k == JOIN + || k == PRODUCT; } bool TermUtil::isComm( Kind k ) { - return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; + return k == EQUAL || k == PLUS || k == MULT || k == AND || k == OR || k == XOR + || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND + || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR + || k == UNION || k == INTERSECTION; } bool TermUtil::isNonAdditive( Kind k ) { |