fixes to cuts

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

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -32,7 +32,7 @@ public:
     ~ackermannize_bv_tactic() override { }
 
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
-        tactic_report report("ackermannize", *g);
+        tactic_report report("ackermannize_bv", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
         TRACE("ackermannize", g->display(tout << "in\n"););

src/api/api_goal.cpp

@@ -202,7 +202,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
             RETURN_Z3(nullptr);
         }
-        to_goal_ref(g)->display_dimacs(buffer);
+        to_goal_ref(g)->display_dimacs(buffer, true);
         // Hack for removing the trailing '\n'
         std::string result = buffer.str();
         SASSERT(result.size() > 0);

src/api/api_solver.cpp

@@ -695,13 +695,13 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s) {
+    Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names) {
         Z3_TRY;
         LOG_Z3_solver_to_string(c, s);
         RESET_ERROR_CODE();
         init_solver(c, s);
         std::ostringstream buffer;
-        to_solver_ref(s)->display_dimacs(buffer);
+        to_solver_ref(s)->display_dimacs(buffer, include_names);
         return mk_c(c)->mk_external_string(buffer.str());
         Z3_CATCH_RETURN("");
     }

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

@@ -2422,7 +2422,7 @@ namespace z3 {
                                    fml));
         }
 
-        std::string dimacs() const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver)); }
+        std::string dimacs(bool include_names = true) const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
 
         param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
 

src/api/python/z3/z3.py

@@ -6907,9 +6907,9 @@ class Solver(Z3PPObject):
         """
         return Z3_solver_to_string(self.ctx.ref(), self.solver)
 
-    def dimacs(self):
+    def dimacs(self, include_names=True):
         """Return a textual representation of the solver in DIMACS format."""
-        return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver)
+        return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
 
     def to_smt2(self):
         """return SMTLIB2 formatted benchmark for solver's assertions"""

src/api/z3_api.h

@@ -6633,9 +6633,9 @@ extern "C" {
        \brief Convert a solver into a DIMACS formatted string.
        \sa Z3_goal_to_diamcs_string for requirements.
 
-       def_API('Z3_solver_to_dimacs_string', STRING, (_in(CONTEXT), _in(SOLVER)))
+       def_API('Z3_solver_to_dimacs_string', STRING, (_in(CONTEXT), _in(SOLVER), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s);
+    Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names);
 
     /*@}*/
 

src/ast/display_dimacs.cpp

@@ -20,7 +20,7 @@ Revision History:
 #include "ast.h"
 #include "display_dimacs.h"
 
-std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
+std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) {
     ast_manager& m = fmls.m();
     unsigned_vector expr2var;
     ptr_vector<expr> exprs;
@@ -113,7 +113,7 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
         }
         out << "0\n";
     }
