mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 22:57:51 +00:00
Code Activity

update params

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-19 19:06:06 -08:00
parent 38ce0882db
commit 3d8dd0d783
3 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/smt_params.cpp
View file

@ -51,7 +51,6 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_core_validate = p.core_validate(); m_core_validate = p.core_validate();
m_sls_enable = p.sls_enable(); m_sls_enable = p.sls_enable();
m_sls_parallel = p.sls_parallel(); m_sls_parallel = p.sls_parallel();
m_finite_set_lattice_refutation = p.finite_set_lattice_refutation();
m_logic = _p.get_sym("logic", m_logic); m_logic = _p.get_sym("logic", m_logic);
m_string_solver = p.string_solver(); m_string_solver = p.string_solver();
m_up_persist_clauses = p.up_persist_clauses(); m_up_persist_clauses = p.up_persist_clauses();

1
src/params/smt_params.h
View file

@ -114,7 +114,6 @@ struct smt_params : public preprocessor_params,
symbol m_proof_log; symbol m_proof_log;
bool m_sls_enable = false; bool m_sls_enable = false;
bool m_sls_parallel = true; bool m_sls_parallel = true;
bool m_finite_set_lattice_refutation = true;
// ----------------------------------- // -----------------------------------
// //

1
src/params/smt_params_helper.pyg
View file

@ -114,7 +114,6 @@ 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'),