add some of the SMT2.5 features

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<expr> core;                                      \
+    ctx.get_check_sat_result()->get_unsat_core(core);           \
+    ctx.regular_stream() << "(";                                \
+    ptr_vector<expr>::const_iterator it  = core.begin();        \
+    ptr_vector<expr>::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())
+        if (!ctx.produce_unsat_cores())
-        throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)");
+            throw cmd_exception("unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)");
-    if (!ctx.has_manager() ||
+        if (!ctx.has_manager() ||
-        ctx.cs_state() != cmd_context::css_unsat)
+            ctx.cs_state() != cmd_context::css_unsat)
-        throw cmd_exception("unsat core is not available");
+            throw cmd_exception("unsat core is not available");
-    ptr_vector<expr> core;
+        PRINT_CORE();
-    ctx.get_check_sat_result()->get_unsat_core(core);
+    });
-    ctx.regular_stream() << "(";
+
-    ptr_vector<expr>::const_iterator it  = core.begin();
+ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", {
-    ptr_vector<expr>::const_iterator end = core.end();
+        if (!ctx.produce_unsat_assumptions())
-    for (bool first = true; it != end; ++it) {
+            throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)");
-        if (first)
+        if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) {
-            first = false;
+            throw cmd_exception("unsat assumptions is not available");
-        else
+        }
-            ctx.regular_stream() << " ";
+        PRINT_CORE();
-        ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
+    });
-    }
+
-    ctx.regular_stream() << ")" << std::endl;
-});
 
 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", "<symbol>", "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", "<symbol> (<sort>*) <sort>", "declare a new function/constant."));
     ctx.insert(alloc(builtin_cmd, "declare-const", "<symbol> <sort>", "declare a new constant."));
     ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\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));

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<symbol> 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<scope>::iterator it  = m_scopes.begin();
+    svector<scope>::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)");

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<symbol> 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

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<sstream>
 
 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<symbol, expr*> 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<symbol> 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<expr_ref_vector> bindings;
+            vector<svector<symbol> > 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<expr_ref_vector>& bindings, vector<svector<symbol> >& ids) {
+            check_lparen("invalid recursive function definition, '(' expected");
+            next();
+            while (!curr_is_rparen()) {
+                expr_ref_vector binding(m());
+                svector<symbol> 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<symbol>& 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<expr_ref_vector> const& bindings, vector<svector<symbol> >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<symbol> 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() {
+        void parse_assumptions() {
-            SASSERT(curr_is_identifier());
-            SASSERT(curr_id() == m_check_sat);
-            next();
-            unsigned spos = expr_stack().size();
             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,6 +2570,9 @@ namespace smt2 {
             m_pop("pop"),
             m_get_value("get-value"),
             m_reset("reset"),
+            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.