mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
delete unused nlsat_symmetry_checker
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
f7905a5d69
commit
f81303f2f3
|
@ -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
|
||||
|
|
|
@ -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"),
|
||||
|
|
|
@ -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<rational> as;
|
||||
vector<var> 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()) {
|
||||
|
|
|
@ -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<unsigned long long> vars_hash;
|
||||
vector<vector<unsigned>> 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<Variable_Information> 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<Monomial_Information> 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<Polynomial_Information> 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_Information> 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<Literal_Information> 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<Clause_Information> &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<Clause_Information> 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<Clause_Information> 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);
|
||||
}
|
||||
}
|
|
@ -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);
|
||||
};
|
||||
}
|
Loading…
Reference in a new issue