add option for prettier proof printing, Issue #706

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

examples/python/mus/mss.py

@@ -73,6 +73,10 @@ class MSSSolver:
              self.varcache[i] = Not(v)
        return self.varcache[i]
 
+   # Retrieve the latest model
+   # Add formulas that are true in the model to 
+   # the current mss
+
    def update_unknown(self):
        self.model = self.s.model()
        new_unknown = set([])
@@ -83,23 +87,29 @@ class MSSSolver:
               new_unknown.add(x)
        self.unknown = new_unknown
       
-   def relax_core(self, core):
+   # Create a name, propositional atom,
-       assert(core <= self.soft_vars)
+   #  for formula 'fml' and return the name.
-       prev = BoolVal(True)
+
-       core_list = [x for x in core]
+   def add_def(self, fml):
-       self.soft_vars -= core
+       name = Bool("%s" % fml)
-       # replace x0, x1, x2, .. by
+       self.s.add(name == fml)
-       # Or(x1, x0), Or(x2, And(x1, x0)), Or(x3, And(x2, And(x1, x0))), ...
+       return name
-       for i in range(len(core_list)-1):
+
-           x = core_list[i]
+   # replace Fs := f0, f1, f2, .. by
-           y = core_list[i+1]
+   # Or(f1, f0), Or(f2, And(f1, f0)), Or(f3, And(f2, And(f1, f0))), ...
-           prevf = And(x, prev)
+
-           prev = Bool("%s" % prevf)
+   def relax_core(self, Fs):
-           self.s.add(prev == prevf)
+       assert(Fs <= self.soft_vars)
-           zf = Or(prev, y)
+       prefix = BoolVal(True)
-           z = Bool("%s" % zf)
+       self.soft_vars -= Fs
-           self.s.add(z == zf)
+       Fs = [ f for f in Fs ]
-           self.soft_vars.add(z)
+       for i in range(len(Fs)-1):
+           prefix = self.add_def(And(Fs[i], prefix))
+           self.soft_vars.add(self.add_def(Or(prefix, Fs[i+1])))
+
+   # Resolve literals from the core that 
+   # are 'explained', e.g., implied by 
+   # other literals.
 
    def resolve_core(self, core):
        new_core = set([])
@@ -111,6 +121,14 @@ class MSSSolver:
        return new_core
 
 
+   # Given a current satisfiable state
+   # Extract an MSS, and ensure that currently 
+   # encoutered cores are avoided in next iterations
+   # by weakening the set of literals that are
+   # examined in next iterations.
+   # Strengthen the solver state by enforcing that
+   # an element from the MCS is encoutered.
+
    def grow(self):
        self.mss = []
        self.mcs = []

src/api/python/z3.py

@@ -118,6 +118,8 @@ def _get_args(args):
     try:
         if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
             return args[0]
+        elif len(args) == 1 and isinstance(args[0], set):
+            return [arg for arg in args[0]]
         else:
             return args
     except:  # len is not necessarily defined when args is not a sequence (use reflection?)

src/ast/pp_params.pyg

@@ -16,4 +16,5 @@ def_module_params('pp',
                           ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
                           ('single_line', BOOL, False, 'ignore line breaks when true'),
                           ('bounded', BOOL, False, 'ignore characters exceeding max width'),
+                          ('pretty_proof', BOOL, False, 'use slower, but prettier, printer for proofs'),
                           ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))

src/cmd_context/basic_cmds.cpp

@@ -29,6 +29,7 @@ Notes:
 #include"gparams.h"
 #include"env_params.h"
 #include"well_sorted.h"
+#include"pp_params.hpp"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -161,14 +162,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
         throw cmd_exception("proof is not well sorted");
     }
     
-    // TODO: reimplement a new SMT2 pretty printer 
+    pp_params params;
-    ast_smt_pp pp(ctx.m());
+    if (params.pretty_proof()) {
-    cmd_is_declared isd(ctx);
+        ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl;
-    pp.set_is_declared(&isd);
+    }
-    pp.set_logic(ctx.get_logic());
+    else {
-    // ctx.regular_stream() << mk_pp(pr, ctx.m()) << "\n";
+        // TODO: reimplement a new SMT2 pretty printer 
-    pp.display_smt2(ctx.regular_stream(), pr);
+        ast_smt_pp pp(ctx.m());
-    ctx.regular_stream() << std::endl;
+        cmd_is_declared isd(ctx);
+        pp.set_is_declared(&isd);
+        pp.set_logic(ctx.get_logic());
+        pp.display_smt2(ctx.regular_stream(), pr);
+        ctx.regular_stream() << std::endl;
+    }
 });
 
 #define PRINT_CORE()                                            \

src/cmd_context/interpolant_cmds.cpp

@@ -28,7 +28,6 @@
 #include"mpq.h"
 #include"expr2var.h"
 #include"pp.h"
-#include"pp_params.hpp"
 #include"iz3interp.h"
 #include"iz3checker.h"
 #include"iz3profiling.h"

src/sat/sat_bceq.cpp

