mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-03-22 13:35:24 -07:00
parent a74ac93bcc 3c8fd83c97
commit 489577feba
19 changed files with 232 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_seq.cpp
View file

@ -148,6 +148,7 @@ extern "C" {
MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);
MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP);
MK_BINARY(Z3_mk_seq_last_index, mk_c(c)->get_seq_fid(), OP_SEQ_LAST_INDEX, SKIP);
MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);

6
src/api/c++/z3++.h
View file

@ -3276,6 +3276,12 @@ namespace z3 {
s.check_error();
return expr(s.ctx(), r);
}
inline expr last_indexof(expr const& s, expr const& substr) {
check_context(s, substr);
Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
s.check_error();
return expr(s.ctx(), r);
}
inline expr to_re(expr const& s) {
MK_EXPR1(Z3_mk_seq_to_re, s);
}

9
src/api/python/z3/z3.py
View file

@ -10154,6 +10154,15 @@ def IndexOf(s, substr, offset):
offset = IntVal(offset, ctx)
return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
def LastIndexOf(s, substr):
"""Retrieve the last index of substring within a string"""
ctx = None
ctx = _get_ctx2(s, substr, ctx)
s = _coerce_seq(s, ctx)
substr = _coerce_seq(substr, ctx)
return ArithRef(Z3_mk_seq_last_index(s.ctx_ref(), s.as_ast(), substr.as_ast()), s.ctx)
def Length(s):
"""Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))

10
src/api/z3_api.h
View file

@ -1171,6 +1171,7 @@ typedef enum {
Z3_OP_SEQ_NTH,
Z3_OP_SEQ_LENGTH,
Z3_OP_SEQ_INDEX,
Z3_OP_SEQ_LAST_INDEX,
Z3_OP_SEQ_TO_RE,
Z3_OP_SEQ_IN_RE,
@ -3446,12 +3447,19 @@ extern "C" {
/**
\brief Return index of first occurrence of \c substr in \c s starting from offset \c offset.
If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well.
The function is under-specified if \c offset is negative or larger than the length of \c s.
The value is -1 if \c offset is negative or larger than the length of \c s.
def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
/**
\brief Return the last occurrence of \c substr in \c s.
If \c s does not contain \c substr, then the value is -1,
def_API('Z3_mk_seq_last_index', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr);
/**
\brief Convert string to integer.

47
src/ast/rewriter/array_rewriter.cpp
View file

@ -36,36 +36,48 @@ void array_rewriter::get_param_descrs(param_descrs & r) {
br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid());
TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m()) << "\n";
});
br_status st;
switch (f->get_decl_kind()) {
case OP_SELECT:
return mk_select_core(num_args, args, result);
st = mk_select_core(num_args, args, result);
break;
case OP_STORE:
return mk_store_core(num_args, args, result);
st = mk_store_core(num_args, args, result);
break;
case OP_ARRAY_MAP:
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_ast());
SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
return mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
st = mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
break;
case OP_SET_UNION:
return mk_set_union(num_args, args, result);
st = mk_set_union(num_args, args, result);
break;
case OP_SET_INTERSECT:
return mk_set_intersect(num_args, args, result);
st = mk_set_intersect(num_args, args, result);
break;
case OP_SET_SUBSET:
SASSERT(num_args == 2);
return mk_set_subset(args[0], args[1], result);
st = mk_set_subset(args[0], args[1], result);
break;
case OP_SET_COMPLEMENT:
SASSERT(num_args == 1);
return mk_set_complement(args[0], result);
st = mk_set_complement(args[0], result);
break;
case OP_SET_DIFFERENCE:
SASSERT(num_args == 2);
return mk_set_difference(args[0], args[1], result);
st = mk_set_difference(args[0], args[1], result);
break;
default:
return BR_FAILED;
}
TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m()) << "\n";
}
tout << "\n --> " << result << "\n";
);
return st;
}
// l_true -- all equal
@ -456,6 +468,17 @@ bool array_rewriter::has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector
}
br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
TRACE("array_rewriter", tout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";);
expr* v = nullptr;
if (m_util.is_const(rhs) && is_lambda(lhs)) {
std::swap(lhs, rhs);
}
if (m_util.is_const(lhs, v) && is_lambda(rhs)) {
quantifier* lam = to_quantifier(rhs);
expr_ref e(m().mk_eq(lam->get_expr(), v), m());
result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
return BR_REWRITE2;
}
if (!m_expand_store_eq) {
return BR_FAILED;
}

103
src/ast/rewriter/seq_rewriter.cpp
View file

@ -391,44 +391,57 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_SEQ_UNIT:
SASSERT(num_args == 1);
return mk_seq_unit(args[0], result);
st = mk_seq_unit(args[0], result);
break;
case OP_SEQ_EMPTY:
return BR_FAILED;
case OP_RE_PLUS:
SASSERT(num_args == 1);
return mk_re_plus(args[0], result);
st = mk_re_plus(args[0], result);
break;
case OP_RE_STAR:
SASSERT(num_args == 1);
st = mk_re_star(args[0], result);
break;
case OP_RE_OPTION:
SASSERT(num_args == 1);
return mk_re_opt(args[0], result);
st = mk_re_opt(args[0], result);
break;
case OP_RE_CONCAT:
if (num_args == 1) {
result = args[0];
return BR_DONE;
st = BR_DONE;
}
else {
SASSERT(num_args == 2);
st = mk_re_concat(args[0], args[1], result);
}
SASSERT(num_args == 2);
st = mk_re_concat(args[0], args[1], result);
break;
case OP_RE_UNION:
if (num_args == 1) {
result = args[0]; return BR_DONE;
result = args[0];
st = BR_DONE;
}
SASSERT(num_args == 2);
return mk_re_union(args[0], args[1], result);
else {
SASSERT(num_args == 2);
st = mk_re_union(args[0], args[1], result);
}
break;
case OP_RE_RANGE:
SASSERT(num_args == 2);
return mk_re_range(args[0], args[1], result);
st = mk_re_range(args[0], args[1], result);
break;
case OP_RE_INTERSECT:
SASSERT(num_args == 2);
return mk_re_inter(args[0], args[1], result);
st = mk_re_inter(args[0], args[1], result);
break;
case OP_RE_COMPLEMENT:
SASSERT(num_args == 1);
return mk_re_complement(args[0], result);
st = mk_re_complement(args[0], result);
break;
case OP_RE_LOOP:
return mk_re_loop(num_args, args, result);
st = mk_re_loop(num_args, args, result);
break;
case OP_RE_EMPTY_SET:
return BR_FAILED;
case OP_RE_FULL_SEQ_SET:
@ -442,23 +455,29 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_SEQ_CONCAT:
if (num_args == 1) {
result = args[0];
return BR_DONE;
st = BR_DONE;
}
SASSERT(num_args == 2);
return mk_seq_concat(args[0], args[1], result);
else {
SASSERT(num_args == 2);
st = mk_seq_concat(args[0], args[1], result);
}
break;
case OP_SEQ_LENGTH:
SASSERT(num_args == 1);
return mk_seq_length(args[0], result);
st = mk_seq_length(args[0], result);
break;
case OP_SEQ_EXTRACT:
SASSERT(num_args == 3);
st = mk_seq_extract(args[0], args[1], args[2], result);
break;
case OP_SEQ_CONTAINS:
SASSERT(num_args == 2);
return mk_seq_contains(args[0], args[1], result);
st = mk_seq_contains(args[0], args[1], result);
break;
case OP_SEQ_AT:
SASSERT(num_args == 2);
return mk_seq_at(args[0], args[1], result);
st = mk_seq_at(args[0], args[1], result);
break;
#if 0
case OP_SEQ_NTH:
SASSERT(num_args == 2);
@ -466,35 +485,49 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
#endif
case OP_SEQ_PREFIX:
SASSERT(num_args == 2);
return mk_seq_prefix(args[0], args[1], result);
st = mk_seq_prefix(args[0], args[1], result);
break;
case OP_SEQ_SUFFIX:
SASSERT(num_args == 2);
return mk_seq_suffix(args[0], args[1], result);
st = mk_seq_suffix(args[0], args[1], result);
break;
case OP_SEQ_INDEX:
if (num_args == 2) {
expr_ref arg3(m_autil.mk_int(0), m());
result = m_util.str.mk_index(args[0], args[1], arg3);
return BR_REWRITE1;
st = BR_REWRITE1;
}
SASSERT(num_args == 3);
return mk_seq_index(args[0], args[1], args[2], result);
else {
SASSERT(num_args == 3);
st = mk_seq_index(args[0], args[1], args[2], result);
}
break;
case OP_SEQ_LAST_INDEX:
SASSERT(num_args == 2);
st = mk_seq_last_index(args[0], args[1], result);
break;
case OP_SEQ_REPLACE:
SASSERT(num_args == 3);
return mk_seq_replace(args[0], args[1], args[2], result);
st = mk_seq_replace(args[0], args[1], args[2], result);
break;
case OP_SEQ_TO_RE:
SASSERT(num_args == 1);
return mk_str_to_regexp(args[0], result);
st = mk_str_to_regexp(args[0], result);
break;
case OP_SEQ_IN_RE:
SASSERT(num_args == 2);
return mk_str_in_regexp(args[0], args[1], result);
st = mk_str_in_regexp(args[0], args[1], result);
break;
case OP_STRING_CONST:
return BR_FAILED;
case OP_STRING_ITOS:
SASSERT(num_args == 1);
return mk_str_itos(args[0], result);
st = mk_str_itos(args[0], result);
break;
case OP_STRING_STOI:
SASSERT(num_args == 1);
return mk_str_stoi(args[0], result);
st = mk_str_stoi(args[0], result);
break;
case _OP_STRING_CONCAT:
case _OP_STRING_PREFIX:
case _OP_STRING_SUFFIX:
@ -908,6 +941,18 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
zstring s1, s2;
bool isc1 = m_util.str.is_string(a, s1);
bool isc2 = m_util.str.is_string(b, s2);
if (isc1 && isc2) {
int idx = s1.last_indexof(s2);
result = m_autil.mk_numeral(rational(idx), true);
return BR_DONE;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
zstring s1, s2;
rational r;

1
src/ast/rewriter/seq_rewriter.h
View file

@ -116,6 +116,7 @@ class seq_rewriter {
br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result);
br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);

2
src/ast/rewriter/th_rewriter.cpp
View file

@ -32,6 +32,7 @@ Notes:
#include "ast/rewriter/var_subst.h"
#include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/well_sorted.h"
@ -184,7 +185,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
st = m_ar_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;
}

24
src/ast/seq_decl_plugin.cpp
View file

@ -273,6 +273,21 @@ int zstring::indexof(zstring const& other, int offset) const {
return -1;
}
int zstring::last_indexof(zstring const& other) const {
if (other.length() == 0) return length();
if (other.length() > length()) return -1;
for (unsigned last = length() - other.length(); last-- > 0; ) {
bool suffix = true;
for (unsigned j = 0; suffix && j < other.length(); ++j) {
suffix = m_buffer[last + j] == other[j];
}
if (suffix) {
return static_cast<int>(last);
}
}
return -1;
}
zstring zstring::extract(int offset, int len) const {
zstring result(m_encoding);
SASSERT(0 <= offset && 0 <= len);
@ -530,6 +545,7 @@ void seq_decl_plugin::init() {
m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA);
m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, seqA);
m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT);
m_sigs[OP_SEQ_LAST_INDEX] = alloc(psig, m, "seq.last_indexof", 1, 2, seqAseqA, intT);
m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
m_sigs[OP_SEQ_NTH] = alloc(psig, m, "seq.nth", 1, 2, seqAintT, A);
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT);
@ -774,7 +790,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, OP_SEQ_INDEX));
}
return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX);
case OP_SEQ_LAST_INDEX:
if (arity != 2) {
m.raise_exception("two arguments expected tin last_indexof");
}
else {
return mk_seq_fun(k, arity, domain, range, OP_SEQ_LAST_INDEX);
}
case OP_SEQ_PREFIX:
return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX);
case _OP_STRING_PREFIX:

5
src/ast/seq_decl_plugin.h
View file

@ -43,6 +43,7 @@ enum seq_op_kind {
OP_SEQ_NTH,
OP_SEQ_LENGTH,
OP_SEQ_INDEX,
OP_SEQ_LAST_INDEX,
OP_SEQ_TO_RE,
OP_SEQ_IN_RE,
@ -113,6 +114,7 @@ public:
bool prefixof(zstring const& other) const;
bool contains(zstring const& other) const;
int indexof(zstring const& other, int offset) const;
int last_indexof(zstring const& other) const;
zstring extract(int lo, int hi) const;
zstring operator+(zstring const& other) const;
bool operator==(const zstring& other) const;
@ -260,6 +262,7 @@ public:
app* mk_prefix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
app* mk_suffix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
app* mk_index(expr* a, expr* b, expr* i) const { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
app* mk_last_index(expr* a, expr* b) const { expr* es[2] = { a, b}; return m.mk_app(m_fid, OP_SEQ_LAST_INDEX, 2, es); }
app* mk_unit(expr* u) const { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
app* mk_char(zstring const& s, unsigned idx) const;
app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
@ -285,6 +288,7 @@ public:
bool is_nth(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_NTH); }
bool is_nth(expr const* n, expr*& s, unsigned& idx) const;
bool is_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); }
bool is_last_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LAST_INDEX); }
bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); }
bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
@ -311,6 +315,7 @@ public:
MATCH_BINARY(is_nth);
MATCH_BINARY(is_index);
MATCH_TERNARY(is_index);
MATCH_BINARY(is_last_index);
MATCH_TERNARY(is_replace);
MATCH_BINARY(is_prefix);
MATCH_BINARY(is_suffix);

11
src/model/model_evaluator.cpp
View file

@ -38,6 +38,7 @@ Revision History:
#include "ast/rewriter/var_subst.h"
namespace {
struct evaluator_cfg : public default_rewriter_cfg {
ast_manager & m;
model_core & m_model;
@ -165,7 +166,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (k == OP_EQ) {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = m.get_sort(args[0])->get_family_id();
sort* s = m.get_sort(args[0]);
family_id s_fid = s->get_family_id();
if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_bv_rw.get_fid())
@ -178,6 +180,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_ar_rw.get_fid())
st = mk_array_eq(args[0], args[1], result);
TRACE("model_evaluator",
tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " "
<< mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";);
if (st != BR_FAILED)
return st;
}
@ -348,7 +353,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_DONE;
}
if (!m_array_equalities) {
return BR_FAILED;
return m_ar_rw.mk_eq_core(a, b, result);
}
vector<expr_ref_vector> stores1, stores2;
@ -389,7 +394,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
);
return BR_REWRITE_FULL;
}
return BR_FAILED;
return m_ar_rw.mk_eq_core(a, b, result);
}
struct args_eq {

45
src/smt/theory_seq.cpp
View file

@ -4150,6 +4150,12 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
if (!arg1 || !arg2) return result;
result = m_util.str.mk_index(arg1, arg2, e3);
}
else if (m_util.str.is_last_index(e, e1, e2)) {
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_last_index(arg1, arg2);
}
else if (m.is_ite(e, e1, e2, e3)) {
if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e2)->get_root()) {
result = try_expand(e2, deps);
@ -4288,6 +4294,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_index(n)) {
add_indexof_axiom(n);
}
else if (m_util.str.is_last_index(n)) {
add_last_indexof_axiom(n);
}
else if (m_util.str.is_replace(n)) {
add_replace_axiom(n);
}
@ -4437,6 +4446,42 @@ void theory_seq::add_indexof_axiom(expr* i) {
}
}
/**
!contains(t, s) => i = -1
|t| = 0 => |s| = 0 or i = -1
|t| = 0 & |s| = 0 => i = 0
|t| != 0 & contains(t, s) => t = xsy & i = len(x)
|s| = 0 or s = s_head*s_tail
|s| = 0 or !contains(s_tail*y, s)
*/
void theory_seq::add_last_indexof_axiom(expr* i) {
expr* s = nullptr, *t = nullptr;
VERIFY(m_util.str.is_last_index(i, t, s));
expr_ref minus_one(m_autil.mk_int(-1), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref s_head(m), s_tail(m);
expr_ref x = mk_skolem(symbol("seq.last_indexof_left"), t, s);
expr_ref y = mk_skolem(symbol("seq.last_indexof_right"), t, s);
mk_decompose(s, s_head, s_tail);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal cnt2 = mk_literal(m_util.str.mk_contains(mk_concat(s_tail, y), s));
literal i_eq_m1 = mk_eq(i, minus_one, false);
literal i_eq_0 = mk_eq(i, zero, false);
literal s_eq_empty = mk_eq_empty(s);
literal t_eq_empty = mk_eq_empty(t);
expr_ref xsy = mk_concat(x, s, y);
add_axiom(cnt, i_eq_m1);
add_axiom(~t_eq_empty, s_eq_empty, i_eq_m1);
add_axiom(~t_eq_empty, ~s_eq_empty, i_eq_0);
add_axiom(t_eq_empty, ~cnt, mk_seq_eq(t, xsy));
add_axiom(t_eq_empty, ~cnt, mk_eq(i, mk_len(x), false));
add_axiom(s_eq_empty, mk_eq(s, mk_concat(s_head, s_tail), false));
add_axiom(s_eq_empty, ~cnt2);
}
/*
let r = replace(a, s, t)

1
src/smt/theory_seq.h
View file

@ -550,6 +550,7 @@ namespace smt {
void push_lit_as_expr(literal l, expr_ref_vector& buf);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
void add_indexof_axiom(expr* e);
void add_last_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
void add_length_axiom(expr* n);

18
src/util/lp/lar_core_solver.h
View file

@ -235,20 +235,17 @@ public:
m_r_upper_bounds.pop(k);
m_column_types.pop(k);
if (m_r_solver.m_factorization != nullptr) {
delete m_r_solver.m_factorization;
m_r_solver.m_factorization = nullptr;
}
delete m_r_solver.m_factorization;
m_r_solver.m_factorization = nullptr;
m_r_x.resize(m_r_A.column_count());
m_r_solver.m_costs.resize(m_r_A.column_count());
m_r_solver.m_d.resize(m_r_A.column_count());
if(!settings().use_tableau())
pop_markowitz_counts(k);
m_d_A.pop(k);
if (m_d_solver.m_factorization != nullptr) {
delete m_d_solver.m_factorization;
m_d_solver.m_factorization = nullptr;
}
// doubles
delete m_d_solver.m_factorization;
m_d_solver.m_factorization = nullptr;
m_d_x.resize(m_d_A.column_count());
pop_basis(k);
@ -421,9 +418,10 @@ public:
unsigned leaving = trace_of_basis_change[i+1];
cs.change_basis_unconditionally(entering, leaving);
}
if (cs.m_factorization != nullptr)
if (cs.m_factorization != nullptr) {
delete cs.m_factorization;
cs.m_factorization = nullptr;
cs.m_factorization = nullptr;
}
} else {
indexed_vector<L> w(cs.m_A.row_count());
// the queues of delayed indices

5
src/util/lp/lp_core_solver_base.h
View file

@ -127,9 +127,8 @@ public:
void init();
virtual ~lp_core_solver_base() {
if (m_factorization != nullptr)
delete m_factorization;
}
delete m_factorization;
}
vector<unsigned> & non_basis() {
return m_nbasis;

4
src/util/lp/lp_dual_simplex.h
View file

@ -34,9 +34,7 @@ class lp_dual_simplex: public lp_solver<T, X> {
vector<bool> m_can_enter_basis;
public:
~lp_dual_simplex() override {
if (m_core_solver != nullptr) {
delete m_core_solver;
}
delete m_core_solver;
}
lp_dual_simplex() : m_core_solver(nullptr) {}

4
src/util/lp/lp_primal_simplex_def.h
View file

@ -263,9 +263,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::solve_with_total
template <typename T, typename X> lp_primal_simplex<T, X>::~lp_primal_simplex() {
if (m_core_solver != nullptr) {
delete m_core_solver;
}
delete m_core_solver;
}
template <typename T, typename X> bool lp_primal_simplex<T, X>::bounds_hold(std::unordered_map<std::string, T> const & solution) {

4
src/util/lp/lp_solver_def.h
View file

@ -86,9 +86,7 @@ template <typename T, typename X> int lp_solver<T, X>::get_column_index_by_name(
template <typename T, typename X> lp_solver<T, X>::~lp_solver(){
if (m_A != nullptr) {
delete m_A;
}
delete m_A;
for (auto t : m_map_from_var_index_to_column_info) {
delete t.second;
}

5
src/util/lp/mps_reader.h
View file

@ -754,10 +754,7 @@ public:
}
for (auto s : m_columns) {
auto col = s.second;
auto b = col->m_bound;
if (b != nullptr) {
delete b;
}
delete col->m_bound;
delete col;
}
}