-    if (!is_from_dimacs) {
+    if (include_names && !is_from_dimacs) {
         for (expr* e : exprs) {
             if (e && is_app(e)) {
                 symbol const& n = to_app(e)->get_decl()->get_name();

src/ast/display_dimacs.h

@@ -21,6 +21,6 @@ Revision History:
 
 #include "ast.h"
 
-std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls);
+std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names);
 
 #endif /* DISPLAY_DIMACS_H__ */

src/math/subpaving/tactic/expr2subpaving.cpp

@@ -147,19 +147,20 @@ struct expr2subpaving::imp {
 
     // Put t as a^k.
     void as_power(expr * t, expr * & a, unsigned & k) {
-        if (!m_autil.is_power(t)) {
+        expr* p = nullptr;
+        if (!m_autil.is_power(t, a, p)) {
             a = t;
             k = 1;
             return;
         }
         rational _k;
-        if (!m_autil.is_numeral(to_app(t)->get_arg(1), _k) || !_k.is_int() || !_k.is_unsigned()) {
+        if (m_autil.is_numeral(p, _k) && _k.is_unsigned() && !_k.is_zero()) {
+            k = _k.get_unsigned();
+        }
+        else {
             a = t;
             k = 1;
-            return;
         }
-        a = to_app(t)->get_arg(0);
-        k = _k.get_unsigned();
     }
 
     subpaving::var process_mul(app * t, unsigned depth, mpz & n, mpz & d) {
@@ -168,7 +169,7 @@ struct expr2subpaving::imp {
             found_non_simplified();
         rational k;
         expr * m;
-        if (m_autil.is_numeral(t->get_arg(0), k)) {
+        if (m_autil.is_numeral(t->get_arg(0), k) && !k.is_zero()) {
             if (num_args != 2)
                 found_non_simplified();
             qm().set(n, k.to_mpq().numerator());

src/sat/sat_aig_cuts.cpp

@@ -24,6 +24,7 @@ namespace sat {
     aig_cuts::aig_cuts() {
         m_cut_set1.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
         m_cut_set2.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
+        m_empty_cuts.init(m_region, m_config.m_max_cutset_size + 1, UINT_MAX);
         m_num_cut_calls = 0;
         m_num_cuts = 0;
     }
@@ -31,9 +32,9 @@ namespace sat {
     vector<cut_set> const& aig_cuts::operator()() {
         if (m_config.m_full) flush_roots();
         unsigned_vector node_ids = filter_valid_nodes();
-        TRACE("aig_simplifier", display(tout););
+        TRACE("cut_simplifier", display(tout););
         augment(node_ids);
-        TRACE("aig_simplifier", display(tout););
+        TRACE("cut_simplifier", display(tout););
         ++m_num_cut_calls;
         return m_cuts;
     }
@@ -326,29 +327,31 @@ namespace sat {
         }
         else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
             m_literals.shrink(m_literals.size() - n.size());
-            TRACE("aig_simplifier", tout << "duplicate\n";);
+            TRACE("cut_simplifier", tout << "duplicate\n";);
         }
         SASSERT(!m_aig[v].empty());
     }
 
     void aig_cuts::add_node(bool_var v, uint64_t lut, unsigned sz, bool_var const* args) {
-        TRACE("aig_simplifier", tout << v << " == " << cut::table2string(sz, lut) << " " << bool_var_vector(sz, args) << "\n";);
+        TRACE("cut_simplifier", tout << v << " == " << cut::table2string(sz, lut) << " " << bool_var_vector(sz, args) << "\n";);
         reserve(v);
         unsigned offset = m_literals.size();
         node n(lut, sz, offset);
         for (unsigned i = 0; i < sz; ++i) {
+            reserve(args[i]);
             m_literals.push_back(literal(args[i], false));
         }
         add_node(v, n);
     }
 
     void aig_cuts::add_node(literal head, bool_op op, unsigned sz, literal const* args) {
-        TRACE("aig_simplifier", tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";);
+        TRACE("cut_simplifier", tout << head << " == " << op << " " << literal_vector(sz, args) << "\n";);
         unsigned v = head.var();
         reserve(v);
         unsigned offset = m_literals.size();
         node n(head.sign(), op, sz, offset);
         m_literals.append(sz, args);
+        for (unsigned i = 0; i < sz; ++i) reserve(args[i].var());
         if (op == and_op || op == xor_op) {
             std::sort(m_literals.c_ptr() + offset, m_literals.c_ptr() + offset + sz);
         }
@@ -374,13 +377,12 @@ namespace sat {
 
     void aig_cuts::flush_roots() {
         if (m_roots.empty()) return;
-        literal_vector to_root;
+        to_root to_root;
-        for (unsigned i = 0; i < m_aig.size(); ++i) {
-            to_root.push_back(literal(i, false));
-        }
         for (unsigned i = m_roots.size(); i-- > 0; ) {
             bool_var v = m_roots[i].first;
             literal  r = m_roots[i].second;
+            reserve(v);
+            reserve(r.var());
             literal rr = to_root[r.var()];
             to_root[v] = r.sign() ? ~rr : rr;
         }
@@ -404,10 +406,10 @@ namespace sat {
             flush_roots(to_root, cs);
         }
         m_roots.reset();
-        TRACE("aig_simplifier", display(tout););
+        TRACE("cut_simplifier", display(tout););
     }
 
-    bool aig_cuts::flush_roots(bool_var var, literal_vector const& to_root, node& n) {
+    bool aig_cuts::flush_roots(bool_var var, to_root const& to_root, node& n) {
         bool changed = false;
         for (unsigned i = 0; i < n.size(); ++i) {
             literal& lit = m_literals[n.offset() + i];
@@ -426,7 +428,7 @@ namespace sat {
         return true;
     }
 
-    void aig_cuts::flush_roots(literal_vector const& to_root, cut_set& cs) {
+    void aig_cuts::flush_roots(to_root const& to_root, cut_set& cs) {
         for (unsigned j = 0; j < cs.size(); ++j) {
             for (unsigned v : cs[j]) {
                 if (to_root[v] != literal(v, false)) {
@@ -708,7 +710,7 @@ namespace sat {
                     m_clause.push_back(lit);
                 }
                 m_clause.push_back(parity ? r : ~r);
-                TRACE("aig_simplifier", tout << "validate: " << m_clause << "\n";);
+                TRACE("cut_simplifier", tout << "validate: " << m_clause << "\n";);
                 on_clause(m_clause);
             }
             return;
@@ -723,7 +725,7 @@ namespace sat {
                     m_clause.push_back(lit);
                 }
                 m_clause.push_back(0 == (n.lut() & (1ull << i)) ? ~r : r);
-                TRACE("aig_simplifier", tout << n.lut() << " " <<  m_clause << "\n";);
+                TRACE("cut_simplifier", tout << n.lut() << " " <<  m_clause << "\n";);
                 on_clause(m_clause);
             }
             return;
@@ -769,7 +771,7 @@ namespace sat {
         svector<bool>   is_var;
 
         validator(aig_cuts& t):t(t),s(p, lim) {
-            p.set_bool("aig_simplifier", false);
+            p.set_bool("cut_simplifier", false);
             s.updt_params(p);
         }
 

src/sat/sat_aig_cuts.h

@@ -102,7 +102,7 @@ namespace sat {
         vector<svector<node>> m_aig;    
         literal_vector        m_literals;
         region                m_region;
-        cut_set               m_cut_set1, m_cut_set2;
+        cut_set               m_cut_set1, m_cut_set2, m_empty_cuts;
         vector<cut_set>       m_cuts;
         unsigned_vector       m_max_cutset_size;
         unsigned_vector       m_last_touched;
@@ -117,6 +117,23 @@ namespace sat {
         uint64_t              m_luts[6];
         literal               m_lits[6];
 
+        class to_root {
+            literal_vector m_to_root;
+            void reserve(bool_var v) {
+                while (v >= m_to_root.size()) {
+                    m_to_root.push_back(literal(m_to_root.size(), false));
+                }
+            }
+        public:
+            literal operator[](bool_var v) const { 
+                return (v < m_to_root.size()) ? m_to_root[v] : literal(v, false); 
+            }
+            literal& operator[](bool_var v) { 
+                reserve(v);
+                return m_to_root[v];
+            }
+        };
+
         class lut {
             aig_cuts& a;
             node const* n;
@@ -132,7 +149,7 @@ namespace sat {
 
         bool is_touched(bool_var v, node const& n);
         bool is_touched(literal lit) const { return is_touched(lit.var()); }
-        bool is_touched(bool_var v) const { return m_last_touched[v] + m_aig.size() >= m_num_cut_calls * m_aig.size(); }
+        bool is_touched(bool_var v) const { return v < m_last_touched.size() && m_last_touched[v] + m_aig.size() >= m_num_cut_calls * m_aig.size(); }
         void reserve(unsigned v);
         bool insert_aux(unsigned v, node const& n);
         void init_cut_set(unsigned id);
@@ -153,13 +170,13 @@ namespace sat {
         void augment_lut(unsigned v,  lut const& n, cut_set& cs);        
         void augment_lut_rec(unsigned v, lut const& n, cut& a, unsigned idx, cut_set& cs);
 
-        cut_set const& lit2cuts(literal lit) const { return m_cuts[lit.var()]; }
+        cut_set const& lit2cuts(literal lit) const { return lit.var() < m_cuts.size() ? m_cuts[lit.var()] : m_empty_cuts; }
 
         bool insert_cut(unsigned v, cut const& c, cut_set& cs);
 
         void flush_roots();
-        bool flush_roots(bool_var var, literal_vector const& to_root, node& n);
+        bool flush_roots(bool_var var, to_root const& to_root, node& n);
-        void flush_roots(literal_vector const& to_root, cut_set& cs);
+        void flush_roots(to_root const& to_root, cut_set& cs);
 
         cut_val eval(node const& n, cut_eval const& env) const;
         lbool get_value(bool_var v) const;
@@ -198,7 +215,7 @@ namespace sat {
         void set_on_clause_add(on_clause_t& on_clause_add);
         void set_on_clause_del(on_clause_t& on_clause_del);
 
-        void inc_max_cutset_size(unsigned v) { m_max_cutset_size[v] += 10; touch(v); }
+        void inc_max_cutset_size(unsigned v) { m_max_cutset_size.reserve(v + 1, 0);  m_max_cutset_size[v] += 10; touch(v); }
         unsigned max_cutset_size(unsigned v) const { return v == UINT_MAX ? m_config.m_max_cutset_size : m_max_cutset_size[v]; }
 
         vector<cut_set> const & operator()();
@@ -206,7 +223,7 @@ namespace sat {
 
         void cut2def(on_clause_t& on_clause, cut const& c, literal r);
 
-        void touch(bool_var v) { m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
+        void touch(bool_var v) { m_last_touched.reserve(v + 1, false);  m_last_touched[v] = v + m_num_cut_calls * m_aig.size(); }
 
         cut_eval simulate(unsigned num_rounds);
 

src/sat/sat_xor_finder.cpp

@@ -56,6 +56,7 @@ namespace sat {
         SASSERT(c.size() > 2);
         unsigned filter = get_clause_filter(c);
         s.init_visited();
+        TRACE("sat_xor", tout << c << "\n";);
         bool parity = false;
         unsigned mask = 0, i = 0;        
         for (literal l : c) {
@@ -110,6 +111,7 @@ namespace sat {
             s.set_external(l.var());
         }
         if (parity == (lits.size() % 2 == 0)) lits[0].neg();
+        TRACE("sat_xor", tout << parity << ": " << lits << "\n";);
         m_on_xor(lits);
     }
 
@@ -129,6 +131,7 @@ namespace sat {
                 m_missing.push_back(i);
             }
         }
+        TRACE("sat_xor", tout << l1 << " " << l2 << "\n";);
         return update_combinations(c, parity, mask);
     }
 
@@ -136,7 +139,7 @@ namespace sat {
         bool parity2 = false;
         for (literal l : c2) {            
             if (!s.is_visited(l.var())) return false;
-            parity2 ^= l.sign();
+            parity2 ^= !l.sign();
         }
         if (c2.size() == c.size() && parity2 != parity) {
             return false;
@@ -145,6 +148,7 @@ namespace sat {
             m_clauses_to_remove.push_back(&c2);
             c2.mark_used();
         }
+        TRACE("sat_xor", tout << c2 << "\n";);
         // insert missing
         unsigned mask = 0;
         m_missing.reset();
@@ -183,6 +187,7 @@ namespace sat {
         // return true if xor clause is covered.
         unsigned sz = c.size();
         for (unsigned i = 0; i < (1ul << sz); ++i) {     
+            TRACE("sat_xor", tout << i << ": " << parity << " " << m_parity[sz][i] << " " << get_combination(i) << "\n";);
             if (parity == m_parity[sz][i] && !get_combination(i)) {
                 return false;
             }

src/solver/solver.cpp

@@ -58,10 +58,10 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum
     return out;
 }
 
-std::ostream& solver::display_dimacs(std::ostream& out) const {
+std::ostream& solver::display_dimacs(std::ostream& out, bool include_names) const {
     expr_ref_vector fmls(get_manager());
     get_assertions(fmls);    
-    return ::display_dimacs(out, fmls);
+    return ::display_dimacs(out, fmls, include_names);
 }
 
 void solver::get_assertions(expr_ref_vector& fmls) const {

src/solver/solver.h

@@ -234,7 +234,7 @@ public:
     /**
        \brief Display the content of this solver in DIMACS format
     */
-    std::ostream& display_dimacs(std::ostream & out) const;
+    std::ostream& display_dimacs(std::ostream & out, bool include_names = true) const;
 
     /**
        \brief expose model converter when solver produces partially reduced set of assertions.

src/tactic/bv/bit_blaster_tactic.cpp

@@ -57,7 +57,7 @@ class bit_blaster_tactic : public tactic {
             if (proofs_enabled && m_blast_quant)
                 throw tactic_exception("quantified variable blasting does not support proof generation");
             
-            tactic_report report("bit-blaster", *g);
+            tactic_report report("bit-blast", *g);
             
             TRACE("before_bit_blaster", g->display(tout););
             m_num_steps = 0;

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -184,7 +184,7 @@ public:
         m_mc = nullptr;
         unsigned num_reduced = 0;
         {
-            tactic_report report("bv-size-reduction", g);
+            tactic_report report("reduce-bv-size", g);
             collect_bounds(g);
             
             // create substitution

src/tactic/goal.cpp

@@ -431,10 +431,10 @@ void goal::display_ll(std::ostream & out) const {
 /**
    \brief Assumes that the formula is already in CNF.
 */
-void goal::display_dimacs(std::ostream & out) const {
+void goal::display_dimacs(std::ostream & out, bool include_names) const {
     expr_ref_vector fmls(m());
     get_formulas(fmls);
-    ::display_dimacs(out, fmls);
+    ::display_dimacs(out, fmls, include_names);
 }
 
 unsigned goal::num_exprs() const {

src/tactic/goal.h

@@ -137,7 +137,7 @@ public:
     void display(std::ostream & out) const;
     void display_ll(std::ostream & out) const;
     void display_as_and(std::ostream & out) const;
-    void display_dimacs(std::ostream & out) const;
+    void display_dimacs(std::ostream & out, bool include_names) const;
     void display_with_dependencies(ast_printer & prn, std::ostream & out) const;
     void display_with_dependencies(ast_printer_context & ctx) const;
     void display_with_dependencies(std::ostream & out) const;