mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

add assert to catch bad lemmas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-11 20:00:48 -08:00
parent ba2f587c26
commit d02d90dab2
3 changed files with 20 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_aig_simplifier.cpp
View file

@ -508,7 +508,7 @@ namespace sat {
} }
/** /**
* Equilvalences modulo cuts are not necessarily DRAT derivable. * Equivalences modulo cuts are not necessarily DRAT derivable.
* To ensure that there is a DRAT derivation we create all resolvents * To ensure that there is a DRAT derivation we create all resolvents
* of the LUT clauses until deriving binary u or ~v and ~u or v. * of the LUT clauses until deriving binary u or ~v and ~u or v.
* each resolvent is DRAT derivable because there are two previous lemmas that * each resolvent is DRAT derivable because there are two previous lemmas that

2
src/smt/params/smt_params_helper.pyg
View file

@ -76,7 +76,7 @@ def_module_params(module_name='smt',
('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'),
('arith.nla', BOOL, False, 'call nonlinear integer solver with incremental linearization'), ('arith.nla', BOOL, True, 'call nonlinear solver'),
('arith.print_ext_var_names', BOOL, False, 'print external variable names'), ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),

43
src/smt/theory_lra.cpp
View file

@ -266,7 +266,6 @@ class theory_lra::imp {
// non-linear arithmetic // non-linear arithmetic
scoped_ptr<nra::solver> m_nra; scoped_ptr<nra::solver> m_nra;
bool m_use_nla;
scoped_ptr<nla::solver> m_nla; scoped_ptr<nla::solver> m_nla;
bool m_use_nra_model; bool m_use_nra_model;
scoped_ptr<scoped_anum> m_a1, m_a2; scoped_ptr<scoped_anum> m_a1, m_a2;
@ -292,25 +291,17 @@ class theory_lra::imp {
} }
void push() { void push() {
if (m_use_nla) { if (m_nla != nullptr)
if (m_nla != nullptr) (*m_nla)->push();
(*m_nla)->push(); if (m_nra != nullptr)
} (*m_nra)->push();
else {
if (m_nra != nullptr)
(*m_nra)->push();
}
} }
void pop(unsigned scopes) { void pop(unsigned scopes) {
if (m_use_nla) { if (m_nla != nullptr)
if (m_nla != nullptr) (*m_nla)->pop(scopes);
(*m_nla)->pop(scopes); if (m_nra != nullptr)
} (*m_nra)->pop(scopes);
else {
if (m_nra != nullptr)
(*m_nra)->pop(scopes);
}
} }
@ -404,7 +395,7 @@ class theory_lra::imp {
lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_switcher.m_use_nla = m_use_nla = lpar.arith_nla(); m_switcher.m_use_nla = lpar.arith_nla();
m_lia = alloc(lp::int_solver, *m_solver.get()); m_lia = alloc(lp::int_solver, *m_solver.get());
get_one(true); get_one(true);
get_zero(true); get_zero(true);
@ -1613,12 +1604,7 @@ public:
} }
bool influences_nl_var(theory_var v) const { bool influences_nl_var(theory_var v) const {
if (!m_use_nla) return m_nla && m_nla->influences_nl_var(get_lpvar(v));
return false; // that is the legacy solver behavior
if (!m_nla)
return false;
return m_nla->influences_nl_var(get_lpvar(v));
} }
bool can_be_used_in_random_update(theory_var v) const { bool can_be_used_in_random_update(theory_var v) const {
@ -1716,7 +1702,7 @@ public:
bool is_eq(theory_var v1, theory_var v2) { bool is_eq(theory_var v1, theory_var v2) {
if (m_use_nra_model) { if (m_use_nra_model) {
lp_assert(!m_use_nla); SASSERT(!m_switcher.m_use_nla);
return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2)); return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
} }
else { else {
@ -3342,6 +3328,13 @@ public:
ctx().mark_as_relevant(c); ctx().mark_as_relevant(c);
} }
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";); TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
DEBUG_CODE(
for (literal const& c : m_core) {
if (ctx().get_assignment(c) == l_true) {
TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
SASSERT(false);
}
});
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr()); ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
} }
} }