mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
refined difference logic check, consolidate scoped modes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
14aff67684
commit
090ca2e46c
|
@ -171,19 +171,32 @@ namespace datalog {
|
|||
*/
|
||||
void display_fact(context & ctx, app * f, std::ostream & out);
|
||||
|
||||
class scoped_coarse_proof {
|
||||
ast_manager& m;
|
||||
class scoped_proof_mode {
|
||||
ast_manager& m;
|
||||
proof_gen_mode m_mode;
|
||||
public:
|
||||
scoped_coarse_proof(ast_manager& m): m(m) {
|
||||
scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) {
|
||||
m_mode = m.proof_mode();
|
||||
m.toggle_proof_mode(PGM_COARSE);
|
||||
m.toggle_proof_mode(mode);
|
||||
}
|
||||
~scoped_coarse_proof() {
|
||||
~scoped_proof_mode() {
|
||||
m.toggle_proof_mode(m_mode);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
class scoped_coarse_proof : public scoped_proof_mode {
|
||||
public:
|
||||
scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {}
|
||||
};
|
||||
|
||||
class scoped_no_proof : public scoped_proof_mode {
|
||||
public:
|
||||
scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {}
|
||||
};
|
||||
|
||||
|
||||
|
||||
class variable_intersection
|
||||
{
|
||||
bool values_match(const expr * v1, const expr * v2);
|
||||
|
|
|
@ -911,22 +911,9 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
template class rewriter_tpl<ite_hoister_cfg>;
|
||||
|
||||
|
||||
class scoped_no_proof {
|
||||
ast_manager& m;
|
||||
proof_gen_mode m_mode;
|
||||
public:
|
||||
scoped_no_proof(ast_manager& m): m(m) {
|
||||
m_mode = m.proof_mode();
|
||||
m.toggle_proof_mode(PGM_DISABLED);
|
||||
}
|
||||
~scoped_no_proof() {
|
||||
m.toggle_proof_mode(m_mode);
|
||||
}
|
||||
};
|
||||
|
||||
void hoist_non_bool_if(expr_ref& fml) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
scoped_no_proof _sp(m);
|
||||
datalog::scoped_no_proof _sp(m);
|
||||
params_ref p;
|
||||
ite_hoister_star ite_rw(m, p);
|
||||
expr_ref tmp(m);
|
||||
|
@ -951,7 +938,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
}
|
||||
|
||||
bool test_ineq(expr* e) const {
|
||||
SASSERT(a.is_le(e) || a.is_ge(e));
|
||||
SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e));
|
||||
SASSERT(to_app(e)->get_num_args() == 2);
|
||||
expr * lhs = to_app(e)->get_arg(0);
|
||||
expr * rhs = to_app(e)->get_arg(1);
|
||||
|
@ -985,6 +972,9 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
|
|||
if (!a.is_int_real(lhs)) {
|
||||
return true;
|
||||
}
|
||||
if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
|
||||
return test_ineq(e);
|
||||
}
|
||||
return test_term(lhs) && test_term(rhs);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue