working on binary drat format

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

src/api/api_solver.cpp

@@ -409,14 +409,18 @@ 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[]) {
+    void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]) {
         Z3_TRY;
-        LOG_Z3_solver_get_levels(c, s, sz, literals, levels);
+        LOG_Z3_solver_get_levels(c, s, literals, sz, levels);
         RESET_ERROR_CODE();
         init_solver(c, s);
+        if (sz != Z3_ast_vector_size(c, literals)) {
+            SET_ERROR_CODE(Z3_IOB, nullptr);
+            return;
+        }
         ptr_vector<expr> _vars;
         for (unsigned i = 0; i < sz; ++i) {
-            expr* e = to_expr(literals[i]);
+            expr* e = to_expr(Z3_ast_vector_get(c, literals, i));
             mk_c(c)->m().is_not(e, e);
             _vars.push_back(e);
         }

src/api/c++/z3++.h

@@ -2233,6 +2233,17 @@ namespace z3 {
         expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
+        expr_vector trail() const { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
+        expr_vector trail(array<unsigned>& levels) const { 
+            Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); 
+            check_error(); 
+            expr_vector result(ctx(), r);
+            unsigned sz = result.size();
+            levels = array<unsigned>(sz); 
+            Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.c_ptr());
+            check_error(); 
+            return result; 
+        }
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s);
 

src/api/python/z3/z3.py

@@ -6727,6 +6727,19 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
 
+    def trail_levels(self):
+        """Return trail and decision levels of the solver state after a check() call. 
+        """
+        trail = self.trail()
+        levels = (ctypes.c_uint * len(trail))
+        Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
+        return trail, levels
+
+    def trail(self):
+        """Return trail of the solver state after a check() call. 
+        """
+        return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
+
     def statistics(self):
         """Return statistics for the last `check()`.
 

src/api/z3_api.h

@@ -6232,9 +6232,9 @@ extern "C" {
        \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)))
+       def_API('Z3_solver_get_levels', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT), _in_array(3, UINT)))
     */
-    void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, unsigned sz, Z3_ast literals[], unsigned levels[]);
+    void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz,  unsigned levels[]);
 
 
     /**

src/sat/sat_config.cpp

@@ -165,6 +165,7 @@ namespace sat {
         m_drat_check_sat  = p.drat_check_sat();
         m_drat_file       = p.drat_file();
         m_drat            = (m_drat_check_unsat || m_drat_file != symbol("") || m_drat_check_sat) && p.threads() == 1;
+        m_drat_binary     = p.drat_binary();
         m_dyn_sub_res     = p.dyn_sub_res();
 
         // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.

src/sat/sat_config.h

@@ -156,6 +156,7 @@ namespace sat {
         bool               m_core_minimize;
         bool               m_core_minimize_partial;
         bool               m_drat;
+        bool               m_drat_binary;
         symbol             m_drat_file;
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;

src/sat/sat_drat.cpp

@@ -27,18 +27,24 @@ namespace sat {
     drat::drat(solver& s):
         s(s),
         m_out(nullptr),
+        m_bout(nullptr),
         m_inconsistent(false),
         m_check_unsat(false),
         m_check_sat(false),
         m_check(false)
     {
         if (s.m_config.m_drat && s.m_config.m_drat_file != symbol()) {
-            m_out = alloc(std::ofstream, s.m_config.m_drat_file.str().c_str());
+            auto mode = s.m_config.m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
+            m_out = alloc(std::ofstream, s.m_config.m_drat_file.str().c_str(), mode);
+            if (s.m_config.m_drat_binary) {
+                std::swap(m_out, m_bout);
+            }
         }
     }
 
     drat::~drat() {
         dealloc(m_out);
+        dealloc(m_bout);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
             if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
@@ -74,6 +80,33 @@ namespace sat {
         (*m_out) << "0\n";
     }
 
+    void drat::bdump(unsigned n, literal const* c, status st) {
+        unsigned char ch = 0;
+        switch (st) {
+        case status::asserted: UNREACHABLE(); return;
+        case status::external: UNREACHABLE(); return; // requires extension to drat format.
+        case status::learned: ch = 'a'; break;
+        case status::deleted: ch = 'd'; break;
+        default: UNREACHABLE(); break;
+        }
+        (*m_bout) << ch;
+
+        for (unsigned i = 0; i < n; ++i) {
+            literal lit = c[i];
+            unsigned v = 2 * lit.var() + (lit.sign() ? 1 : 0);
+            do {
+                ch = static_cast<unsigned char>(v & ((1 << 7) - 1));
+                v >>= 7;
+                if (v) ch |= (1 << 7);
+                //std::cout << std::hex << ((unsigned char)ch) << std::dec << " ";
+                (*m_bout) << ch;
+            }
+            while (v);
+        }
+        ch = 0;
+        (*m_bout) << 0;
+    }
+
     bool drat::is_cleaned(clause& c) const {
         literal last = null_literal;
         unsigned n = c.size();
@@ -513,6 +546,7 @@ namespace sat {
 
     void drat::add() {
         if (m_out) (*m_out) << "0\n";
+        if (m_bout) bdump(0, nullptr, learned);
         if (m_check_unsat) {
             SASSERT(m_inconsistent);
         }
@@ -521,6 +555,7 @@ namespace sat {
         declare(l);
         status st = get_status(learned);
         if (m_out) dump(1, &l, st);
+        if (m_bout) bdump(1, &l, st);
         if (m_check) append(l, st);
     }
     void drat::add(literal l1, literal l2, bool learned) {
@@ -529,6 +564,7 @@ namespace sat {
         literal ls[2] = {l1, l2};
         status st = get_status(learned);
         if (m_out) dump(2, ls, st);
+        if (m_bout) bdump(2, ls, st);
         if (m_check) append(l1, l2, st);
     }
     void drat::add(clause& c, bool learned) {
@@ -536,6 +572,7 @@ namespace sat {
         for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
         status st = get_status(learned);
         if (m_out) dump(c.size(), c.begin(), st);
+        if (m_bout) bdump(c.size(), c.begin(), st);
         if (m_check_unsat) append(c, get_status(learned));
     }
     void drat::add(literal_vector const& lits, svector<premise> const& premises) {
@@ -554,6 +591,7 @@ namespace sat {
     void drat::add(literal_vector const& c) {
         for (unsigned i = 0; i < c.size(); ++i) declare(c[i]);
         if (m_out) dump(c.size(), c.begin(), status::learned);
+        if (m_bout) bdump(c.size(), c.begin(), status::learned);
         if (m_check) {
             switch (c.size()) {
             case 0: add(); break;
@@ -570,11 +608,13 @@ namespace sat {
 
     void drat::del(literal l) {
         if (m_out) dump(1, &l, status::deleted);
+        if (m_bout) bdump(1, &l, status::deleted);
         if (m_check_unsat) append(l, status::deleted);
     }
     void drat::del(literal l1, literal l2) {
         literal ls[2] = {l1, l2};
         if (m_out) dump(2, ls, status::deleted);
+        if (m_bout) bdump(2, ls, status::deleted);
         if (m_check) 
             append(l1, l2, status::deleted);
     }
@@ -593,17 +633,15 @@ namespace sat {
 #endif
 
         TRACE("sat", tout << "del: " << c << "\n";);
-        if (m_out) {
+        if (m_out) dump(c.size(), c.begin(), status::deleted);
-            dump(c.size(), c.begin(), status::deleted);
+        if (m_bout) bdump(c.size(), c.begin(), status::deleted);
-        }
         if (m_check) {
             clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); 
             append(*c1, status::deleted);
         }
     }
     
-    void drat::check_model(model const& m) {
+    void drat::check_model(model const& m) {        
-        std::cout << "check model on " << m_proof.size() << "\n";
     }
 
 }

src/sat/sat_drat.h

@@ -46,6 +46,7 @@ namespace sat {
         typedef svector<unsigned> watch;
         solver& s;
         std::ostream*           m_out;
+        std::ostream*           m_bout;
         ptr_vector<clause>      m_proof;
         svector<status>         m_status;
         literal_vector          m_units;
@@ -55,6 +56,7 @@ namespace sat {
         bool                    m_check_unsat, m_check_sat, m_check;
 
         void dump(unsigned n, literal const* c, status st);
+        void bdump(unsigned n, literal const* c, status st);
         void append(literal l, status st);
         void append(literal l1, literal l2, status st);
         void append(clause& c, status st);

src/sat/sat_params.pyg

@@ -39,6 +39,7 @@ def_module_params('sat',
                           ('threads', UINT, 1, 'number of parallel threads to use'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
+                          ('drat.binary', BOOL, False, 'use Binary DRAT output format'),
                           ('drat.check_unsat', BOOL, False, 'build up internal proof and check'),
                           ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
                           ('cardinality.solver', BOOL, True, 'use cardinality solver'),

src/sat/sat_solver.cpp

@@ -337,7 +337,6 @@ namespace sat {
         
         switch (num_lits) {
         case 0:
-            if (m_config.m_drat) m_drat.add();
             set_conflict(justification());
             return nullptr;
         case 1:
@@ -2290,6 +2289,7 @@ namespace sat {
         unsigned new_sz = j;
         switch (new_sz) {
         case 0:
+            if (m_config.m_drat) m_drat.add();
             set_conflict(justification());
             return false;
         case 1:

src/shell/dimacs_frontend.cpp

@@ -248,7 +248,11 @@ unsigned read_dimacs(char const * file_name) {
     
     lbool r;
     vector<sat::literal_vector> tracking_clauses;
-    sat::solver solver2(p, limit);
+    params_ref p2;
+    p2.copy(p);
+    p2.set_sym("drat.file", symbol::null);
+    
+    sat::solver solver2(p2, limit);
     if (p.get_bool("dimacs.core", false)) {
         g_solver = &solver2;        
         sat::literal_vector assumptions;