mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
afc4c700b1
commit
cfcd7f18a9
|
@ -49,7 +49,6 @@ extern "C" {
|
|||
LOG_Z3_mk_string(c, str);
|
||||
RESET_ERROR_CODE();
|
||||
zstring s(str);
|
||||
std::cout << "mk-string " << str << "\n";
|
||||
app* a = mk_c(c)->sutil().str.mk_string(s);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
|
|
|
@ -721,6 +721,10 @@ namespace smt {
|
|||
else if (m_params.m_string_solver == "seq") {
|
||||
setup_unknown();
|
||||
}
|
||||
else if (m_params.m_string_solver == "char") {
|
||||
setup_QF_BV();
|
||||
setup_char();
|
||||
}
|
||||
else if (m_params.m_string_solver == "auto") {
|
||||
setup_unknown();
|
||||
}
|
||||
|
|
|
@ -770,7 +770,7 @@ namespace smt {
|
|||
// convert iValue to a constant
|
||||
zstring iValue_str(iValue.to_string());
|
||||
for (unsigned idx = 0; idx < iValue_str.length(); ++idx) {
|
||||
expr_ref chTerm(u.mk_char(iValue_str[idx]), sub_m);
|
||||
expr_ref chTerm(u.mk_char(iValue_str[idx]), m);
|
||||
eqc_chars.push_back(chTerm);
|
||||
}
|
||||
return true;
|
||||
|
@ -908,6 +908,7 @@ namespace smt {
|
|||
expr_ref_vector abstracted_boolean_formulas(m);
|
||||
|
||||
smt_params subsolver_params;
|
||||
subsolver_params.m_string_solver = symbol("char");
|
||||
smt::kernel subsolver(m, subsolver_params);
|
||||
subsolver.set_logic(symbol("QF_S"));
|
||||
|
||||
|
|
Loading…
Reference in a new issue