mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

remove output

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-18 16:41:00 +03:00
parent 0f896503a9
commit 1c163dbad2
6 changed files with 45 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/arith_internalize.cpp
View file

@ -51,6 +51,16 @@ namespace arith {
}
}
void solver::initialize_value(expr* var, expr* value) {
rational r;
if (!a.is_numeral(value, r)) {
IF_VERBOSE(5, verbose_stream() << "numeric constant expected in initialization " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
return;
}
lp().move_lpvar_to_value(get_lpvar(mk_evar(var)), r);
}
lpvar solver::get_one(bool is_int) {
return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
}

3
src/sat/smt/arith_solver.h
View file

@ -485,6 +485,8 @@ namespace arith {
bool validate_conflict();
public:
solver(euf::solver& ctx, theory_id id);
~solver() override;
@ -512,6 +514,7 @@ namespace arith {
void internalize(expr* e) override;
void eq_internalized(euf::enode* n) override;
void apply_sort_cnstr(euf::enode* n, sort* s) override {}
void initialize_value(expr* var, expr* value) override;
bool is_shared(theory_var v) const override;
lbool get_phase(bool_var v) override;
bool include_func_interp(func_decl* f) const override;

49
src/sat/smt/euf_solver.cpp
View file

@ -195,6 +195,30 @@ namespace euf {
m_reason_unknown.clear();
for (auto* s : m_solvers)
s->init_search();
for (auto const& [var, value] : m_initial_values) {
if (m.is_bool(var)) {
auto lit = expr2literal(var);
if (lit == sat::null_literal) {
IF_VERBOSE(5, verbose_stream() << "no literal associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
continue;
}
if (m.is_true(value))
s().set_phase(lit);
else if (m.is_false(value))
s().set_phase(~lit);
else
IF_VERBOSE(5, verbose_stream() << "malformed value " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
continue;
}
auto* th = m_id2solver.get(var->get_sort()->get_family_id(), nullptr);
if (!th) {
IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
continue;
}
th->initialize_value(var, value);
}
}
bool solver::is_external(bool_var v) {
@ -1257,27 +1281,10 @@ namespace euf {
}
void solver::user_propagate_initialize_value(expr* var, expr* value) {
if (m.is_bool(var)) {
auto lit = expr2literal(var);
if (lit == sat::null_literal) {
IF_VERBOSE(5, verbose_stream() << "no literal associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
return;
}
if (m.is_true(value))
s().set_phase(lit);
else if (m.is_false(value))
s().set_phase(~lit);
else
IF_VERBOSE(5, verbose_stream() << "malformed value " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
return;
}
auto* th = m_id2solver.get(var->get_sort()->get_family_id(), nullptr);
if (!th) {
IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
return;
}
// th->initialize_value(var, value);
IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
m_initial_values.push_back({expr_ref(var, m), expr_ref(value, m)});
push(push_back_vector(m_initial_values));
}

2
src/sat/smt/euf_solver.h
View file

@ -189,6 +189,8 @@ namespace euf {
euf::enode* mk_true();
euf::enode* mk_false();
vector<std::pair<expr_ref, expr_ref>> m_initial_values;
// replay
typedef std::tuple<expr_ref, unsigned, sat::bool_var> reinit_t;
vector<reinit_t> m_reinit;

2
src/sat/smt/sat_th.h
View file

@ -152,6 +152,8 @@ namespace euf {
virtual void finalize() {}
virtual void initialize_value(expr* v, expr* value) { IF_VERBOSE(5, verbose_stream() << "value initialzation is not supported for theory\n"); }
};
class th_proof_hint : public sat::proof_hint {

1
src/smt/theory_lra.cpp
View file

@ -1422,7 +1422,6 @@ public:
m_num_conflicts = 0;
for (auto const& [v, r] : m_values)
lp().move_lpvar_to_value(v, r);
display(verbose_stream() << "init search\n");
}
bool can_get_value(theory_var v) const {