From a625301a4175abb521ef46ff125efb208a943c98 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Sep 2017 15:05:10 -0700 Subject: [PATCH] expose incremental cubing over API Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 1 + src/api/python/z3/z3.py | 23 +++++ src/sat/sat_lookahead.cpp | 84 ++++++------------- src/sat/sat_lookahead.h | 6 +- src/sat/sat_params.pyg | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 8 ++ src/tactic/portfolio/CMakeLists.txt | 1 + .../portfolio/bounded_int2bv_solver.cpp | 2 +- src/tactic/portfolio/fd_solver.h | 2 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- 10 files changed, 63 insertions(+), 68 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 24f22d8ee..520ba3d91 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2735,6 +2735,7 @@ def get_header_files_for_components(component_src_dirs): def mk_install_tactic_cpp(cnames, path): component_src_dirs = [] for cname in cnames: + print("Component %s" % cname) c = get_component(cname) component_src_dirs.append(c.src_dir) h_files_full_path = get_header_files_for_components(component_src_dirs) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9e03c5f99..94221b3db 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6294,10 +6294,33 @@ class Solver(Z3PPObject): candidates = _cs return _to_expr_ref(Z3_solver_lookahead(self.ctx.ref(), self.solver, candidates), self.ctx) + def cube(self): + """Get set of cubes""" + rounds = 0 + while True: + r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver), self.ctx) + if (is_false(r)): + if (rounds == 0): + yield r + return + if (is_true(r)): + yield r + return + rounds += 1 + yield r + def proof(self): """Return a proof for the last `check()`. Proof construction must be enabled.""" return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) + def from_file(self, filename): + """Parse assertions from a file""" + self.add([f for f in parse_smt2_file(filename)]) + + def from_string(self, s): + """Parse assertions from a string""" + self.add([f for f in parse_smt2_string(s)]) + def assertions(self): """Return an AST vector containing all added constraints. diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index f4bfb14e2..a68367f6b 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -657,7 +657,6 @@ namespace sat { } // case watched::EXTERNAL: } - // std::cout << "tsum: " << tsum << "\n"; } #endif // std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n"; @@ -2221,7 +2220,7 @@ namespace sat { SASSERT(dl_no_overflow(base)); unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); scoped_level _sl(*this, dl_truth); - IF_VERBOSE(2, verbose_stream() << "double: " << l << "\n";); + IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";); init_lookahead_reward(); assign(l); propagate(); @@ -2353,63 +2352,24 @@ namespace sat { } lbool lookahead::cube() { -#if 0 literal_vector lits; while (true) { lbool result = cube(lits); if (lits.empty() || result != l_undef) { return result; } - display_cube(std::cout, cube); - } -#endif - lbool result = l_false; - init_search(); - m_model.reset(); - scoped_level _sl(*this, c_fixed_truth); - literal_vector cube; - svector is_decision; - m_search_mode = lookahead_mode::searching; - double freevars_threshold = 0; - while (true) { - TRACE("sat", display(tout);); - inc_istamp(); - checkpoint(); - literal l = choose(); - if (inconsistent()) { - TRACE("sat", tout << "inconsistent: " << cube << "\n";); - freevars_threshold = m_freevars.size(); - if (!backtrack(cube, is_decision)) return result; - continue; - } - if (l == null_literal) { - return l_true; - } - unsigned depth = cube.size(); - if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || - (m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) { - display_cube(std::cout, cube); - freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); - result = l_undef; - set_conflict(); - if (!backtrack(cube, is_decision)) return result; - continue; - } - TRACE("sat", tout << "choose: " << l << " cube: " << cube << "\n";); - ++m_stats.m_decisions; - push(l, c_fixed_truth); - cube.push_back(l); - is_decision.push_back(true); - SASSERT(inconsistent() || !is_unsat()); + display_cube(std::cout, lits); } + return l_undef; } lbool lookahead::cube(literal_vector& lits) { lits.reset(); - bool is_first = (m_cube_state.m_lit == null_literal); + bool is_first = m_cube_state.m_first; if (is_first) { init_search(); m_model.reset(); + m_cube_state.m_first = false; } scoped_level _sl(*this, c_fixed_truth); m_search_mode = lookahead_mode::searching; @@ -2421,39 +2381,43 @@ namespace sat { while (true) { TRACE("sat", display(tout);); - inc_istamp(); checkpoint(); - m_cube_state.m_lit = choose(); + inc_istamp(); if (inconsistent()) { - TRACE("sat", tout << "inconsistent: " << cube << "\n";); + TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = m_freevars.size(); - if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result; + if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } - if (m_cube_state.m_lit == null_literal) { - return l_true; - } + pick_up_work: depth = m_cube_state.m_cube.size(); if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) || (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)); - m_cube_state.m_result = l_undef; set_conflict(); - if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result; lits.append(m_cube_state.m_cube); + backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); return l_undef; } - pick_up_work: - TRACE("sat", tout << "choose: " << m_cube_state.m_lit << " cube: " << m_cube_state.m_cube << "\n";); + literal lit = choose(); + if (inconsistent()) { + TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); + m_cube_state.m_freevars_threshold = m_freevars.size(); + if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; + continue; + } + if (lit == null_literal) { + return l_true; + } + TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";); ++m_stats.m_decisions; - push(m_cube_state.m_lit, c_fixed_truth); - m_cube_state.m_cube.push_back(m_cube_state.m_lit); + push(lit, c_fixed_truth); + m_cube_state.m_cube.push_back(lit); m_cube_state.m_is_decision.push_back(true); SASSERT(inconsistent() || !is_unsat()); } - lbool result = m_cube_state.m_result; m_cube_state.reset(); - return result; + return l_undef; } void lookahead::init_model() { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 3fcf3e18b..87247611c 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -140,17 +140,15 @@ namespace sat { #endif struct cube_state { + bool m_first; svector m_is_decision; literal_vector m_cube; - literal m_lit; - lbool m_result; double m_freevars_threshold; cube_state() { reset(); } void reset() { + m_first = true; m_is_decision.reset(); m_cube.reset(); - m_lit = null_literal; - m_result = l_false; m_freevars_threshold = 0; } }; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 67659aa24..01708b775 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -40,7 +40,7 @@ def_module_params('sat', ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), - ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, hs (Heule Schur), heuleu (Heule Unit), or unit'), + ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), or unit'), ('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_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index da8f22e86..908e56da8 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -345,6 +345,14 @@ public: return result; } virtual expr_ref cube() { + if (!m_internalized) { + dep2asm_t dep2asm; + m_model = 0; + lbool r = internalize_formulas(); + if (r != l_true) return expr_ref(m.mk_true(), m); + m_internalized = true; + } + convert_internalized(); sat::literal_vector lits; lbool result = m_solver.cube(lits); if (result == l_false || lits.empty()) { diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index a8a9b2bba..570db8f6a 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -18,4 +18,5 @@ z3_add_component(portfolio ufbv_tactic TACTIC_HEADERS default_tactic.h + fd_solver.h ) diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 09791f7c9..ec83766a0 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -163,7 +163,7 @@ public: virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); } - virtual expr_ref cube() { return m_solver->cube(); } + virtual expr_ref cube() { flush_assertions(); return m_solver->cube(); } virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h index 6726f42aa..b54ba74f4 100644 --- a/src/tactic/portfolio/fd_solver.h +++ b/src/tactic/portfolio/fd_solver.h @@ -29,7 +29,7 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p); tactic * mk_fd_tactic(ast_manager & m, params_ref const & p); /* - ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)") + ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)") */ #endif diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index d76260e0d..ee4b14178 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -99,7 +99,7 @@ public: virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); } - virtual expr_ref cube() { return m_solver->cube(); } + virtual expr_ref cube() { flush_assertions(); return m_solver->cube(); } virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {