mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

allow for string solver none and empty for #2268

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-07 02:32:39 +02:00
parent 689818c8bb
commit cbbb77bf2c
2 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -67,7 +67,7 @@ def_module_params(module_name='smt',
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'), ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver) \'empty\' (a no-op solver that forces an answer unknown if strings were used) \'none\' (no solver)'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'), ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),

12
src/smt/smt_setup.cpp
View file

@ -735,6 +735,13 @@ namespace smt {
else if (m_params.m_string_solver == "auto") { else if (m_params.m_string_solver == "auto") {
setup_unknown(); setup_unknown();
} }
else if (m_params.m_string_solver == "empty") {
m_context.register_plugin(alloc(smt::theory_seq_empty, m_manager));
}
else if (m_params.m_string_solver == "none") {
// don't register any solver.
}
else { else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
} }
@ -901,7 +908,10 @@ namespace smt {
setup_seq(); setup_seq();
} }
else if (m_params.m_string_solver == "empty") { else if (m_params.m_string_solver == "empty") {
m_context.register_plugin(alloc(smt::theory_seq_empty, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_seq_empty, m_manager));
}
else if (m_params.m_string_solver == "none") {
// don't register any solver.
} }
else if (m_params.m_string_solver == "auto") { else if (m_params.m_string_solver == "auto") {
if (st.m_has_seq_non_str) { if (st.m_has_seq_non_str) {