mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Fixing #7465 (#7551)

Browse source 
* Fixed bug in UP

* Put decrement at the right position

* Fixed replaying in UP

* Set UP persist clauses to false
This commit is contained in:
Clemens Eisenhofer 2025-02-11 18:20:25 +01:00 committed by GitHub
parent c2b7b58c78
commit acd48b6a30
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params_helper.pyg
View file

@ -103,7 +103,7 @@ def_module_params(module_name='smt',
('arith.print_ext_var_names', BOOL, False, 'print external variable names'), ('arith.print_ext_var_names', BOOL, False, 'print external variable names'),
('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
('up.persist_clauses', BOOL, True, 'replay propagated clauses below the levels they are asserted'), ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'),
('array.weak', BOOL, False, 'weak array theory'), ('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory'), ('array.extensional', BOOL, True, 'extensional array theory'),
('clause_proof', BOOL, False, 'record a clausal proof'), ('clause_proof', BOOL, False, 'record a clausal proof'),

7
src/smt/smt_internalizer.cpp
View file

@ -1142,10 +1142,13 @@ namespace smt {
for (unsigned i = 0; i < num_lits; i++) { for (unsigned i = 0; i < num_lits; i++) {
literal curr = lits[i]; literal curr = lits[i];
lbool val = get_assignment(curr); lbool val = get_assignment(curr);
switch(val) { switch (val) {
case l_false: case l_false:
TRACE("simplify_aux_clause_literals", display_literal_verbose(tout << get_assign_level(curr) << " " << get_scope_level() << " " << curr << ":", curr); tout << "\n"; ); TRACE("simplify_aux_clause_literals", display_literal_verbose(tout << get_assign_level(curr) << " " << get_scope_level() << " " << curr << ":", curr); tout << "\n"; );
simp_lits.push_back(~curr); if (curr != prev) {
prev = curr;
simp_lits.push_back(~curr);
}
break; // ignore literal break; // ignore literal
// fall through // fall through
case l_undef: case l_undef:

12
src/smt/theory_user_propagator.cpp
View file

@ -339,22 +339,20 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
m_lits.push_back(lit); m_lits.push_back(lit);
if (ctx.get_fparams().m_up_persist_clauses)
ctx.mk_th_axiom(get_id(), m_lits);
else
ctx.mk_th_lemma(get_id(), m_lits);
if (ctx.get_fparams().m_up_persist_clauses) { if (ctx.get_fparams().m_up_persist_clauses) {
ctx.mk_th_axiom(get_id(), m_lits);
expr_ref_vector clause(m); expr_ref_vector clause(m);
for (auto lit : m_lits) for (auto l : m_lits)
clause.push_back(ctx.literal2expr(lit)); clause.push_back(ctx.literal2expr(l));
m_clauses_to_replay.push_back(clause); m_clauses_to_replay.push_back(clause);
if (m_replay_qhead + 1 < m_clauses_to_replay.size()) if (m_replay_qhead + 1 < m_clauses_to_replay.size())
std::swap(m_clauses_to_replay[m_replay_qhead], m_clauses_to_replay[m_clauses_to_replay.size()-1]); std::swap(m_clauses_to_replay[m_replay_qhead], m_clauses_to_replay[m_clauses_to_replay.size()-1]);
ctx.push_trail(value_trail<unsigned>(m_replay_qhead)); ctx.push_trail(value_trail<unsigned>(m_replay_qhead));
++m_replay_qhead; ++m_replay_qhead;
ctx.mk_th_axiom(get_id(), m_lits);
} }
else
ctx.mk_th_lemma(get_id(), m_lits);
} }
TRACE("user_propagate", ctx.display(tout);); TRACE("user_propagate", ctx.display(tout););