From: PaulMeng Date: Fri, 20 Apr 2018 15:15:00 +0000 (-0500) Subject: Symmetry detection module (#1749) X-Git-Tag: cvc5-1.0.0~5136 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=adc22697d4c44c54993aa2048dcbd705cbebd466;p=cvc5.git Symmetry detection module (#1749) --- 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& 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 >& parts, + const vector& assertions) +{ + Partition p = detect(assertions); + + for (map >::const_iterator subvar_to_vars_it = + p.d_subvar_to_vars.begin(); + subvar_to_vars_it != p.d_subvar_to_vars.end(); + ++subvar_to_vars_it) + { + parts.push_back(subvar_to_vars_it->second); + } +} + +SymmetryDetect::Partition SymmetryDetect::findPartitions(Node node) +{ + Trace("sym-dt") + << "------------------------------------------------------------" + << endl; + Trace("sym-dt") << "[sym-dt] findPartitions gets a term: " << node << endl; + map::iterator partition = d_term_partition.find(node); + + // Return its partition from cache if we have processed the node before + if (partition != d_term_partition.end()) + { + Trace("sym-dt") << "[sym-dt] We have seen the node " << node + << " before, thus we return its partition from cache." + << endl; + return partition->second; + } + + // The new partition for node + Partition p; + // If node is a variable + if (node.isVar() && node.getKind() != kind::BOUND_VARIABLE) + { + vector 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 children; + // Partitions of children + vector partitions; + + // Get all children of node + Trace("sym-dt") << "[sym-dt] collectChildren for: " << node + << " with operator " << node.getKind() << endl; + collectChildren(node, children); + Trace("sym-dt") << "[sym-dt] children: " << children + << endl; + + // Create partitions for children + for (vector::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 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::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& partitions, + map& subvar_to_var, + map& subvar_to_expr) +{ + Trace("sym-dt") + << "[sym-dt] Start testing if singleton partitions can be merged!" + << endl; + + if (!subvar_to_expr.empty()) + { + // Replacement variables + vector repls; + // Variables that have been merged + unordered_set merged; + // Put the variable in repls + repls.push_back((subvar_to_expr.begin())->first); + + for (map::iterator expr_it1 = subvar_to_expr.begin(); + expr_it1 != subvar_to_expr.end(); + ++expr_it1) + { + // Skip expr_it1->first, if it has been merged + if (merged.find(expr_it1->first) != merged.end()) + { + continue; + } + + Partition p; + vector subs; + vector part; + Node fst_var = subvar_to_var.find(expr_it1->first)->second; + + part.push_back(fst_var); + subs.push_back(fst_var); + merged.insert(expr_it1->first); + p.d_var_to_subvar[fst_var] = expr_it1->first; + Node sub_expr1 = + (expr_it1->second) + .substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + + for (map::iterator expr_it2 = subvar_to_expr.begin(); + expr_it2 != subvar_to_expr.end(); + ++expr_it2) + { + if (merged.find(expr_it2->first) != merged.end()) + { + continue; + } + if ((expr_it1->second).getType() != (expr_it2->second).getType()) + { + continue; + } + vector subs2; + Node snd_var = subvar_to_var.find(expr_it2->first)->second; + + subs2.push_back(snd_var); + Node sub_expr2 = + (expr_it2->second) + .substitute( + subs2.begin(), subs2.end(), repls.begin(), repls.end()); + Trace("sym-dt") << "[sym-dt] Testing if " << sub_expr1 + << " is equivalent to " << sub_expr2 << endl; + + if (sub_expr1 == sub_expr2) + { + Trace("sym-dt") << "[sym-dt] Merge variable " << fst_var + << " with variable " << snd_var << endl; + merged.insert(expr_it2->first); + part.push_back(snd_var); + p.d_var_to_subvar[snd_var] = expr_it1->first; + } + } + 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& partitions, unordered_set& vars) +{ + Trace("sym-dt") << "[sym-dt] Start post-processing partitions with size = " + << partitions.size() << endl; + + // Mapping between the substitution variable to the actual variable + map subvar_to_var; + // Mapping between the substitution variable to the actual expression + map subvar_to_expr; + // Partitions that have 2 or more variables + vector new_partitions; + + // Collect singleton partitions: subvar_to_expr, subvar_to_var, and variables + for (vector::const_iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + 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& 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& children) +{ + Kind k = node.getKind(); + + if(!theory::quantifiers::TermUtil::isAssoc(k)) + { + children.insert(children.end(), node.begin(), node.end()); + return; + } + + Node cur; + vector visit; + visit.push_back(node); + unordered_set visited; + + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.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 vars; + Node fresh_var = NodeManager::currentNM()->mkSkolem( + "sym_bk", pt.d_variables[0].getType()); + Trace("sym-dt") + << "[sym-dt] A partition from leaves of the partition trie:{"; + + for (vector::iterator var_it = pt.d_variables.begin(); + var_it != pt.d_variables.end(); + ++var_it) + { + Trace("sym-dt") << " " << *var_it; + vars.push_back(*var_it); + part.d_var_to_subvar[*var_it] = fresh_var; + } + Trace("sym-dt") << " }" << endl; + part.d_subvar_to_vars[fresh_var] = vars; + } + else + { + for (map::iterator part_it = pt.d_children.begin(); + part_it != pt.d_children.end(); + ++part_it) + { + getNewPartition(part, part_it->second); + } + } +} + +void SymmetryDetect::getVariables(vector& partitions, + unordered_set& vars) +{ + for (vector::iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + for (map >::iterator sub_var_it = + (*part_it).d_subvar_to_vars.begin(); + sub_var_it != (*part_it).d_subvar_to_vars.end(); + ++sub_var_it) + { + vars.insert((sub_var_it->second).begin(), (sub_var_it->second).end()); + } + } +} + +void SymmetryDetect::PartitionTrie::addNode(Node target_var, + vector& partitions) +{ + Trace("sym-dt") << "[sym-dt] Add a variable {" << target_var + << "} to the partition trie..." << endl; + vector subvars; + + for (vector::iterator part_it = partitions.begin(); + part_it != partitions.end(); + ++part_it) + { + map::iterator var_sub_it = + (*part_it).d_var_to_subvar.find(target_var); + + if (var_sub_it != (*part_it).d_var_to_subvar.end()) + { + for (map >::iterator sub_vars_it = + (*part_it).d_subvar_to_vars.begin(); + sub_vars_it != (*part_it).d_subvar_to_vars.end(); + ++sub_vars_it) + { + 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& subvars) +{ + if (subvars.empty()) + { + d_variables.push_back(target_var); + } + else + { + vector new_subs; + map::iterator children_it = + d_children.find(subvars[0]); + + if (subvars.begin() + 1 < subvars.end()) + { + new_subs.insert(new_subs.begin(), subvars.begin() + 1, subvars.end()); + } + if (children_it != d_children.end()) + { + (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 >::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::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 +#include +#include +#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(true); + d_falseNode = NodeManager::currentNM()->mkConst(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 >& parts, const std::vector& 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 d_var_to_subvar; + + /** Mapping between the substitution variable and variables w-> { x, y, z } */ + std::map > 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 d_variables; + + /** The mapping from a node to its children */ + std::map d_children; + + /** Add variable v to the trie, indexed by + * parts[0].var_to_subvar[v]....parts[n].var_to_subvar[v]. */ + void addNode(Node v, std::vector& parts); + void addNode(Node v, std::vector& subs); + + /** Get all the new regions of a partition and store in part */ + void getNewPartition(Partition& part, PartitionTrie& pt); + }; + + + /** True and false constant nodes */ + Node d_trueNode; + Node d_falseNode; + + /** Cache for partitions */ + std::map d_term_partition; + + /** detect + * + * Called on the input assertions, where assertions are interpreted as a + * conjunction. This computes a partition P of the variables in assertions + * such that for each set S in P, then all automorphisms for S applied to + * assertions result in an equisatisfiable formula. + */ + Partition detect(const std::vector& assertions); + + /** Find symmetries in node */ + 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& children); + + /** Print a partition */ + void printPartition(Partition p); + + /** Retrieve all variables from partitions and put in vars */ + void getVariables(std::vector& partitions, + std::unordered_set& vars); + + /** Process singleton partitions and add all variables to vars + * It collects all partitions with more than 1 variable and save it in + * partitions first. And then it collects the substitution variable to + * variable and to term mappings respectively from partitions with 1 + * variable and invokes matches function on the mappings to check + * if any subset of the variables can be merged. If yes, they will be merged + * and put in partitions. The remaining ones after the merge check will be + * put in the partitions as well. + * */ + void processSingletonPartitions(std::vector& partitions, + std::unordered_set& vars); + + /** Do matches on singleton partitions + * This function checks if any subset of the expressions corresponding to + * substitution variables are equivalent under variables substitution. + * If the expressions are equivalent, we will merge the variables corresponding + * to the same substitution variables and put them in partitions. + * For example, suppose we have subvar_to_var: {w1 -> u, w2 -> x, w3 -> y, + * w4 -> z} and subvar_to_expr: {w1 -> u>2, w2 -> x>0, w3 -> y>0, w4 -> z>1}. + * Since [x/w]>0 is equivalent [y/w]>0 but not equivalent to [z/w]>1 and [u/w]>2, + * and [u/w]>2 is not equivalent to [z/w]>1, we would merge x and y and put + * w5->{x, y} and also w1->{u}, w4->{z} in partitions. + * */ + void matches(std::vector& partitions, + std::map& subvar_to_var, + std::map& subvar_to_expr); +}; +} // 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> 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 ) { diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 56965f272..a29236914 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1490,6 +1490,12 @@ REG1_TESTS = \ regress1/sygus/twolets2-orig.sy \ regress1/sygus/unbdd_inv_gen_ex7.sy \ regress1/sygus/unbdd_inv_gen_winf1.sy \ + regress1/sym/sym1.smt2 \ + regress1/sym/sym2.smt2 \ + regress1/sym/sym3.smt2 \ + regress1/sym/sym4.smt2 \ + regress1/sym/sym5.smt2 \ + regress1/sym/sym6.smt2 \ regress1/test12.cvc \ regress1/trim.cvc \ regress1/uf2.smt2 \ diff --git a/test/regress/regress1/sym/sym1.smt2 b/test/regress/regress1/sym/sym1.smt2 new file mode 100644 index 000000000..ac1c0215f --- /dev/null +++ b/test/regress/regress1/sym/sym1.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) + + +(declare-fun p (Int) Bool) +(declare-fun A () (Set Int)) +(declare-fun F () (Set Int)) + + + +(assert (= F (insert x y (singleton z)))) +(assert (subset F A)) +(assert (= x y)) + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym2.smt2 b/test/regress/regress1/sym/sym2.smt2 new file mode 100644 index 000000000..cff424ba9 --- /dev/null +++ b/test/regress/regress1/sym/sym2.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + + +(assert (> (- (+ (* 3 x) (* 3 y) (* 3 z)) u v) 0)) +(assert (> (+ u v) 0)) +(assert (> (+ x y) 0)) +(assert (> x 0)) +(assert (> z 0)) +(assert (> u 0)) +(assert (> v 0)) +(assert (< u 10)) +(assert (< v 10)) + + + + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym3.smt2 b/test/regress/regress1/sym/sym3.smt2 new file mode 100644 index 000000000..52f9855c9 --- /dev/null +++ b/test/regress/regress1/sym/sym3.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + +(declare-fun p (Int Int) Int) +(declare-fun A () (Set Int)) + + +(assert (or (> (+ x y z) 3) (< (p x (+ (* 3 y) (* 3 z))) 5))) +(assert (subset A (insert y (singleton z)))) + + + +(check-sat) + diff --git a/test/regress/regress1/sym/sym4.smt2 b/test/regress/regress1/sym/sym4.smt2 new file mode 100644 index 000000000..5582ef7d0 --- /dev/null +++ b/test/regress/regress1/sym/sym4.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --symmetry-detect +(set-info :smt-lib-version 2.6) +(set-logic QF_LIA) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun x_0 () Int) +(declare-fun x_1 () Int) +(declare-fun x_2 () Int) +(declare-fun x_3 () Int) +(declare-fun x_4 () Int) +(declare-fun x_5 () Int) +(declare-fun x_6 () Int) +(declare-fun x_7 () Int) +(declare-fun x_8 () Int) +(declare-fun x_9 () Int) +(declare-fun x_10 () Int) +(declare-fun x_11 () Int) +(declare-fun x_12 () Int) +(declare-fun x_13 () Int) +(declare-fun x_14 () Int) +(declare-fun x_15 () Int) +(declare-fun x_16 () Int) +(assert (>= x_0 0)) +(assert (>= x_1 0)) +(assert (>= x_2 0)) +(assert (>= x_3 0)) +(assert (>= x_4 0)) +(assert (>= x_5 0)) +(assert (>= x_6 0)) +(assert (>= x_7 0)) +(assert (>= x_8 0)) +(assert (>= x_9 0)) +(assert (>= x_10 0)) +(assert (>= x_11 0)) +(assert (>= x_12 0)) +(assert (>= x_13 0)) +(assert (>= x_14 0)) +(assert (>= x_15 0)) +(assert (>= x_16 0)) +(assert (<= (+ (* 37 x_0) (* 37 x_1) (* 37 x_2) (* 37 x_3) (* 37 x_4) (* 37 x_5) (* 37 x_6) (* 37 x_7) (* 37 x_8) (* 37 x_9) (* 37 x_10) (* (- 404) x_11) (* 37 x_12) (* 37 x_13) (* 37 x_14) (* 37 x_15) (* 37 x_16)) 0)) +(assert (<= (+ (* 41 x_0) (* 41 x_1) (* 41 x_2) (* 41 x_3) (* 41 x_4) (* 41 x_5) (* 41 x_6) (* 41 x_7) (* 41 x_8) (* 41 x_9) (* 41 x_10) (* 41 x_11) (* (- 400) x_12) (* 41 x_13) (* 41 x_14) (* 41 x_15) (* 41 x_16)) 0)) +(assert (<= (+ (* 43 x_0) (* 43 x_1) (* 43 x_2) (* 43 x_3) (* 43 x_4) (* 43 x_5) (* 43 x_6) (* 43 x_7) (* 43 x_8) (* 43 x_9) (* 43 x_10) (* 43 x_11) (* 43 x_12) (* (- 398) x_13) (* 43 x_14) (* 43 x_15) (* 43 x_16)) 0)) +(assert (<= (+ (* 47 x_0) (* 47 x_1) (* 47 x_2) (* 47 x_3) (* 47 x_4) (* 47 x_5) (* 47 x_6) (* 47 x_7) (* 47 x_8) (* 47 x_9) (* 47 x_10) (* 47 x_11) (* 47 x_12) (* 47 x_13) (* (- 394) x_14) (* 47 x_15) (* 47 x_16)) 0)) +(assert (<= (+ (* 53 x_0) (* 53 x_1) (* 53 x_2) (* 53 x_3) (* 53 x_4) (* 53 x_5) (* 53 x_6) (* 53 x_7) (* 53 x_8) (* 53 x_9) (* 53 x_10) (* 53 x_11) (* 53 x_12) (* 53 x_13) (* 53 x_14) (* (- 388) x_15) (* 53 x_16)) 0)) +(assert (<= (+ (* 59 x_0) (* 59 x_1) (* 59 x_2) (* 59 x_3) (* 59 x_4) (* 59 x_5) (* 59 x_6) (* 59 x_7) (* 59 x_8) (* 59 x_9) (* 59 x_10) (* 59 x_11) (* 59 x_12) (* 59 x_13) (* 59 x_14) (* 59 x_15) (* (- 382) x_16)) 0)) +(assert (>= (+ x_0 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12 x_13 x_14 x_15 x_16) 1)) +(check-sat) +(exit) \ No newline at end of file diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 new file mode 100644 index 000000000..f5ef1d003 --- /dev/null +++ b/test/regress/regress1/sym/sym5.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status unsat) +(declare-fun A () (Set Int)) +(declare-fun B () (Set Int)) +(declare-fun C () (Set Int)) + +(declare-fun f () Int) +(declare-fun g () Int) +(declare-fun h () Int) +(declare-fun i () Int) +(declare-fun j () Int) + +(assert (subset A (insert g h i (singleton f)))) +(assert (= C (setminus A B) )) +(assert (subset B A)) +(assert (= C (intersection A B))) +(assert (member j C)) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2 new file mode 100644 index 000000000..3da6b4cb4 --- /dev/null +++ b/test/regress/regress1/sym/sym6.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --symmetry-detect +(set-logic ALL) +(set-info :status sat) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) + + +(assert (= (+ w y u) (+ v z))) + +(assert (> (+ x (* 2 y)) (+ u v))) + +(assert (= (- x) (- (- y)))) + + + +(assert (or (< (+ x y z) 10) (> (+ v u) 10))) + + +(check-sat) +