mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 14:17:47 +00:00
Code Activity

Add finite_set.lattice_refutation parameter to smt_params_helper.pyg

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-19 01:56:22 +00:00
parent 9d66c844af
commit f04723ca27
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/smt_params_helper.pyg
View file

@ -114,6 +114,7 @@ def_module_params(module_name='smt',
('up.persist_clauses', BOOL, False, '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'),
('finite_set.lattice_refutation', BOOL, True, 'enable lattice refutation for finite set theory'),
('clause_proof', BOOL, False, 'record a clausal proof'), ('clause_proof', BOOL, False, 'record a clausal proof'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'), ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),

6
src/smt/theory_finite_set.cpp
View file

@ -260,7 +260,8 @@ namespace smt {
ctx.push_trail(push_back_vector(m_eqs)); ctx.push_trail(push_back_vector(m_eqs));
m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms
} }
m_lattice_refutation.add_equality(v1, v2); if (ctx.get_fparams().m_finite_set_lattice_refutation)
m_lattice_refutation.add_equality(v1, v2);
// Check if Z3 has a boolean variable for it // Check if Z3 has a boolean variable for it
TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";); TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";);
@ -287,7 +288,8 @@ namespace smt {
ctx.push_trail(push_back_vector(m_diseqs)); ctx.push_trail(push_back_vector(m_diseqs));
m_axioms.extensionality_axiom(e1, e2); m_axioms.extensionality_axiom(e1, e2);
} }
m_lattice_refutation.add_disequality(v1,v2); if (ctx.get_fparams().m_finite_set_lattice_refutation)
m_lattice_refutation.add_disequality(v1,v2);
} }
// //