adding trail/levels

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

src/api/api_solver.cpp

@@ -386,7 +386,7 @@ extern "C" {
         init_solver(c, s);
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
-        expr_ref_vector fmls = to_solver_ref(s)->get_units(mk_c(c)->m());
+        expr_ref_vector fmls = to_solver_ref(s)->get_units();
         for (expr* f : fmls) {
             v->m_ast_vector.push_back(f);
         }
@@ -401,7 +401,7 @@ extern "C" {
         init_solver(c, s);
         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
-        expr_ref_vector fmls = to_solver_ref(s)->get_non_units(mk_c(c)->m());
+        expr_ref_vector fmls = to_solver_ref(s)->get_non_units();
         for (expr* f : fmls) {
             v->m_ast_vector.push_back(f);
         }
@@ -409,6 +409,40 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, unsigned sz, Z3_ast literals[], unsigned levels[]) {
+        Z3_TRY;
+        LOG_Z3_solver_get_levels(c, s, sz, literals, levels);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        ptr_vector<expr> _vars;
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* e = to_expr(literals[i]);
+            mk_c(c)->m().is_not(e, e);
+            _vars.push_back(e);
+        }
+        unsigned_vector _levels(sz);
+        to_solver_ref(s)->get_levels(_vars, _levels);
+        for (unsigned i = 0; i < sz; ++i) {
+            levels[i] = _levels[i];
+        }
+        Z3_CATCH;
+    }
+
+    Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s) {
+        Z3_TRY;
+        LOG_Z3_solver_get_trail(c, s);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector trail = to_solver_ref(s)->get_trail();
+        for (expr* f : trail) {
+            v->m_ast_vector.push_back(f);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {

src/api/z3_api.h

@@ -6213,6 +6213,13 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
 
+    /**
+       \brief Return the trail modulo model conversion, in order of decision level
+       The decision level can be retrieved using \c Z3_solver_get_level based on the trail.
+
+       def_API('Z3_solver_get_trail', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
+    */
+    Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s);
 
     /**
        \brief Return the set of non units in the solver state.
@@ -6221,6 +6228,15 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s);
 
+    /**
+       \brief retrieve the decision depth of Boolean literals (variables or their negations).
+       Assumes a check-sat call and no other calls (to extract models) have been invoked.
+       
+       def_API('Z3_solver_get_levels', VOID, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _in_array(2, UINT)))
+    */
+    void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, unsigned sz, Z3_ast literals[], unsigned levels[]);
+
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 

src/muz/spacer/spacer_iuc_solver.h

@@ -122,6 +122,8 @@ public:
     void assert_expr_core(expr *t) override  { m_solver.assert_expr(t); }
     void assert_expr_core2(expr *t, expr *a) override   { NOT_IMPLEMENTED_YET(); }
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
+    expr_ref_vector get_trail() { return m_solver.get_trail(); }
 
     void push() override;
     void pop(unsigned n) override;

src/opt/opt_solver.cpp

@@ -208,6 +208,9 @@ namespace opt {
         return m_context.preferred_sat(asms, cores);
     }
 
+    void opt_solver::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
+        return m_context.get_levels(vars, depth);
+    }
 
 
     /**

src/opt/opt_solver.h

@@ -108,6 +108,8 @@ namespace opt {
         ast_manager& get_manager() const override { return m; }
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
         lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override;
+        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
+        expr_ref_vector get_trail() override { return m_context.get_trail(); }
         expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
 
         void set_logic(symbol const& logic);

src/sat/sat_solver.h

@@ -300,6 +300,7 @@ namespace sat {
         unsigned lvl(bool_var v) const { return m_level[v]; }
         unsigned lvl(literal l) const { return m_level[l.var()]; }
         unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
+        unsigned trail_size() const { return m_trail.size(); }
         literal  trail_literal(unsigned i) const { return m_trail[i]; }
         literal  scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
         void assign(literal l, justification j) {

src/sat/sat_solver/inc_sat_solver.cpp

@@ -318,6 +318,29 @@ public:
         r.reset();
         r.append(m_core.size(), m_core.c_ptr());
     }
+
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        unsigned sz = vars.size();
+        depth.resize(sz);
+        for (unsigned i = 0; i < sz; ++i) {
+            auto bv = m_map.to_bool_var(vars[i]);
+            depth = bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv);
+        }
+    }
+
+    expr_ref_vector get_trail() override {
+        expr_ref_vector result(m);
+        unsigned sz = m_solver.trail_size();
+        expr_ref_vector lit2expr(m);
+        lit2expr.resize(m_solver.num_vars() * 2);
+        m_map.mk_inv(lit2expr);
+        for (unsigned i = 0; i < sz; ++i) {
+            sat::literal lit = m_solver.trail_literal(i);
+            result.push_back(lit2expr[lit.index()].get());
+        }
+        return result;
+    }
+
     proof * get_proof() override {
         UNREACHABLE();
         return nullptr;

src/smt/smt_context.cpp

@@ -4423,6 +4423,22 @@ namespace smt {
             m = const_cast<model*>(m_model.get());
     }
 
+    void context::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
+        unsigned sz = vars.size(); 
+        depth.resize(sz);
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* v = vars[i];
+            bool_var bv = m_expr2bool_var.get(v->get_id(), null_bool_var);
+            depth[i] = bv == null_bool_var ? UINT_MAX : get_assign_level(bv);            
+        }
+    }
+
+    expr_ref_vector context::get_trail() {        
+        expr_ref_vector result(get_manager());
+        get_assignments(result);
+        return result;
+    }
+
     void context::get_proto_model(proto_model_ref & m) const {
         m = const_cast<proto_model*>(m_proto_model.get());
     }

src/smt/smt_context.h

@@ -1575,6 +1575,10 @@ namespace smt {
             return m_unsat_core.get(idx);
         }
 
+        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth);
+
+        expr_ref_vector get_trail();
+
         void get_model(model_ref & m) const;
 
         bool update_model(bool refinalize);

src/smt/smt_internalizer.cpp

@@ -196,7 +196,7 @@ namespace smt {
         TRACE("incompleteness_bug", tout << "[internalize-assertion]: #" << n->get_id() << "\n";);
         flet<unsigned> l(m_generation, generation);
         m_stats.m_max_generation = std::max(m_generation, m_stats.m_max_generation);
-        if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
+        if (::get_depth(n) > DEEP_EXPR_THRESHOLD) {
             // if the expression is deep, then execute topological sort to avoid
             // stack overflow.
             // a caveat is that theory internalizers do rely on recursive descent so

src/smt/smt_kernel.cpp

@@ -147,6 +147,14 @@ namespace smt {
             return m_kernel.get_unsat_core_expr(idx);
         }
 
+        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
+            m_kernel.get_levels(vars, depth);
+        }
+
+        expr_ref_vector get_trail() {
+            return m_kernel.get_trail();
+        }
+        
         failure last_failure() const {
             return m_kernel.get_last_search_failure();
         }
@@ -396,4 +404,13 @@ namespace smt {
         return m_imp->m_kernel;
     }
 
+    void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
+        m_imp->get_levels(vars, depth);
+    }
+
+    expr_ref_vector kernel::get_trail() {
+        return m_imp->get_trail();
+    }
+
+
 };

src/smt/smt_kernel.h

@@ -219,6 +219,16 @@ namespace smt {
         */
         expr* next_decision();
 
