mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
snapshot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fc3cbcbe02
commit
7afbf8165e
|
@ -323,15 +323,6 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_solver_assert_lemma(c, s, a);
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
CHECK_FORMULA(a,);
|
||||
to_solver_ref(s)->assert_lemma(to_expr(a));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) {
|
||||
Z3_TRY;
|
||||
|
|
|
@ -239,29 +239,6 @@ namespace Microsoft.Z3
|
|||
Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Assert a lemma (or multiple) into the solver.
|
||||
/// </summary>
|
||||
public void AssertLemma(params BoolExpr[] constraints)
|
||||
{
|
||||
Contract.Requires(constraints != null);
|
||||
Contract.Requires(Contract.ForAll(constraints, c => c != null));
|
||||
|
||||
Context.CheckContextMatch<BoolExpr>(constraints);
|
||||
foreach (BoolExpr a in constraints)
|
||||
{
|
||||
Native.Z3_solver_assert_lemma(Context.nCtx, NativeObject, a.NativeObject);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Assert a lemma (or multiple) into the solver.
|
||||
/// </summary>
|
||||
public void AddLemma(IEnumerable<BoolExpr> constraints)
|
||||
{
|
||||
AssertLemma(constraints.ToArray());
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The number of assertions in the solver.
|
||||
/// </summary>
|
||||
|
@ -325,6 +302,7 @@ namespace Microsoft.Z3
|
|||
return lboolToStatus(r);
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Retrieve fixed assignments to the set of variables in the form of consequences.
|
||||
/// Each consequence is an implication of the form
|
||||
|
|
|
@ -6135,16 +6135,6 @@ extern "C" {
|
|||
*/
|
||||
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p);
|
||||
|
||||
/**
|
||||
\brief add a lemma. A lemma is a assumed to be a consequence of the current assertions.
|
||||
Adding a lemma should therefore be a logical no-op. Solvers are free to ignore lemmas.
|
||||
|
||||
\pre \c a must be a Boolean expression
|
||||
|
||||
def_API('Z3_solver_assert_lemma', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST)))
|
||||
*/
|
||||
void Z3_API Z3_solver_assert_lemma(Z3_context c, Z3_solver s, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief load solver assertions from a file.
|
||||
|
||||
|
|
|
@ -319,9 +319,8 @@ struct pb2bv_rewriter::imp {
|
|||
sums.insert(sum);
|
||||
}
|
||||
}
|
||||
uint_set::iterator it = sums.begin(), end = sums.end();
|
||||
for (; it != end; ++it) {
|
||||
oc.push_back(*it);
|
||||
for (unsigned u : sums) {
|
||||
oc.push_back(u);
|
||||
}
|
||||
std::sort(oc.begin(), oc.end());
|
||||
DEBUG_CODE(
|
||||
|
|
|
@ -42,9 +42,13 @@ namespace sat {
|
|||
asymm_branch & m_asymm_branch;
|
||||
stopwatch m_watch;
|
||||
unsigned m_elim_literals;
|
||||
unsigned m_elim_learned_literals;
|
||||
unsigned m_hidden_tautologies;
|
||||
report(asymm_branch & a):
|
||||
m_asymm_branch(a),
|
||||
m_elim_literals(a.m_elim_literals) {
|
||||
m_elim_literals(a.m_elim_literals),
|
||||
m_elim_learned_literals(a.m_elim_learned_literals),
|
||||
m_hidden_tautologies(a.m_hidden_tautologies) {
|
||||
m_watch.start();
|
||||
}
|
||||
|
||||
|
@ -53,12 +57,35 @@ namespace sat {
|
|||
IF_VERBOSE(SAT_VB_LVL,
|
||||
verbose_stream() << " (sat-asymm-branch :elim-literals "
|
||||
<< (m_asymm_branch.m_elim_literals - m_elim_literals)
|
||||
<< " :elim-learned-literals " << (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals)
|
||||
<< " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
|
||||
<< " :cost " << m_asymm_branch.m_counter
|
||||
<< mem_stat()
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
|
||||
}
|
||||
};
|
||||
|
||||
bool asymm_branch::process(scc* scc) {
|
||||
unsigned elim0 = m_elim_literals;
|
||||
unsigned eliml0 = m_elim_learned_literals;
|
||||
for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) {
|
||||
unsigned elim = m_elim_literals;
|
||||
if (scc) scc->init_big(true);
|
||||
process(scc, s.m_clauses);
|
||||
process(scc, s.m_learned);
|
||||
s.propagate(false);
|
||||
if (s.m_inconsistent)
|
||||
break;
|
||||
std::cout << "elim: " << m_elim_literals - elim << "\n";
|
||||
if (m_elim_literals == elim)
|
||||
break;
|
||||
}
|
||||
std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
|
||||
std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
|
||||
return m_elim_literals > elim0;
|
||||
}
|
||||
|
||||
|
||||
void asymm_branch::process(scc* scc, clause_vector& clauses) {
|
||||
int64 limit = -m_asymm_branch_limit;
|
||||
std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
|
||||
|
@ -119,26 +146,23 @@ namespace sat {
|
|||
TRACE("asymm_branch_detail", s.display(tout););
|
||||
report rpt(*this);
|
||||
svector<char> saved_phase(s.m_phase);
|
||||
if (m_asymm_branch) {
|
||||
m_counter = 0;
|
||||
process(nullptr, s.m_clauses);
|
||||
m_counter = -m_counter;
|
||||
}
|
||||
if (m_asymm_branch_sampled) {
|
||||
scc scc(s, m_params);
|
||||
while (true) {
|
||||
unsigned elim = m_elim_literals;
|
||||
scc.init_big(true);
|
||||
process(&scc, s.m_clauses);
|
||||
process(&scc, s.m_learned);
|
||||
s.propagate(false);
|
||||
if (s.m_inconsistent)
|
||||
break;
|
||||
std::cout << m_elim_literals - elim << "\n";
|
||||
if (m_elim_literals == elim)
|
||||
break;
|
||||
|
||||
bool change = true;
|
||||
unsigned counter = 0;
|
||||
while (change && counter < 2) {
|
||||
++counter;
|
||||
change = false;
|
||||
if (m_asymm_branch_sampled) {
|
||||
scc sc(s, m_params);
|
||||
if (process(&sc)) change = true;
|
||||
}
|
||||
if (m_asymm_branch) {
|
||||
m_counter = 0;
|
||||
if (process(nullptr)) change = true;
|
||||
m_counter = -m_counter;
|
||||
}
|
||||
}
|
||||
|
||||
s.m_phase = saved_phase;
|
||||
m_asymm_branch_limit *= 2;
|
||||
if (m_asymm_branch_limit > UINT_MAX)
|
||||
|
@ -172,8 +196,13 @@ namespace sat {
|
|||
};
|
||||
|
||||
void asymm_branch::sort(scc& scc, clause const& c) {
|
||||
sort(scc, c.begin(), c.end());
|
||||
}
|
||||
|
||||
void asymm_branch::sort(scc& scc, literal const* begin, literal const* end) {
|
||||
m_pos.reset(); m_neg.reset();
|
||||
for (literal l : c) {
|
||||
for (; begin != end; ++begin) {
|
||||
literal l = *begin;
|
||||
m_pos.push_back(l);
|
||||
m_neg.push_back(~l);
|
||||
}
|
||||
|
@ -203,23 +232,42 @@ namespace sat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) {
|
||||
int right = scc.get_right(m_pos.back());
|
||||
m_to_delete.reset();
|
||||
for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
|
||||
literal lit = m_pos[i];
|
||||
SASSERT(scc.get_left(lit) < scc.get_left(last));
|
||||
int right2 = scc.get_right(lit);
|
||||
if (right2 > right) {
|
||||
// lit => last, so lit can be deleted
|
||||
m_to_delete.push_back(lit);
|
||||
void asymm_branch::minimize(scc& scc, literal_vector& lemma) {
|
||||
scc.ensure_big(true);
|
||||
sort(scc, lemma.begin(), lemma.end());
|
||||
uhle(scc);
|
||||
if (!m_to_delete.empty()) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < lemma.size(); ++i) {
|
||||
literal l = lemma[i];
|
||||
if (!m_to_delete.contains(l)) {
|
||||
lemma[j++] = l;
|
||||
}
|
||||
}
|
||||
else {
|
||||
right = right2;
|
||||
// std::cout << lemma.size() << " -> " << j << "\n";
|
||||
lemma.shrink(j);
|
||||
}
|
||||
}
|
||||
|
||||
void asymm_branch::uhle(scc& scc) {
|
||||
m_to_delete.reset();
|
||||
if (m_to_delete.empty()) {
|
||||
int right = scc.get_right(m_pos.back());
|
||||
for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
|
||||
literal lit = m_pos[i];
|
||||
SASSERT(scc.get_left(lit) < scc.get_left(last));
|
||||
int right2 = scc.get_right(lit);
|
||||
if (right2 > right) {
|
||||
// lit => last, so lit can be deleted
|
||||
m_to_delete.push_back(lit);
|
||||
}
|
||||
else {
|
||||
right = right2;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (m_to_delete.empty()) {
|
||||
right = scc.get_right(m_neg[0]);
|
||||
int right = scc.get_right(m_neg[0]);
|
||||
for (unsigned i = 1; i < m_neg.size(); ++i) {
|
||||
literal lit = m_neg[i];
|
||||
int right2 = scc.get_right(lit);
|
||||
|
@ -232,20 +280,11 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
if (!m_to_delete.empty()) {
|
||||
#if 0
|
||||
std::cout << "delete " << m_to_delete << "\n";
|
||||
}
|
||||
|
||||
std::cout << "pos\n";
|
||||
for (literal l : m_pos) {
|
||||
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
|
||||
}
|
||||
std::cout << "neg\n";
|
||||
for (literal l : m_neg) {
|
||||
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
|
||||
}
|
||||
std::cout << "\n";
|
||||
#endif
|
||||
bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) {
|
||||
uhle(scc);
|
||||
if (!m_to_delete.empty()) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
if (!m_to_delete.contains(c[i])) {
|
||||
|
@ -314,10 +353,13 @@ namespace sat {
|
|||
return re_attach(scoped_d, c, new_sz);
|
||||
}
|
||||
|
||||
bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
|
||||
m_elim_literals += c.size() - new_sz;
|
||||
switch(new_sz) {
|
||||
case 0:
|
||||
bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
|
||||
m_elim_literals += c.size() - new_sz;
|
||||
if (c.is_learned()) {
|
||||
m_elim_learned_literals += c.size() - new_sz;
|
||||
}
|
||||
switch(new_sz) {
|
||||
case 0:
|
||||
s.set_conflict(justification());
|
||||
return false;
|
||||
case 1:
|
||||
|
@ -329,7 +371,7 @@ namespace sat {
|
|||
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
|
||||
case 2:
|
||||
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
s.mk_bin_clause(c[0], c[1], false);
|
||||
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
scoped_d.del_clause();
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
return false;
|
||||
|
@ -345,10 +387,13 @@ namespace sat {
|
|||
bool asymm_branch::process_sampled(scc& scc, clause & c) {
|
||||
scoped_detach scoped_d(s, c);
|
||||
sort(scc, c);
|
||||
#if 0
|
||||
if (uhte(scc, c)) {
|
||||
++m_hidden_tautologies;
|
||||
scoped_d.del_clause();
|
||||
return false;
|
||||
}
|
||||
#endif
|
||||
return uhle(scoped_d, scc, c);
|
||||
}
|
||||
|
||||
|
@ -381,7 +426,7 @@ namespace sat {
|
|||
// clause must not be used for propagation
|
||||
scoped_detach scoped_d(s, c);
|
||||
unsigned new_sz = c.size();
|
||||
unsigned flip_position = 2 + m_rand(c.size() - 2); // don't flip on the watch literals.
|
||||
unsigned flip_position = m_rand(c.size());
|
||||
bool found_conflict = flip_literal_at(c, flip_position, new_sz);
|
||||
SASSERT(!s.inconsistent());
|
||||
SASSERT(s.scope_lvl() == 0);
|
||||
|
@ -399,11 +444,12 @@ namespace sat {
|
|||
|
||||
void asymm_branch::updt_params(params_ref const & _p) {
|
||||
sat_asymm_branch_params p(_p);
|
||||
m_asymm_branch = p.asymm_branch();
|
||||
m_asymm_branch_delay = p.asymm_branch_delay();
|
||||
m_asymm_branch = p.asymm_branch();
|
||||
m_asymm_branch_rounds = p.asymm_branch_rounds();
|
||||
m_asymm_branch_delay = p.asymm_branch_delay();
|
||||
m_asymm_branch_sampled = p.asymm_branch_sampled();
|
||||
m_asymm_branch_limit = p.asymm_branch_limit();
|
||||
m_asymm_branch_all = p.asymm_branch_all();
|
||||
m_asymm_branch_limit = p.asymm_branch_limit();
|
||||
m_asymm_branch_all = p.asymm_branch_all();
|
||||
if (m_asymm_branch_limit > UINT_MAX)
|
||||
m_asymm_branch_limit = UINT_MAX;
|
||||
}
|
||||
|
@ -414,10 +460,13 @@ namespace sat {
|
|||
|
||||
void asymm_branch::collect_statistics(statistics & st) const {
|
||||
st.update("elim literals", m_elim_literals);
|
||||
st.update("hidden tautologies", m_hidden_tautologies);
|
||||
}
|
||||
|
||||
void asymm_branch::reset_statistics() {
|
||||
m_elim_literals = 0;
|
||||
m_elim_learned_literals = 0;
|
||||
m_hidden_tautologies = 0;
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -39,6 +39,7 @@ namespace sat {
|
|||
|
||||
// config
|
||||
bool m_asymm_branch;
|
||||
unsigned m_asymm_branch_rounds;
|
||||
unsigned m_asymm_branch_delay;
|
||||
bool m_asymm_branch_sampled;
|
||||
bool m_asymm_branch_propagate;
|
||||
|
@ -47,20 +48,27 @@ namespace sat {
|
|||
|
||||
// stats
|
||||
unsigned m_elim_literals;
|
||||
unsigned m_elim_learned_literals;
|
||||
unsigned m_hidden_tautologies;
|
||||
|
||||
literal_vector m_pos, m_neg; // literals (complements of literals) in clauses sorted by discovery time (m_left in scc).
|
||||
literal_vector m_to_delete;
|
||||
|
||||
struct compare_left;
|
||||
|
||||
void sort(scc& scc, literal const* begin, literal const* end);
|
||||
void sort(scc & scc, clause const& c);
|
||||
|
||||
bool uhle(scoped_detach& scoped_d, scc & scc, clause & c);
|
||||
|
||||
void uhle(scc & scc);
|
||||
|
||||
bool uhte(scc & scc, clause & c);
|
||||
|
||||
bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz);
|
||||
|
||||
bool process(scc* scc);
|
||||
|
||||
bool process(clause & c);
|
||||
|
||||
bool process_sampled(scc& scc, clause & c);
|
||||
|
@ -86,6 +94,8 @@ namespace sat {
|
|||
void collect_statistics(statistics & st) const;
|
||||
void reset_statistics();
|
||||
|
||||
void minimize(scc& scc, literal_vector& lemma);
|
||||
|
||||
void init_search() { m_calls = 0; }
|
||||
|
||||
inline void dec(unsigned c) { m_counter -= c; }
|
||||
|
|
|
@ -2,6 +2,7 @@ def_module_params(module_name='sat',
|
|||
class_name='sat_asymm_branch_params',
|
||||
export=True,
|
||||
params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
|
||||
('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
|
||||
('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
|
||||
('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'),
|
||||
('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
|
||||
|
|
|
@ -24,24 +24,8 @@ Revision History:
|
|||
|
||||
namespace sat {
|
||||
|
||||
config::config(params_ref const & p):
|
||||
m_restart_max(0),
|
||||
m_always_true("always_true"),
|
||||
m_always_false("always_false"),
|
||||
m_caching("caching"),
|
||||
m_random("random"),
|
||||
m_geometric("geometric"),
|
||||
m_luby("luby"),
|
||||
m_dyn_psm("dyn_psm"),
|
||||
m_psm("psm"),
|
||||
m_glue("glue"),
|
||||
m_glue_psm("glue_psm"),
|
||||
m_psm_glue("psm_glue") {
|
||||
m_num_threads = 1;
|
||||
m_lookahead_simplify = false;
|
||||
m_lookahead_simplify_bca = false;
|
||||
m_elim_vars = false;
|
||||
m_incremental = false;
|
||||
config::config(params_ref const & p) {
|
||||
m_incremental = false; // ad-hoc parameter
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
@ -50,21 +34,21 @@ namespace sat {
|
|||
m_max_memory = megabytes_to_bytes(p.max_memory());
|
||||
|
||||
symbol s = p.restart();
|
||||
if (s == m_luby)
|
||||
if (s == symbol("luby"))
|
||||
m_restart = RS_LUBY;
|
||||
else if (s == m_geometric)
|
||||
else if (s == symbol("geometric"))
|
||||
m_restart = RS_GEOMETRIC;
|
||||
else
|
||||
throw sat_param_exception("invalid restart strategy");
|
||||
|
||||
s = p.phase();
|
||||
if (s == m_always_false)
|
||||
if (s == symbol("always_false"))
|
||||
m_phase = PS_ALWAYS_FALSE;
|
||||
else if (s == m_always_true)
|
||||
else if (s == symbol("always_true"))
|
||||
m_phase = PS_ALWAYS_TRUE;
|
||||
else if (s == m_caching)
|
||||
else if (s == symbol("caching"))
|
||||
m_phase = PS_CACHING;
|
||||
else if (s == m_random)
|
||||
else if (s == symbol("random"))
|
||||
m_phase = PS_RANDOM;
|
||||
else
|
||||
throw sat_param_exception("invalid phase selection strategy");
|
||||
|
@ -90,24 +74,18 @@ namespace sat {
|
|||
m_local_search_threads = p.local_search_threads();
|
||||
m_lookahead_simplify = p.lookahead_simplify();
|
||||
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
|
||||
if (p.lookahead_reward() == symbol("heule_schur")) {
|
||||
if (p.lookahead_reward() == symbol("heule_schur"))
|
||||
m_lookahead_reward = heule_schur_reward;
|
||||
}
|
||||
else if (p.lookahead_reward() == symbol("heuleu")) {
|
||||
else if (p.lookahead_reward() == symbol("heuleu"))
|
||||
m_lookahead_reward = heule_unit_reward;
|
||||
}
|
||||
else if (p.lookahead_reward() == symbol("ternary")) {
|
||||
else if (p.lookahead_reward() == symbol("ternary"))
|
||||
m_lookahead_reward = ternary_reward;
|
||||
}
|
||||
else if (p.lookahead_reward() == symbol("unit")) {
|
||||
else if (p.lookahead_reward() == symbol("unit"))
|
||||
m_lookahead_reward = unit_literal_reward;
|
||||
}
|
||||
else if (p.lookahead_reward() == symbol("march_cu")) {
|
||||
else if (p.lookahead_reward() == symbol("march_cu"))
|
||||
m_lookahead_reward = march_cu_reward;
|
||||
}
|
||||
else {
|
||||
else
|
||||
throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
|
||||
}
|
||||
|
||||
m_lookahead_cube_fraction = p.lookahead_cube_fraction();
|
||||
m_lookahead_cube_cutoff = p.lookahead_cube_cutoff();
|
||||
|
@ -120,29 +98,23 @@ namespace sat {
|
|||
// --------------------------------
|
||||
|
||||
s = p.gc();
|
||||
if (s == m_dyn_psm) {
|
||||
m_gc_strategy = GC_DYN_PSM;
|
||||
m_gc_initial = p.gc_initial();
|
||||
m_gc_increment = p.gc_increment();
|
||||
m_gc_small_lbd = p.gc_small_lbd();
|
||||
m_gc_k = p.gc_k();
|
||||
if (m_gc_k > 255)
|
||||
m_gc_k = 255;
|
||||
}
|
||||
else {
|
||||
if (s == m_glue_psm)
|
||||
m_gc_strategy = GC_GLUE_PSM;
|
||||
else if (s == m_glue)
|
||||
m_gc_strategy = GC_GLUE;
|
||||
else if (s == m_psm)
|
||||
m_gc_strategy = GC_PSM;
|
||||
else if (s == m_psm_glue)
|
||||
m_gc_strategy = GC_PSM_GLUE;
|
||||
else
|
||||
throw sat_param_exception("invalid gc strategy");
|
||||
m_gc_initial = p.gc_initial();
|
||||
m_gc_increment = p.gc_increment();
|
||||
}
|
||||
if (s == symbol("dyn_psm"))
|
||||
m_gc_strategy = GC_DYN_PSM;
|
||||
else if (s == symbol("glue_psm"))
|
||||
m_gc_strategy = GC_GLUE_PSM;
|
||||
else if (s == symbol("glue"))
|
||||
m_gc_strategy = GC_GLUE;
|
||||
else if (s == symbol("psm"))
|
||||
m_gc_strategy = GC_PSM;
|
||||
else if (s == symbol("psm_glue"))
|
||||
m_gc_strategy = GC_PSM_GLUE;
|
||||
else
|
||||
throw sat_param_exception("invalid gc strategy");
|
||||
m_gc_initial = p.gc_initial();
|
||||
m_gc_increment = p.gc_increment();
|
||||
m_gc_small_lbd = p.gc_small_lbd();
|
||||
m_gc_k = std::min(255u, p.gc_k());
|
||||
|
||||
m_minimize_lemmas = p.minimize_lemmas();
|
||||
m_core_minimize = p.core_minimize();
|
||||
m_core_minimize_partial = p.core_minimize_partial();
|
||||
|
@ -154,18 +126,15 @@ namespace sat {
|
|||
|
||||
// Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.
|
||||
m_branching_heuristic = BH_VSIDS;
|
||||
if (p.branching_heuristic() == symbol("vsids")) {
|
||||
if (p.branching_heuristic() == symbol("vsids"))
|
||||
m_branching_heuristic = BH_VSIDS;
|
||||
}
|
||||
else if (p.branching_heuristic() == symbol("chb")) {
|
||||
else if (p.branching_heuristic() == symbol("chb"))
|
||||
m_branching_heuristic = BH_CHB;
|
||||
}
|
||||
else if (p.branching_heuristic() == symbol("lrb")) {
|
||||
else if (p.branching_heuristic() == symbol("lrb"))
|
||||
m_branching_heuristic = BH_LRB;
|
||||
}
|
||||
else {
|
||||
else
|
||||
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
|
||||
}
|
||||
|
||||
m_anti_exploration = p.branching_anti_exploration();
|
||||
m_step_size_init = 0.40;
|
||||
m_step_size_dec = 0.000001;
|
||||
|
@ -177,21 +146,16 @@ namespace sat {
|
|||
|
||||
// PB parameters
|
||||
s = p.pb_solver();
|
||||
if (s == symbol("circuit")) {
|
||||
if (s == symbol("circuit"))
|
||||
m_pb_solver = PB_CIRCUIT;
|
||||
}
|
||||
else if (s == symbol("sorting")) {
|
||||
else if (s == symbol("sorting"))
|
||||
m_pb_solver = PB_SORTING;
|
||||
}
|
||||
else if (s == symbol("totalizer")) {
|
||||
else if (s == symbol("totalizer"))
|
||||
m_pb_solver = PB_TOTALIZER;
|
||||
}
|
||||
else if (s == symbol("solver")) {
|
||||
else if (s == symbol("solver"))
|
||||
m_pb_solver = PB_SOLVER;
|
||||
}
|
||||
else {
|
||||
else
|
||||
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
|
||||
}
|
||||
|
||||
sat_simplifier_params sp(_p);
|
||||
m_elim_vars = sp.elim_vars();
|
||||
|
|
|
@ -101,6 +101,7 @@ namespace sat {
|
|||
unsigned m_gc_increment;
|
||||
unsigned m_gc_small_lbd;
|
||||
unsigned m_gc_k;
|
||||
bool m_gc_burst;
|
||||
|
||||
bool m_minimize_lemmas;
|
||||
bool m_dyn_sub_res;
|
||||
|
@ -110,20 +111,7 @@ namespace sat {
|
|||
symbol m_drat_file;
|
||||
bool m_drat_check_unsat;
|
||||
bool m_drat_check_sat;
|
||||
|
||||
symbol m_always_true;
|
||||
symbol m_always_false;
|
||||
symbol m_caching;
|
||||
symbol m_random;
|
||||
symbol m_geometric;
|
||||
symbol m_luby;
|
||||
|
||||
symbol m_dyn_psm;
|
||||
symbol m_psm;
|
||||
symbol m_glue;
|
||||
symbol m_glue_psm;
|
||||
symbol m_psm_glue;
|
||||
|
||||
pb_solver m_pb_solver;
|
||||
|
||||
// branching heuristic settings.
|
||||
|
|
|
@ -87,6 +87,7 @@ namespace sat{
|
|||
simp.m_neg_cls.reset();
|
||||
simp.collect_clauses(pos_l, simp.m_pos_cls, false);
|
||||
simp.collect_clauses(neg_l, simp.m_neg_cls, false);
|
||||
VERIFY(!s.is_external(v));
|
||||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
simp.save_clauses(mc_entry, simp.m_pos_cls);
|
||||
simp.save_clauses(mc_entry, simp.m_neg_cls);
|
||||
|
@ -99,7 +100,7 @@ namespace sat{
|
|||
pos_occs.reset();
|
||||
neg_occs.reset();
|
||||
literal_vector lits;
|
||||
add_clauses(b, lits);
|
||||
add_clauses(b, lits);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
@ -301,12 +301,10 @@ namespace sat {
|
|||
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
|
||||
literal l1 = ~to_literal(l_idx);
|
||||
watch_list const & wlist = s.m_watches[l_idx];
|
||||
watch_list::const_iterator it = wlist.begin();
|
||||
watch_list::const_iterator end = wlist.end();
|
||||
for (; it != end; ++it) {
|
||||
if (!it->is_binary_unblocked_clause())
|
||||
for (watched const& w : wlist) {
|
||||
if (!w.is_binary_unblocked_clause())
|
||||
continue;
|
||||
literal l2 = it->get_literal();
|
||||
literal l2 = w.get_literal();
|
||||
if (l1.index() > l2.index())
|
||||
continue;
|
||||
literal ls[2] = { l1, l2 };
|
||||
|
@ -316,11 +314,8 @@ namespace sat {
|
|||
}
|
||||
|
||||
// copy clauses
|
||||
clause_vector::const_iterator it = s.m_clauses.begin();
|
||||
clause_vector::const_iterator end = s.m_clauses.end();
|
||||
for (; it != end; ++it) {
|
||||
clause& c = *(*it);
|
||||
add_clause(c.size(), c.begin());
|
||||
for (clause* c : s.m_clauses) {
|
||||
add_clause(c->size(), c->begin());
|
||||
}
|
||||
m_num_non_binary_clauses = s.m_clauses.size();
|
||||
|
||||
|
@ -568,12 +563,11 @@ namespace sat {
|
|||
best_var = v = l.var();
|
||||
bool tt = cur_solution(v);
|
||||
coeff_vector const& falsep = m_vars[v].m_watch[!tt];
|
||||
coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
|
||||
for (; it != end; ++it) {
|
||||
int slack = constraint_slack(it->m_constraint_id);
|
||||
for (pbcoeff const& pbc : falsep) {
|
||||
int slack = constraint_slack(pbc.m_constraint_id);
|
||||
if (slack < 0)
|
||||
++best_bsb;
|
||||
else if (slack < static_cast<int>(it->m_coeff))
|
||||
else if (slack < static_cast<int>(pbc.m_coeff))
|
||||
best_bsb += num_unsat;
|
||||
}
|
||||
++cit;
|
||||
|
@ -583,7 +577,7 @@ namespace sat {
|
|||
v = l.var();
|
||||
unsigned bsb = 0;
|
||||
coeff_vector const& falsep = m_vars[v].m_watch[!cur_solution(v)];
|
||||
coeff_vector::const_iterator it = falsep.begin(), end = falsep.end();
|
||||
auto it = falsep.begin(), end = falsep.end();
|
||||
for (; it != end; ++it) {
|
||||
int slack = constraint_slack(it->m_constraint_id);
|
||||
if (slack < 0) {
|
||||
|
@ -637,22 +631,20 @@ namespace sat {
|
|||
coeff_vector const& truep = m_vars[flipvar].m_watch[flip_is_true];
|
||||
coeff_vector const& falsep = m_vars[flipvar].m_watch[!flip_is_true];
|
||||
|
||||
coeff_vector::const_iterator it = truep.begin(), end = truep.end();
|
||||
for (; it != end; ++it) {
|
||||
unsigned ci = it->m_constraint_id;
|
||||
for (auto const& pbc : truep) {
|
||||
unsigned ci = pbc.m_constraint_id;
|
||||
constraint& c = m_constraints[ci];
|
||||
int old_slack = c.m_slack;
|
||||
c.m_slack -= it->m_coeff;
|
||||
c.m_slack -= pbc.m_coeff;
|
||||
if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat
|
||||
unsat(ci);
|
||||
}
|
||||
}
|
||||
it = falsep.begin(), end = falsep.end();
|
||||
for (; it != end; ++it) {
|
||||
unsigned ci = it->m_constraint_id;
|
||||
for (auto const& pbc : falsep) {
|
||||
unsigned ci = pbc.m_constraint_id;
|
||||
constraint& c = m_constraints[ci];
|
||||
int old_slack = c.m_slack;
|
||||
c.m_slack += it->m_coeff;
|
||||
c.m_slack += pbc.m_coeff;
|
||||
if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat
|
||||
sat(ci);
|
||||
}
|
||||
|
|
|
@ -2254,7 +2254,7 @@ namespace sat {
|
|||
init();
|
||||
if (inconsistent()) return;
|
||||
inc_istamp();
|
||||
literal l = choose();
|
||||
literal l = choose();
|
||||
if (inconsistent()) return;
|
||||
SASSERT(m_trail_lim.empty());
|
||||
unsigned num_units = 0;
|
||||
|
@ -2266,7 +2266,7 @@ namespace sat {
|
|||
++num_units;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << " :propagations " << m_stats.m_propagations << ")\n";);
|
||||
|
||||
if (m_s.inconsistent()) return;
|
||||
|
||||
|
@ -2315,16 +2315,8 @@ namespace sat {
|
|||
void lookahead::add_hyper_binary() {
|
||||
|
||||
unsigned num_lits = m_s.num_vars() * 2;
|
||||
unsigned num_bins = 0;
|
||||
|
||||
#if 0
|
||||
std::cout << "binary trail size: " << m_binary_trail.size() << "\n";
|
||||
std::cout << "Are windfalls still on the trail at base level?\n";
|
||||
#endif
|
||||
|
||||
unsigned disconnected1 = 0;
|
||||
unsigned disconnected2 = 0;
|
||||
|
||||
#if 1
|
||||
typedef std::pair<unsigned, unsigned> u_pair;
|
||||
hashtable<u_pair, pair_hash<unsigned_hash, unsigned_hash>, default_eq<u_pair> > imp;
|
||||
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
||||
|
@ -2355,14 +2347,16 @@ namespace sat {
|
|||
literal_vector const& lits = m_binary[idx];
|
||||
for (unsigned sz = bin_size[idx]; sz > 0; --sz) {
|
||||
literal v = lits[lits.size() - sz];
|
||||
if (v != get_parent(v)) continue;
|
||||
if (m_s.was_eliminated(v.var())) continue;
|
||||
if (imp.contains(std::make_pair(u.index(), v.index()))) continue;
|
||||
if (scc.reaches(u, v)) continue;
|
||||
candidates.push_back(std::make_pair(u, v));
|
||||
if (v == get_parent(v) &&
|
||||
!m_s.was_eliminated(v.var()) &&
|
||||
!imp.contains(std::make_pair(u.index(), v.index())) &&
|
||||
!scc.reaches(u, v)) {
|
||||
candidates.push_back(std::make_pair(u, v));
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < 5; ++i) {
|
||||
|
||||
for (unsigned count = 0; count < 5; ++count) {
|
||||
scc.init_big(true);
|
||||
unsigned k = 0;
|
||||
union_find_default_ctx ufctx;
|
||||
|
@ -2373,7 +2367,7 @@ namespace sat {
|
|||
literal v = candidates[j].second;
|
||||
if (!scc.reaches(u, v)) {
|
||||
if (uf.find(u.index()) != uf.find(v.index())) {
|
||||
++disconnected1;
|
||||
++num_bins;
|
||||
uf.merge(u.index(), v.index());
|
||||
uf.merge((~u).index(), (~v).index());
|
||||
VERIFY(!m_s.was_eliminated(u.var()));
|
||||
|
@ -2389,48 +2383,11 @@ namespace sat {
|
|||
std::cout << candidates.size() << " -> " << k << "\n";
|
||||
if (k == candidates.size()) break;
|
||||
candidates.shrink(k);
|
||||
if (k == 0) break;
|
||||
}
|
||||
|
||||
std::cout << "candidates: " << candidates.size() << "\n";
|
||||
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
union_find_default_ctx ufctx;
|
||||
union_find<union_find_default_ctx> uf(ufctx);
|
||||
for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
|
||||
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
||||
literal u = get_parent(to_literal(idx));
|
||||
if (null_literal != u) {
|
||||
for (watched const& w : m_s.m_watches[idx]) {
|
||||
if (!w.is_binary_clause()) continue;
|
||||
literal v = get_parent(w.get_literal());
|
||||
if (null_literal != v) {
|
||||
uf.merge(u.index(), v.index());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < m_binary.size(); ++i) {
|
||||
literal u = to_literal(i);
|
||||
if (u == get_parent(u) && !m_s.was_eliminated(u.var())) {
|
||||
for (literal v : m_binary[i]) {
|
||||
if (v == get_parent(v) &&
|
||||
!m_s.was_eliminated(v.var()) &&
|
||||
uf.find(u.index()) != uf.find(v.index())) {
|
||||
++disconnected2;
|
||||
uf.merge(u.index(), v.index());
|
||||
// m_s.mk_clause(~u, v, true);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";);
|
||||
//IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";);
|
||||
//m_stats.m_bca += disconnected;
|
||||
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << num_bins << ")\n";);
|
||||
m_stats.m_bca += num_bins;
|
||||
}
|
||||
|
||||
void lookahead::normalize_parents() {
|
||||
|
|
|
@ -18,10 +18,11 @@ def_module_params('sat',
|
|||
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
|
||||
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
|
||||
('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
|
||||
('gc.initial', UINT, 20000, 'learned clauses garbage collection frequence'),
|
||||
('gc.initial', UINT, 20000, 'learned clauses garbage collection frequency'),
|
||||
('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
|
||||
('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
|
||||
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
|
||||
('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'),
|
||||
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
|
||||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('core.minimize', BOOL, False, 'minimize computed core'),
|
||||
|
|
|
@ -51,6 +51,8 @@ namespace sat {
|
|||
|
||||
struct pframe;
|
||||
|
||||
bool reaches_aux(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
|
||||
|
||||
public:
|
||||
|
||||
scc(solver & s, params_ref const & p);
|
||||
|
@ -66,11 +68,12 @@ namespace sat {
|
|||
\brief create binary implication graph and associated data-structures to check transitivity.
|
||||
*/
|
||||
void init_big(bool learned);
|
||||
void ensure_big(bool learned) { if (m_left.empty()) init_big(learned); }
|
||||
int get_left(literal l) const { return m_left[l.index()]; }
|
||||
int get_right(literal l) const { return m_right[l.index()]; }
|
||||
literal get_parent(literal l) const { return m_parent[l.index()]; }
|
||||
literal get_root(literal l) const { return m_root[l.index()]; }
|
||||
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
|
||||
bool reaches(literal u, literal v) const { return reaches_aux(u, v) || reaches_aux(~v, ~u); }
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -77,6 +77,7 @@ namespace sat {
|
|||
inline bool simplifier::is_external(bool_var v) const {
|
||||
return
|
||||
s.is_assumption(v) ||
|
||||
(s.is_external(v) && s.is_incremental()) ||
|
||||
(s.is_external(v) && s.m_ext &&
|
||||
(!m_ext_use_list.get(literal(v, false)).empty() ||
|
||||
!m_ext_use_list.get(literal(v, true)).empty()));
|
||||
|
@ -154,6 +155,7 @@ namespace sat {
|
|||
else {
|
||||
remove_clause(c);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
inline void simplifier::unblock_clause(clause & c) {
|
||||
|
@ -1354,6 +1356,7 @@ namespace sat {
|
|||
|
||||
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
|
||||
VERIFY(!s.is_external(l));
|
||||
if (new_entry == 0 && !s.m_retain_blocked_clauses)
|
||||
new_entry = &(mc.mk(k, l.var()));
|
||||
m_to_remove.push_back(&c);
|
||||
|
@ -1365,20 +1368,22 @@ namespace sat {
|
|||
}
|
||||
|
||||
void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
|
||||
SASSERT(!s.is_external(l.var()));
|
||||
prepare_block_clause(c, l, new_entry, model_converter::BLOCK_LIT);
|
||||
if (!s.m_retain_blocked_clauses)
|
||||
mc.insert(*new_entry, c);
|
||||
mc.insert(*new_entry, c);
|
||||
}
|
||||
|
||||
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
|
||||
SASSERT(!s.is_external(l.var()));
|
||||
model_converter::entry * new_entry = 0;
|
||||
prepare_block_clause(c, l, new_entry, k);
|
||||
if (!s.m_retain_blocked_clauses)
|
||||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
}
|
||||
|
||||
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
|
||||
if (new_entry == 0 && !s.m_retain_blocked_clauses)
|
||||
SASSERT(!s.is_external(blocked));
|
||||
VERIFY(!s.is_external(blocked));
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(k, blocked.var()));
|
||||
literal l2 = it->get_literal();
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
|
||||
|
@ -1394,15 +1399,13 @@ namespace sat {
|
|||
|
||||
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
||||
prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
|
||||
if (!s.m_retain_blocked_clauses)
|
||||
mc.insert(*new_entry, l, it->get_literal());
|
||||
mc.insert(*new_entry, l, it->get_literal());
|
||||
}
|
||||
|
||||
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
|
||||
model_converter::entry * new_entry = 0;
|
||||
prepare_block_binary(it, l, blocked, new_entry, k);
|
||||
if (!s.m_retain_blocked_clauses)
|
||||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
}
|
||||
|
||||
void bca() {
|
||||
|
@ -1779,6 +1782,7 @@ namespace sat {
|
|||
|
||||
// eliminate variable
|
||||
++s.m_stats.m_elim_var_res;
|
||||
VERIFY(!s.is_external(v));
|
||||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
save_clauses(mc_entry, m_pos_cls);
|
||||
save_clauses(mc_entry, m_neg_cls);
|
||||
|
@ -1867,7 +1871,10 @@ namespace sat {
|
|||
checkpoint();
|
||||
if (m_elim_counter < 0)
|
||||
break;
|
||||
if (try_eliminate(v)) {
|
||||
if (is_external(v)) {
|
||||
// skip
|
||||
}
|
||||
else if (try_eliminate(v)) {
|
||||
m_num_elim_vars++;
|
||||
}
|
||||
else if (elim_vars_bdd_enabled() && elim_bdd(v)) {
|
||||
|
|
|
@ -163,6 +163,7 @@ namespace sat {
|
|||
void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
|
||||
|
||||
bool is_external(bool_var v) const;
|
||||
bool is_external(literal l) const { return is_external(l.var()); }
|
||||
bool was_eliminated(bool_var v) const;
|
||||
lbool value(bool_var v) const;
|
||||
lbool value(literal l) const;
|
||||
|
|
|
@ -904,6 +904,11 @@ namespace sat {
|
|||
propagate(false);
|
||||
if (check_inconsistent()) return l_false;
|
||||
cleanup();
|
||||
if (m_config.m_gc_burst) {
|
||||
// force gc
|
||||
m_conflicts_since_gc = m_gc_threshold + 1;
|
||||
gc();
|
||||
}
|
||||
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
|
||||
m_restart_threshold = m_config.m_burst_search;
|
||||
lbool r = bounded_search();
|
||||
|
@ -1326,6 +1331,7 @@ namespace sat {
|
|||
void solver::add_assumption(literal lit) {
|
||||
m_assumption_set.insert(lit);
|
||||
m_assumptions.push_back(lit);
|
||||
VERIFY(is_external(lit.var()));
|
||||
}
|
||||
|
||||
void solver::pop_assumption() {
|
||||
|
@ -1438,14 +1444,12 @@ namespace sat {
|
|||
CASSERT("sat_simplify_bug", check_invariant());
|
||||
}
|
||||
|
||||
|
||||
if (m_config.m_lookahead_simplify) {
|
||||
lookahead lh(*this);
|
||||
lh.simplify();
|
||||
lh.collect_statistics(m_aux_stats);
|
||||
}
|
||||
|
||||
|
||||
sort_watch_lits();
|
||||
CASSERT("sat_simplify_bug", check_invariant());
|
||||
|
||||
|
@ -1585,6 +1589,8 @@ namespace sat {
|
|||
}
|
||||
for (literal l : m_assumptions) {
|
||||
if (value_at(l, m) != l_true) {
|
||||
VERIFY(is_external(l.var()));
|
||||
IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";);
|
||||
TRACE("sat",
|
||||
tout << l << " does not model check\n";
|
||||
tout << "trail: " << m_trail << "\n";
|
||||
|
@ -1641,7 +1647,7 @@ namespace sat {
|
|||
void solver::gc() {
|
||||
if (m_conflicts_since_gc <= m_gc_threshold)
|
||||
return;
|
||||
IF_VERBOSE(1, verbose_stream() << "gc\n";);
|
||||
IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";);
|
||||
CASSERT("sat_gc_bug", check_invariant());
|
||||
switch (m_config.m_gc_strategy) {
|
||||
case GC_GLUE:
|
||||
|
@ -2099,6 +2105,7 @@ namespace sat {
|
|||
|
||||
pop_reinit(m_scope_lvl - new_scope_lvl);
|
||||
TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout););
|
||||
// unsound: m_asymm_branch.minimize(m_scc, m_lemma);
|
||||
clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
|
||||
if (lemma) {
|
||||
lemma->set_glue(glue);
|
||||
|
|
|
@ -263,6 +263,7 @@ namespace sat {
|
|||
unsigned num_clauses() const;
|
||||
unsigned num_restarts() const { return m_restarts; }
|
||||
bool is_external(bool_var v) const { return m_external[v] != 0; }
|
||||
bool is_external(literal l) const { return is_external(l.var()); }
|
||||
void set_external(bool_var v);
|
||||
void set_non_external(bool_var v);
|
||||
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
|
||||
|
@ -305,6 +306,7 @@ namespace sat {
|
|||
bool canceled() { return !m_rlimit.inc(); }
|
||||
config const& get_config() const { return m_config; }
|
||||
void set_incremental(bool b) { m_config.m_incremental = b; }
|
||||
bool is_incremental() const { return m_config.m_incremental; }
|
||||
extension* get_extension() const { return m_ext.get(); }
|
||||
void set_extension(extension* e);
|
||||
bool set_root(literal l, literal r);
|
||||
|
|
|
@ -251,15 +251,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr* e) {
|
||||
dep2asm_t dep2asm;
|
||||
goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
|
||||
for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
|
||||
g->assert_expr(m_fmls[i].get());
|
||||
}
|
||||
VERIFY(l_undef != internalize_goal(g, dep2asm, true));
|
||||
}
|
||||
|
||||
virtual ast_manager& get_manager() const { return m; }
|
||||
virtual void assert_expr_core(expr * t) {
|
||||
m_internalized = false;
|
||||
|
@ -526,7 +517,7 @@ private:
|
|||
m_pc = g->pc();
|
||||
m_mc = g->mc();
|
||||
TRACE("sat", g->display_with_dependencies(tout););
|
||||
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, false, is_lemma);
|
||||
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, m_solver.get_config().m_incremental, is_lemma);
|
||||
m_goal2sat.get_interpreted_atoms(atoms);
|
||||
if (!atoms.empty()) {
|
||||
std::stringstream strm;
|
||||
|
|
|
@ -114,10 +114,6 @@ namespace smt {
|
|||
m_name2assertion.insert(a, t);
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr* t) {
|
||||
// no-op
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
m_context.push();
|
||||
}
|
||||
|
|
|
@ -180,12 +180,6 @@ public:
|
|||
m_solver2->assert_expr(t, a);
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr* t) {
|
||||
m_solver1->assert_lemma(t);
|
||||
if (m_solver2_initialized)
|
||||
m_solver2->assert_lemma(t);
|
||||
}
|
||||
|
||||
virtual void push() {
|
||||
switch_inc_mode();
|
||||
m_solver1->push();
|
||||
|
|
|
@ -104,12 +104,6 @@ public:
|
|||
|
||||
virtual void assert_expr_core(expr * t, expr * a) = 0;
|
||||
|
||||
/**
|
||||
\brief Add a lemma to the assertion stack. A lemma is assumed to be a consequence of already
|
||||
asserted formulas. The solver is free to ignore lemmas.
|
||||
*/
|
||||
virtual void assert_lemma(expr * t) {}
|
||||
|
||||
/**
|
||||
\brief Create a backtracking point.
|
||||
*/
|
||||
|
|
|
@ -105,10 +105,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr * t) {
|
||||
m_solver->assert_lemma(t);
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
flush_assertions();
|
||||
m_solver->push();
|
||||
|
|
|
@ -68,16 +68,6 @@ public:
|
|||
m_solver->assert_expr(bounds);
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr* t) {
|
||||
expr_ref tmp(t, m);
|
||||
expr_ref_vector bounds(m);
|
||||
proof_ref tmp_proof(m);
|
||||
m_rewriter(t, tmp, tmp_proof);
|
||||
m_solver->assert_lemma(tmp);
|
||||
m_rewriter.flush_side_constraints(bounds);
|
||||
m_solver->assert_expr(bounds);
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
m_rewriter.push();
|
||||
m_solver->push();
|
||||
|
|
|
@ -62,10 +62,6 @@ public:
|
|||
m_assertions.push_back(t);
|
||||
}
|
||||
|
||||
virtual void assert_lemma(expr * t) {
|
||||
m_solver->assert_lemma(t);
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
flush_assertions();
|
||||
m_rewriter.push();
|
||||
|
|
Loading…
Reference in a new issue