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

Merge pull request #1000 from mtrberzi/theory_str-smt-setup

Browse source 
smt_setup for strings/sequences
This commit is contained in:
Nikolaj Bjorner 2017-05-02 20:44:23 -07:00 committed by GitHub
parent cc7a176c89 92755b0185
commit 52dfdedb9b
7 changed files with 53 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/params/smt_params.cpp
View file

@ -40,6 +40,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_max_conflicts = p.max_conflicts();
m_core_validate = p.core_validate();
m_logic = _p.get_sym("logic", m_logic);
m_string_solver = p.string_solver();
model_params mp(_p);
m_model_compact = mp.compact();
if (_p.get_bool("arith.greatest_error_pivot", false))

10
src/smt/params/smt_params.h
View file

@ -214,6 +214,13 @@ struct smt_params : public preprocessor_params,
bool m_dump_goal_as_smt;
bool m_auto_config;
// -----------------------------------
//
// Solver selection
//
// -----------------------------------
symbol m_string_solver;
smt_params(params_ref const & p = params_ref()):
m_display_proof(false),
m_display_dot_proof(false),
@ -282,7 +289,8 @@ struct smt_params : public preprocessor_params,
m_at_labels_cex(false),
m_check_at_labels(false),
m_dump_goal_as_smt(false),
m_auto_config(true) {
m_auto_config(true),
m_string_solver(symbol("seq")){
updt_local_params(p);
}

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

@ -62,6 +62,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)'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),

38
src/smt/smt_setup.cpp
View file

@ -120,6 +120,8 @@ namespace smt {
setup_QF_FP();
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
setup_QF_FPBV();
else if (m_logic == "QF_S")
setup_QF_S();
else
setup_unknown();
}
@ -161,6 +163,8 @@ namespace smt {
setup_QF_BVRE();
else if (m_logic == "QF_AUFLIA")
setup_QF_AUFLIA(st);
else if (m_logic == "QF_S")
setup_QF_S();
else if (m_logic == "AUFLIA")
setup_AUFLIA(st);
else if (m_logic == "AUFLIRA")
@ -201,7 +205,7 @@ namespace smt {
void setup::setup_QF_BVRE() {
setup_QF_BV();
setup_QF_LIA();
setup_seq();
m_context.register_plugin(alloc(theory_seq, m_manager));
}
void setup::setup_QF_UF(static_features const & st) {
@ -700,6 +704,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
}
void setup::setup_QF_S() {
m_context.register_plugin(alloc(smt::theory_seq, m_manager));
}
bool is_arith(static_features const & st) {
return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0;
}
@ -814,8 +822,21 @@ namespace smt {
m_context.register_plugin(mk_theory_dl(m_manager));
}
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq, m_manager));
void setup::setup_seq(static_features const & st) {
// check params for what to do here when it's ambiguous
if (m_params.m_string_solver == "z3str3") {
setup_str();
} else if (m_params.m_string_solver == "seq") {
m_context.register_plugin(alloc(smt::theory_seq, m_manager));
} else if (m_params.m_string_solver == "auto") {
if (st.m_has_seq_non_str) {
m_context.register_plugin(alloc(smt::theory_seq, m_manager));
} else {
setup_str();
}
} else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
}
}
void setup::setup_card() {
@ -827,13 +848,20 @@ namespace smt {
m_context.register_plugin(alloc(theory_fpa, m_manager));
}
void setup::setup_str() {
m_context.register_plugin(alloc(smt::theory_seq, m_manager));
}
void setup::setup_unknown() {
static_features st(m_manager);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
setup_arith();
setup_arrays();
setup_bv();
setup_datatypes();
setup_dl();
setup_seq();
setup_seq(st);
setup_card();
setup_fpa();
}
@ -848,7 +876,7 @@ namespace smt {
setup_datatypes();
setup_bv();
setup_dl();
setup_seq();
setup_seq(st);
setup_card();
setup_fpa();
return;

4
src/smt/smt_setup.h
View file

@ -77,6 +77,7 @@ namespace smt {
void setup_QF_AUFLIA(static_features const & st);
void setup_QF_FP();
void setup_QF_FPBV();
void setup_QF_S();
void setup_LRA();
void setup_AUFLIA(bool simple_array = true);
void setup_AUFLIA(static_features const & st);
@ -93,11 +94,12 @@ namespace smt {
void setup_bv();
void setup_arith();
void setup_dl();
void setup_seq();
void setup_seq(static_features const & st);
void setup_card();
void setup_i_arith();
void setup_mi_arith();
void setup_fpa();
void setup_str();
public:
setup(context & c, smt_params & params);

6
src/solver/smt_logics.cpp
View file

@ -24,7 +24,7 @@ Revision History:
bool smt_logics::supported_logic(symbol const & s) {
return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) ||
logic_has_arith(s) || logic_has_bv(s) ||
logic_has_array(s) || logic_has_seq(s) ||
logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
logic_has_horn(s) || logic_has_fpa(s);
}
@ -132,6 +132,10 @@ bool smt_logics::logic_has_seq(symbol const & s) {
return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
}
bool smt_logics::logic_has_str(symbol const & s) {
return s == "QF_S" || s == "ALL";
}
bool smt_logics::logic_has_fpa(symbol const & s) {
return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
}

1
src/solver/smt_logics.h
View file

@ -30,6 +30,7 @@ public:
static bool logic_has_bv(symbol const & s);
static bool logic_has_array(symbol const & s);
static bool logic_has_seq(symbol const & s);
static bool logic_has_str(symbol const & s);
static bool logic_has_fpa(symbol const & s);
static bool logic_has_horn(symbol const& s);
static bool logic_has_pb(symbol const& s);