add consequence command

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

src/cmd_context/basic_cmds.cpp

@@ -753,6 +753,42 @@ public:
     }
 };
 
+class get_consequences_cmd : public cmd {
+    ptr_vector<expr> m_assumptions;
+    ptr_vector<expr> m_variables;
+    unsigned         m_count;
+public:
+    get_consequences_cmd(): cmd("get-consequences"), m_count(0) {}
+    virtual char const * get_usage() const { return "(<boolean-variable>*) (<variable>*)"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; }
+    virtual unsigned get_arity() const { return 2; }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; }
+    virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { 
+        if (m_count == 0) {
+            m_assumptions.append(num, tlist);
+            ++m_count;
+        }
+        else {
+            m_variables.append(num, tlist);
+        }
+    }
+    virtual void failure_cleanup(cmd_context & ctx) {}
+    virtual void execute(cmd_context & ctx) {
+        ast_manager& m = ctx.m();
+        expr_ref_vector assumptions(m), variables(m), consequences(m);
+        assumptions.append(m_assumptions.size(), m_assumptions.c_ptr());
+        variables.append(m_variables.size(), m_variables.c_ptr());
+        ctx.get_consequences(assumptions, variables, consequences);
+        ctx.regular_stream() << consequences << "\n";
+    }
+    virtual void prepare(cmd_context & ctx) { reset(ctx); }
+
+    virtual void reset(cmd_context& ctx) {
+        m_assumptions.reset(); m_variables.reset(); m_count = 0;
+    }
+    virtual void finalize(cmd_context & ctx) {}
+};
+
 // provides "help" for builtin cmds
 class builtin_cmd : public cmd {
     char const * m_usage;
@@ -776,6 +812,7 @@ void install_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(get_option_cmd));
     ctx.insert(alloc(get_info_cmd));
     ctx.insert(alloc(set_info_cmd));
+    ctx.insert(alloc(get_consequences_cmd));
     ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
     ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));
     ctx.insert(alloc(builtin_cmd, "push", "<number>?", "push 1 (or <number>) scopes."));

src/cmd_context/cmd_context.cpp

@@ -1505,6 +1505,31 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
 }
 
+void cmd_context::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector & conseq) {
+    unsigned timeout = m_params.m_timeout;
+    unsigned rlimit  = m_params.m_rlimit;
+    lbool r;
+    m_check_sat_result = m_solver.get(); // solver itself stores the result.
+    m_solver->set_progress_callback(this);
+    cancel_eh<reslimit> eh(m().limit());
+    scoped_ctrl_c ctrlc(eh);
+    scoped_timer timer(timeout, &eh);
+    scoped_rlimit _rlimit(m().limit(), rlimit);
+    try {
+        r = m_solver->get_consequences(assumptions, vars, conseq);
+    }
+    catch (z3_error & ex) {
+        throw ex;
+    }
+    catch (z3_exception & ex) {
+        m_solver->set_reason_unknown(ex.msg());
+        r = l_undef;
+    }
+    m_solver->set_status(r);
+    display_sat_result(r);
+}
+
+
 void cmd_context::reset_assertions() {
     if (!m_global_decls) {
         reset(false);

src/cmd_context/cmd_context.h

@@ -392,6 +392,7 @@ public:
     void push(unsigned n);
     void pop(unsigned n);
     void check_sat(unsigned num_assumptions, expr * const * assumptions);
+    void get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector & conseq);
     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);