From cbbb77bf2c812537eeb2bfeb0fde9cff93d50281 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 May 2019 02:32:39 +0200 Subject: [PATCH] allow for string solver none and empty for #2268 Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- src/smt/smt_setup.cpp | 12 +++++++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 53249e1f0..c76075b68 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -67,7 +67,7 @@ def_module_params(module_name='smt', ('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'), ('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'), ('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'), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 70199f2e6..2e4295d92 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -735,6 +735,13 @@ namespace smt { else if (m_params.m_string_solver == "auto") { 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 { throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); } @@ -901,7 +908,10 @@ namespace smt { setup_seq(); } 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") { if (st.m_has_seq_non_str) {