mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 04:15:51 +00:00
added sequences to get-interpolant and compute-interpolant
This commit is contained in:
Ken McMillan
parent
bbe036bc03
commit
e651f45bc0
5 changed files with 253 additions and 38 deletions
|
|
@ -2002,6 +2002,7 @@ public:
|
|||
app * mk_distinct_expanded(unsigned num_args, expr * const * args);
|
||||
app * mk_true() { return m_true; }
|
||||
app * mk_false() { return m_false; }
|
||||
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
|
||||
|
||||
func_decl* mk_and_decl() {
|
||||
sort* domain[2] = { m_bool_sort, m_bool_sort };
|
||||
|
|
|
|||
|
|
@ -255,6 +255,7 @@ public:
|
|||
void reset_cancel() { set_cancel(false); }
|
||||
context_params & params() { return m_params; }
|
||||
solver_factory &get_solver_factory() { return *m_solver_factory; }
|
||||
solver_factory &get_interpolating_solver_factory() { return *m_interpolating_solver_factory; }
|
||||
void global_params_updated(); // this method should be invoked when global (and module) params are updated.
|
||||
bool set_logic(symbol const & s);
|
||||
bool has_logic() const { return m_logic != symbol::null; }
|
||||
|
|
|
|||
|
|
@ -32,44 +32,9 @@ Notes:
|
|||
#include"iz3interp.h"
|
||||
#include"iz3checker.h"
|
||||
|
||||
static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check) {
|
||||
|
||||
// get the proof, if there is one
|
||||
|
||||
if (!ctx.produce_interpolants())
|
||||
throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
|
||||
if (!ctx.has_manager() ||
|
||||
ctx.cs_state() != cmd_context::css_unsat)
|
||||
throw cmd_exception("proof is not available");
|
||||
expr_ref pr(ctx.m());
|
||||
pr = ctx.get_check_sat_result()->get_proof();
|
||||
if (pr == 0)
|
||||
throw cmd_exception("proof is not available");
|
||||
|
||||
// get the assertions
|
||||
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
ptr_vector<ast> cnsts(end - it);
|
||||
for (int i = 0; it != end; ++it, ++i)
|
||||
cnsts[i] = *it;
|
||||
|
||||
// compute an interpolant
|
||||
static void show_interpolant_and_maybe_check(cmd_context & ctx, ptr_vector<ast> &cnsts, expr *t, ptr_vector<ast> &interps, bool check)
|
||||
{
|
||||
|
||||
ptr_vector<ast> interps;
|
||||
|
||||
try {
|
||||
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
|
||||
}
|
||||
catch (iz3_bad_tree &) {
|
||||
throw cmd_exception("interpolation pattern contains non-asserted formula");
|
||||
}
|
||||
catch (iz3_incompleteness &) {
|
||||
throw cmd_exception("incompleteness in interpolator");
|
||||
}
|
||||
|
||||
|
||||
// if we lived, print it out
|
||||
for(unsigned i = 0; i < interps.size(); i++){
|
||||
ctx.regular_stream() << mk_pp(interps[i], ctx.m()) << std::endl;
|
||||
#if 0
|
||||
|
|
@ -100,6 +65,52 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool ch
|
|||
for(unsigned i = 0; i < interps.size(); i++){
|
||||
ctx.m().dec_ref(interps[i]);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
static void check_can_interpolate(cmd_context & ctx){
|
||||
if (!ctx.produce_interpolants())
|
||||
throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
|
||||
}
|
||||
|
||||
|
||||
static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check) {
|
||||
|
||||
check_can_interpolate(ctx);
|
||||
|
||||
// get the proof, if there is one
|
||||
|
||||
if (!ctx.has_manager() ||
|
||||
ctx.cs_state() != cmd_context::css_unsat)
|
||||
throw cmd_exception("proof is not available");
|
||||
expr_ref pr(ctx.m());
|
||||
pr = ctx.get_check_sat_result()->get_proof();
|
||||
if (pr == 0)
|
||||
throw cmd_exception("proof is not available");
|
||||
|
||||
// get the assertions from the context
|
||||
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
ptr_vector<ast> cnsts(end - it);
|
||||
for (int i = 0; it != end; ++it, ++i)
|
||||
cnsts[i] = *it;
|
||||
|
||||
// compute an interpolant
|
||||
|
||||
ptr_vector<ast> interps;
|
||||
|
||||
try {
|
||||
iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
|
||||
}
|
||||
catch (iz3_bad_tree &) {
|
||||
throw cmd_exception("interpolation pattern contains non-asserted formula");
|
||||
}
|
||||
catch (iz3_incompleteness &) {
|
||||
throw cmd_exception("incompleteness in interpolator");
|
||||
}
|
||||
|
||||
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, check);
|
||||
}
|
||||
|
||||
static void get_interpolant(cmd_context & ctx, expr * t) {
|
||||
|
|
@ -110,11 +121,130 @@ static void get_and_check_interpolant(cmd_context & ctx, expr * t) {
|
|||
get_interpolant_and_maybe_check(ctx,t,true);
|
||||
}
|
||||
|
||||
UNARY_CMD(get_interpolant_cmd, "get-interpolant", "<fmla>", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
|
||||
|
||||
static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check){
|
||||
|
||||
// get the proof, if there is one
|
||||
|
||||
check_can_interpolate(ctx);
|
||||
|
||||
// create a fresh solver suitable for interpolation
|
||||
bool proofs_enabled, models_enabled, unsat_core_enabled;
|
||||
params_ref p;
|
||||
ast_manager &_m = ctx.m();
|
||||
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
|
||||
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
|
||||
|
||||
ptr_vector<ast> cnsts;
|
||||
ptr_vector<ast> interps;
|
||||
model_ref m;
|
||||
|
||||
// compute an interpolant
|
||||
|
||||
lbool res;
|
||||
try {
|
||||
res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, 0);
|
||||
}
|
||||
catch (iz3_incompleteness &) {
|
||||
throw cmd_exception("incompleteness in interpolator");
|
||||
}
|
||||
|
||||
switch(res){
|
||||
case l_false:
|
||||
ctx.regular_stream() << "unsat\n";
|
||||
show_interpolant_and_maybe_check(ctx, cnsts, t, interps, check);
|
||||
break;
|
||||
|
||||
case l_true:
|
||||
ctx.regular_stream() << "sat\n";
|
||||
// TODO: how to return the model to the context, if it exists?
|
||||
break;
|
||||
|
||||
case l_undef:
|
||||
ctx.regular_stream() << "unknown\n";
|
||||
// TODO: how to return the model to the context, if it exists?
|
||||
break;
|
||||
}
|
||||
|
||||
for(unsigned i = 0; i < cnsts.size(); i++)
|
||||
ctx.m().dec_ref(cnsts[i]);
|
||||
|
||||
}
|
||||
|
||||
static expr *make_tree(cmd_context & ctx, const ptr_vector<expr> &exprs){
|
||||
if(exprs.size() == 0)
|
||||
throw cmd_exception("not enough arguments");
|
||||
expr *foo = exprs[0];
|
||||
for(unsigned i = 1; i < exprs.size(); i++){
|
||||
foo = ctx.m().mk_and(ctx.m().mk_interp(foo),exprs[i]);
|
||||
}
|
||||
return foo;
|
||||
}
|
||||
|
||||
static void get_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs) {
|
||||
expr *foo = make_tree(ctx,exprs);
|
||||
ctx.m().inc_ref(foo);
|
||||
get_interpolant(ctx,foo);
|
||||
ctx.m().dec_ref(foo);
|
||||
}
|
||||
|
||||
static void compute_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs) {
|
||||
expr *foo = make_tree(ctx, exprs);
|
||||
ctx.m().inc_ref(foo);
|
||||
compute_interpolant_and_maybe_check(ctx,foo,false);
|
||||
ctx.m().dec_ref(foo);
|
||||
}
|
||||
|
||||
|
||||
// UNARY_CMD(get_interpolant_cmd, "get-interpolant", "<fmla>", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
|
||||
|
||||
// UNARY_CMD(get_and_check_interpolant_cmd, "get-and-check-interpolant", "<fmla>", "get and check interpolant for marked positions in fmla", CPK_EXPR, expr *, get_and_check_interpolant(ctx, arg););
|
||||
|
||||
class get_interpolant_cmd : public parametric_cmd {
|
||||
protected:
|
||||
ptr_vector<expr> m_targets;
|
||||
public:
|
||||
get_interpolant_cmd(char const * name = "get-interpolant"):parametric_cmd(name) {}
|
||||
|
||||
virtual char const * get_usage() const { return "<fmla>+"; }
|
||||
|
||||
virtual char const * get_main_descr() const {
|
||||
return "get interpolant for formulas";
|
||||
}
|
||||
|
||||
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
|
||||
}
|
||||
|
||||
virtual void prepare(cmd_context & ctx) {
|
||||
parametric_cmd::prepare(ctx);
|
||||
m_targets.resize(0);
|
||||
}
|
||||
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
return CPK_EXPR;
|
||||
}
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
|
||||
m_targets.push_back(arg);
|
||||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
get_interpolant(ctx,m_targets);
|
||||
}
|
||||
};
|
||||
|
||||
class compute_interpolant_cmd : public get_interpolant_cmd {
|
||||
public:
|
||||
compute_interpolant_cmd(char const * name = "compute-interpolant"):get_interpolant_cmd(name) {}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
compute_interpolant(ctx,m_targets);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
void install_interpolant_cmds(cmd_context & ctx) {
|
||||
ctx.insert(alloc(get_interpolant_cmd));
|
||||
ctx.insert(alloc(compute_interpolant_cmd));
|
||||
// ctx.insert(alloc(get_and_check_interpolant_cmd));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -278,6 +278,37 @@ public:
|
|||
interps[i] = i < _interps.size() ? _interps[i] : mk_false();
|
||||
}
|
||||
|
||||
bool has_interp(hash_map<ast,bool> &memo, const ast &t){
|
||||
if(memo.find(t) != memo.end())
|
||||
return memo[t];
|
||||
bool res = false;
|
||||
if(op(t) == Interp)
|
||||
res = true;
|
||||
else if(op(t) == And){
|
||||
int nargs = num_args(t);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
res |= has_interp(memo, arg(t,i));
|
||||
}
|
||||
memo[t] = res;
|
||||
return res;
|
||||
}
|
||||
|
||||
void collect_conjuncts(std::vector<ast> &cnsts, hash_map<ast,bool> &memo, const ast &t){
|
||||
if(!has_interp(memo,t))
|
||||
cnsts.push_back(t);
|
||||
else {
|
||||
int nargs = num_args(t);
|
||||
for(int i = 0; i < nargs; i++)
|
||||
collect_conjuncts(cnsts, memo, arg(t,i));
|
||||
}
|
||||
}
|
||||
|
||||
void assert_conjuncts(solver &s, std::vector<ast> &cnsts, const ast &t){
|
||||
hash_map<ast,bool> memo;
|
||||
collect_conjuncts(cnsts,memo,t);
|
||||
for(unsigned i = 0; i < cnsts.size(); i++)
|
||||
s.assert_expr(to_expr(cnsts[i].raw()));
|
||||
}
|
||||
|
||||
iz3interp(ast_manager &_m_manager)
|
||||
: iz3base(_m_manager) {}
|
||||
|
|
@ -329,6 +360,37 @@ void iz3interpolate(ast_manager &_m_manager,
|
|||
interps[i] = itp.uncook(_interps[i]);
|
||||
}
|
||||
|
||||
lbool iz3interpolate(ast_manager &_m_manager,
|
||||
solver &s,
|
||||
ast *tree,
|
||||
ptr_vector<ast> &cnsts,
|
||||
ptr_vector<ast> &interps,
|
||||
model_ref &m,
|
||||
interpolation_options_struct * options)
|
||||
{
|
||||
iz3interp itp(_m_manager);
|
||||
iz3mgr::ast _tree = itp.cook(tree);
|
||||
std::vector<iz3mgr::ast> _cnsts;
|
||||
itp.assert_conjuncts(s,_cnsts,_tree);
|
||||
lbool res = s.check_sat(0,0);
|
||||
if(res == l_false){
|
||||
ast *proof = s.get_proof();
|
||||
iz3mgr::ast _proof = itp.cook(proof);
|
||||
std::vector<iz3mgr::ast> _interps;
|
||||
itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options);
|
||||
interps.resize(_interps.size());
|
||||
for(unsigned i = 0; i < interps.size(); i++)
|
||||
interps[i] = itp.uncook(_interps[i]);
|
||||
}
|
||||
else if(m){
|
||||
s.get_model(m);
|
||||
}
|
||||
cnsts.resize(_cnsts.size());
|
||||
for(unsigned i = 0; i < cnsts.size(); i++)
|
||||
cnsts[i] = itp.uncook(_cnsts[i]);
|
||||
return res;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
#define IZ3_INTERP_H
|
||||
|
||||
#include "iz3hash.h"
|
||||
#include "solver.h"
|
||||
|
||||
struct interpolation_options_struct {
|
||||
stl_ext::hash_map<std::string,std::string> map;
|
||||
|
|
@ -37,6 +38,9 @@ struct iz3_incompleteness {
|
|||
|
||||
typedef interpolation_options_struct *interpolation_options;
|
||||
|
||||
/* Compute an interpolant from a proof. This version uses the parents vector
|
||||
representation, for compatibility with the old API. */
|
||||
|
||||
void iz3interpolate(ast_manager &_m_manager,
|
||||
ast *proof,
|
||||
const ptr_vector<ast> &cnsts,
|
||||
|
|
@ -45,6 +49,9 @@ void iz3interpolate(ast_manager &_m_manager,
|
|||
const ptr_vector<ast> &theory,
|
||||
interpolation_options_struct * options = 0);
|
||||
|
||||
/* Compute an interpolant from a proof. This version uses the ast
|
||||
representation, for compatibility with the new API. */
|
||||
|
||||
void iz3interpolate(ast_manager &_m_manager,
|
||||
ast *proof,
|
||||
const ptr_vector<ast> &cnsts,
|
||||
|
|
@ -52,4 +59,18 @@ void iz3interpolate(ast_manager &_m_manager,
|
|||
ptr_vector<ast> &interps,
|
||||
interpolation_options_struct * options);
|
||||
|
||||
/* Compute an interpolant from an ast representing an interpolation
|
||||
problem, if unsat, else return a model (if enabled). Uses the
|
||||
given solver to produce the proof/model. Also returns a vector
|
||||
of the constraints in the problem, helpful for checking correctness.
|
||||
*/
|
||||
|
||||
lbool iz3interpolate(ast_manager &_m_manager,
|
||||
solver &s,
|
||||
ast *tree,
|
||||
ptr_vector<ast> &cnsts,
|
||||
ptr_vector<ast> &interps,
|
||||
model_ref &m,
|
||||
interpolation_options_struct * options);
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue