mirror of
https://github.com/Z3Prover/z3
synced 2025-04-09 02:41:52 +00:00
134 lines
4 KiB
C++
134 lines
4 KiB
C++
/*++
|
|
Copyright (c) 2018 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
qe_mbi.h
|
|
|
|
Abstract:
|
|
|
|
Model-based interpolation utilities
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
|
|
|
|
Revision History:
|
|
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
#include "qe/qe_arith.h"
|
|
|
|
namespace qe {
|
|
enum mbi_result {
|
|
mbi_sat,
|
|
mbi_unsat,
|
|
mbi_augment,
|
|
mbi_undef,
|
|
};
|
|
|
|
class mbi_plugin {
|
|
protected:
|
|
ast_manager& m;
|
|
func_decl_ref_vector m_shared;
|
|
public:
|
|
mbi_plugin(ast_manager& m): m(m), m_shared(m) {}
|
|
virtual ~mbi_plugin() {}
|
|
|
|
/**
|
|
* Set the shared symbols.
|
|
*/
|
|
virtual void set_shared(func_decl_ref_vector const& vars) {
|
|
m_shared.reset();
|
|
m_shared.append(vars);
|
|
}
|
|
|
|
/**
|
|
* \brief Utility that works modulo a background state.
|
|
* - vars
|
|
* variables to preferably project onto (other variables would require quantification to fit interpolation signature)
|
|
* - lits
|
|
* set of literals to check satisfiability with respect to.
|
|
* - mdl
|
|
* optional model for caller.
|
|
* on return:
|
|
* - mbi_sat:
|
|
* populates mdl with a satisfying state, and lits with implicant for background state.
|
|
* - mbi_unsat:
|
|
* populates lits to be inconsistent with background state.
|
|
* For all practical purposes it is a weakening of lits or even a subset of lits.
|
|
* - mbi_augment:
|
|
* populates lits with strengthening of lits (superset)
|
|
* - mbi_undef:
|
|
* inconclusive,
|
|
*/
|
|
virtual mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) = 0;
|
|
|
|
/**
|
|
* \brief Block conjunction of lits from future mbi_augment or mbi_sat.
|
|
*/
|
|
virtual void block(expr_ref_vector const& lits) = 0;
|
|
|
|
/**
|
|
* \brief perform a full check, consume internal auguments if necessary.
|
|
*/
|
|
lbool check(expr_ref_vector& lits, model_ref& mdl);
|
|
|
|
virtual lbool check_ag(expr_ref_vector& lits, model_ref& mdl, bool force_model) {
|
|
return l_undef;
|
|
}
|
|
|
|
|
|
};
|
|
|
|
class prop_mbi_plugin : public mbi_plugin {
|
|
solver_ref m_solver;
|
|
public:
|
|
prop_mbi_plugin(solver* s);
|
|
~prop_mbi_plugin() override {}
|
|
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
|
|
void block(expr_ref_vector const& lits) override;
|
|
};
|
|
|
|
|
|
class euf_arith_mbi_plugin : public mbi_plugin {
|
|
expr_ref_vector m_atoms;
|
|
obj_hashtable<expr> m_atom_set;
|
|
expr_ref_vector m_fmls;
|
|
solver_ref m_solver;
|
|
solver_ref m_dual_solver;
|
|
struct is_atom_proc;
|
|
struct is_arith_var_proc;
|
|
|
|
app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies);
|
|
bool get_literals(model_ref& mdl, expr_ref_vector& lits);
|
|
void collect_atoms(expr_ref_vector const& fmls);
|
|
void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
|
|
void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
|
|
void substitute(vector<def> const& defs, expr_ref_vector& lits);
|
|
void filter_private_arith(app_ref_vector& avars);
|
|
public:
|
|
euf_arith_mbi_plugin(solver* s, solver* emptySolver);
|
|
~euf_arith_mbi_plugin() override {}
|
|
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
|
|
void project(model_ref& mdl, expr_ref_vector& lits);
|
|
void block(expr_ref_vector const& lits) override;
|
|
};
|
|
|
|
/**
|
|
* use cases for interpolation.
|
|
*/
|
|
class interpolator {
|
|
ast_manager& m;
|
|
public:
|
|
interpolator(ast_manager& m):m(m) {}
|
|
lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
|
|
lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
|
|
lbool vurtego(mbi_plugin &a, mbi_plugin &b, expr_ref &itp, model_ref &mdl);
|
|
};
|
|
|
|
};
|