diff --git a/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt index 7aa1d83c5..077c420f9 100644 --- a/src/nlsat/CMakeLists.txt +++ b/src/nlsat/CMakeLists.txt @@ -9,7 +9,6 @@ z3_add_component(nlsat nlsat_types.cpp nlsat_simple_checker.cpp nlsat_variable_ordering_strategy.cpp - nlsat_symmetry_checker.cpp COMPONENT_DEPENDENCIES polynomial sat diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 73067d48b..00d179901 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -6,7 +6,6 @@ def_module_params('nlsat', ('linxi_simple_check', BOOL, False, "linxi precheck about variables sign"), ('linxi_variable_ordering_strategy', UINT, 0, "linxi Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"), ('cell_sample', BOOL, True, "cell sample projection"), - ('linxi_symmetry_check', BOOL, False, "linxi symmetry check and learning"), ('lazy', UINT, 0, "how lazy the solver is."), ('reorder', BOOL, True, "reorder variables."), ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"), diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 486d88cc6..30ca55e31 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -36,7 +36,6 @@ Revision History: #include "nlsat/nlsat_simplify.h" #include "nlsat/nlsat_simple_checker.h" #include "nlsat/nlsat_variable_ordering_strategy.h" -#include "nlsat/nlsat_symmetry_checker.h" #define NLSAT_EXTRA_VERBOSE @@ -226,7 +225,6 @@ namespace nlsat { //#linxi begin bool m_linxi_simple_check; unsigned m_linxi_variable_ordering_strategy; - bool m_linxi_symmetry_check; bool m_linxi_set_0_more; bool m_cell_sample; //#linxi end @@ -302,7 +300,6 @@ namespace nlsat { //#linxi begin m_linxi_simple_check = p.linxi_simple_check(); m_linxi_variable_ordering_strategy = p.linxi_variable_ordering_strategy(); - m_linxi_symmetry_check = p.linxi_symmetry_check(); //#linxi end @@ -1836,41 +1833,7 @@ namespace nlsat { //#linxi end Variable Ordering Strategy -//#linxi begin symmetry check - void symmetry_check() { - unsigned arith_num = m_is_int.size(); - if (arith_num > 10000) - return ; - Symmetry_Checker checker(m_pm, m_qm, m_clauses, m_atoms, m_is_int, arith_num); - for (var x = 0; x < arith_num; ++x) { - for (var y = x + 1; y < arith_num; ++y) { - if (checker.check_symmetry(x, y)) { - TRACE("linxi_symmetry_checker", - tout << "symmetry: " << x << ", " << y << "\n"; - ); - rational zero(0); - vector as; - vector xs; - as.push_back(rational(1)); - xs.push_back(x); - as.push_back(rational(-1)); - xs.push_back(y); - polynomial_ref pr(m_pm); - pr = m_pm.mk_linear(2, as.data(), xs.data(), zero); - poly* p = pr.get(); - bool is_even = false; - literal lit = ~mk_ineq_literal(atom::GT, 1, &p, &is_even); - clause *cla = mk_clause(1, &lit, true, nullptr); - } - } - } - TRACE("linxi_symmetry_checker", - display(tout); - ); - - } -//#linxi end symmetry check void apply_reorder() { m_reordered = false; if (!can_reorder()) @@ -1887,13 +1850,6 @@ namespace nlsat { lbool check() { -//#linxi begin symmetry check - if (m_linxi_symmetry_check) { - symmetry_check(); - } - // exit(0); -//#linxi end symmetry check - //#linxi begin simple check if (m_linxi_simple_check) { if (!simple_check()) { diff --git a/src/nlsat/nlsat_symmetry_checker.cpp b/src/nlsat/nlsat_symmetry_checker.cpp deleted file mode 100644 index 8d0ee8766..000000000 --- a/src/nlsat/nlsat_symmetry_checker.cpp +++ /dev/null @@ -1,356 +0,0 @@ -#include "nlsat/nlsat_symmetry_checker.h" - -struct Debug_Tracer { - std::string tag_str; - Debug_Tracer(std::string _tag_str) { - tag_str = _tag_str; - TRACE("linxi_symmetry_checker", - tout << "Debug_Tracer begin\n"; - tout << tag_str << "\n"; - ); - } - ~Debug_Tracer() { - TRACE("linxi_symmetry_checker", - tout << "Debug_Tracer end\n"; - tout << tag_str << "\n"; - ); - } -}; - -// #define _LINXI_DEBUG - -#ifdef _LINXI_DEBUG -#define LINXI_DEBUG_CORE(x) std::stringstream DEBUG_ss_##x; DEBUG_ss_##x << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__; Debug_Tracer DEBUG_dt_##x(DEBUG_ss_##x.str()); -#define LINXI_DEBUG_TRANS(x) LINXI_DEBUG_CORE(x); -#define LINXI_DEBUG LINXI_DEBUG_TRANS(__LINE__); -#define LINXI_HERE TRACE("linxi_symmetry_checker", tout << "here\n";); -#else -#define LINXI_DEBUG { }((void) 0 ); -#define LINXI_HERE { }((void) 0 ); -#endif - - - -namespace nlsat { - struct Symmetry_Checker::imp { - // solver / - pmanager ± - unsynch_mpq_manager &qm; - const clause_vector &clauses; - const atom_vector &atoms; - const bool_vector &is_int; - const unsigned arith_var_num; - // vector vars_hash; - vector> vars_occur; - bool is_check; - var tx, ty; - struct Variable_Information { - unsigned long long hash_value; - unsigned deg; - var x; - bool is_int; - bool operator< (const Variable_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Variable_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (deg != rhs.deg) - return false; - if (x != rhs.x) - return false; - if (is_int != rhs.is_int) - return false; - return true; - } - bool operator!= (const Variable_Information &rhs) const { - return !(*this == rhs); - } - }; - unsigned long long VAR_BASE = 601; - void collect_var_info(Variable_Information &var_info, var x, unsigned deg) { - LINXI_DEBUG; - if (is_check) { - if (x == tx) { - x = ty; - } - else if (x == ty) { - x = tx; - } - else { - // do nothing - } - } - else { - vars_occur[x].push_back(deg); - } - var_info.deg = deg; - var_info.x = x; - var_info.is_int = is_int[x]; - var_info.hash_value = 0; - for (unsigned i = 0; i < deg; ++i) { - var_info.hash_value = var_info.hash_value*VAR_BASE + (unsigned long long)x; - } - var_info.hash_value = var_info.hash_value*VAR_BASE + (unsigned long long)var_info.is_int; - } - struct Monomial_Information { - unsigned long long hash_value; - unsigned long long coef; - vector vars_info; - bool operator< (const Monomial_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Monomial_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (coef != rhs.coef) - return false; - if (vars_info.size() != rhs.vars_info.size()) - return false; - for (unsigned i = 0, sz = vars_info.size(); i < sz; ++i) { - if (vars_info[i] != rhs.vars_info[i]) - return false; - } - return true; - } - bool operator!= (const Monomial_Information &rhs) const { - return !(*this == rhs); - } - }; - unsigned long long MONO_BASE = 99991; - - void collect_mono_info(Monomial_Information &mono_info, monomial *m, unsigned long long coef) { - LINXI_DEBUG; - unsigned sz = pm.size(m); - mono_info.vars_info.resize(sz); - for (unsigned i = 0; i < sz; ++i) { - collect_var_info(mono_info.vars_info[i], pm.get_var(m, i), pm.degree(m, i)); - } - mono_info.coef = coef; - mono_info.hash_value = coef; - std::sort(mono_info.vars_info.begin(), mono_info.vars_info.end()); - for (unsigned i = 0; i < sz; ++i) { - mono_info.hash_value = mono_info.hash_value*MONO_BASE + mono_info.vars_info[i].hash_value; - } - } - struct Polynomial_Information { - unsigned long long hash_value; - bool is_even; - vector monos_info; - bool operator< (const Polynomial_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Polynomial_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (is_even != rhs.is_even) - return false; - if (monos_info.size() != rhs.monos_info.size()) - return false; - for (unsigned i = 0, sz = monos_info.size(); i < sz; ++i) { - if (monos_info[i] != rhs.monos_info[i]) - return false; - } - return true; - } - bool operator!= (const Polynomial_Information &rhs) const { - return !(*this == rhs); - } - }; - unsigned long long POLY_BASE = 99991; - void collect_poly_info(Polynomial_Information &poly_info, poly *p, bool is_even) { - LINXI_DEBUG; - unsigned sz = pm.size(p); - poly_info.monos_info.resize(sz); - for (unsigned i = 0; i < sz; ++i) { - collect_mono_info(poly_info.monos_info[i], pm.get_monomial(p, i), qm.get_uint64(pm.coeff(p, i))); - } - poly_info.hash_value = 0; - std::sort(poly_info.monos_info.begin(), poly_info.monos_info.end()); - for (unsigned i = 0; i < sz; ++i) { - poly_info.hash_value = poly_info.hash_value*POLY_BASE + poly_info.monos_info[i].hash_value; - } - poly_info.is_even = is_even; - if (is_even) { - poly_info.hash_value = poly_info.hash_value*poly_info.hash_value; - } - } - struct Atom_Information { - unsigned long long hash_value; - atom::kind akd; - vector polys_info; - bool operator< (const Atom_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Atom_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (akd != rhs.akd) - return false; - if (polys_info.size() != rhs.polys_info.size()) - return false; - for (unsigned i = 0, sz = polys_info.size(); i < sz; ++i) { - if (polys_info[i] != rhs.polys_info[i]) - return false; - } - return true; - } - bool operator!= (const Atom_Information &rhs) const { - return !(*this == rhs); - } - }; - unsigned long long ATOM_BASE = 233; - void collect_atom_info(Atom_Information &atom_info, ineq_atom *iat) { - LINXI_DEBUG; - unsigned sz = iat->size(); - atom_info.polys_info.resize(sz); - for (unsigned i = 0; i < sz; ++i) { - collect_poly_info(atom_info.polys_info[i], iat->p(i), iat->is_even(i)); - } - atom_info.hash_value = 0; - std::sort(atom_info.polys_info.begin(), atom_info.polys_info.end()); - for (unsigned i = 0; i < sz; ++i) { - atom_info.hash_value = atom_info.hash_value*ATOM_BASE + atom_info.polys_info[i].hash_value; - } - atom_info.akd = iat->get_kind(); - atom_info.hash_value = atom_info.hash_value*ATOM_BASE + (unsigned long long)atom_info.akd; - } - struct Literal_Information { - unsigned long long hash_value; - vector atom_info; // not atoms - bool operator< (const Literal_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Literal_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (atom_info.size() != rhs.atom_info.size()) - return false; - for (unsigned i = 0, sz = atom_info.size(); i < sz; ++i) { - if (atom_info[i] != rhs.atom_info[i]) - return false; - } - return true; - } - bool operator!= (const Literal_Information &rhs) const { - return !(*this == rhs); - } - }; - void collect_lit_info(Literal_Information &lit_info, literal lit) { - LINXI_DEBUG; - atom *at = atoms[lit.var()]; - if (at == nullptr || !at->is_ineq_atom()) { - lit_info.hash_value = lit.to_uint(); - } - else { - lit_info.atom_info.resize(1); - collect_atom_info(lit_info.atom_info[0], to_ineq_atom(at)); - lit_info.hash_value = lit_info.atom_info[0].hash_value; - } - } - struct Clause_Information { - unsigned long long hash_value; - vector lits_info; - bool operator< (const Clause_Information &rhs) const { - return hash_value < rhs.hash_value; - } - bool operator== (const Clause_Information &rhs) const { - if (hash_value != rhs.hash_value) - return false; - if (lits_info.size() != rhs.lits_info.size()) - return false; - for (unsigned i = 0, sz = lits_info.size(); i < sz; ++i) { - if (lits_info[i] != rhs.lits_info[i]) - return false; - } - return true; - } - bool operator!= (const Clause_Information &rhs) const { - return !(*this == rhs); - } - }; - unsigned long long CLA_BASE = 9973; - void collect_cla_info(Clause_Information &cla_info, clause *cla) { - LINXI_DEBUG; - unsigned sz = cla->size(); - cla_info.lits_info.resize(sz); - for (unsigned i = 0; i < sz; ++i) { - literal lit = (*cla)[i]; - collect_lit_info(cla_info.lits_info[i], lit); - } - cla_info.hash_value = 0; - std::sort(cla_info.lits_info.begin(), cla_info.lits_info.end()); - for (unsigned i = 0; i < sz; ++i) { - cla_info.hash_value = cla_info.hash_value*CLA_BASE + cla_info.lits_info[i].hash_value; - } - } - - void collect_clas_info(vector &clas_info) { - LINXI_DEBUG; - unsigned sz = clauses.size(); - clas_info.resize(sz); - for (unsigned i = 0; i < sz; ++i) { - collect_cla_info(clas_info[i], clauses[i]); - } - std::sort(clas_info.begin(), clas_info.end()); - if (!is_check) { - for (unsigned i = 0; i < arith_var_num; ++i) { - std::sort(vars_occur[i].begin(), vars_occur[i].begin()); - } - } - } - vector ori_clas_info; - imp(pmanager &_pm, unsynch_mpq_manager &_qm, const clause_vector &_clauses, const atom_vector &_atoms, const bool_vector &_is_int, const unsigned &_arith_var_num) : - // sol(_sol), - pm(_pm), - qm(_qm), - clauses(_clauses), - atoms(_atoms), - is_int(_is_int), - arith_var_num(_arith_var_num), - is_check(false) { - vars_occur.resize(arith_var_num); - collect_clas_info(ori_clas_info); - // vars_hash.resize(arith_var_num, 0); - } - vector check_clas_info; - bool check_occur_same(var x, var y) { - if (vars_occur[x].size() != vars_occur[y].size()) - return false; - for (unsigned i = 0, sz = vars_occur[x].size(); i < sz; ++i) { - if (vars_occur[x][i] != vars_occur[y][i]) - return false; - } - return true; - } - bool check_symmetry(var x, var y) { - if (!check_occur_same(x, y)) { - return false; - } - is_check = true; - tx = x, ty = y; - collect_clas_info(check_clas_info); - for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) { - if (ori_clas_info[i] != check_clas_info[i]) - return false; - } - return true; - } - }; - Symmetry_Checker::Symmetry_Checker(pmanager &_pm, unsynch_mpq_manager &_qm, const clause_vector &_clauses, const atom_vector &_atoms, const bool_vector &_is_int, const unsigned &_arith_var_num) { - LINXI_DEBUG; - // m_imp = alloc(imp, _sol, _pm, _am, _clauses, _learned, _atoms, _arith_var_num); - m_imp = alloc(imp, _pm, _qm, _clauses, _atoms, _is_int, _arith_var_num); - } - Symmetry_Checker::~Symmetry_Checker() { - LINXI_DEBUG; - dealloc(m_imp); - } - // bool Symmetry_Checker::operator()() { - // LINXI_DEBUG; - - // } - bool Symmetry_Checker::check_symmetry(var x, var y) { - return m_imp->check_symmetry(x, y); - } -} \ No newline at end of file diff --git a/src/nlsat/nlsat_symmetry_checker.h b/src/nlsat/nlsat_symmetry_checker.h deleted file mode 100644 index 1db5cb24b..000000000 --- a/src/nlsat/nlsat_symmetry_checker.h +++ /dev/null @@ -1,13 +0,0 @@ -#include "nlsat/nlsat_clause.h" - -namespace nlsat { - class Symmetry_Checker { - struct imp; - imp * m_imp; - public: - // Simple_Checker(solver &_sol, pmanager &_pm, anum_manager &_am, const clause_vector &_clauses, clause_vector &_learned, const atom_vector &_atoms, const unsigned &_arith_var_num); - Symmetry_Checker(pmanager &_pm, unsynch_mpq_manager &_qm, const clause_vector &_clauses, const atom_vector &_atoms, const bool_vector &_is_int, const unsigned &_arith_var_num); - ~Symmetry_Checker(); - bool check_symmetry(var x, var y); - }; -} \ No newline at end of file