From f2dfc0dc24c8594ae4d1181bfbb4b1848d057a94 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Apr 2018 15:46:21 -0700 Subject: [PATCH] including all touched tautology literals each round Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 25 ++++++++++++++++++------ src/tactic/portfolio/CMakeLists.txt | 2 ++ src/tactic/portfolio/parallel_tactic.cpp | 16 +-------------- src/tactic/smtlogics/qfbv_tactic.cpp | 7 ++++--- 4 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 52c7236a0..ae156cb4b 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1069,8 +1069,8 @@ namespace sat { // Find literals that are in the intersection of all resolvents with l. // bool resolution_intersection(literal l, bool adding) { + unsigned tsz = m_tautology.size(); reset_intersection(); - m_tautology.reset(); if (!process_var(l.var())) return false; bool first = true; VERIFY(s.value(l) == l_undef); @@ -1086,6 +1086,7 @@ namespace sat { } if (!first || s.is_marked(lit)) { reset_intersection(); + m_tautology.shrink(tsz); return false; // intersection is empty or does not add anything new. } first = false; @@ -1122,22 +1123,30 @@ namespace sat { for (literal lit : m_new_intersection) add_intersection(lit); } - if (m_intersection.empty()) + if (m_intersection.empty()) { + m_tautology.shrink(tsz); return false; + } } } + if (m_intersection.empty()) { + m_tautology.shrink(tsz); + } // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); return first; } bool check_abce_tautology(literal l) { - m_tautology.reset(); + unsigned tsz = m_tautology.size(); if (!process_var(l.var())) return false; for (watched & w : s.get_wlist(l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); VERIFY(lit != ~l); - if (!s.is_marked(~lit)) return false; + if (!s.is_marked(~lit)) { + m_tautology.shrink(tsz); + return false; + } m_tautology.push_back(~lit); } } @@ -1153,7 +1162,10 @@ namespace sat { break; } } - if (!tautology) return false; + if (!tautology) { + m_tautology.shrink(tsz); + return false; + } } return true; } @@ -1352,6 +1364,7 @@ namespace sat { unsigned sz = 0, sz0 = m_covered_clause.size(); for (literal l : m_covered_clause) s.mark_visited(l); shuffle(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand); + m_tautology.reset(); m_mc.stackv().reset(); m_ala_qhead = 0; @@ -1394,7 +1407,6 @@ namespace sat { * tautology depends on resolution intersection. * literals used for resolution intersection may have to be flipped. */ - m_tautology.reset(); for (literal l : m_covered_clause) { m_tautology.push_back(l); s.mark_visited(l); @@ -1610,6 +1622,7 @@ namespace sat { Then the following binary clause is blocked: l \/ ~l' */ void bca(literal l) { + m_tautology.reset(); if (resolution_intersection(l, true)) { // this literal is pure. return; diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 055251467..ed5ec8cf7 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -18,6 +18,8 @@ z3_add_component(portfolio smtlogic_tactics subpaving_tactic ufbv_tactic + PYG_FILES + parallel_params.pyg TACTIC_HEADERS default_tactic.h fd_solver.h diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index b19bab487..e01e58051 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -159,8 +159,6 @@ class parallel_tactic : public tactic { ref m_solver; // solver state unsigned m_depth; // number of nested calls to cubing double m_width; // estimate of fraction of problem handled by state - unsigned m_cube_cutoff; // saved configuration value - double m_cube_fraction; // saved configuration value unsigned m_restart_max; // saved configuration value expr_ref_vector cube_literals(expr* cube) { @@ -185,8 +183,6 @@ class parallel_tactic : public tactic { m_depth(0), m_width(1.0) { - m_cube_cutoff = p.get_uint("sat.lookahead.cube.cutoff", 8); - m_cube_fraction = p.get_double("sat.lookahead.cube.fraction", 0.4); m_restart_max = p.get_uint("sat.restart.max", 10); } @@ -280,17 +276,7 @@ class parallel_tactic : public tactic { } void set_cube_params() { - unsigned cutoff = m_cube_cutoff; - double fraction = m_cube_fraction; - if (true || (m_depth == 1 && cutoff > 0)) { - m_params.set_sym("lookahead.cube.cutoff", symbol("depth")); - m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u)); - } - else { - m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat")); - m_params.set_double("lookahead.cube.fraction", fraction); - } - get_solver().updt_params(m_params); + // get_solver().updt_params(m_params); } void set_conquer_params() { diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index f28129a52..0eb235791 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,6 +29,7 @@ Notes: #include "tactic/aig/aig_tactic.h" #include "sat/tactic/sat_tactic.h" #include "tactic/portfolio/parallel_tactic.h" +#include "tactic/portfolio/parallel_params.hpp" #include "ackermannization/ackermannize_bv_tactic.h" #define MEMLIMIT 300 @@ -128,11 +129,11 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { - + parallel_params pp(p); + bool use_parallel = pp.enable(); tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), - //mk_parallel_tactic(m, p)); - mk_sat_tactic(m)); + use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());