@@ -493,14 +493,14 @@ namespace sat {
     void bceq::operator()() {
         if (!m_solver.m_config.m_bcd) return;
         flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
-        flet<bool> _disable_min(m_solver.m_config.m_minimize_core, false);
+        flet<bool> _disable_min(m_solver.m_config.m_core_minimize, false);
         flet<bool> _disable_opt(m_solver.m_config.m_optimize_model, false);
         flet<unsigned> _bound_maxc(m_solver.m_config.m_max_conflicts, 1500);
 
         use_list     ul;        
         solver       s(m_solver.m_params, m_solver.rlimit(), 0);
         s.m_config.m_bcd            = false;
-        s.m_config.m_minimize_core  = false;
+        s.m_config.m_core_minimize  = false;
         s.m_config.m_optimize_model = false;
         s.m_config.m_max_conflicts  = 1500;
         m_use_list = &ul;

src/sat/sat_config.cpp

@@ -107,8 +107,8 @@ namespace sat {
             m_gc_increment    = p.gc_increment();
         }
         m_minimize_lemmas = p.minimize_lemmas();
-        m_minimize_core   = p.minimize_core();
+        m_core_minimize   = p.core_minimize();
-        m_minimize_core_partial   = p.minimize_core_partial();
+        m_core_minimize_partial   = p.core_minimize_partial();
         m_optimize_model  = p.optimize_model();
         m_bcd             = p.bcd();
         m_dyn_sub_res     = p.dyn_sub_res();

src/sat/sat_config.h

@@ -69,8 +69,8 @@ namespace sat {
 
         bool               m_minimize_lemmas;
         bool               m_dyn_sub_res;
-        bool               m_minimize_core;
+        bool               m_core_minimize;
-        bool               m_minimize_core_partial;
+        bool               m_core_minimize_partial;
         bool               m_optimize_model;
         bool               m_bcd;
 

src/sat/sat_mus.cpp

@@ -58,7 +58,7 @@ namespace sat {
     }
 
     lbool mus::operator()() {
-        flet<bool> _disable_min(s.m_config.m_minimize_core, false);
+        flet<bool> _disable_min(s.m_config.m_core_minimize, false);
         flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
         flet<bool> _is_active(m_is_active, true);
         IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
@@ -69,7 +69,7 @@ namespace sat {
     }
 
     lbool mus::mus1() {
-        bool minimize_partial = s.m_config.m_minimize_core_partial;
+        bool minimize_partial = s.m_config.m_core_minimize_partial;
         TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
         literal_vector& core = get_core();
         literal_vector& mus = m_mus;
@@ -96,7 +96,7 @@ namespace sat {
                 // IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";);
                 break;
             }
-            if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
+            if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
                 IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
                 set_core();
                 return l_true;
@@ -172,7 +172,7 @@ namespace sat {
 
     lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
         lbool is_sat = l_true;
-        if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
+        if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
             IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
             return l_true;
         }

src/sat/sat_params.pyg

@@ -19,8 +19,8 @@ def_module_params('sat',
                           ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
-                          ('minimize_core', BOOL, False, 'minimize computed core'),
+                          ('core.minimize', BOOL, False, 'minimize computed core'),
-                          ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
+                          ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
                           ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

src/sat/sat_solver.cpp

@@ -937,7 +937,7 @@ namespace sat {
 
 
     bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
-        flet<bool> _min1(m_config.m_minimize_core, false);
+        flet<bool> _min1(m_config.m_core_minimize, false);
         m_weight = 0;
         m_blocker.reset();
         svector<lbool> values;
@@ -2015,7 +2015,7 @@ namespace sat {
             idx--;
         }        
         reset_unmark(old_size);
-        if (m_config.m_minimize_core) {
+        if (m_config.m_core_minimize) {
             if (m_min_core_valid && m_min_core.size() < m_core.size()) {
                 IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
                 m_core.reset();

src/smt/theory_arith_eq.h

@@ -64,7 +64,7 @@ namespace smt {
                     lower(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
 
-                    TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
+                    TRACE("arith_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
                           display_var(tout, v);
                           display_var(tout, v2););
                     m_stats.m_fixed_eqs++;
@@ -175,7 +175,7 @@ namespace smt {
         timer.stop();
         ok++;
         if (ok % 100000 == 0) {
-            TRACE("propagate_cheap_eq", 
+            TRACE("arith_eq", 
                   tout << total << " " << ok << " " 
                   << static_cast<double>(ok)/static_cast<double>(total) 
                   << " " << timer.get_seconds() << "\n";
@@ -216,7 +216,7 @@ namespace smt {
     void theory_arith<Ext>::propagate_cheap_eq(unsigned rid) {
         if (!propagate_eqs())
             return;
-        TRACE("propagate_cheap_eq", tout << "checking if row " << rid << " can propagate equality.\n";
+        TRACE("arith_eq", tout << "checking if row " << rid << " can propagate equality.\n";
               display_row_info(tout, rid););
         row const & r = m_rows[rid];
         theory_var x;
@@ -258,7 +258,7 @@ namespace smt {
                 // found equality x = y
                 antecedents ante(*this);
                 collect_fixed_var_justifications(r, ante);
-                TRACE("propagate_cheap_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
+                TRACE("arith_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
                 m_stats.m_offset_eqs++;
                 propagate_eq_to_core(x, y, ante);
             }
@@ -299,7 +299,7 @@ namespace smt {
                             antecedents ante(*this);
                             collect_fixed_var_justifications(r, ante);
                             collect_fixed_var_justifications(r2, ante);
-                            TRACE("propagate_cheap_eq", tout << "propagate eq two rows:\n"; 
+                            TRACE("arith_eq", tout << "propagate eq two rows:\n"; 
                                   tout << "swapped: " << swapped << "\n";
                                   tout << "x  : v" << x << "\n";
                                   tout << "x2 : v" << x2 << "\n";
@@ -343,7 +343,7 @@ namespace smt {
                     antecedents.eqs().size(), antecedents.eqs().c_ptr(),
                     _x, _y, 
                     antecedents.num_params(), antecedents.params("eq-propagate")));
-        TRACE("propagate_eq_to_core", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
+        TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
               display_var(tout, x);
               display_var(tout, y););
         ctx.assign_eq(_x, _y, eq_justification(js));