+        /**
+           \brief retrieve depth of variables from decision stack.
+        */
+        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth);
+
+        /**
+           \brief retrieve trail of assignment stack.
+        */
+        expr_ref_vector get_trail();
+
         /**
            \brief (For debubbing purposes) Prints the state of the kernel
         */

src/smt/smt_solver.cpp

@@ -195,6 +195,14 @@ namespace smt {
             return m_context.check(cube, clauses);
         }
 
+        void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+            m_context.get_levels(vars, depth);
+        }
+
+        expr_ref_vector get_trail() override {
+            return m_context.get_trail();
+        }
+
         struct scoped_minimize_core {
             smt_solver& s;
             expr_ref_vector m_assumptions;

src/solver/combined_solver.cpp

@@ -314,6 +314,20 @@ public:
             m_solver2->get_model(m);
     }
 
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        if (m_use_solver1_results)
+            m_solver1->get_levels(vars, depth);
+        else
+            m_solver2->get_levels(vars, depth);
+    }
+
+    expr_ref_vector get_trail() override {
+        if (m_use_solver1_results)
+            return m_solver1->get_trail();
+        else
+            return m_solver2->get_trail();
+    }
+
     proof * get_proof() override {
         if (m_use_solver1_results)
             return m_solver1->get_proof();

src/solver/solver.cpp

@@ -251,7 +251,8 @@ void solver::updt_params(params_ref const & p) {
 }
 
 
-expr_ref_vector solver::get_units(ast_manager& m) {
+expr_ref_vector solver::get_units() {
+    ast_manager& m = get_manager();
     expr_ref_vector fmls(m), result(m), tmp(m);
     get_assertions(fmls);
     obj_map<expr, bool> units;
@@ -284,7 +285,8 @@ expr_ref_vector solver::get_units(ast_manager& m) {
 }
 
 
-expr_ref_vector solver::get_non_units(ast_manager& m) {
+expr_ref_vector solver::get_non_units() {
+    ast_manager& m = get_manager();
     expr_ref_vector result(m), fmls(m);
     get_assertions(fmls);
     family_id bfid = m.get_basic_family_id();
@@ -320,6 +322,7 @@ expr_ref_vector solver::get_non_units(ast_manager& m) {
     return result;
 }
 
+
 lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     lbool r = l_undef;
     try {

src/solver/solver.h

@@ -243,9 +243,13 @@ public:
     /**
        \brief extract units from solver.
     */
-    expr_ref_vector get_units(ast_manager& m);
+    expr_ref_vector get_units();
 
-    expr_ref_vector get_non_units(ast_manager& m);
+    expr_ref_vector get_non_units();
+
+    virtual expr_ref_vector get_trail() = 0; // { return expr_ref_vector(get_manager()); }
+    
+    virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;
 
     class scoped_push {
         solver& s;

src/solver/solver_pool.cpp

@@ -119,6 +119,14 @@ public:
         }
     }
 
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        m_base->get_levels(vars, depth);
+    }
+
+    expr_ref_vector get_trail() override {
+        return m_base->get_trail();
+    }
+
     lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
         SASSERT(!m_pushed || get_scope_level() > 0);
         m_proof.reset();

src/solver/tactic2solver.cpp

@@ -85,6 +85,14 @@ public:
 
     model_converter_ref get_model_converter() const override { return m_mc; }
 
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        throw default_exception("cannot retrieve depth from solvers created using tactics");
+    }
+
+    expr_ref_vector get_trail() override {
+        throw default_exception("cannot retrieve trail from solvers created using tactcis");
+    }
+
 };
 
 ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }

src/tactic/fd_solver/bounded_int2bv_solver.cpp

@@ -155,6 +155,12 @@ public:
             if (mc) (*mc)(mdl);
         }
     }
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        m_solver->get_levels(vars, depth);
+    }
+    expr_ref_vector get_trail() override {
+        return m_solver->get_trail();
+    }
     model_converter* external_model_converter() const {
         return concat(mc0(), local_model_converter());
     }

src/tactic/fd_solver/enum2bv_solver.cpp

@@ -178,7 +178,13 @@ public:
         return r;
     }
 
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        m_solver->get_levels(vars, depth);
+    }
 
+    expr_ref_vector get_trail() override {
+        return m_solver->get_trail();
+    }
 
     unsigned get_num_assertions() const override {
         return m_solver->get_num_assertions();

src/tactic/fd_solver/pb2bv_solver.cpp

@@ -96,6 +96,13 @@ public:
             if (mc) (*mc)(mdl);
         }
     } 
+    void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
+        m_solver->get_levels(vars, depth);
+    }
+
+    expr_ref_vector get_trail() override {
+        return m_solver->get_trail();
+    }
 
     model_converter* external_model_converter() const{
         return concat(mc0(), local_model_converter());