fixes

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

src/api/api_goal.cpp

@@ -178,4 +178,18 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
+    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g) {
+        Z3_TRY;
+        LOG_Z3_goal_to_dimacs_string(c, g);
+        RESET_ERROR_CODE();
+        std::ostringstream buffer;
+        to_goal_ref(g)->display_dimacs(buffer);
+        // Hack for removing the trailing '\n'
+        std::string result = buffer.str();
+        SASSERT(result.size() > 0);
+        result.resize(result.size()-1);
+        return mk_c(c)->mk_external_string(result);
+        Z3_CATCH_RETURN("");
+    }
+
 };

src/api/api_solver.cpp

@@ -139,6 +139,10 @@ extern "C" {
             SET_ERROR_CODE(Z3_PARSER_ERROR);
             return;
         }
+
+        bool initialized = to_solver(s)->m_solver.get() != 0;
+        if (!initialized)
+            init_solver(c, s);
         ptr_vector<expr>::const_iterator it  = ctx->begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx->end_assertions();
         for (; it != end; ++it) {

src/api/dotnet/Goal.cs

@@ -208,6 +208,15 @@ namespace Microsoft.Z3
             return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Goal to DIMACS formatted string conversion.
+        /// </summary>
+        /// <returns>A string representation of the Goal.</returns>
+        public string ToDimacs()
+        {
+            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject);
+        }
+
         /// <summary>
         /// Goal to BoolExpr conversion.
         /// </summary>

src/api/python/z3/z3.py

@@ -4971,6 +4971,10 @@ class Goal(Z3PPObject):
         """Return a textual representation of the s-expression representing the goal."""
         return Z3_goal_to_string(self.ctx.ref(), self.goal)
 
