working on named assertions support

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/api/api_parsers.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include"cmd_context.h"
 #include"smt2parser.h"
 #include"smtparser.h"
+#include"solver_na2as.h"
 
 extern "C" {
 
@@ -251,20 +252,19 @@ extern "C" {
     // ---------------
     // Support for SMTLIB2
 
-    class z3_context_solver : public solver {
+    class z3_context_solver : public solver_na2as {
         api::context & m_ctx;
         smt::kernel & ctx() const { return m_ctx.get_smt_kernel(); }
     public:
         virtual ~z3_context_solver() {}
         z3_context_solver(api::context& c) : m_ctx(c) {}
-        virtual void init(ast_manager & m, symbol const & logic) {}
+        virtual void init_core(ast_manager & m, symbol const & logic) {}
         virtual void collect_statistics(statistics & st) const {}
-        virtual void reset() { ctx().reset(); }
+        virtual void reset_core() { ctx().reset(); }
         virtual void assert_expr(expr * t) { ctx().assert_expr(t); }
-        virtual void push() { ctx().push(); }
+        virtual void push_core() { ctx().push(); }
-        virtual void pop(unsigned n) { ctx().pop(n); }
+        virtual void pop_core(unsigned n) { ctx().pop(n); }
-        virtual unsigned get_scope_level() const { return ctx().get_scope_level(); }
+        virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
             return ctx().check(num_assumptions, assumptions);
         }
         virtual void get_unsat_core(ptr_vector<expr> & r) {

src/smt/ni_solver.cpp

@@ -18,8 +18,9 @@ Notes:
 #include"ni_solver.h"
 #include"smt_kernel.h"
 #include"cmd_context.h"
+#include"solver_na2as.h"
 
-class ni_smt_solver : public solver {
+class ni_smt_solver : public solver_na2as {
 protected:
     cmd_context &       m_cmd_ctx;
     smt::kernel *       m_context;
@@ -32,7 +33,7 @@ public:
             dealloc(m_context);
     }
 
-    virtual void init(ast_manager & m, symbol const & logic) {
+    virtual void init_core(ast_manager & m, symbol const & logic) {
         // do nothing
     }
 
@@ -45,7 +46,7 @@ public:
         }
     }
 
-    virtual void reset() {
+    virtual void reset_core() {
         if (m_context != 0) {
             #pragma omp critical (ni_solver) 
             {
@@ -59,18 +60,14 @@ public:
         // do nothing
     }
 
-    virtual void push() {
+    virtual void push_core() {
         // do nothing
     }
 
-    virtual void pop(unsigned n) {
+    virtual void pop_core(unsigned n) {
         // do nothing
     }
 
-    virtual unsigned get_scope_level() const {
-        return m_cmd_ctx.num_scopes();
-    }
-
     void assert_exprs() {
         ptr_vector<expr>::const_iterator it  = m_cmd_ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = m_cmd_ctx.end_assertions();
@@ -92,7 +89,7 @@ public:
         assert_exprs();
     }
 
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
         // erase current solver, and create a new one.
         init_solver();
 
@@ -165,15 +162,15 @@ public:
     
     virtual ~qi_smt_solver() {}
 
-    virtual void init(ast_manager & m, symbol const & logic) {
+    virtual void init_core(ast_manager & m, symbol const & logic) {
         if (m_inc_mode) {
             init_solver();
             m_inc_mode = true;
         }
     }
 
-    virtual void reset() {
+    virtual void reset_core() {
-        ni_smt_solver::reset();
+        ni_smt_solver::reset_core();
         m_inc_mode = false;
     }
 
@@ -196,31 +193,23 @@ public:
         }
     }
 
-    virtual void push() {
+    virtual void push_core() {
         switch_to_inc();
         SASSERT(m_context);
         m_context->push();
         SASSERT(m_inc_mode);
     }
 
-    virtual void pop(unsigned n) {
+    virtual void pop_core(unsigned n) {
         switch_to_inc();
         SASSERT(m_context);
         m_context->pop(n);
         SASSERT(m_inc_mode);
     }
 
-    virtual unsigned get_scope_level() const {
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-        if (!m_inc_mode)
-            return 0;
-        else
-            return m_context->get_scope_level();
-    }
-
-
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
         if (!m_inc_mode) {
-            lbool r = ni_smt_solver::check_sat(num_assumptions, assumptions);
+            lbool r = ni_smt_solver::check_sat_core(num_assumptions, assumptions);
             SASSERT(!m_inc_mode);
             return r;
         }

src/smt/smt_solver.cpp

@@ -16,14 +16,14 @@ Author:
 Notes:
 
 --*/
-#include"solver.h"
+#include"solver_na2as.h"
 #include"smt_kernel.h"
 #include"reg_decl_plugins.h"
 #include"front_end_params.h"
 
 namespace smt {
 
-    class solver : public ::solver {
+    class solver : public solver_na2as {
         front_end_params * m_params;
         smt::kernel *     m_context;
     public:
@@ -57,7 +57,7 @@ namespace smt {
             }
         }
 
-        virtual void init(ast_manager & m, symbol const & logic) {
+        virtual void init_core(ast_manager & m, symbol const & logic) {
             SASSERT(m_params);
             reset();
 #pragma omp critical (solver)
@@ -77,7 +77,7 @@ namespace smt {
             }
         }
 
-        virtual void reset() {
+        virtual void reset_core() {
             if (m_context != 0) {
 #pragma omp critical (solver)
                 {
@@ -92,24 +92,17 @@ namespace smt {
             m_context->assert_expr(t);
         }
 
-        virtual void push() {
+        virtual void push_core() {
             SASSERT(m_context);
             m_context->push();
         }
 
-        virtual void pop(unsigned n) {
+        virtual void pop_core(unsigned n) {
             SASSERT(m_context);
             m_context->pop(n);
         }
 
-        virtual unsigned get_scope_level() const {
+        virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-            if (m_context)
-                return m_context->get_scope_level();
-            else
-                return 0;
-        }
-
-        virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
             SASSERT(m_context);
             return m_context->check(num_assumptions, assumptions);
         }

src/solver/solver.h

@@ -95,6 +95,13 @@ public:
     */
     virtual void assert_expr(expr * t) = 0;
 
+    /**
+       \brief Add a new formula \c t to the assertion stack, and "tag" it with \c a.
+       The propositional varialbe \c a is used to track the use of \c t in a proof
+       of unsatisfiability.
+    */
+    virtual void assert_expr(expr * t, expr * a) = 0;
+
     /**
        \brief Create a backtracking point.
     */

src/solver/solver_na2as.cpp

@@ -0,0 +1,96 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    solver_na2as.cpp
+
+Abstract:
+
+    Solver that implements "named" assertions using assumptions (aka answer literals).
+    That is, a named assertion assert_expr(t, a) is mapped into
+          a implies t
+    and 'a' is used as an extra assumption for check_sat.
+
+Author:
+
+    Leonardo (leonardo) 2012-11-02
+
+Notes:
+
+--*/
+#include"solver_na2as.h"
+
+solver_na2as::solver_na2as() {
+    m_manager = 0;
+}
+
+solver_na2as::~solver_na2as() {
+    reset();
+}
+
+void solver_na2as::assert_expr(expr * t, expr * a) {
+    SASSERT(m_manager != 0);
+    expr * new_t = m_manager->mk_implies(a, t);
+    m_manager->inc_ref(a);
+    m_assumptions.push_back(a);
+    assert_expr(new_t);
+}
+    
+void solver_na2as::init(ast_manager & m, symbol const & logic) {
+    SASSERT(m_assumptions.empty());
+    m_manager = &m;
+    init_core(m, logic);
+}
+
+struct append_assumptions {
+    ptr_vector<expr> & m_assumptions;
+    unsigned           m_old_sz;
+    append_assumptions(ptr_vector<expr> & _m_assumptions, 
+                       unsigned num_assumptions, 
+                       expr * const * assumptions):
+        m_assumptions(_m_assumptions) {
+        m_old_sz = m_assumptions.size();
+        m_assumptions.append(num_assumptions, assumptions);
+    }
+
+    ~append_assumptions() {
+        m_assumptions.shrink(m_old_sz);
+    }
+};
+
+lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    append_assumptions app(m_assumptions, num_assumptions, assumptions);
+    return check_sat_core(num_assumptions, assumptions);
+}
+
+void solver_na2as::push() {
+    m_scopes.push_back(m_assumptions.size());
+    push_core();
+}
+
+void solver_na2as::pop(unsigned n) {
+    pop_core(n);
+    unsigned lvl = m_scopes.size();
+    SASSERT(n <= lvl);
+    unsigned new_lvl = lvl - n;
+    restore_assumptions(m_scopes[new_lvl]);
+    m_scopes.shrink(new_lvl);
+}
+
+void solver_na2as::restore_assumptions(unsigned old_sz) {
+    SASSERT(m_manager);
+    for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
+        m_manager->dec_ref(m_assumptions[i]);
+    }
+    m_assumptions.shrink(old_sz);
+}
+
+unsigned solver_na2as::get_scope_level() const {
+    return m_scopes.size();
+}
+
+void solver_na2as::reset() {
+    if (m_manager)
+        restore_assumptions(0);
+}

src/solver/solver_na2as.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    solver_na2as.h
+
+Abstract:
+
+    Solver that implements "named" assertions using assumptions (aka answer literals).
+    That is, a named assertion assert_expr(t, a) is mapped into
+          a implies t
+    and 'a' is used as an extra assumption for check_sat.
+
+Author:
+
+    Leonardo (leonardo) 2012-11-02
+
+Notes:
+
+--*/
+#ifndef _SOLVER_NA2AS_H_
+#define _SOLVER_NA2AS_H_
+
+#include"solver.h"
+
+class solver_na2as : public solver {
+    ast_manager *      m_manager;
+    ptr_vector<expr>   m_assumptions;
+    unsigned_vector    m_scopes;
+    void restore_assumptions(unsigned old_sz);
+public:
+    solver_na2as();
+    virtual ~solver_na2as();
+
+    virtual void assert_expr(expr * t, expr * a);
+    virtual void assert_expr(expr * t) = 0;
+    
+    // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual void reset();
+protected:
+    virtual void init_core(ast_manager & m, symbol const & logic) = 0;
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
+    virtual void push_core() = 0;
+    virtual void pop_core(unsigned n) = 0;
+    virtual void reset_core() = 0;
+};
+
+
+#endif

src/solver/strategic_solver.cpp

@@ -128,7 +128,7 @@ void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory
     m_logic2fct.insert(logic, fct);
 }
 
-void strategic_solver_core::init(ast_manager & m, symbol const & logic) {
+void strategic_solver_core::init_core(ast_manager & m, symbol const & logic) {
     m_manager = &m;
     m_logic   = logic;
     if (m_inc_mode) {
@@ -165,7 +165,7 @@ void strategic_solver_core::collect_statistics(statistics & st) const {
     }
 }
 
-void strategic_solver_core::reset() {
+void strategic_solver_core::reset_core() {
     m_logic    = symbol::null;
     m_inc_mode = false;
     m_check_sat_executed = false;
@@ -199,14 +199,14 @@ void strategic_solver_core::assert_expr(expr * t) {
     }
 }
 
-void strategic_solver_core::push() {
+void strategic_solver_core::push_core() {
     DEBUG_CODE(m_num_scopes++;);
     init_inc_solver();
     if (m_inc_solver)
         m_inc_solver->push();
 }
 
-void strategic_solver_core::pop(unsigned n) {
+void strategic_solver_core::pop_core(unsigned n) {
     DEBUG_CODE({
             SASSERT(n <= m_num_scopes);
             m_num_scopes -= n;
@@ -216,13 +216,6 @@ void strategic_solver_core::pop(unsigned n) {
         m_inc_solver->pop(n);
 }
 
-unsigned strategic_solver_core::get_scope_level() const {
-    if (m_inc_solver)
-        return m_inc_solver->get_scope_level();
-    else
-        return 0;
-}
-
 struct aux_timeout_eh : public event_handler {
     solver *        m_solver;
     volatile bool   m_canceled;
@@ -278,7 +271,7 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions
     return m_inc_solver->check_sat(num_assumptions, assumptions);
 }
 
-lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
     reset_results();
     m_check_sat_executed = true;
     if (num_assumptions > 0 || // assumptions were provided
@@ -427,8 +420,8 @@ void strategic_solver_core::display(std::ostream & out) const {
 strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) {
 }
 
-void strategic_solver::init(ast_manager & m, symbol const & logic) {
+void strategic_solver::init_core(ast_manager & m, symbol const & logic) {
-    strategic_solver_core::init(m, logic);
+    strategic_solver_core::init_core(m, logic);
     m_ctx = alloc(ctx, m);
 }
 
@@ -449,24 +442,24 @@ void strategic_solver::assert_expr(expr * t) {
     m_ctx->m_assertions.push_back(t);
 }
 
-void strategic_solver::push() {
+void strategic_solver::push_core() {
     SASSERT(m_ctx);
-    strategic_solver_core::push();
+    strategic_solver_core::push_core();
     m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
 }
 
-void strategic_solver::pop(unsigned n) {
+void strategic_solver::pop_core(unsigned n) {
     SASSERT(m_ctx);
     unsigned new_lvl = m_ctx->m_scopes.size() - n;
     unsigned old_sz  = m_ctx->m_scopes[new_lvl];
     m_ctx->m_assertions.shrink(old_sz);
     m_ctx->m_scopes.shrink(new_lvl);
-    strategic_solver_core::pop(n);
+    strategic_solver_core::pop_core(n);
 }
 
-void strategic_solver::reset() {
+void strategic_solver::reset_core() {
     m_ctx = 0;
-    strategic_solver_core::reset();
+    strategic_solver_core::reset_core();
 }
 
 

src/solver/strategic_solver.h

@@ -19,7 +19,7 @@ Notes:
 #ifndef _STRATEGIC_SOLVER_H_
 #define _STRATEGIC_SOLVER_H_
 
-#include"solver.h"
+#include"solver_na2as.h"
 #include"tactic.h"
 
 class progress_callback;
@@ -46,7 +46,7 @@ struct front_end_params;
    It goes back to non_incremental mode when:
        - reset is invoked.
 */
-class strategic_solver_core : public solver {
+class strategic_solver_core : public solver_na2as {
 public:
     // Behavior when the incremental solver returns unknown.
     enum inc_unknown_behavior {
@@ -123,14 +123,13 @@ public:
     
     virtual void display(std::ostream & out) const;
     
-    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void init_core(ast_manager & m, symbol const & logic);
     virtual void collect_statistics(statistics & st) const;
-    virtual void reset();
+    virtual void reset_core();
     virtual void assert_expr(expr * t);
-    virtual void push();
+    virtual void push_core();
-    virtual void pop(unsigned n);
+    virtual void pop_core(unsigned n);
-    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
     virtual void get_unsat_core(ptr_vector<expr> & r);
     virtual void get_model(model_ref & m);
     virtual proof * get_proof();
@@ -153,12 +152,12 @@ class strategic_solver : public strategic_solver_core {
 public:
     strategic_solver() {}
 
-    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void init_core(ast_manager & m, symbol const & logic);
 
     virtual void assert_expr(expr * t);
-    virtual void push();
+    virtual void push_core();
-    virtual void pop(unsigned n);
+    virtual void pop_core(unsigned n);
-    virtual void reset();
+    virtual void reset_core();
 
     virtual unsigned get_num_assertions() const;
     virtual expr * get_assertion(unsigned idx) const;

src/solver/tactic2solver.cpp

@@ -31,7 +31,7 @@ tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic):
 tactic2solver_core::~tactic2solver_core() {
 }
 
-void tactic2solver_core::init(ast_manager & m, symbol const & logic) {
+void tactic2solver_core::init_core(ast_manager & m, symbol const & logic) {
     m_ctx = alloc(ctx, m, logic);
 }
 
@@ -62,7 +62,7 @@ void tactic2solver_core::collect_param_descrs(param_descrs & r) {
     }
 }
 
-void tactic2solver_core::reset() {
+void tactic2solver_core::reset_core() {
     SASSERT(m_ctx);
     m_ctx->m_assertions.reset();
     m_ctx->m_scopes.reset();
@@ -75,13 +75,13 @@ void tactic2solver_core::assert_expr(expr * t) {
     m_ctx->m_result = 0;
 }
 
-void tactic2solver_core::push() {
+void tactic2solver_core::push_core() {
     SASSERT(m_ctx);
     m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
     m_ctx->m_result = 0;
 }
 
-void tactic2solver_core::pop(unsigned n) {
+void tactic2solver_core::pop_core(unsigned n) {
     SASSERT(m_ctx);
     unsigned new_lvl = m_ctx->m_scopes.size() - n;
     unsigned old_sz  = m_ctx->m_scopes[new_lvl];
@@ -90,12 +90,7 @@ void tactic2solver_core::pop(unsigned n) {
     m_ctx->m_result = 0;
 }
 
-unsigned tactic2solver_core::get_scope_level() const {
+lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
-    SASSERT(m_ctx);
-    return m_ctx->m_scopes.size();
-}
-
-lbool tactic2solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     SASSERT(m_ctx);
     ast_manager & m = m_ctx->m();
     params_ref p = m_params;

src/solver/tactic2solver.h

@@ -22,7 +22,7 @@ Notes:
 #ifndef _TACTIC2SOLVER_H_
 #define _TACTIC2SOLVER_H_
 
-#include"solver.h"
+#include"solver_na2as.h"
 #include"tactic.h"
 
 /**
@@ -32,7 +32,7 @@ Notes:
    option for applications trying to solve many easy queries that a
    similar to each other.
 */
-class tactic2solver_core : public solver {
+class tactic2solver_core : public solver_na2as {
     struct ctx {
         symbol                       m_logic;
         expr_ref_vector              m_assertions;
@@ -63,13 +63,13 @@ public:
     virtual void set_produce_models(bool f) { m_produce_models = f; }
     virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
 
-    virtual void init(ast_manager & m, symbol const & logic);
-    virtual void reset();
     virtual void assert_expr(expr * t);
-    virtual void push();
+
-    virtual void pop(unsigned n);
+    virtual void init_core(ast_manager & m, symbol const & logic);
-    virtual unsigned get_scope_level() const;
+    virtual void reset_core();
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+    virtual void push_core();
+    virtual void pop_core(unsigned n);
+    virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
 
     virtual void set_cancel(bool f);