mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix to arithmetic internalize for multiplier

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-06 11:06:13 -07:00
parent 05f63277cf
commit 9c4003d12e
4 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/euf_proof_checker.cpp
View file

@ -521,12 +521,17 @@ namespace euf {
core_solver->assert_expr(m.mk_not(mk_or(clause)));
lbool ch = core_solver->check_sat(assumptions);
std::cout << "failed to verify\n" << clause << "\n";
std::cout << "check result: " << ch << "\n";
if (ch == l_false) {
core_solver->get_unsat_core(core);
std::cout << "core\n";
for (expr* f : core)
std::cout << mk_pp(f, m) << "\n";
}
return;
SASSERT(false);
exit(0);

4
src/smt/smt_context_pp.cpp
View file

@ -241,7 +241,7 @@ namespace smt {
if (!is_relevant(lit)) out << " n ";
out << ": ";
display_verbose(out, m, 1, &lit, m_bool_var2expr.data());
if (level > 0) {
if (level > 0 || true) {
auto j = get_justification(lit.var());
display(out << " ", j);
}
@ -635,7 +635,7 @@ namespace smt {
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
out << "justification " << j.get_justification()->get_from_theory() << ": ";
// display_literals_smt2(out, lits);
display_literals_smt2(out, lits);
break;
}
default:

1
src/smt/theory_arith_core.h
View file

@ -390,6 +390,7 @@ namespace smt {
if (v == null_theory_var) {
v = mk_var(e);
}
return v;
}

14
src/smt/theory_lra.cpp
View file

@ -378,7 +378,7 @@ class theory_lra::imp {
if (a.is_extended_numeral(arg2, val))
std::swap(arg1, arg2);
if (a.is_extended_numeral(arg1, val)) {
st.add(internalize_term_core(to_app(arg2)), val);
st.add(internalize_term_core(to_app(arg2)), sign * val);
if (reflect(arg)) {
internalize_term_core(to_app(arg1));
mk_enode(arg);
@ -386,7 +386,8 @@ class theory_lra::imp {
return;
}
}
st.add(internalize_term_core(arg), sign);
else
st.add(internalize_term_core(arg), sign);
}
theory_var internalize_numeral(app* n, rational const& val) {
@ -1326,7 +1327,7 @@ public:
n1->get_th_var(get_id()) != null_theory_var &&
n2->get_th_var(get_id()) != null_theory_var && n1 != n2) {
// verbose_stream() << "ineq\n";
m_arith_eq_adapter.mk_axioms(n1, n2);
// m_arith_eq_adapter.mk_axioms(n1, n2);
}
// else
// verbose_stream() << "skip\n";
@ -2120,7 +2121,6 @@ public:
result = final_check_core();
TRACE("arith", tout << "result: " << result << "\n";);
if (result == FC_DONE) {
verbose_stream() << "second round\n";
validate_solution();
}
return result;
@ -2247,7 +2247,7 @@ public:
}
if (st == FC_DONE) {
if (assume_eqs()) {
verbose_stream() << "not done\n";
// verbose_stream() << "not done\n";
return FC_CONTINUE;
}
@ -2939,6 +2939,7 @@ public:
literal_vector m_core2;
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {
TRACE("arith", tout << lit << " <- " << core << " #eqs " << eqs.size() << "\n");
if (core.size() < small_lemma_size() && eqs.empty()) {
m_core2.reset();
for (auto const& c : core) {
@ -3805,7 +3806,8 @@ public:
for (auto const& p : m_params) tout << " " << p;
tout << "\n";
display_evidence(tout, m_explanation);
display(tout << "is-conflict: " << is_conflict << "\n"););
//display(tout << "is-conflict: " << is_conflict << "\n");
);
TRACE("arith_conflict",
display_evidence(tout, m_explanation);