+    def dimacs(self):
+        """Return a textual representation of the goal in DIMACS format."""
+        return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal)
+
     def translate(self, target):
         """Copy goal `self` to context `target`.
 
@@ -6300,7 +6304,7 @@ class Solver(Z3PPObject):
 
     def from_file(self, filename):
         """Parse assertions from a file"""
-        Z3_solver_from_file(self.ctx.ref(), self.solver)
+        Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
 
     def from_string(self, s):
         """Parse assertions from a string"""

src/api/z3_api.h

@@ -5568,6 +5568,13 @@ extern "C" {
     */
     Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g);
 
+    /**
+       \brief Convert a goal into a DIMACS formatted string.
+
+       def_API('Z3_goal_to_dimacs_string', STRING, (_in(CONTEXT), _in(GOAL)))
+    */
+    Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g);
+
     /*@}*/
 
     /** @name Tactics and Probes */

src/sat/sat_asymm_branch.cpp

@@ -57,7 +57,7 @@ namespace sat {
     };
     
     void asymm_branch::operator()(bool force) {
-        if (!m_asymm_branch)
+        if (!m_asymm_branch && !m_asymm_branch_all)
             return;
         s.propagate(false); // must propagate, since it uses s.push()
         if (s.m_inconsistent)
@@ -92,7 +92,6 @@ namespace sat {
                 }
                 s.checkpoint();
                 clause & c = *(*it);
-                m_counter -= c.size();
                 if (!process(c))
                     continue; // clause was removed
                 *it2 = *it;
@@ -114,57 +113,52 @@ namespace sat {
         CASSERT("asymm_branch", s.check_invariant());
     }
 
-    bool asymm_branch::process(clause & c) {
+    bool asymm_branch::process_all(clause & c) {
-        if (c.is_blocked()) return true;
+        // try asymmetric branching on all literals in clause.
-        TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
+        
-        SASSERT(s.scope_lvl() == 0);
+        // clause must not be used for propagation
-        SASSERT(s.m_qhead == s.m_trail.size());
+        scoped_detach scoped_d(s, c);
-#ifdef Z3DEBUG
-        unsigned trail_sz = s.m_trail.size();
-#endif
-        SASSERT(!s.inconsistent());
         unsigned sz = c.size();
         SASSERT(sz > 0);
-        unsigned i;
+        unsigned i = 0, new_sz = sz;
-        // check if the clause is already satisfied
+        bool found = false;
-        for (i = 0; i < sz; i++) {
+        for (; i < sz; i++) {
-            if (s.value(c[i]) == l_true) {
+            found = flip_literal_at(c, i, new_sz);
-                s.detach_clause(c);
+            if (found) break;
-                s.del_clause(c);
-                return false;
-            }
         }
-        // try asymmetric branching
+        return !found || cleanup(scoped_d, c, i, new_sz);
-        // clause must not be used for propagation
+    }
-        solver::scoped_detach scoped_d(s, c);
+
+    bool asymm_branch::propagate_literal(clause const& c, literal l) {
+        m_counter -= c.size();
+        SASSERT(!s.inconsistent());
+        TRACE("asymm_branch_detail", tout << "assigning: " << l << "\n";);
+        s.assign(l, justification());
+        s.propagate_core(false); // must not use propagate(), since check_missed_propagation may fail for c
+        return s.inconsistent();
+    }
+
+    bool asymm_branch::flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz) {
+        bool found_conflict = false;
+        unsigned i = 0, sz = c.size();        
         s.push();
-        for (i = 0; i < sz - 1; i++) {
+        for (i = 0; !found_conflict && i < sz; i++) {
-            literal l = c[i];
+            if (i == flip_index) continue;
-            SASSERT(!s.inconsistent());
+            found_conflict = propagate_literal(c, ~c[i]);
-            TRACE("asymm_branch_detail", tout << "assigning: " << ~l << "\n";);
+        }
-            s.assign(~l, justification());
+        if (!found_conflict) {
-            s.propagate_core(false); // must not use propagate(), since check_missed_propagation may fail for c
+            SASSERT(sz == i);
-            if (s.inconsistent())
+            found_conflict = propagate_literal(c, c[flip_index]);
-                break;
         }
         s.pop(1);
-        SASSERT(!s.inconsistent());
+        new_sz = i;
-        SASSERT(s.scope_lvl() == 0);
+        return found_conflict;
-        SASSERT(trail_sz == s.m_trail.size());
+    }
-        SASSERT(s.m_qhead == s.m_trail.size());
+    
-        if (i == sz - 1) {
+    bool asymm_branch::cleanup(scoped_detach& scoped_d, clause& c, unsigned skip_idx, unsigned new_sz) {
-            // clause size can't be reduced.
-            return true;
-        }
-        // clause can be reduced 
-        unsigned new_sz = i+1;
-        SASSERT(new_sz >= 1);
-        SASSERT(new_sz < sz);
-        TRACE("asymm_branch", tout << c << "\nnew_size: " << new_sz << "\n";
-              for (unsigned i = 0; i < c.size(); i++) tout << static_cast<int>(s.value(c[i])) << " "; tout << "\n";);
-        // cleanup reduced clause
         unsigned j = 0;
-        for (i = 0; i < new_sz; i++) {
+        for (unsigned i = 0; i < new_sz; i++) {            
+            if (skip_idx == i) continue;
             literal l = c[i];
             switch (s.value(l)) {
             case l_undef:
@@ -181,7 +175,7 @@ namespace sat {
             }
         }
         new_sz = j;
-        m_elim_literals += sz - new_sz;
+        m_elim_literals += c.size() - new_sz;
         switch(new_sz) {
         case 0:
             s.set_conflict(justification());
@@ -208,12 +202,65 @@ namespace sat {
             return true;
         }
     }
+
+    bool asymm_branch::process(clause & c) {
+        if (c.is_blocked()) return true;
+        TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
+        SASSERT(s.scope_lvl() == 0);
+        SASSERT(s.m_qhead == s.m_trail.size());
+        SASSERT(!s.inconsistent());
+
+#ifdef Z3DEBUG
+        unsigned trail_sz = s.m_trail.size();
+#endif
+        unsigned sz = c.size();
+        SASSERT(sz > 0);
+        unsigned i;
+        // check if the clause is already satisfied
+        for (i = 0; i < sz; i++) {
+            if (s.value(c[i]) == l_true) {
+                s.detach_clause(c);
+                s.del_clause(c);
+                return false;
+            }
+        }
+        if (m_asymm_branch_all) return process_all(c);
+
+        m_counter -= c.size();
+        // try asymmetric branching
+        // clause must not be used for propagation
+        scoped_detach scoped_d(s, c);
+        s.push();
+        bool found_conflict = false;
+        for (i = 0; i < sz - 1 && !found_conflict; i++) {
+            found_conflict = propagate_literal(c, ~c[i]);
+        }
+        s.pop(1);
+        SASSERT(!s.inconsistent());
+        SASSERT(s.scope_lvl() == 0);
+        SASSERT(trail_sz == s.m_trail.size());
+        SASSERT(s.m_qhead == s.m_trail.size());
+        SASSERT(found_conflict == (i != sz - 1));
+        if (!found_conflict) {
+            // clause size can't be reduced.
+            return true;
+        }
+        // clause can be reduced 
+        unsigned new_sz = i+1;
+        SASSERT(new_sz >= 1);
+        SASSERT(new_sz < sz);
+        TRACE("asymm_branch", tout << c << "\nnew_size: " << new_sz << "\n";
+              for (unsigned i = 0; i < c.size(); i++) tout << static_cast<int>(s.value(c[i])) << " "; tout << "\n";);
+        // cleanup and attach reduced clause
+        return cleanup(scoped_d, c, sz, new_sz);
+    }
     
     void asymm_branch::updt_params(params_ref const & _p) {
         sat_asymm_branch_params p(_p);
         m_asymm_branch        = p.asymm_branch();
         m_asymm_branch_rounds = p.asymm_branch_rounds();
         m_asymm_branch_limit  = p.asymm_branch_limit();
+        m_asymm_branch_all    = p.asymm_branch_all();
         if (m_asymm_branch_limit > INT_MAX)
             m_asymm_branch_limit = INT_MAX;
     }

src/sat/sat_asymm_branch.h

@@ -25,6 +25,7 @@ Revision History:
 
 namespace sat {
     class solver;
+    class scoped_detach;
 
     class asymm_branch {
         struct report;
@@ -34,6 +35,7 @@ namespace sat {
 
         // config
         bool                   m_asymm_branch;
+        bool                   m_asymm_branch_all;
         unsigned               m_asymm_branch_rounds;
         unsigned               m_asymm_branch_limit;
 
@@ -41,6 +43,15 @@ namespace sat {
         unsigned m_elim_literals;
 
         bool process(clause & c);
+        
+        bool process_all(clause & c);
+        
+        bool flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz);
+        
+        bool cleanup(scoped_detach& scoped_d, clause& c, unsigned skip_index, unsigned new_sz);
+
+        bool propagate_literal(clause const& c, literal l);
+
     public:
         asymm_branch(solver & s, params_ref const & p);
 

src/sat/sat_asymm_branch_params.pyg

@@ -3,4 +3,5 @@ def_module_params(module_name='sat',
                   export=True,
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
                           ('asymm_branch.rounds', UINT, 32, 'maximum number of rounds of asymmetric branching'),
-                          ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching')))
+                          ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
+                          ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause')))

src/sat/sat_config.cpp

@@ -190,7 +190,6 @@ namespace sat {
         else {
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
         }
-        m_dimacs_display  = p.dimacs_display();
         m_dimacs_inprocess_display  = p.dimacs_inprocess_display();
 
         sat_simplifier_params sp(_p);

src/sat/sat_config.h

@@ -108,7 +108,6 @@ namespace sat {
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
 
-        bool               m_dimacs_display;
         bool               m_dimacs_inprocess_display;
 
         symbol             m_always_true;

src/sat/sat_lookahead.cpp

@@ -1989,6 +1989,7 @@ namespace sat {
         scoped_level _sl(*this, c_fixed_truth);
         m_search_mode = lookahead_mode::searching;
         unsigned depth = 0;
+        unsigned init_trail = m_trail.size();
         
         if (!is_first) {
             goto pick_up_work;
@@ -2010,7 +2011,12 @@ namespace sat {
                 (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
                 m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
                 set_conflict();
+#if 0
+                // return cube of all literals, not just the ones in the main cube
+                lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail);
+#else
                 lits.append(m_cube_state.m_cube);
+#endif
                 backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
                 return l_undef;
             }

src/sat/sat_params.pyg

@@ -42,6 +42,5 @@ def_module_params('sat',
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
-                          ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
                           ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
 

src/sat/sat_probing.cpp

@@ -62,11 +62,9 @@ namespace sat {
         SASSERT(s.value(l.var()) == l_undef);
         literal_vector * implied_lits = updt_cache ? 0 : cached_implied_lits(l);
         if (implied_lits) {
-            literal_vector::iterator it  = implied_lits->begin();
+            for (literal lit : *implied_lits) {
-            literal_vector::iterator end = implied_lits->end();
+                if (m_assigned.contains(lit)) {
-            for (; it != end; ++it) {
+                    s.assign(lit, justification());
-                if (m_assigned.contains(*it)) {
-                    s.assign(*it, justification());
                     m_num_assigned++;
                 }
             }
@@ -137,10 +135,9 @@ namespace sat {
 
         if (m_probing_binary) {
             watch_list & wlist = s.get_wlist(~l);
-            for (unsigned i = 0; i < wlist.size(); i++) {
+            for (watched & w : wlist) {
-                watched & w = wlist[i];
                 if (!w.is_binary_clause())
-                    break;
+                    continue;
                 literal l2 = w.get_literal();
                 if (l.index() > l2.index())
                     continue;

src/sat/sat_solver.cpp

@@ -861,13 +861,6 @@ namespace sat {
         m_stats.m_units = init_trail_size();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(at_base_lvl());
-        if (m_config.m_dimacs_display) {
-            display_dimacs(std::cout);
-            for (unsigned i = 0; i < num_lits; ++i) {
-                std::cout << dimacs_lit(lits[i]) << " 0\n";
-            }
-            return l_undef;
-        }
         if (m_config.m_lookahead_search && num_lits == 0) {
             return lookahead_search();
         }
@@ -1422,6 +1415,7 @@ namespace sat {
         m_restarts                = 0;
         m_simplifications         = 0;
         m_conflicts_since_init    = 0;
+        m_next_simplify           = 0;
         m_min_d_tk                = 1.0;
         m_search_lvl              = 0;
         m_stopwatch.reset();
@@ -3942,14 +3936,6 @@ namespace sat {
         }
     }
 
-    void solver::asymmetric_branching() {
-        if (!at_base_lvl() || inconsistent())
-            return;
-        m_asymm_branch();
-        if (m_ext)
-            m_ext->clauses_modifed();
-    }
-
     // -----------------------
     //
     // Statistics

src/sat/sat_solver.h

@@ -182,6 +182,7 @@ namespace sat {
         friend struct mk_stat;
         friend class ccc;
         friend class elim_vars;
+        friend class scoped_detach;
     public:
         solver(params_ref const & p, reslimit& l);
         ~solver();
@@ -231,25 +232,6 @@ namespace sat {
         bool attach_nary_clause(clause & c);
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
-        class scoped_detach {
-            solver& s;
-            clause& c;
-            bool m_deleted;
-        public:
-            scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
-                s.detach_clause(c);
-            }            
-            ~scoped_detach() {
-                if (!m_deleted) s.attach_clause(c);
-            }
-
-            void del_clause() {
-                if (!m_deleted) {
-                    s.del_clause(c);
-                    m_deleted = true;
-                }
-            }
-        };
         class scoped_disable_checkpoint {
             solver& s;
         public:
@@ -653,6 +635,27 @@ namespace sat {
         void display(std::ostream & out) const;
     };
 
+    class scoped_detach {
+        solver& s;
+        clause& c;
+        bool m_deleted;
+    public:
+        scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
+            s.detach_clause(c);
+        }            
+        ~scoped_detach() {
+            if (!m_deleted) s.attach_clause(c);
+        }
+        
+        void del_clause() {
+            if (!m_deleted) {
+                s.del_clause(c);
+                m_deleted = true;
+            }
+        }
+    };
+
+
     std::ostream & operator<<(std::ostream & out, mk_stat const & stat);
 };
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -188,12 +188,6 @@ public:
             IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";);
             r = l_undef;            
         }
-        if (r == l_undef && m_solver.get_config().m_dimacs_display) {
-            for (auto const& kv : m_map) {
-                std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, m) << "\n";
-            }
-        }
-
         switch (r) {
         case l_true:
             if (sz > 0) {

src/sat/tactic/sat_tactic.cpp

@@ -68,11 +68,6 @@ class sat_tactic : public tactic {
             TRACE("sat_dimacs", m_solver.display_dimacs(tout););
             dep2assumptions(dep2asm, assumptions);
             lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr());
-            if (r == l_undef && m_solver.get_config().m_dimacs_display) {
-                for (auto const& kv : map) {
-                    std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, g->m()) << "\n";
-                }
-            }
             if (r == l_false) {
                 expr_dependency * lcore = 0;
                 if (produce_core) {

src/tactic/goal.cpp

@@ -488,6 +488,11 @@ void goal::display_dimacs(std::ostream & out) const {
         }
         out << "0\n";
     }
+    for (auto const& kv : expr2var) {
+        expr* key = kv.m_key;
+        if (is_app(key)) 
+            out << "c " << kv.m_value << " " << to_app(key)->get_decl()->get_name() << "\n";
+    }
 }
 
 unsigned goal::num_exprs() const {

src/tactic/portfolio/parallel_tactic.cpp

@@ -214,7 +214,7 @@ class parallel_tactic : public tactic {
 
         void set_type(task_type t) { m_type = t; }
 
-        expr_ref_vector const& cubes() const { SASSERT(m_type == conquer); return m_cubes; }
+        expr_ref_vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; }
 
         // remove up to n cubes from list of cubes.
         expr_ref_vector split_cubes(unsigned n) {