From e2565d8d824c74e6734c413c4304d6437d1a8a68 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Dec 2015 18:41:10 -0800 Subject: [PATCH] add some of the SMT2.5 features Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 73 ++++++++++---- src/cmd_context/cmd_context.cpp | 31 ++++++ src/cmd_context/cmd_context.h | 5 + src/parsers/smt2/smt2parser.cpp | 174 ++++++++++++++++++++++++++++++-- 4 files changed, 256 insertions(+), 27 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 4abaad9f8..5c70523a8 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -165,26 +165,39 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { ctx.regular_stream() << std::endl; }); +#define PRINT_CORE() \ + ptr_vector core; \ + ctx.get_check_sat_result()->get_unsat_core(core); \ + ctx.regular_stream() << "("; \ + ptr_vector::const_iterator it = core.begin(); \ + ptr_vector::const_iterator end = core.end(); \ + for (bool first = true; it != end; ++it) { \ + if (first) \ + first = false; \ + else \ + ctx.regular_stream() << " "; \ + ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); \ + } \ + ctx.regular_stream() << ")" << std::endl; \ + ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { - if (!ctx.produce_unsat_cores()) - throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)"); - if (!ctx.has_manager() || - ctx.cs_state() != cmd_context::css_unsat) - throw cmd_exception("unsat core is not available"); - ptr_vector core; - ctx.get_check_sat_result()->get_unsat_core(core); - ctx.regular_stream() << "("; - ptr_vector::const_iterator it = core.begin(); - ptr_vector::const_iterator end = core.end(); - for (bool first = true; it != end; ++it) { - if (first) - first = false; - else - ctx.regular_stream() << " "; - ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); - } - ctx.regular_stream() << ")" << std::endl; -}); + if (!ctx.produce_unsat_cores()) + throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)"); + if (!ctx.has_manager() || + ctx.cs_state() != cmd_context::css_unsat) + throw cmd_exception("unsat core is not available"); + PRINT_CORE(); + }); + +ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", { + if (!ctx.produce_unsat_assumptions()) + throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)"); + if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) { + throw cmd_exception("unsat assumptions is not available"); + } + PRINT_CORE(); + }); + ATOMIC_CMD(labels_cmd, "labels", "retrieve Simplify-like labels", { if (!ctx.has_manager() || @@ -201,6 +214,11 @@ ATOMIC_CMD(labels_cmd, "labels", "retrieve Simplify-like labels", { ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when in interactive mode", ctx.display_assertions();); + + + +ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions();); + UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) ctx.print_success(); @@ -226,6 +244,7 @@ protected: symbol m_interactive_mode; symbol m_produce_proofs; symbol m_produce_unsat_cores; + symbol m_produce_unsat_assumptions; symbol m_produce_models; symbol m_produce_assignments; symbol m_produce_interpolants; @@ -241,9 +260,9 @@ protected: bool is_builtin_option(symbol const & s) const { return s == m_print_success || s == m_print_warning || s == m_expand_definitions || - s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || + s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_regular_output_channel || s == m_diagnostic_output_channel || + s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls; } @@ -258,6 +277,7 @@ public: m_interactive_mode(":interactive-mode"), m_produce_proofs(":produce-proofs"), m_produce_unsat_cores(":produce-unsat-cores"), + m_produce_unsat_assumptions(":produce-unsat-assumptions"), m_produce_models(":produce-models"), m_produce_assignments(":produce-assignments"), m_produce_interpolants(":produce-interpolants"), @@ -336,6 +356,10 @@ class set_option_cmd : public set_get_option_cmd { check_not_initialized(ctx, m_produce_unsat_cores); ctx.set_produce_unsat_cores(to_bool(value)); } + else if (m_option == m_produce_unsat_assumptions) { + check_not_initialized(ctx, m_produce_unsat_assumptions); + ctx.set_produce_unsat_assumptions(to_bool(value)); + } else if (m_option == m_produce_models) { ctx.set_produce_models(to_bool(value)); } @@ -737,8 +761,15 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(builtin_cmd, "declare-fun", " (*) ", "declare a new function/constant.")); ctx.insert(alloc(builtin_cmd, "declare-const", " ", "declare a new constant.")); ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(*) (+)", "declare mutually recursive datatypes.\n ::= ( +)\n ::= ( *)\n ::= ( )\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))")); + ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals")); + + // ctx.insert(alloc(builtin_cmd, "define-fun-rec", "hfun-defi", "define a function satisfying recursive equations")); + // ctx.insert(alloc(builtin_cmd, "define-funs-rec", "( hfun_decin+1 ) ( htermin+1 )", "define multiple mutually recursive functions")); + // ctx.insert(alloc(get_unsat_assumptions_cmd)); + ctx.insert(alloc(reset_assertions_cmd)); } + void install_ext_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(help_cmd)); ctx.insert(alloc(pp_cmd)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4fa7b88bf..f863393fb 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -313,6 +313,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_print_success(m_params.m_smtlib2_compliant), m_random_seed(0), m_produce_unsat_cores(false), + m_produce_unsat_assumptions(false), m_produce_assignments(false), m_status(UNKNOWN), m_numeral_as_real(false), @@ -831,6 +832,17 @@ void cmd_context::insert(symbol const & s, object_ref * r) { m_object_refs.insert(s, r); } +void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e) { + expr_ref eq(m()), lhs(m()); + lhs = m().mk_app(f, binding.size(), binding.c_ptr()); + eq = m().mk_eq(lhs, e); + if (!ids.empty()) { + eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq); + } + warning_msg("recursive functions are currently only partially supported: they are translated into recursive equations without special handling"); + // TBD: basic implementation asserts axiom. Life-time of recursive equation follows scopes (unlikely to be what SMT-LIB 2.5 wants). + assert_expr(eq); +} func_decl * cmd_context::find_func_decl(symbol const & s) const { builtin_decl d; @@ -1480,6 +1492,24 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } } +void cmd_context::reset_assertions() { + if (m_opt) { + m_opt = 0; + } + if (m_solver) { + m_solver = 0; + mk_solver(); + } + restore_assertions(0); + svector::iterator it = m_scopes.begin(); + svector::iterator end = m_scopes.end(); + for (; it != end; ++it) { + it->m_assertions_lim = 0; + if (m_solver) m_solver->push(); + } +} + + void cmd_context::display_model(model_ref& mdl) { if (mdl) { model_params p; @@ -1672,6 +1702,7 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) { st.display_smt2(regular_stream()); } + void cmd_context::display_assertions() { if (!m_interactive_mode) throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)"); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 9aac7bf06..013ca7554 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -156,6 +156,7 @@ protected: bool m_print_success; unsigned m_random_seed; bool m_produce_unsat_cores; + bool m_produce_unsat_assumptions; bool m_produce_assignments; status m_status; bool m_numeral_as_real; @@ -308,7 +309,9 @@ public: void set_produce_unsat_cores(bool flag); void set_produce_proofs(bool flag); void set_produce_interpolants(bool flag); + void set_produce_unsat_assumptions(bool flag) { m_produce_unsat_assumptions = flag; } bool produce_assignments() const { return m_produce_assignments; } + bool produce_unsat_assumptions() const { return m_produce_unsat_assumptions; } void set_produce_assignments(bool flag) { m_produce_assignments = flag; } void set_status(status st) { m_status = st; } status get_status() const { return m_status; } @@ -342,6 +345,7 @@ public: void insert(probe_info * p) { tactic_manager::insert(p); } void insert_user_tactic(symbol const & s, sexpr * d); void insert_aux_pdecl(pdecl * p); + void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e); func_decl * find_func_decl(symbol const & s) const; func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range) const; @@ -390,6 +394,7 @@ public: void push(unsigned n); void pop(unsigned n); void check_sat(unsigned num_assumptions, expr * const * assumptions); + void reset_assertions(); // display the result produced by a check-sat or check-sat-using commands in the regular stream void display_sat_result(lbool r); // check if result produced by check-sat or check-sat-using matches the known status diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 6931a7973..b95be8ee5 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -29,6 +29,7 @@ Revision History: #include"has_free_vars.h" #include"ast_smt2_pp.h" #include"parser_params.hpp" +#include namespace smt2 { typedef cmd_exception parser_exception; @@ -98,6 +99,9 @@ namespace smt2 { symbol m_pop; symbol m_get_value; symbol m_reset; + symbol m_check_sat_assuming; + symbol m_define_fun_rec; + symbol m_define_funs_rec; symbol m_underscore; typedef std::pair named_expr; @@ -1843,6 +1847,132 @@ namespace smt2 { next(); } + void parse_define_fun_rec() { + // ( define-fun-rec hfun_defi ) + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_define_fun_rec); + SASSERT(m_num_bindings == 0); + next(); + + expr_ref_vector binding(m()); + svector ids; + func_decl_ref f(m()); + parse_rec_fun_decl(f, binding, ids); + m_ctx.insert(f); + parse_rec_fun_body(f, binding, ids); + check_rparen("invalid function/constant definition, ')' expected"); + m_ctx.print_success(); + next(); + } + + void parse_define_funs_rec() { + // ( define-funs-rec ( hfun_decin+1 ) ( htermin+1 ) ) + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_define_funs_rec); + SASSERT(m_num_bindings == 0); + next(); + func_decl_ref_vector decls(m()); + vector bindings; + vector > ids; + expr_ref_vector bodies(m()); + parse_rec_fun_decls(decls, bindings, ids); + for (unsigned i = 0; i < decls.size(); ++i) { + m_ctx.insert(decls[i].get()); + } + parse_rec_fun_bodies(decls, bindings, ids); + + check_rparen("invalid function/constant definition, ')' expected"); + m_ctx.print_success(); + next(); + } + + void parse_rec_fun_decls(func_decl_ref_vector& decls, vector& bindings, vector >& ids) { + check_lparen("invalid recursive function definition, '(' expected"); + next(); + while (!curr_is_rparen()) { + expr_ref_vector binding(m()); + svector id; + func_decl_ref f(m()); + + check_lparen("invalid recursive function definition, '(' expected"); + next(); + + parse_rec_fun_decl(f, binding, id); + decls.push_back(f); + bindings.push_back(binding); + ids.push_back(id); + + check_rparen("invalid recursive function definition, ')' expected"); + next(); + } + next(); + } + + void parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector& ids) { + SASSERT(m_num_bindings == 0); + check_identifier("invalid function/constant definition, symbol expected"); + symbol id = curr_id(); + next(); + unsigned sym_spos = symbol_stack().size(); + unsigned sort_spos = sort_stack().size(); + unsigned expr_spos = expr_stack().size(); + unsigned num_vars = parse_sorted_vars(); + SASSERT(num_vars == m_num_bindings); + parse_sort(); + f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back()); + bindings.append(num_vars, expr_stack().c_ptr() + expr_spos); + ids.append(num_vars, symbol_stack().c_ptr() + sym_spos); + symbol_stack().shrink(sym_spos); + sort_stack().shrink(sort_spos); + expr_stack().shrink(expr_spos); + m_env.end_scope(); + m_num_bindings = 0; + } + + void parse_rec_fun_bodies(func_decl_ref_vector const& decls, vector const& bindings, vector >const & ids) { + unsigned i = 0; + check_lparen("invalid recursive function definition, '(' expected"); + next(); + while (!curr_is_rparen() && i < decls.size()) { + parse_rec_fun_body(decls[i], bindings[i], ids[i]); + ++i; + } + + if (i != decls.size()) { + throw parser_exception("the number of declarations does not match number of supplied definitions"); + } + check_rparen("invalid recursive function definition, ')' expected"); + next(); + } + + void parse_rec_fun_body(func_decl* f, expr_ref_vector const& bindings, svector const& ids) { + SASSERT(m_num_bindings == 0); + expr_ref body(m()); + unsigned sym_spos = symbol_stack().size(); + unsigned num_vars = bindings.size(); + m_env.begin_scope(); + m_symbol_stack.append(ids.size(), ids.c_ptr()); + m_num_bindings = num_vars; + for (unsigned i = 0; i < num_vars; ++i) { + m_env.insert(ids[i], local(bindings[i], num_vars)); + } + parse_expr(); + body = expr_stack().back(); + expr_stack().pop_back(); + symbol_stack().shrink(sym_spos); + m_env.end_scope(); + m_num_bindings = 0; + if (m().get_sort(body) != f->get_range()) { + std::ostringstream buffer; + buffer << "invalid function definition, sort mismatch. Expcected " + << mk_pp(f->get_range(), m()) << " but function body has sort " + << mk_pp(m().get_sort(body), m()); + throw parser_exception(buffer.str().c_str()); + } + m_ctx.insert_rec_fun(f, bindings, ids, body); + } + + void parse_define_const() { SASSERT(curr_is_identifier()); SASSERT(curr_id() == m_define_const); @@ -1978,11 +2108,7 @@ namespace smt2 { next(); } - void parse_check_sat() { - SASSERT(curr_is_identifier()); - SASSERT(curr_id() == m_check_sat); - next(); - unsigned spos = expr_stack().size(); + void parse_assumptions() { while (!curr_is_rparen()) { bool sign; expr_ref t_ref(m()); @@ -2015,6 +2141,27 @@ namespace smt2 { if (sign) check_rparen_next("invalid check-sat command, ')' expected"); } + } + + void parse_check_sat() { + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_check_sat); + next(); + unsigned spos = expr_stack().size(); + parse_assumptions(); + m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos); + next(); + expr_stack().shrink(spos); + } + + void parse_check_sat_assuming() { + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_check_sat_assuming); + next(); + unsigned spos = expr_stack().size(); + check_rparen_next("invalid check-sat-assuming command, '(', expected"); + parse_assumptions(); + check_rparen_next("invalid check-sat-assuming command, ')', expected"); m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos); next(); expr_stack().shrink(spos); @@ -2371,6 +2518,18 @@ namespace smt2 { parse_reset(); return; } + if (s == m_check_sat_assuming) { + parse_check_sat_assuming(); + return; + } + if (s == m_define_fun_rec) { + parse_define_fun_rec(); + return; + } + if (s == m_define_funs_rec) { + parse_define_funs_rec(); + return; + } parse_ext_cmd(line, pos); } @@ -2411,7 +2570,10 @@ namespace smt2 { m_pop("pop"), m_get_value("get-value"), m_reset("reset"), - m_underscore("_"), + m_check_sat_assuming("check-sat-assuming"), + m_define_fun_rec("define-fun-rec"), + m_define_funs_rec("define-funs-rec"), + m_underscore("_"), m_num_open_paren(0) { // the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created. // SASSERT(!m_ctx.has_manager());