From e651f45bc0ed7e2f272ea7adbe27a505fbae4fb7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 9 Apr 2013 15:52:30 -0700 Subject: [PATCH] added sequences to get-interpolant and compute-interpolant --- src/ast/ast.h | 1 + src/cmd_context/cmd_context.h | 1 + src/cmd_context/interpolant_cmds.cpp | 206 ++++++++++++++++++++++----- src/interp/iz3interp.cpp | 62 ++++++++ src/interp/iz3interp.h | 21 +++ 5 files changed, 253 insertions(+), 38 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 141c1c9a2..2753d0006 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -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 }; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index eac9a39ce..e34975183 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -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; } diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index bfade815c..ca22b3907 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -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::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - ptr_vector 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 &cnsts, expr *t, ptr_vector &interps, bool check) +{ - ptr_vector 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::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); + ptr_vector cnsts(end - it); + for (int i = 0; it != end; ++it, ++i) + cnsts[i] = *it; + + // compute an interpolant + + ptr_vector 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", "", "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 sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic()); + + ptr_vector cnsts; + ptr_vector 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 &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 &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 &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", "", "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", "", "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 m_targets; +public: + get_interpolant_cmd(char const * name = "get-interpolant"):parametric_cmd(name) {} + + virtual char const * get_usage() const { return "+"; } + + 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)); } diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index f3bde143d..6a9c54716 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -278,6 +278,37 @@ public: interps[i] = i < _interps.size() ? _interps[i] : mk_false(); } + bool has_interp(hash_map &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 &cnsts, hash_map &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 &cnsts, const ast &t){ + hash_map 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 &cnsts, + ptr_vector &interps, + model_ref &m, + interpolation_options_struct * options) +{ + iz3interp itp(_m_manager); + iz3mgr::ast _tree = itp.cook(tree); + std::vector _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 _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; +} + diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 017791186..7174205f1 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -21,6 +21,7 @@ Revision History: #define IZ3_INTERP_H #include "iz3hash.h" +#include "solver.h" struct interpolation_options_struct { stl_ext::hash_map 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 &cnsts, @@ -45,6 +49,9 @@ void iz3interpolate(ast_manager &_m_manager, const ptr_vector &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 &cnsts, @@ -52,4 +59,18 @@ void iz3interpolate(ast_manager &_m_manager, ptr_vector &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 &cnsts, + ptr_vector &interps, + model_ref &m, + interpolation_options_struct * options); + #endif