mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Merge remote-tracking branch 'upstream/master' into lackr
This commit is contained in:
Mikolas Janota
commit
c2edf2c5bf
30 changed files with 420 additions and 153 deletions
|
|
@ -76,7 +76,6 @@ namespace api {
|
|||
m_sutil(m()),
|
||||
m_last_result(m()),
|
||||
m_ast_trail(m()),
|
||||
m_replay_stack(),
|
||||
m_pmanager(m_limit) {
|
||||
|
||||
m_error_code = Z3_OK;
|
||||
|
|
@ -100,23 +99,12 @@ namespace api {
|
|||
m_fpa_fid = m().mk_family_id("fpa");
|
||||
m_seq_fid = m().mk_family_id("seq");
|
||||
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
|
||||
|
||||
if (!m_user_ref_count) {
|
||||
m_replay_stack.push_back(0);
|
||||
}
|
||||
|
||||
install_tactics(*this);
|
||||
}
|
||||
|
||||
|
||||
context::~context() {
|
||||
m_last_obj = 0;
|
||||
if (!m_user_ref_count) {
|
||||
for (unsigned i = 0; i < m_replay_stack.size(); ++i) {
|
||||
dealloc(m_replay_stack[i]);
|
||||
}
|
||||
m_ast_trail.reset();
|
||||
}
|
||||
reset_parser();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ namespace api {
|
|||
bv_util m_bv_util;
|
||||
datalog::dl_decl_util m_datalog_util;
|
||||
fpa_util m_fpa_util;
|
||||
datatype_util m_dtutil;
|
||||
datatype_util m_dtutil;
|
||||
seq_util m_sutil;
|
||||
|
||||
// Support for old solver API
|
||||
|
|
@ -67,8 +67,6 @@ namespace api {
|
|||
|
||||
ast_ref_vector m_last_result; //!< used when m_user_ref_count == true
|
||||
ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false
|
||||
unsigned_vector m_ast_lim;
|
||||
ptr_vector<ast_ref_vector> m_replay_stack;
|
||||
|
||||
ref<api::object> m_last_obj; //!< reference to the last API object returned by the APIs
|
||||
|
||||
|
|
@ -123,7 +121,7 @@ namespace api {
|
|||
bv_util & bvutil() { return m_bv_util; }
|
||||
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
|
||||
fpa_util & fpautil() { return m_fpa_util; }
|
||||
datatype_util& dtutil() { return m_dtutil; }
|
||||
datatype_util& dtutil() { return m_dtutil; }
|
||||
seq_util& sutil() { return m_sutil; }
|
||||
family_id get_basic_fid() const { return m_basic_fid; }
|
||||
family_id get_array_fid() const { return m_array_fid; }
|
||||
|
|
@ -181,8 +179,6 @@ namespace api {
|
|||
void interrupt();
|
||||
|
||||
void invoke_error_handler(Z3_error_code c);
|
||||
|
||||
static void out_of_memory_handler(void * _ctx);
|
||||
|
||||
void check_sorts(ast * n);
|
||||
|
||||
|
|
|
|||
|
|
@ -9095,6 +9095,10 @@ def _coerce_seq(s, ctx=None):
|
|||
if isinstance(s, str):
|
||||
ctx = _get_ctx(ctx)
|
||||
s = StringVal(s, ctx)
|
||||
if not is_expr(s):
|
||||
raise Z3Exception("Non-expression passed as a sequence")
|
||||
if not is_seq(s):
|
||||
raise Z3Exception("Non-sequence passed as a sequence")
|
||||
return s
|
||||
|
||||
def _get_ctx2(a, b, ctx=None):
|
||||
|
|
|
|||
|
|
@ -923,7 +923,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
|
|||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
|
||||
expr_ref quotient(m);
|
||||
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext);
|
||||
// b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
|
||||
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext);
|
||||
|
||||
dbg_decouple("fpa2bv_div_quotient", quotient);
|
||||
|
||||
|
|
|
|||
|
|
@ -29,12 +29,27 @@ Notes:
|
|||
expr_ref sym_expr::accept(expr* e) {
|
||||
ast_manager& m = m_t.get_manager();
|
||||
expr_ref result(m);
|
||||
if (m_is_pred) {
|
||||
switch (m_ty) {
|
||||
case t_pred: {
|
||||
var_subst subst(m);
|
||||
subst(m_t, 1, &e, result);
|
||||
break;
|
||||
}
|
||||
else {
|
||||
case t_char:
|
||||
result = m.mk_eq(e, m_t);
|
||||
break;
|
||||
case t_range: {
|
||||
bv_util bv(m);
|
||||
rational r1, r2, r3;
|
||||
unsigned sz;
|
||||
if (bv.is_numeral(m_t, r1, sz) && bv.is_numeral(e, r2, sz) && bv.is_numeral(m_s, r3, sz)) {
|
||||
result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));
|
||||
}
|
||||
else {
|
||||
result = m.mk_and(bv.mk_ule(m_t, e), bv.mk_ule(e, m_s));
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
|
@ -104,8 +119,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _start(bv.mk_numeral(start, nb), m);
|
||||
expr_ref _stop(bv.mk_numeral(stop, nb), m);
|
||||
expr_ref cond(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(cond));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
|
||||
return a.detach();
|
||||
}
|
||||
else {
|
||||
|
|
@ -208,7 +222,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_RE_RANGE:
|
||||
return BR_FAILED;
|
||||
case OP_RE_INTERSECT:
|
||||
return BR_FAILED;
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_inter(args[0], args[1], result);
|
||||
case OP_RE_LOOP:
|
||||
return mk_re_loop(num_args, args, result);
|
||||
case OP_RE_EMPTY_SET:
|
||||
|
|
@ -359,7 +374,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
|
|||
es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
|
||||
}
|
||||
result = m_autil.mk_add(es.size(), es.c_ptr());
|
||||
return BR_DONE;
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
@ -703,7 +718,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
|
|||
void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond) {
|
||||
expr* acc;
|
||||
if (!m().is_true(cond) && next.find(idx, acc)) {
|
||||
cond = m().mk_or(cond, acc);
|
||||
expr* args[2] = { cond, acc };
|
||||
cond = mk_or(m(), 2, args);
|
||||
}
|
||||
trail.push_back(cond);
|
||||
next.insert(idx, cond);
|
||||
|
|
@ -715,8 +731,14 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
|
|||
unsigned state = aut.init();
|
||||
uint_set visited;
|
||||
eautomaton::moves mvs;
|
||||
aut.get_moves_from(state, mvs, true);
|
||||
while (!aut.is_final_state(state)) {
|
||||
unsigned_vector states;
|
||||
aut.get_epsilon_closure(state, states);
|
||||
bool has_final = false;
|
||||
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
|
||||
has_final = aut.is_final_state(states[i]);
|
||||
}
|
||||
aut.get_moves_from(state, mvs, true);
|
||||
while (!has_final) {
|
||||
if (mvs.size() != 1) {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -735,6 +757,12 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
|
|||
state = mvs[0].dst();
|
||||
mvs.reset();
|
||||
aut.get_moves_from(state, mvs, true);
|
||||
states.reset();
|
||||
has_final = false;
|
||||
aut.get_epsilon_closure(state, states);
|
||||
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
|
||||
has_final = aut.is_final_state(states[i]);
|
||||
}
|
||||
}
|
||||
return mvs.empty();
|
||||
}
|
||||
|
|
@ -773,6 +801,14 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
|||
}
|
||||
|
||||
br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
|
||||
if (m_util.re.is_empty(b)) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(b)) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
scoped_ptr<eautomaton> aut;
|
||||
expr_ref_vector seq(m());
|
||||
if (!(aut = m_re2aut(b))) {
|
||||
|
|
@ -817,7 +853,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
|
|||
aut->get_moves_from(state, mvs, false);
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
eautomaton::move const& mv = mvs[j];
|
||||
SASSERT(mv.t());
|
||||
SASSERT(mv.t());
|
||||
if (mv.t()->is_char() && m().is_value(mv.t()->get_char()) && m().is_value(ch)) {
|
||||
if (mv.t()->get_char() == ch) {
|
||||
add_next(next, trail, mv.dst(), acc);
|
||||
|
|
@ -828,7 +864,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
|
|||
}
|
||||
else {
|
||||
cond = mv.t()->accept(ch);
|
||||
if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
|
||||
if (m().is_false(cond)) {
|
||||
continue;
|
||||
}
|
||||
expr* args[2] = { cond, acc };
|
||||
cond = mk_and(m(), 2, args);
|
||||
add_next(next, trail, mv.dst(), cond);
|
||||
}
|
||||
}
|
||||
|
|
@ -856,18 +896,18 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
|
|||
return BR_FAILED;
|
||||
}
|
||||
br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
|
||||
if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(b)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(b)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (is_epsilon(a)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
|
|
@ -916,6 +956,38 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
|
|||
}
|
||||
|
||||
|
||||
/**
|
||||
(emp n r) = emp
|
||||
(r n emp) = emp
|
||||
(all n r) = r
|
||||
(r n all) = r
|
||||
(r n r) = r
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
|
||||
if (a == b) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(b)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(a)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(b)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
||||
br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result) {
|
||||
rational n1, n2;
|
||||
switch (num_args) {
|
||||
|
|
@ -945,13 +1017,26 @@ br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_re
|
|||
(a* + b)* = (a + b)*
|
||||
(a + b*)* = (a + b)*
|
||||
(a*b*)* = (a + b)*
|
||||
a+* = a*
|
||||
emp* = ""
|
||||
all* = all
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
|
||||
expr* b, *c, *b1, *c1;
|
||||
if (m_util.re.is_star(a) || m_util.re.is_empty(a) || m_util.re.is_full(a)) {
|
||||
if (m_util.re.is_star(a) || m_util.re.is_full(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_empty(a)) {
|
||||
sort* seq_sort = 0;
|
||||
VERIFY(m_util.is_re(a, seq_sort));
|
||||
result = m_util.re.mk_to_re(m_util.str.mk_empty(seq_sort));
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_plus(a, b)) {
|
||||
result = m_util.re.mk_star(b);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_union(a, b, c)) {
|
||||
if (m_util.re.is_star(b, b1)) {
|
||||
result = m_util.re.mk_star(m_util.re.mk_union(b1, c));
|
||||
|
|
@ -961,6 +1046,14 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
|
|||
result = m_util.re.mk_star(m_util.re.mk_union(b, c1));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (is_epsilon(b)) {
|
||||
result = m_util.re.mk_star(c);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (is_epsilon(c)) {
|
||||
result = m_util.re.mk_star(b);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
}
|
||||
if (m_util.re.is_concat(a, b, c) &&
|
||||
m_util.re.is_star(b, b1) && m_util.re.is_star(c, c1)) {
|
||||
|
|
@ -972,9 +1065,34 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
|
|||
}
|
||||
|
||||
/*
|
||||
emp+ = emp
|
||||
all+ = all
|
||||
a*+ = a*
|
||||
a++ = a+
|
||||
a+ = aa*
|
||||
*/
|
||||
br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
|
||||
if (m_util.re.is_empty(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_full(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (is_epsilon(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_plus(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.re.is_star(a)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
// result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
|
||||
// return BR_REWRITE2;
|
||||
|
|
@ -1052,14 +1170,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
|
|||
rs.pop_back();
|
||||
}
|
||||
else {
|
||||
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
|
||||
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-1)), m());
|
||||
rs[rs.size()-1] = s2;
|
||||
}
|
||||
}
|
||||
else {
|
||||
break;
|
||||
}
|
||||
TRACE("seq", tout << "change back\n";);
|
||||
change = true;
|
||||
lchange = true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,20 +27,27 @@ Notes:
|
|||
#include"automaton.h"
|
||||
|
||||
class sym_expr {
|
||||
bool m_is_pred;
|
||||
enum ty {
|
||||
t_char,
|
||||
t_pred,
|
||||
t_range
|
||||
};
|
||||
ty m_ty;
|
||||
expr_ref m_t;
|
||||
expr_ref m_s;
|
||||
unsigned m_ref;
|
||||
sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), m_ref(0) {}
|
||||
sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {}
|
||||
public:
|
||||
expr_ref accept(expr* e);
|
||||
static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, false, t); }
|
||||
static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return alloc(sym_expr, false, tr); }
|
||||
static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, true, t); }
|
||||
static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); }
|
||||
static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); }
|
||||
static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); }
|
||||
static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); }
|
||||
void inc_ref() { ++m_ref; }
|
||||
void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
bool is_char() const { return !m_is_pred; }
|
||||
bool is_pred() const { return m_is_pred; }
|
||||
bool is_char() const { return m_ty == t_char; }
|
||||
bool is_pred() const { return !is_char(); }
|
||||
expr* get_char() const { SASSERT(is_char()); return m_t; }
|
||||
|
||||
};
|
||||
|
|
@ -88,6 +95,7 @@ class seq_rewriter {
|
|||
br_status mk_str_to_regexp(expr* a, expr_ref& result);
|
||||
br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_union(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
|
||||
br_status mk_re_star(expr* a, expr_ref& result);
|
||||
br_status mk_re_plus(expr* a, expr_ref& result);
|
||||
br_status mk_re_opt(expr* a, expr_ref& result);
|
||||
|
|
|
|||
|
|
@ -612,9 +612,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
|
||||
|
||||
case OP_RE_UNION:
|
||||
return mk_assoc_fun(k, arity, domain, range, k, k);
|
||||
|
||||
case OP_RE_CONCAT:
|
||||
case OP_RE_INTERSECT:
|
||||
return mk_assoc_fun(k, arity, domain, range, k, k);
|
||||
|
||||
case OP_SEQ_CONCAT:
|
||||
|
|
|
|||
|
|
@ -268,6 +268,7 @@ public:
|
|||
MATCH_TERNARY(is_extract);
|
||||
MATCH_BINARY(is_contains);
|
||||
MATCH_BINARY(is_at);
|
||||
MATCH_BINARY(is_index);
|
||||
MATCH_TERNARY(is_index);
|
||||
MATCH_TERNARY(is_replace);
|
||||
MATCH_BINARY(is_prefix);
|
||||
|
|
|
|||
|
|
@ -43,6 +43,8 @@ Notes:
|
|||
#include"model_smt2_pp.h"
|
||||
#include"model_v2_pp.h"
|
||||
#include"model_params.hpp"
|
||||
#include"th_rewriter.h"
|
||||
#include"tactic_exception.h"
|
||||
|
||||
func_decls::func_decls(ast_manager & m, func_decl * f):
|
||||
m_decls(TAG(func_decl*, f, 0)) {
|
||||
|
|
@ -1462,7 +1464,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
throw ex;
|
||||
}
|
||||
catch (z3_exception & ex) {
|
||||
throw cmd_exception(ex.msg());
|
||||
m_solver->set_reason_unknown(ex.msg());
|
||||
r = l_undef;
|
||||
}
|
||||
m_solver->set_status(r);
|
||||
}
|
||||
|
|
@ -1624,6 +1627,7 @@ void cmd_context::validate_model() {
|
|||
TRACE("model_validate", tout << "checking\n" << mk_ismt2_pp(a, m()) << "\nresult:\n" << mk_ismt2_pp(r, m()) << "\n";);
|
||||
if (m().is_true(r))
|
||||
continue;
|
||||
|
||||
// The evaluator for array expressions is not complete
|
||||
// If r contains as_array/store/map/const expressions, then we do not generate the error.
|
||||
// TODO: improve evaluator for model expressions.
|
||||
|
|
|
|||
|
|
@ -105,6 +105,8 @@ public:
|
|||
// create an automaton from initial state, final states, and moves
|
||||
automaton(M& m, unsigned init, unsigned_vector const& final, moves const& mvs): m(m) {
|
||||
m_init = init;
|
||||
m_delta.push_back(moves());
|
||||
m_delta_inv.push_back(moves());
|
||||
for (unsigned i = 0; i < final.size(); ++i) {
|
||||
add_to_final_states(final[i]);
|
||||
}
|
||||
|
|
@ -331,6 +333,7 @@ public:
|
|||
// Src - ET -> dst - e -> dst1 => Src - ET -> dst1 if out_degree(dst) = 1,
|
||||
//
|
||||
void compress() {
|
||||
SASSERT(!m_delta.empty());
|
||||
for (unsigned i = 0; i < m_delta.size(); ++i) {
|
||||
for (unsigned j = 0; j < m_delta[i].size(); ++j) {
|
||||
move const& mv = m_delta[i][j];
|
||||
|
|
@ -419,6 +422,7 @@ public:
|
|||
}
|
||||
}
|
||||
}
|
||||
SASSERT(!m_delta.empty());
|
||||
while (true) {
|
||||
SASSERT(!m_delta.empty());
|
||||
unsigned src = m_delta.size() - 1;
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
#include"arith_rewriter.h"
|
||||
#include"bv_rewriter.h"
|
||||
#include"pb_rewriter.h"
|
||||
#include"seq_rewriter.h"
|
||||
#include"datatype_rewriter.h"
|
||||
#include"array_rewriter.h"
|
||||
#include"fpa_rewriter.h"
|
||||
|
|
@ -39,6 +40,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
datatype_rewriter m_dt_rw;
|
||||
pb_rewriter m_pb_rw;
|
||||
fpa_rewriter m_f_rw;
|
||||
seq_rewriter m_seq_rw;
|
||||
unsigned long long m_max_memory;
|
||||
unsigned m_max_steps;
|
||||
bool m_model_completion;
|
||||
|
|
@ -55,7 +57,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
m_ar_rw(m, p),
|
||||
m_dt_rw(m),
|
||||
m_pb_rw(m),
|
||||
m_f_rw(m) {
|
||||
m_f_rw(m),
|
||||
m_seq_rw(m) {
|
||||
m_b_rw.set_flat(false);
|
||||
m_a_rw.set_flat(false);
|
||||
m_bv_rw.set_flat(false);
|
||||
|
|
@ -139,6 +142,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
st = m_dt_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_f_rw.get_fid())
|
||||
st = m_f_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_seq_rw.get_fid())
|
||||
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
}
|
||||
|
|
@ -157,6 +162,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
|||
st = m_pb_rw.mk_app_core(f, num, args, result);
|
||||
else if (fid == m_f_rw.get_fid())
|
||||
st = m_f_rw.mk_app_core(f, num, args, result);
|
||||
else if (fid == m_seq_rw.get_fid())
|
||||
st = m_seq_rw.mk_app_core(f, num, args, result);
|
||||
else if (evaluate(f, num, args, result)) {
|
||||
TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
|
||||
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
|
||||
|
|
|
|||
|
|
@ -132,7 +132,8 @@ namespace opt {
|
|||
m_objective_refs(m),
|
||||
m_enable_sat(false),
|
||||
m_is_clausal(false),
|
||||
m_pp_neat(false)
|
||||
m_pp_neat(false),
|
||||
m_unknown("unknown")
|
||||
{
|
||||
params_ref p;
|
||||
p.set_bool("model", true);
|
||||
|
|
@ -487,7 +488,7 @@ namespace opt {
|
|||
if (m_solver.get()) {
|
||||
return m_solver->reason_unknown();
|
||||
}
|
||||
return std::string("unknown");
|
||||
return m_unknown;
|
||||
}
|
||||
|
||||
void context::display_bounds(std::ostream& out, bounds_t const& b) const {
|
||||
|
|
|
|||
|
|
@ -163,6 +163,7 @@ namespace opt {
|
|||
symbol m_maxsat_engine;
|
||||
symbol m_logic;
|
||||
svector<symbol> m_labels;
|
||||
std::string m_unknown;
|
||||
public:
|
||||
context(ast_manager& m);
|
||||
virtual ~context();
|
||||
|
|
@ -184,6 +185,7 @@ namespace opt {
|
|||
virtual void get_labels(svector<symbol> & r);
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r) {}
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
|
||||
|
||||
virtual void display_assignment(std::ostream& out);
|
||||
virtual bool is_pareto() { return m_pareto.get() != 0; }
|
||||
|
|
|
|||
|
|
@ -290,6 +290,10 @@ namespace opt {
|
|||
std::string opt_solver::reason_unknown() const {
|
||||
return m_context.last_failure_as_string();
|
||||
}
|
||||
|
||||
void opt_solver::set_reason_unknown(char const* msg) {
|
||||
m_context.set_reason_unknown(msg);
|
||||
}
|
||||
|
||||
void opt_solver::get_labels(svector<symbol> & r) {
|
||||
r.reset();
|
||||
|
|
|
|||
|
|
@ -99,6 +99,7 @@ namespace opt {
|
|||
virtual void get_model(model_ref & _m);
|
||||
virtual proof * get_proof();
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void set_reason_unknown(char const* msg);
|
||||
virtual void get_labels(svector<symbol> & r);
|
||||
virtual void set_progress_callback(progress_callback * callback);
|
||||
virtual unsigned get_num_assertions() const;
|
||||
|
|
|
|||
|
|
@ -432,8 +432,10 @@ namespace smt2 {
|
|||
}
|
||||
}
|
||||
|
||||
void unknown_sort(symbol id) {
|
||||
std::string msg = "unknown sort '";
|
||||
void unknown_sort(symbol id, char const* context = "") {
|
||||
std::string msg = context;
|
||||
if (context[0]) msg += ": ";
|
||||
msg += "unknown sort '";
|
||||
msg += id.str() + "'";
|
||||
throw parser_exception(msg.c_str());
|
||||
}
|
||||
|
|
@ -528,12 +530,12 @@ namespace smt2 {
|
|||
SASSERT(sexpr_stack().size() == stack_pos + 1);
|
||||
}
|
||||
|
||||
sort * parse_sort_name() {
|
||||
sort * parse_sort_name(char const* context = "") {
|
||||
SASSERT(curr_is_identifier());
|
||||
symbol id = curr_id();
|
||||
psort_decl * d = m_ctx.find_psort_decl(id);
|
||||
if (d == 0)
|
||||
unknown_sort(id);
|
||||
unknown_sort(id, context);
|
||||
if (!d->has_var_params() && d->get_num_params() != 0)
|
||||
throw parser_exception("sort constructor expects parameters");
|
||||
sort * r = d->instantiate(pm());
|
||||
|
|
@ -689,23 +691,24 @@ namespace smt2 {
|
|||
next();
|
||||
}
|
||||
|
||||
void parse_sort() {
|
||||
void parse_sort(char const* context) {
|
||||
unsigned stack_pos = sort_stack().size();
|
||||
unsigned num_frames = 0;
|
||||
do {
|
||||
if (curr_is_identifier()) {
|
||||
sort_stack().push_back(parse_sort_name());
|
||||
sort_stack().push_back(parse_sort_name(context));
|
||||
}
|
||||
else if (curr_is_rparen()) {
|
||||
if (num_frames == 0)
|
||||
throw parser_exception("invalid sort, unexpected ')'");
|
||||
if (num_frames == 0) {
|
||||
throw parser_exception(std::string(context) + " invalid sort, unexpected ')'");
|
||||
}
|
||||
pop_sort_app_frame();
|
||||
num_frames--;
|
||||
}
|
||||
else {
|
||||
check_lparen_next("invalid sort, symbol, '_' or '(' expected");
|
||||
if (!curr_is_identifier())
|
||||
throw parser_exception("invalid sort, symbol or '_' expected");
|
||||
throw parser_exception(std::string(context) + " invalid sort, symbol or '_' expected");
|
||||
if (curr_id_is_underscore()) {
|
||||
sort_stack().push_back(parse_indexed_sort());
|
||||
}
|
||||
|
|
@ -723,7 +726,7 @@ namespace smt2 {
|
|||
unsigned sz = 0;
|
||||
check_lparen_next(context);
|
||||
while (!curr_is_rparen()) {
|
||||
parse_sort();
|
||||
parse_sort(context);
|
||||
sz++;
|
||||
}
|
||||
next();
|
||||
|
|
@ -1151,7 +1154,7 @@ namespace smt2 {
|
|||
symbol_stack().push_back(curr_id());
|
||||
TRACE("parse_sorted_vars", tout << "push_back curr_id(): " << curr_id() << "\n";);
|
||||
next();
|
||||
parse_sort();
|
||||
parse_sort("invalid sorted variables");
|
||||
check_rparen_next("invalid sorted variable, ')' expected");
|
||||
num++;
|
||||
}
|
||||
|
|
@ -1243,7 +1246,7 @@ namespace smt2 {
|
|||
has_as = true;
|
||||
next();
|
||||
symbol r = parse_indexed_identifier();
|
||||
parse_sort();
|
||||
parse_sort("Invalid qualified identifier");
|
||||
check_rparen_next("invalid qualified identifier, ')' expected");
|
||||
return r;
|
||||
}
|
||||
|
|
@ -1848,7 +1851,7 @@ namespace smt2 {
|
|||
unsigned sort_spos = sort_stack().size();
|
||||
unsigned expr_spos = expr_stack().size();
|
||||
unsigned num_vars = parse_sorted_vars();
|
||||
parse_sort();
|
||||
parse_sort("Invalid function definition");
|
||||
parse_expr();
|
||||
if (m().get_sort(expr_stack().back()) != sort_stack().back())
|
||||
throw parser_exception("invalid function/constant definition, sort mismatch");
|
||||
|
|
@ -1936,7 +1939,7 @@ namespace smt2 {
|
|||
unsigned expr_spos = expr_stack().size();
|
||||
unsigned num_vars = parse_sorted_vars();
|
||||
SASSERT(num_vars == m_num_bindings);
|
||||
parse_sort();
|
||||
parse_sort("Invalid recursive function definition");
|
||||
f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back());
|
||||
bindings.append(num_vars, expr_stack().c_ptr() + expr_spos);
|
||||
ids.append(num_vars, symbol_stack().c_ptr() + sym_spos);
|
||||
|
|
@ -1999,7 +2002,7 @@ namespace smt2 {
|
|||
check_identifier("invalid constant definition, symbol expected");
|
||||
symbol id = curr_id();
|
||||
next();
|
||||
parse_sort();
|
||||
parse_sort("Invalid constant definition");
|
||||
parse_expr();
|
||||
if (m().get_sort(expr_stack().back()) != sort_stack().back())
|
||||
throw parser_exception("invalid constant definition, sort mismatch");
|
||||
|
|
@ -2020,7 +2023,7 @@ namespace smt2 {
|
|||
next();
|
||||
unsigned spos = sort_stack().size();
|
||||
unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('");
|
||||
parse_sort();
|
||||
parse_sort("Invalid function declaration");
|
||||
func_decl_ref f(m());
|
||||
f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back());
|
||||
sort_stack().shrink(spos);
|
||||
|
|
@ -2037,7 +2040,7 @@ namespace smt2 {
|
|||
check_identifier("invalid constant declaration, symbol expected");
|
||||
symbol id = curr_id();
|
||||
next();
|
||||
parse_sort();
|
||||
parse_sort("Invalid constant declaration");
|
||||
SASSERT(!sort_stack().empty());
|
||||
func_decl_ref c(m());
|
||||
c = m().mk_const_decl(id, sort_stack().back());
|
||||
|
|
@ -2300,9 +2303,9 @@ namespace smt2 {
|
|||
next();
|
||||
}
|
||||
unsigned spos = sort_stack().size();
|
||||
parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name");
|
||||
parse_sorts("Invalid function name. Expecting sort list startig with '(' to disambiguate function name");
|
||||
unsigned domain_size = sort_stack().size() - spos;
|
||||
parse_sort();
|
||||
parse_sort("Invalid function name");
|
||||
func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back());
|
||||
sort_stack().shrink(spos);
|
||||
check_rparen_next("invalid function declaration reference, ')' expected");
|
||||
|
|
@ -2375,7 +2378,7 @@ namespace smt2 {
|
|||
break;
|
||||
}
|
||||
case CPK_SORT:
|
||||
parse_sort();
|
||||
parse_sort("invalid command argument, sort expected");
|
||||
m_curr_cmd->set_next_arg(m_ctx, sort_stack().back());
|
||||
return;
|
||||
case CPK_SORT_LIST: {
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ namespace smt2 {
|
|||
}
|
||||
m_spos++;
|
||||
}
|
||||
|
||||
|
||||
void scanner::read_comment() {
|
||||
SASSERT(curr() == ';');
|
||||
next();
|
||||
|
|
@ -62,7 +62,7 @@ namespace smt2 {
|
|||
next();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::read_quoted_symbol() {
|
||||
SASSERT(curr() == '|');
|
||||
bool escape = false;
|
||||
|
|
@ -105,7 +105,7 @@ namespace smt2 {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::read_symbol() {
|
||||
SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':' || curr() == '-');
|
||||
m_string.reset();
|
||||
|
|
@ -113,14 +113,14 @@ namespace smt2 {
|
|||
next();
|
||||
return read_symbol_core();
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::read_number() {
|
||||
SASSERT('0' <= curr() && curr() <= '9');
|
||||
rational q(1);
|
||||
m_number = rational(curr() - '0');
|
||||
next();
|
||||
bool is_float = false;
|
||||
|
||||
|
||||
while (true) {
|
||||
char c = curr();
|
||||
if ('0' <= c && c <= '9') {
|
||||
|
|
@ -139,7 +139,7 @@ namespace smt2 {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (is_float)
|
||||
if (is_float)
|
||||
m_number /= q;
|
||||
TRACE("scanner", tout << "new number: " << m_number << "\n";);
|
||||
return is_float ? FLOAT_TOKEN : INT_TOKEN;
|
||||
|
|
@ -160,14 +160,14 @@ namespace smt2 {
|
|||
return read_symbol_core();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::read_string() {
|
||||
SASSERT(curr() == '\"');
|
||||
next();
|
||||
m_string.reset();
|
||||
while (true) {
|
||||
char c = curr();
|
||||
if (c == EOF)
|
||||
if (c == EOF)
|
||||
throw scanner_exception("unexpected end of string", m_line, m_spos);
|
||||
if (c == '\n') {
|
||||
new_line();
|
||||
|
|
@ -183,7 +183,7 @@ namespace smt2 {
|
|||
next();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::read_bv_literal() {
|
||||
SASSERT(curr() == '#');
|
||||
next();
|
||||
|
|
@ -200,7 +200,7 @@ namespace smt2 {
|
|||
}
|
||||
else if ('a' <= c && c <= 'f') {
|
||||
m_number *= rational(16);
|
||||
m_number += rational(10 + (c - 'a'));
|
||||
m_number += rational(10 + (c - 'a'));
|
||||
}
|
||||
else if ('A' <= c && c <= 'F') {
|
||||
m_number *= rational(16);
|
||||
|
|
@ -236,9 +236,9 @@ namespace smt2 {
|
|||
throw scanner_exception("invalid bit-vector literal, expecting 'x' or 'b'", m_line, m_spos);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
|
||||
m_interactive(interactive),
|
||||
m_interactive(interactive),
|
||||
m_spos(0),
|
||||
m_curr(0), // avoid Valgrind warning
|
||||
m_line(1),
|
||||
|
|
@ -248,7 +248,7 @@ namespace smt2 {
|
|||
m_bend(0),
|
||||
m_stream(stream),
|
||||
m_cache_input(false) {
|
||||
|
||||
|
||||
m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
|
||||
|
||||
for (int i = 0; i < 256; ++i) {
|
||||
|
|
@ -287,7 +287,7 @@ namespace smt2 {
|
|||
m_normalized[static_cast<int>('/')] = 'a';
|
||||
next();
|
||||
}
|
||||
|
||||
|
||||
scanner::token scanner::scan() {
|
||||
while (true) {
|
||||
signed char c = curr();
|
||||
|
|
|
|||
|
|
@ -60,6 +60,8 @@ class inc_sat_solver : public solver {
|
|||
model_converter_ref m_mc2;
|
||||
expr_dependency_ref m_dep_core;
|
||||
svector<double> m_weights;
|
||||
std::string m_unknown;
|
||||
|
||||
|
||||
typedef obj_map<expr, sat::literal> dep2asm_t;
|
||||
public:
|
||||
|
|
@ -73,7 +75,8 @@ public:
|
|||
m_map(m),
|
||||
m_bb_rewriter(m, p),
|
||||
m_num_scopes(0),
|
||||
m_dep_core(m) {
|
||||
m_dep_core(m),
|
||||
m_unknown("no reason given") {
|
||||
m_params.set_bool("elim_vars", false);
|
||||
m_solver.updt_params(m_params);
|
||||
params_ref simp2_p = p;
|
||||
|
|
@ -243,8 +246,12 @@ public:
|
|||
UNREACHABLE();
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual std::string reason_unknown() const {
|
||||
return "no reason given";
|
||||
return m_unknown;
|
||||
}
|
||||
virtual void set_reason_unknown(char const* msg) {
|
||||
m_unknown = msg;
|
||||
}
|
||||
virtual void get_labels(svector<symbol> & r) {
|
||||
}
|
||||
|
|
|
|||
|
|
@ -72,6 +72,7 @@ namespace smt {
|
|||
m_not_l(null_literal),
|
||||
m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
|
||||
m_unsat_proof(m),
|
||||
m_unknown("unknown"),
|
||||
m_unsat_core(m),
|
||||
#ifdef Z3DEBUG
|
||||
m_trail_enabled(true),
|
||||
|
|
@ -4110,8 +4111,7 @@ namespace smt {
|
|||
m_fingerprints.display(tout);
|
||||
);
|
||||
failure fl = get_last_search_failure();
|
||||
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
|
||||
// don't generate model.
|
||||
if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS) {
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
@ -4126,7 +4126,6 @@ namespace smt {
|
|||
if (m_fparams.m_model_compact)
|
||||
m_proto_model->compress();
|
||||
TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
|
||||
//SASSERT(validate_model());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -71,6 +71,7 @@ namespace smt {
|
|||
|
||||
std::ostream& display_last_failure(std::ostream& out) const;
|
||||
std::string last_failure_as_string() const;
|
||||
void set_reason_unknown(char const* msg) { m_unknown = msg; }
|
||||
void set_progress_callback(progress_callback *callback);
|
||||
|
||||
|
||||
|
|
@ -197,6 +198,7 @@ namespace smt {
|
|||
// -----------------------------------
|
||||
proto_model_ref m_proto_model;
|
||||
model_ref m_model;
|
||||
std::string m_unknown;
|
||||
void mk_proto_model(lbool r);
|
||||
struct scoped_mk_model;
|
||||
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ namespace smt {
|
|||
std::string context::last_failure_as_string() const {
|
||||
std::string r;
|
||||
switch(m_last_search_failure) {
|
||||
case OK: r = "ok"; break;
|
||||
case OK: r = m_unknown; break;
|
||||
case TIMEOUT: r = "timeout"; break;
|
||||
case MEMOUT: r = "memout"; break;
|
||||
case CANCELED: r = "canceled"; break;
|
||||
|
|
@ -79,7 +79,7 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
|
||||
case UNKNOWN: r = "incomplete"; break;
|
||||
case UNKNOWN: r = m_unknown; break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -238,7 +238,7 @@ namespace smt {
|
|||
out << "equivalence classes:\n";
|
||||
first = false;
|
||||
}
|
||||
out << "#" << n->get_id() << " -> #" << r->get_id() << "\n";
|
||||
out << "#" << n->get_id() << " -> #" << r->get_id() << ": ";
|
||||
out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -123,6 +123,10 @@ namespace smt {
|
|||
return m_kernel.last_failure_as_string();
|
||||
}
|
||||
|
||||
void set_reason_unknown(char const* msg) {
|
||||
m_kernel.set_reason_unknown(msg);
|
||||
}
|
||||
|
||||
void get_assignments(expr_ref_vector & result) {
|
||||
m_kernel.get_assignments(result);
|
||||
}
|
||||
|
|
@ -284,6 +288,10 @@ namespace smt {
|
|||
return m_imp->last_failure_as_string();
|
||||
}
|
||||
|
||||
void kernel::set_reason_unknown(char const* msg) {
|
||||
m_imp->set_reason_unknown(msg);
|
||||
}
|
||||
|
||||
void kernel::get_assignments(expr_ref_vector & result) {
|
||||
m_imp->get_assignments(result);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -155,6 +155,12 @@ namespace smt {
|
|||
*/
|
||||
std::string last_failure_as_string() const;
|
||||
|
||||
|
||||
/**
|
||||
\brief Set the reason for unknown.
|
||||
*/
|
||||
void set_reason_unknown(char const* msg);
|
||||
|
||||
/**
|
||||
\brief Return the set of formulas assigned by the kernel.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -95,6 +95,10 @@ namespace smt {
|
|||
return m_context.last_failure_as_string();
|
||||
}
|
||||
|
||||
virtual void set_reason_unknown(char const* msg) {
|
||||
m_context.set_reason_unknown(msg);
|
||||
}
|
||||
|
||||
virtual void get_labels(svector<symbol> & r) {
|
||||
buffer<symbol> tmp;
|
||||
m_context.get_relevant_labels(0, tmp);
|
||||
|
|
|
|||
|
|
@ -221,6 +221,11 @@ final_check_status theory_seq::final_check_eh() {
|
|||
TRACE("seq", tout << ">>propagate_automata\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (!check_extensionality()) {
|
||||
++m_stats.m_extensionality;
|
||||
TRACE("seq", tout << ">>extensionality\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (is_solved()) {
|
||||
TRACE("seq", tout << ">>is_solved\n";);
|
||||
return FC_DONE;
|
||||
|
|
@ -239,9 +244,9 @@ bool theory_seq::branch_variable() {
|
|||
unsigned k = (i + start) % sz;
|
||||
eq const& e = m_eqs[k];
|
||||
unsigned id = e.id();
|
||||
TRACE("seq", tout << e.ls() << " = " << e.rs() << "\n";);
|
||||
|
||||
s = find_branch_start(2*id);
|
||||
TRACE("seq", tout << s << " " << 2*id << ": " << e.ls() << " = " << e.rs() << "\n";);
|
||||
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
|
||||
insert_branch_start(2*id, s);
|
||||
if (found) {
|
||||
|
|
@ -292,11 +297,14 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
|
|||
|
||||
expr_ref v0(m);
|
||||
v0 = m_util.str.mk_empty(m.get_sort(l));
|
||||
if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr()) && l_false != assume_equality(l, v0)) {
|
||||
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
|
||||
return true;
|
||||
literal_vector lits;
|
||||
if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) {
|
||||
if (l_false != assume_equality(l, v0)) {
|
||||
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
|
||||
return true;
|
||||
}
|
||||
lits.push_back(~mk_eq_empty(l));
|
||||
}
|
||||
// start = 0;
|
||||
for (; start < rs.size(); ++start) {
|
||||
unsigned j = start;
|
||||
SASSERT(!m_util.str.is_concat(rs[j]));
|
||||
|
|
@ -320,11 +328,11 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
|
|||
all_units &= m_util.str.is_unit(rs[j]);
|
||||
}
|
||||
if (all_units) {
|
||||
literal_vector lits;
|
||||
lits.push_back(~mk_eq_empty(l));
|
||||
for (unsigned i = 0; i < rs.size(); ++i) {
|
||||
v0 = mk_concat(i + 1, rs.c_ptr());
|
||||
lits.push_back(~mk_eq(l, v0, false));
|
||||
if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - i - 1, rs.c_ptr() + i + 1)) {
|
||||
v0 = mk_concat(i + 1, rs.c_ptr());
|
||||
lits.push_back(~mk_eq(l, v0, false));
|
||||
}
|
||||
}
|
||||
set_conflict(dep, lits);
|
||||
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
|
||||
|
|
@ -501,11 +509,23 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
|
|||
}
|
||||
|
||||
expr_ref theory_seq::mk_last(expr* s) {
|
||||
zstring str;
|
||||
if (m_util.str.is_string(s, str) && str.length() > 0) {
|
||||
return expr_ref(m_util.str.mk_char(str, str.length()-1), m);
|
||||
}
|
||||
sort* char_sort = 0;
|
||||
VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
|
||||
return mk_skolem(m_seq_last, s, 0, 0, char_sort);
|
||||
}
|
||||
|
||||
expr_ref theory_seq::mk_first(expr* s) {
|
||||
zstring str;
|
||||
if (m_util.str.is_string(s, str) && str.length() > 0) {
|
||||
return expr_ref(m_util.str.mk_string(str.extract(0, str.length()-1)), m);
|
||||
}
|
||||
return mk_skolem(m_seq_first, s);
|
||||
}
|
||||
|
||||
|
||||
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
|
||||
expr* e1, *e2;
|
||||
|
|
@ -541,6 +561,44 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
|
|||
}
|
||||
}
|
||||
|
||||
/*
|
||||
\brief Check extensionality (for sequences).
|
||||
*/
|
||||
bool theory_seq::check_extensionality() {
|
||||
context& ctx = get_context();
|
||||
unsigned sz = get_num_vars();
|
||||
unsigned_vector seqs;
|
||||
for (unsigned v = 0; v < sz; ++v) {
|
||||
enode* n = get_enode(v);
|
||||
expr* o1 = n->get_owner();
|
||||
if (n != n->get_root()) {
|
||||
continue;
|
||||
}
|
||||
if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) {
|
||||
dependency* dep = 0;
|
||||
expr_ref e1 = canonize(o1, dep);
|
||||
for (unsigned i = 0; i < seqs.size(); ++i) {
|
||||
enode* n2 = get_enode(seqs[i]);
|
||||
expr* o2 = n2->get_owner();
|
||||
if (m_exclude.contains(o1, o2)) {
|
||||
continue;
|
||||
}
|
||||
expr_ref e2 = canonize(n2->get_owner(), dep);
|
||||
m_lhs.reset(); m_rhs.reset();
|
||||
bool change = false;
|
||||
if (!m_seq_rewrite.reduce_eq(o1, o2, m_lhs, m_rhs, change)) {
|
||||
m_exclude.update(o1, o2);
|
||||
continue;
|
||||
}
|
||||
TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
|
||||
ctx.assume_eq(n, n2);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
seqs.push_back(v);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/*
|
||||
- Eqs = 0
|
||||
|
|
@ -634,15 +692,12 @@ void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
|
|||
expr* o1 = n1->get_owner();
|
||||
expr* o2 = n2->get_owner();
|
||||
if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) {
|
||||
//std::cout << "concats:\n" << mk_pp(o1,m) << "\n" << mk_pp(o2,m) << "\n";
|
||||
return;
|
||||
}
|
||||
if (has_length(o1) && !has_length(o2)) {
|
||||
//std::cout << "enforce length: " << mk_pp(o1,m) << " -> " << mk_pp(o2,m) << "\n";
|
||||
enforce_length(n2);
|
||||
}
|
||||
else if (has_length(o2) && !has_length(o1)) {
|
||||
//std::cout << "enforce length: " << mk_pp(o2,m) << " -> " << mk_pp(o1,m) << "\n";
|
||||
enforce_length(n1);
|
||||
}
|
||||
}
|
||||
|
|
@ -778,7 +833,6 @@ bool theory_seq::solve_eqs(unsigned i) {
|
|||
bool change = false;
|
||||
for (; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
|
||||
eq const& e = m_eqs[i];
|
||||
TRACE("seq", tout << i << "\n";);
|
||||
if (solve_eq(e.ls(), e.rs(), e.dep())) {
|
||||
if (i + 1 != m_eqs.size()) {
|
||||
eq e1 = m_eqs[m_eqs.size()-1];
|
||||
|
|
@ -835,7 +889,6 @@ bool theory_seq::propagate_max_length(expr* l, expr* r, dependency* deps) {
|
|||
}
|
||||
rational hi;
|
||||
if (is_tail(l, s, idx) && has_length(s) && m_util.str.is_empty(r) && !upper_bound(s, hi)) {
|
||||
//std::cout << "max length " << mk_pp(s, m) << " " << idx << "\n";
|
||||
propagate_lit(deps, 0, 0, mk_literal(m_autil.mk_le(m_util.str.mk_length(s), m_autil.mk_int(idx+1))));
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1008,7 +1061,7 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
}
|
||||
TRACE("seq",
|
||||
for (unsigned j = 0; j < lhs.size(); ++j) {
|
||||
tout << mk_pp(lhs[j].get(), m) << " ";
|
||||
tout << mk_pp(lhs[j].get(), m) << " " << mk_pp(rhs[j].get(), m) << "\n";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << n.ls(i) << " != " << n.rs(i) << "\n";);
|
||||
|
|
@ -1018,10 +1071,9 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
expr* nr = rhs[j].get();
|
||||
if (m_util.is_seq(nl) || m_util.is_re(nl)) {
|
||||
ls.reset();
|
||||
rs.reset();
|
||||
SASSERT(!m_util.str.is_concat(nl));
|
||||
SASSERT(!m_util.str.is_concat(nr));
|
||||
ls.push_back(nl); rs.push_back(nr);
|
||||
rs.reset();
|
||||
m_util.str.get_concat(nl, ls);
|
||||
m_util.str.get_concat(nr, rs);
|
||||
new_ls.push_back(ls);
|
||||
new_rs.push_back(rs);
|
||||
}
|
||||
|
|
@ -1253,6 +1305,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
|
|||
st.update("seq solve !=", m_stats.m_solve_nqs);
|
||||
st.update("seq solve =", m_stats.m_solve_eqs);
|
||||
st.update("seq add axiom", m_stats.m_add_axiom);
|
||||
st.update("seq extensionality", m_stats.m_extensionality);
|
||||
}
|
||||
|
||||
void theory_seq::init_model(expr_ref_vector const& es) {
|
||||
|
|
@ -1539,8 +1592,9 @@ void theory_seq::propagate() {
|
|||
++m_axioms_head;
|
||||
}
|
||||
while (!m_replay.empty() && !ctx.inconsistent()) {
|
||||
(*m_replay[m_replay.size()-1])(*this);
|
||||
TRACE("seq", tout << "replay at level: " << ctx.get_scope_level() << "\n";);
|
||||
apply* app = m_replay[m_replay.size() - 1];
|
||||
(*app)(*this);
|
||||
m_replay.pop_back();
|
||||
}
|
||||
if (m_new_solution) {
|
||||
|
|
@ -1592,7 +1646,7 @@ void theory_seq::deque_axiom(expr* n) {
|
|||
lit or s = "" or !prefix(s, x*s1)
|
||||
*/
|
||||
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
|
||||
expr_ref s1 = mk_skolem(m_seq_first, s);
|
||||
expr_ref s1 = mk_first(s);
|
||||
expr_ref c = mk_last(s);
|
||||
expr_ref s1c = mk_concat(s1, m_util.str.mk_unit(c));
|
||||
literal s_eq_emp = mk_eq_empty(s);
|
||||
|
|
@ -1628,30 +1682,34 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
|
|||
(len(s) <= len(t) -> i <= len(t)-len(s))
|
||||
*/
|
||||
void theory_seq::add_indexof_axiom(expr* i) {
|
||||
expr* s, *t, *offset;
|
||||
expr* s, *t, *offset = 0;
|
||||
rational r;
|
||||
VERIFY(m_util.str.is_index(i, t, s, offset));
|
||||
VERIFY(m_util.str.is_index(i, t, s) ||
|
||||
m_util.str.is_index(i, t, s, offset));
|
||||
expr_ref minus_one(m_autil.mk_int(-1), m);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref xsy(m);
|
||||
|
||||
// offset >= len(t) => indexof(s, t, offset) = -1
|
||||
expr_ref len_t(m_util.str.mk_length(t), m);
|
||||
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
|
||||
add_axiom(offset_ge_len, mk_eq(i, minus_one, false));
|
||||
|
||||
if (m_autil.is_numeral(offset, r) && r.is_zero()) {
|
||||
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
|
||||
expr_ref x = mk_skolem(m_contains_left, t, s);
|
||||
expr_ref y = mk_skolem(m_contains_right, t, s);
|
||||
xsy = mk_concat(x,s,y);
|
||||
xsy = mk_concat(x, s, y);
|
||||
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
|
||||
literal eq_empty = mk_eq_empty(s);
|
||||
add_axiom(cnt, mk_eq(i, minus_one, false));
|
||||
add_axiom(~eq_empty, mk_eq(i, zero, false));
|
||||
add_axiom(eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
|
||||
add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false));
|
||||
tightest_prefix(s, x, ~cnt);
|
||||
}
|
||||
else {
|
||||
// offset >= len(t) => indexof(s, t, offset) = -1
|
||||
|
||||
expr_ref len_t(m_util.str.mk_length(t), m);
|
||||
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
|
||||
add_axiom(offset_ge_len, mk_eq(i, minus_one, false));
|
||||
|
||||
expr_ref x = mk_skolem(m_indexof_left, t, s, offset);
|
||||
expr_ref y = mk_skolem(m_indexof_right, t, s, offset);
|
||||
expr_ref indexof0(m_util.str.mk_index(y, s, zero), m);
|
||||
|
|
@ -1922,18 +1980,18 @@ void theory_seq::add_extract_axiom(expr* e) {
|
|||
expr_ref ls(m_util.str.mk_length(s), m);
|
||||
expr_ref lx(m_util.str.mk_length(x), m);
|
||||
expr_ref le(m_util.str.mk_length(e), m);
|
||||
expr_ref ls_minus_i(mk_sub(ls, i), m);
|
||||
expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
|
||||
expr_ref xe = mk_concat(x, e);
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
|
||||
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
|
||||
literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
|
||||
literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero));
|
||||
literal li_ge_ls = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
|
||||
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
|
||||
|
||||
add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
|
||||
add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false));
|
||||
add_axiom(~i_ge_0, i_ge_ls, ~l_ge_ls, mk_eq(le, ls_minus_i, false));
|
||||
add_axiom(~i_ge_0, i_ge_ls, ~li_ge_ls, mk_eq(le, l, false));
|
||||
add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false));
|
||||
}
|
||||
|
||||
|
|
@ -1947,8 +2005,8 @@ void theory_seq::add_at_axiom(expr* e) {
|
|||
expr* s, *i;
|
||||
VERIFY(m_util.str.is_at(e, s, i));
|
||||
expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
|
||||
x = mk_skolem(m_at_left, s);
|
||||
y = mk_skolem(m_at_right, s);
|
||||
x = mk_skolem(m_at_left, s, i);
|
||||
y = mk_skolem(m_at_right, s, i);
|
||||
xey = mk_concat(x, e, y);
|
||||
zero = m_autil.mk_int(0);
|
||||
one = m_autil.mk_int(1);
|
||||
|
|
@ -2027,6 +2085,15 @@ literal theory_seq::mk_eq_empty(expr* _e) {
|
|||
expr_ref e(_e, m);
|
||||
SASSERT(m_util.is_seq(e));
|
||||
expr_ref emp(m);
|
||||
zstring s;
|
||||
if (m_util.str.is_string(e, s)) {
|
||||
if (s.length() == 0) {
|
||||
return true_literal;
|
||||
}
|
||||
else {
|
||||
return false_literal;
|
||||
}
|
||||
}
|
||||
emp = m_util.str.mk_empty(m.get_sort(e));
|
||||
return mk_equals(e, emp);
|
||||
}
|
||||
|
|
@ -2034,10 +2101,11 @@ literal theory_seq::mk_eq_empty(expr* _e) {
|
|||
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
|
||||
context& ctx = get_context();
|
||||
literal_vector lits;
|
||||
if (l1 != null_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
|
||||
if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
|
||||
if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
|
||||
if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
|
||||
if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal) return;
|
||||
if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
|
||||
if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
|
||||
if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
|
||||
if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
|
||||
TRACE("seq", ctx.display_literals_verbose(tout << "axiom: ", lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
m_new_propagation = true;
|
||||
++m_stats.m_add_axiom;
|
||||
|
|
@ -2077,8 +2145,8 @@ void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs)
|
|||
|
||||
}
|
||||
TRACE("seq",
|
||||
tout << mk_pp(ctx.bool_var2expr(lit.var()), m) << " => "
|
||||
<< mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
|
||||
ctx.display_literals_verbose(tout, 1, &lit);
|
||||
tout << " => " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
|
||||
justification* js =
|
||||
ctx.mk_justification(
|
||||
ext_theory_eq_propagation_justification(
|
||||
|
|
@ -2121,7 +2189,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
propagate_non_empty(lit, e1);
|
||||
|
||||
// lit => e1 = first ++ (unit last)
|
||||
expr_ref f1 = mk_skolem(m_seq_first, e1);
|
||||
expr_ref f1 = mk_first(e1);
|
||||
expr_ref f2 = mk_last(e1);
|
||||
f = mk_concat(f1, m_util.str.mk_unit(f2));
|
||||
propagate_eq(lit, e1, f, true);
|
||||
|
|
@ -2231,6 +2299,7 @@ void theory_seq::push_scope_eh() {
|
|||
}
|
||||
|
||||
void theory_seq::pop_scope_eh(unsigned num_scopes) {
|
||||
context& ctx = get_context();
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
m_dm.pop_scope(num_scopes);
|
||||
|
|
@ -2240,6 +2309,10 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
|
|||
m_nqs.pop_scope(num_scopes);
|
||||
m_atoms.resize(m_atoms_lim[m_atoms_lim.size()-num_scopes]);
|
||||
m_atoms_lim.shrink(m_atoms_lim.size()-num_scopes);
|
||||
m_rewrite.reset();
|
||||
if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) {
|
||||
m_replay.reset();
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::restart_eh() {
|
||||
|
|
@ -2566,7 +2639,8 @@ bool theory_seq::add_prefix2prefix(expr* e) {
|
|||
return false;
|
||||
}
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
|
||||
switch (assume_equality(e2, emp)) {
|
||||
literal e2_is_emp = mk_eq_empty(e2);
|
||||
switch (ctx.get_assignment(e2_is_emp)) {
|
||||
case l_true:
|
||||
return false; // done
|
||||
case l_undef:
|
||||
|
|
@ -2574,16 +2648,19 @@ bool theory_seq::add_prefix2prefix(expr* e) {
|
|||
default:
|
||||
break;
|
||||
}
|
||||
expr_ref head1(m), tail1(m), head2(m), tail2(m);
|
||||
|
||||
expr_ref head1(m), tail1(m), head2(m), tail2(m), conc(m);
|
||||
mk_decompose(e1, head1, tail1);
|
||||
mk_decompose(e2, head2, tail2);
|
||||
conc = mk_concat(head2, tail2);
|
||||
propagate_eq(~e2_is_emp, e2, conc, true);
|
||||
|
||||
literal lit = mk_eq(head1, head2, false);
|
||||
switch (ctx.get_assignment(lit)) {
|
||||
case l_true: {
|
||||
literal_vector lits;
|
||||
lits.push_back(~ctx.get_literal(e));
|
||||
lits.push_back(~mk_eq(e2, emp, false));
|
||||
lits.push_back(~e2_is_emp);
|
||||
lits.push_back(lit);
|
||||
propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_prefix(tail1, tail2)));
|
||||
return false;
|
||||
|
|
@ -2610,28 +2687,32 @@ bool theory_seq::add_suffix2suffix(expr* e) {
|
|||
}
|
||||
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m);
|
||||
|
||||
switch (assume_equality(e2, emp)) {
|
||||
literal e2_is_emp = mk_eq_empty(e2);
|
||||
switch (ctx.get_assignment(e2_is_emp)) {
|
||||
case l_true:
|
||||
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is empty\n";);
|
||||
return false; // done
|
||||
case l_undef:
|
||||
ctx.force_phase(mk_eq(e2, emp, false));
|
||||
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(e2, m) << " is unassigned\n";);
|
||||
ctx.force_phase(e2_is_emp);
|
||||
return true; // retry
|
||||
case l_false:
|
||||
break;
|
||||
}
|
||||
expr_ref first2 = mk_skolem(m_seq_first, e2);
|
||||
expr_ref first2 = mk_first(e2);
|
||||
expr_ref last2 = mk_last(e2);
|
||||
expr_ref first1 = mk_skolem(m_seq_first, e1);
|
||||
expr_ref first1 = mk_first(e1);
|
||||
expr_ref last1 = mk_last(e1);
|
||||
expr_ref conc = mk_concat(first2, m_util.str.mk_unit(last2));
|
||||
propagate_eq(~mk_eq(e2, emp, false), e2, conc);
|
||||
propagate_eq(~e2_is_emp, e2, conc, true);
|
||||
|
||||
literal last_eq = mk_eq(last1, last2, false);
|
||||
switch (ctx.get_assignment(last_eq)) {
|
||||
case l_false:
|
||||
TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is false\n";);
|
||||
return false; // done
|
||||
case l_undef:
|
||||
TRACE("seq", tout << mk_pp(e, m) << " " << last1 << " = " << last2 << " is unassigned\n";);
|
||||
ctx.force_phase(~last_eq);
|
||||
return true;
|
||||
case l_true:
|
||||
|
|
@ -2640,9 +2721,10 @@ bool theory_seq::add_suffix2suffix(expr* e) {
|
|||
|
||||
literal_vector lits;
|
||||
lits.push_back(~ctx.get_literal(e));
|
||||
lits.push_back(~mk_eq(e2, emp, false));
|
||||
lits.push_back(~e2_is_emp);
|
||||
lits.push_back(last_eq);
|
||||
propagate_lit(0, lits.size(), lits.c_ptr(), ~mk_literal(m_util.str.mk_suffix(first1, first2)));
|
||||
TRACE("seq", tout << mk_pp(e, m) << " saturate\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -192,6 +192,7 @@ namespace smt {
|
|||
expr_ref m_e;
|
||||
public:
|
||||
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
|
||||
virtual ~replay_length_coherence() {}
|
||||
virtual void operator()(theory_seq& th) {
|
||||
th.check_length_coherence(m_e);
|
||||
m_e.reset();
|
||||
|
|
@ -202,6 +203,7 @@ namespace smt {
|
|||
expr_ref m_e;
|
||||
public:
|
||||
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
|
||||
virtual ~replay_axiom() {}
|
||||
virtual void operator()(theory_seq& th) {
|
||||
th.enque_axiom(m_e);
|
||||
m_e.reset();
|
||||
|
|
@ -239,6 +241,7 @@ namespace smt {
|
|||
unsigned m_solve_nqs;
|
||||
unsigned m_solve_eqs;
|
||||
unsigned m_add_axiom;
|
||||
unsigned m_extensionality;
|
||||
};
|
||||
ast_manager& m;
|
||||
dependency_manager m_dm;
|
||||
|
|
@ -312,6 +315,7 @@ namespace smt {
|
|||
bool check_length_coherence(expr* e);
|
||||
bool propagate_length_coherence(expr* e);
|
||||
|
||||
bool check_extensionality();
|
||||
bool solve_eqs(unsigned start);
|
||||
bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
|
||||
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
|
||||
|
|
@ -334,7 +338,7 @@ namespace smt {
|
|||
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
|
||||
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
|
||||
void propagate_eq(dependency* dep, enode* n1, enode* n2);
|
||||
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
|
||||
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
|
||||
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
|
||||
|
||||
u_map<unsigned> m_branch_start;
|
||||
|
|
@ -353,6 +357,7 @@ namespace smt {
|
|||
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
|
||||
expr_ref mk_nth(expr* s, expr* idx);
|
||||
expr_ref mk_last(expr* e);
|
||||
expr_ref mk_first(expr* e);
|
||||
expr_ref canonize(expr* e, dependency*& eqs);
|
||||
bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
|
||||
bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs);
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ public:
|
|||
virtual void get_model(model_ref & m) = 0;
|
||||
virtual proof * get_proof() = 0;
|
||||
virtual std::string reason_unknown() const = 0;
|
||||
virtual void set_reason_unknown(char const* msg) = 0;
|
||||
virtual void get_labels(svector<symbol> & r) = 0;
|
||||
virtual ast_manager& get_manager() = 0;
|
||||
};
|
||||
|
|
@ -75,6 +76,7 @@ struct simple_check_sat_result : public check_sat_result {
|
|||
virtual proof * get_proof();
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void get_labels(svector<symbol> & r);
|
||||
virtual void set_reason_unknown(char const* msg) { m_unknown = msg; }
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -297,6 +297,11 @@ public:
|
|||
return m_solver2->reason_unknown();
|
||||
}
|
||||
|
||||
virtual void set_reason_unknown(char const* msg) {
|
||||
m_solver1->set_reason_unknown(msg);
|
||||
m_solver2->set_reason_unknown(msg);
|
||||
}
|
||||
|
||||
virtual void get_labels(svector<symbol> & r) {
|
||||
if (m_use_solver1_results)
|
||||
return m_solver1->get_labels(r);
|
||||
|
|
|
|||
|
|
@ -65,6 +65,7 @@ public:
|
|||
virtual void get_model(model_ref & m);
|
||||
virtual proof * get_proof();
|
||||
virtual std::string reason_unknown() const;
|
||||
virtual void set_reason_unknown(char const* msg);
|
||||
virtual void get_labels(svector<symbol> & r) {}
|
||||
|
||||
virtual void set_progress_callback(progress_callback * callback) {}
|
||||
|
|
@ -225,6 +226,12 @@ std::string tactic2solver::reason_unknown() const {
|
|||
return std::string("unknown");
|
||||
}
|
||||
|
||||
void tactic2solver::set_reason_unknown(char const* msg) {
|
||||
if (m_result.get()) {
|
||||
m_result->set_reason_unknown(msg);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned tactic2solver::get_num_assertions() const {
|
||||
return m_assertions.size();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -384,7 +384,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
if (!seen.contains(f))
|
||||
{
|
||||
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
|
||||
func_interp * val = bv_mdl->get_func_interp(f);
|
||||
func_interp * val = bv_mdl->get_func_interp(f)->copy();
|
||||
float_mdl->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue