From 2746528aab9e92e31bf22e1d8d7f0a4aa6516683 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Nov 2017 17:16:36 -0800 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/api/api_goal.cpp | 14 +++ src/api/api_solver.cpp | 4 + src/api/dotnet/Goal.cs | 9 ++ src/api/python/z3/z3.py | 6 +- src/api/z3_api.h | 7 ++ src/sat/sat_asymm_branch.cpp | 141 +++++++++++++++-------- src/sat/sat_asymm_branch.h | 11 ++ src/sat/sat_asymm_branch_params.pyg | 3 +- src/sat/sat_config.cpp | 1 - src/sat/sat_config.h | 1 - src/sat/sat_lookahead.cpp | 6 + src/sat/sat_params.pyg | 1 - src/sat/sat_probing.cpp | 13 +-- src/sat/sat_solver.cpp | 16 +-- src/sat/sat_solver.h | 41 ++++--- src/sat/sat_solver/inc_sat_solver.cpp | 6 - src/sat/tactic/sat_tactic.cpp | 5 - src/tactic/goal.cpp | 5 + src/tactic/portfolio/parallel_tactic.cpp | 2 +- 19 files changed, 186 insertions(+), 106 deletions(-) diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index 0f1b9056b..cf248c10e 100644 --- a/src/api/api_goal.cpp +++ b/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(""); + } + }; diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ad8a3cc29..53ce36720 100644 --- a/src/api/api_solver.cpp +++ b/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::const_iterator it = ctx->begin_assertions(); ptr_vector::const_iterator end = ctx->end_assertions(); for (; it != end; ++it) { diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 521b453f8..25aeba741 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -208,6 +208,15 @@ namespace Microsoft.Z3 return Native.Z3_goal_to_string(Context.nCtx, NativeObject); } + /// + /// Goal to DIMACS formatted string conversion. + /// + /// A string representation of the Goal. + public string ToDimacs() + { + return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject); + } + /// /// Goal to BoolExpr conversion. /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d0273cc24..6b6c90019 100644 --- a/src/api/python/z3/z3.py +++ b/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""" diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5548f6796..ffda1ecbd 100644 --- a/src/api/z3_api.h +++ b/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 */ diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 03d121599..c11ae7e20 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/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) { - 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()); -#ifdef Z3DEBUG - unsigned trail_sz = s.m_trail.size(); -#endif - SASSERT(!s.inconsistent()); + bool asymm_branch::process_all(clause & c) { + // try asymmetric branching on all literals in clause. + + // clause must not be used for propagation + scoped_detach scoped_d(s, c); 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; - } + unsigned i = 0, new_sz = sz; + bool found = false; + for (; i < sz; i++) { + found = flip_literal_at(c, i, new_sz); + if (found) break; } - // try asymmetric branching - // clause must not be used for propagation - solver::scoped_detach scoped_d(s, c); + return !found || cleanup(scoped_d, c, i, new_sz); + } + + 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++) { - literal l = c[i]; - 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 - if (s.inconsistent()) - break; + for (i = 0; !found_conflict && i < sz; i++) { + if (i == flip_index) continue; + found_conflict = propagate_literal(c, ~c[i]); + } + if (!found_conflict) { + SASSERT(sz == i); + found_conflict = propagate_literal(c, c[flip_index]); } 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()); - if (i == sz - 1) { - // 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(s.value(c[i])) << " "; tout << "\n";); - // cleanup reduced clause + new_sz = i; + return found_conflict; + } + + bool asymm_branch::cleanup(scoped_detach& scoped_d, clause& c, unsigned skip_idx, unsigned new_sz) { 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(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; } diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index f2d064da6..fe5f04845 100644 --- a/src/sat/sat_asymm_branch.h +++ b/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); diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg index 8940c64a6..d564c3fb0 100644 --- a/src/sat/sat_asymm_branch_params.pyg +++ b/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'))) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index c1c4ff5f8..4dce25b99 100644 --- a/src/sat/sat_config.cpp +++ b/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); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index e1e40e100..6de1261ad 100644 --- a/src/sat/sat_config.h +++ b/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; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 60594c0d4..a41468936 100644 --- a/src/sat/sat_lookahead.cpp +++ b/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; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 229bd8a4b..7b33ee8e7 100644 --- a/src/sat/sat_params.pyg +++ b/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'))) diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index ff599c9b2..cafc5e3bb 100644 --- a/src/sat/sat_probing.cpp +++ b/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(); - literal_vector::iterator end = implied_lits->end(); - for (; it != end; ++it) { - if (m_assigned.contains(*it)) { - s.assign(*it, justification()); + for (literal lit : *implied_lits) { + if (m_assigned.contains(lit)) { + s.assign(lit, 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++) { - watched & w = wlist[i]; + for (watched & w : wlist) { if (!w.is_binary_clause()) - break; + continue; literal l2 = w.get_literal(); if (l.index() > l2.index()) continue; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f5b04e646..ba6e63680 100644 --- a/src/sat/sat_solver.cpp +++ b/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 diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 43e36de46..bf5f0975b 100644 --- a/src/sat/sat_solver.h +++ b/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); }; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index f922be580..b9bc81e3d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/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) { diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index e049df8a7..3a5c414ef 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/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) { diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 1b2a70f47..311c9838b 100644 --- a/src/tactic/goal.cpp +++ b/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 { diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index 381a13a48..7651ace16 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/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) {