mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
60c0e73b2f
|
@ -127,13 +127,13 @@ public class Solver extends Z3Object
|
|||
* using the Boolean constants in ps.
|
||||
*
|
||||
* Remarks:
|
||||
* This API is an alternative to <see cref="Check"/> with assumptions for
|
||||
* This API is an alternative to {@link check} with assumptions for
|
||||
* extracting unsat cores.
|
||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||
* combination
|
||||
* of the Boolean variables provided using <see cref="AssertAndTrack"/>
|
||||
* of the Boolean variables provided using {@link assertAndTrack}
|
||||
* and the Boolean literals
|
||||
* provided using <see cref="Check"/> with assumptions.
|
||||
* provided using {@link check} with assumptions.
|
||||
**/
|
||||
public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
|
||||
{
|
||||
|
@ -152,13 +152,13 @@ public class Solver extends Z3Object
|
|||
* using the Boolean constant p.
|
||||
*
|
||||
* Remarks:
|
||||
* This API is an alternative to <see cref="Check"/> with assumptions for
|
||||
* This API is an alternative to {@link check} with assumptions for
|
||||
* extracting unsat cores.
|
||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||
* combination
|
||||
* of the Boolean variables provided using <see cref="AssertAndTrack"/>
|
||||
* of the Boolean variables provided using {@link assertAndTrack}
|
||||
* and the Boolean literals
|
||||
* provided using <see cref="Check"/> with assumptions.
|
||||
* provided using {@link check} with assumptions.
|
||||
*/
|
||||
public void assertAndTrack(BoolExpr constraint, BoolExpr p)
|
||||
{
|
||||
|
@ -294,7 +294,7 @@ public class Solver extends Z3Object
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a clone of the current solver with respect to <c>ctx</c>.
|
||||
* Create a clone of the current solver with respect to{@code ctx}.
|
||||
*/
|
||||
public Solver translate(Context ctx)
|
||||
{
|
||||
|
|
|
@ -419,11 +419,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
|
|||
|
||||
dbg_decouple("fpa2bv_add_exp_delta", exp_delta);
|
||||
|
||||
// cap the delta
|
||||
expr_ref cap(m), cap_le_delta(m);
|
||||
cap = m_bv_util.mk_numeral(sbits+2, ebits);
|
||||
cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
|
||||
m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
|
||||
if (log2(sbits + 2) < ebits + 2)
|
||||
{
|
||||
// cap the delta
|
||||
expr_ref cap(m), cap_le_delta(m);
|
||||
cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2);
|
||||
cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta));
|
||||
m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta);
|
||||
exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta);
|
||||
dbg_decouple("fpa2bv_add_exp_cap", cap);
|
||||
}
|
||||
|
||||
dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);
|
||||
|
||||
|
|
|
@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
dl_decl_plugin.h
|
||||
seq_decl_plugin.h
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
decl_plugin for the theory of sequences
|
||||
|
||||
Author:
|
||||
|
||||
|
@ -43,7 +43,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
|
|||
if (*s != '\\' || *(s + 1) == 0) {
|
||||
return false;
|
||||
}
|
||||
if (*(s + 1) == 'x' &&
|
||||
if (*(s + 1) == 'x' &&
|
||||
is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) {
|
||||
result = d1*16 + d2;
|
||||
s += 4;
|
||||
|
@ -100,7 +100,7 @@ zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
|
|||
if (is_escape_char(s, ch)) {
|
||||
m_buffer.push_back(ch);
|
||||
}
|
||||
else {
|
||||
else {
|
||||
m_buffer.push_back(*s);
|
||||
++s;
|
||||
}
|
||||
|
@ -115,7 +115,7 @@ zstring::zstring(zstring const& other) {
|
|||
zstring::zstring(unsigned num_bits, bool const* ch) {
|
||||
SASSERT(num_bits == 8 || num_bits == 16);
|
||||
m_encoding = (num_bits == 8)?ascii:unicode;
|
||||
unsigned n = 0;
|
||||
unsigned n = 0;
|
||||
for (unsigned i = 0; i < num_bits; ++i) {
|
||||
n |= (((unsigned)ch[i]) << i);
|
||||
}
|
||||
|
@ -158,10 +158,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
|
|||
}
|
||||
|
||||
static const char esc_table[32][6] =
|
||||
{ "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F",
|
||||
{ "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F",
|
||||
"\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F"
|
||||
};
|
||||
|
||||
|
||||
std::string zstring::encode() const {
|
||||
SASSERT(m_encoding == ascii);
|
||||
std::ostringstream strm;
|
||||
|
@ -220,7 +220,7 @@ int zstring::indexof(zstring const& other, int offset) const {
|
|||
bool prefix = true;
|
||||
for (unsigned j = 0; prefix && j < other.length(); ++j) {
|
||||
prefix = m_buffer[i + j] == other[j];
|
||||
}
|
||||
}
|
||||
if (prefix) {
|
||||
return static_cast<int>(i);
|
||||
}
|
||||
|
@ -250,7 +250,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const {
|
|||
}
|
||||
|
||||
|
||||
seq_decl_plugin::seq_decl_plugin(): m_init(false),
|
||||
seq_decl_plugin::seq_decl_plugin(): m_init(false),
|
||||
m_stringc_sym("String"),
|
||||
m_charc_sym("Char"),
|
||||
m_string(0),
|
||||
|
@ -258,7 +258,7 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false),
|
|||
m_re(0) {}
|
||||
|
||||
void seq_decl_plugin::finalize() {
|
||||
for (unsigned i = 0; i < m_sigs.size(); ++i)
|
||||
for (unsigned i = 0; i < m_sigs.size(); ++i)
|
||||
dealloc(m_sigs[i]);
|
||||
m_manager->dec_ref(m_string);
|
||||
m_manager->dec_ref(m_char);
|
||||
|
@ -266,7 +266,7 @@ void seq_decl_plugin::finalize() {
|
|||
}
|
||||
|
||||
bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
|
||||
return
|
||||
return
|
||||
s->get_name().is_numerical() &&
|
||||
(idx = s->get_name().get_num(), true);
|
||||
}
|
||||
|
@ -283,7 +283,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
|
||||
if (s->get_family_id() == sP->get_family_id() &&
|
||||
s->get_decl_kind() == sP->get_decl_kind() &&
|
||||
s->get_num_parameters() == sP->get_num_parameters()) {
|
||||
|
@ -308,7 +308,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
|
|||
void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
|
||||
ptr_vector<sort> binding;
|
||||
ast_manager& m = *m_manager;
|
||||
TRACE("seq_verbose",
|
||||
TRACE("seq_verbose",
|
||||
tout << sig.m_name << ": ";
|
||||
for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " ";
|
||||
if (range) tout << " range: " << mk_pp(range, m);
|
||||
|
@ -375,7 +375,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
|
|||
for (unsigned i = 0; i < dsz; ++i) {
|
||||
strm << mk_pp(sig.m_dom[i].get(), m) << " ";
|
||||
}
|
||||
|
||||
|
||||
m.raise_exception(strm.str().c_str());
|
||||
}
|
||||
if (!range && dsz == 0) {
|
||||
|
@ -438,7 +438,7 @@ void seq_decl_plugin::init() {
|
|||
m_sigs.resize(LAST_SEQ_OP);
|
||||
// TBD: have (par ..) construct and load parameterized signature from premable.
|
||||
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA);
|
||||
m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA);
|
||||
m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA);
|
||||
m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA);
|
||||
m_sigs[OP_SEQ_PREFIX] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
|
||||
m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
|
||||
|
@ -548,10 +548,10 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
|
|||
match_right_assoc(*m_sigs[k], arity, domain, range, rng);
|
||||
func_decl_info info(m_family_id, k_seq);
|
||||
info.set_right_associative();
|
||||
return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
|
||||
return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
|
||||
}
|
||||
|
||||
func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
init();
|
||||
ast_manager& m = *m_manager;
|
||||
|
@ -568,7 +568,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
func_decl_info info(m_family_id, k, 1, ¶m);
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info);
|
||||
}
|
||||
|
||||
|
||||
case OP_SEQ_UNIT:
|
||||
case OP_RE_PLUS:
|
||||
case OP_RE_STAR:
|
||||
|
@ -593,7 +593,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
}
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
|
||||
|
||||
|
||||
case OP_RE_LOOP:
|
||||
switch (arity) {
|
||||
case 1:
|
||||
|
@ -601,7 +601,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
if (num_parameters == 0 || num_parameters > 2 || !parameters[0].is_int() || (num_parameters == 2 && !parameters[1].is_int())) {
|
||||
m.raise_exception("Expecting two numeral parameters to function re-loop");
|
||||
}
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
case 2:
|
||||
if (m_re != domain[0] || !arith_util(m).is_int(domain[1])) {
|
||||
m.raise_exception("Incorrect type of arguments passed to re.loop. Expecting regular expression and two integer parameters");
|
||||
|
@ -613,26 +613,26 @@ 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, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
default:
|
||||
m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
|
||||
m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
|
||||
}
|
||||
|
||||
|
||||
|
||||
case OP_STRING_CONST:
|
||||
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
|
||||
m.raise_exception("invalid string declaration");
|
||||
}
|
||||
}
|
||||
return m.mk_const_decl(m_stringc_sym, m_string,
|
||||
func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
|
||||
|
||||
|
||||
case OP_RE_UNION:
|
||||
case OP_RE_CONCAT:
|
||||
case OP_RE_INTERSECT:
|
||||
case OP_RE_CONCAT:
|
||||
case OP_RE_INTERSECT:
|
||||
return mk_assoc_fun(k, arity, domain, range, k, k);
|
||||
|
||||
case OP_SEQ_CONCAT:
|
||||
case OP_SEQ_CONCAT:
|
||||
return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT);
|
||||
|
||||
case _OP_STRING_CONCAT:
|
||||
case _OP_STRING_CONCAT:
|
||||
return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k);
|
||||
|
||||
case OP_SEQ_REPLACE:
|
||||
|
@ -743,8 +743,8 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
|
|||
|
||||
|
||||
bool seq_decl_plugin::is_value(app* e) const {
|
||||
return
|
||||
is_app_of(e, m_family_id, OP_SEQ_EMPTY) ||
|
||||
return
|
||||
is_app_of(e, m_family_id, OP_SEQ_EMPTY) ||
|
||||
(is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
|
||||
m_manager->is_value(e->get_arg(0)));
|
||||
}
|
||||
|
@ -782,7 +782,7 @@ app* seq_util::str::mk_char(char ch) {
|
|||
zstring s(ch, zstring::ascii);
|
||||
return mk_char(s, 0);
|
||||
}
|
||||
|
||||
|
||||
bool seq_util::str::is_char(expr* n, zstring& c) const {
|
||||
if (u.is_char(n)) {
|
||||
c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
|
||||
|
@ -809,7 +809,7 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
|
|||
while (is_concat(e, e1, e2)) {
|
||||
get_concat(e1, es);
|
||||
e = e2;
|
||||
}
|
||||
}
|
||||
if (!is_empty(e)) {
|
||||
es.push_back(e);
|
||||
}
|
||||
|
@ -835,7 +835,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& h
|
|||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) {
|
||||
|
@ -847,5 +847,5 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) {
|
|||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
return false;
|
||||
}
|
||||
|
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
decl_plugin for the theory of sequences
|
||||
|
||||
Author:
|
||||
|
||||
|
@ -41,7 +41,7 @@ enum seq_op_kind {
|
|||
OP_SEQ_EXTRACT,
|
||||
OP_SEQ_REPLACE,
|
||||
OP_SEQ_AT,
|
||||
OP_SEQ_LENGTH,
|
||||
OP_SEQ_LENGTH,
|
||||
OP_SEQ_INDEX,
|
||||
OP_SEQ_TO_RE,
|
||||
OP_SEQ_IN_RE,
|
||||
|
@ -61,19 +61,19 @@ enum seq_op_kind {
|
|||
|
||||
// string specific operators.
|
||||
OP_STRING_CONST,
|
||||
OP_STRING_ITOS,
|
||||
OP_STRING_STOI,
|
||||
OP_STRING_ITOS,
|
||||
OP_STRING_STOI,
|
||||
// internal only operators. Converted to SEQ variants.
|
||||
_OP_STRING_STRREPL,
|
||||
_OP_STRING_CONCAT,
|
||||
_OP_STRING_LENGTH,
|
||||
_OP_STRING_STRREPL,
|
||||
_OP_STRING_CONCAT,
|
||||
_OP_STRING_LENGTH,
|
||||
_OP_STRING_STRCTN,
|
||||
_OP_STRING_PREFIX,
|
||||
_OP_STRING_SUFFIX,
|
||||
_OP_STRING_IN_REGEXP,
|
||||
_OP_STRING_TO_REGEXP,
|
||||
_OP_STRING_CHARAT,
|
||||
_OP_STRING_SUBSTR,
|
||||
_OP_STRING_PREFIX,
|
||||
_OP_STRING_SUFFIX,
|
||||
_OP_STRING_IN_REGEXP,
|
||||
_OP_STRING_TO_REGEXP,
|
||||
_OP_STRING_CHARAT,
|
||||
_OP_STRING_SUBSTR,
|
||||
_OP_STRING_STRIDOF,
|
||||
_OP_REGEXP_EMPTY,
|
||||
_OP_REGEXP_FULL,
|
||||
|
@ -85,10 +85,10 @@ enum seq_op_kind {
|
|||
class zstring {
|
||||
public:
|
||||
enum encoding {
|
||||
ascii,
|
||||
ascii,
|
||||
unicode
|
||||
};
|
||||
private:
|
||||
private:
|
||||
buffer<unsigned> m_buffer;
|
||||
encoding m_encoding;
|
||||
public:
|
||||
|
@ -101,7 +101,7 @@ public:
|
|||
zstring replace(zstring const& src, zstring const& dst) const;
|
||||
unsigned num_bits() const { return (m_encoding==ascii)?8:16; }
|
||||
encoding get_encoding() const { return m_encoding; }
|
||||
std::string encode() const;
|
||||
std::string encode() const;
|
||||
unsigned length() const { return m_buffer.size(); }
|
||||
unsigned operator[](unsigned i) const { return m_buffer[i]; }
|
||||
bool empty() const { return m_buffer.empty(); }
|
||||
|
@ -113,7 +113,7 @@ public:
|
|||
zstring operator+(zstring const& other) const;
|
||||
std::ostream& operator<<(std::ostream& out) const;
|
||||
};
|
||||
|
||||
|
||||
class seq_decl_plugin : public decl_plugin {
|
||||
struct psig {
|
||||
symbol m_name;
|
||||
|
@ -161,18 +161,18 @@ public:
|
|||
|
||||
virtual ~seq_decl_plugin() {}
|
||||
virtual void finalize();
|
||||
|
||||
|
||||
virtual decl_plugin * mk_fresh() { return alloc(seq_decl_plugin); }
|
||||
|
||||
|
||||
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
|
||||
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
||||
|
||||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
|
||||
|
||||
virtual bool is_value(app * e) const;
|
||||
|
||||
virtual bool is_unique_value(app * e) const { return is_value(e); }
|
||||
|
@ -181,8 +181,8 @@ public:
|
|||
|
||||
bool is_char(ast* a) const { return a == m_char; }
|
||||
|
||||
app* mk_string(symbol const& s);
|
||||
app* mk_string(zstring const& s);
|
||||
app* mk_string(symbol const& s);
|
||||
app* mk_string(zstring const& s);
|
||||
|
||||
};
|
||||
|
||||
|
@ -244,12 +244,12 @@ public:
|
|||
bool is_string(expr const* n, symbol& s) const {
|
||||
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
|
||||
}
|
||||
|
||||
|
||||
bool is_string(expr const* n, zstring& s) const;
|
||||
bool is_char(expr* n, zstring& s) const;
|
||||
|
||||
bool is_empty(expr const* n) const { symbol s;
|
||||
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
|
||||
bool is_empty(expr const* n) const { symbol s;
|
||||
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
|
||||
}
|
||||
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
|
||||
bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
|
||||
|
@ -265,7 +265,7 @@ public:
|
|||
bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
|
||||
bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
|
||||
|
||||
|
||||
|
||||
MATCH_BINARY(is_concat);
|
||||
MATCH_UNARY(is_length);
|
||||
MATCH_TERNARY(is_extract);
|
||||
|
@ -278,7 +278,7 @@ public:
|
|||
MATCH_BINARY(is_suffix);
|
||||
MATCH_UNARY(is_itos);
|
||||
MATCH_UNARY(is_stoi);
|
||||
MATCH_BINARY(is_in_re);
|
||||
MATCH_BINARY(is_in_re);
|
||||
MATCH_UNARY(is_unit);
|
||||
|
||||
void get_concat(expr* e, expr_ref_vector& es) const;
|
||||
|
@ -301,7 +301,7 @@ public:
|
|||
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
|
||||
app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
|
||||
app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
|
||||
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
|
||||
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
|
||||
app* mk_loop(expr* r, unsigned lo);
|
||||
app* mk_loop(expr* r, unsigned lo, unsigned hi);
|
||||
|
||||
|
@ -325,23 +325,23 @@ public:
|
|||
MATCH_UNARY(is_plus);
|
||||
MATCH_UNARY(is_opt);
|
||||
bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
|
||||
bool is_loop(expr const* n, expr*& body, unsigned& lo);
|
||||
bool is_loop(expr const* n, expr*& body, unsigned& lo);
|
||||
};
|
||||
str str;
|
||||
re re;
|
||||
|
||||
seq_util(ast_manager& m):
|
||||
m(m),
|
||||
seq_util(ast_manager& m):
|
||||
m(m),
|
||||
seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))),
|
||||
m_fid(seq.get_family_id()),
|
||||
str(*this),
|
||||
re(*this) {
|
||||
re(*this) {
|
||||
}
|
||||
|
||||
~seq_util() {}
|
||||
|
||||
family_id get_family_id() const { return m_fid; }
|
||||
|
||||
|
||||
};
|
||||
|
||||
#endif /* SEQ_DECL_PLUGIN_H_ */
|
||||
|
|
|
@ -24,16 +24,16 @@ m_rw(m) {}
|
|||
fpa_simplifier_plugin::~fpa_simplifier_plugin() {}
|
||||
|
||||
bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
set_reduce_invoked();
|
||||
|
||||
SASSERT(f->get_family_id() == get_family_id());
|
||||
|
||||
return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE;
|
||||
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
|
||||
}
|
||||
|
||||
bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
|
||||
return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE;
|
||||
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
|
@ -7,7 +7,7 @@ Module Name:
|
|||
|
||||
Abstract:
|
||||
|
||||
Simplifier for the floating-point theory
|
||||
Simplifier for the theory of sequences
|
||||
|
||||
Author:
|
||||
|
||||
|
@ -24,7 +24,7 @@ m_rw(m) {}
|
|||
seq_simplifier_plugin::~seq_simplifier_plugin() {}
|
||||
|
||||
bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
set_reduce_invoked();
|
||||
|
||||
SASSERT(f->get_family_id() == get_family_id());
|
||||
|
||||
|
|
|
@ -26,17 +26,17 @@ namespace smt {
|
|||
|
||||
class fpa2bv_conversion_trail_elem : public trail<theory_fpa> {
|
||||
ast_manager & m;
|
||||
obj_map<expr, expr*> & m_conversions;
|
||||
expr * m_e;
|
||||
obj_map<expr, expr*> & m_map;
|
||||
expr_ref key;
|
||||
public:
|
||||
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
|
||||
m(m), m_conversions(c), m_e(e) { m.inc_ref(e); }
|
||||
virtual ~fpa2bv_conversion_trail_elem() {}
|
||||
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & map, expr * e) :
|
||||
m(m), m_map(map), key(e, m) { }
|
||||
virtual ~fpa2bv_conversion_trail_elem() { }
|
||||
virtual void undo(theory_fpa & th) {
|
||||
expr * v = m_conversions.find(m_e);
|
||||
m_conversions.remove(m_e);
|
||||
m.dec_ref(v);
|
||||
m.dec_ref(m_e);
|
||||
expr * val = m_map.find(key);
|
||||
m_map.remove(key);
|
||||
m.dec_ref(val);
|
||||
key = 0;
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -153,6 +153,8 @@ namespace smt {
|
|||
|
||||
theory_fpa::~theory_fpa()
|
||||
{
|
||||
m_trail_stack.reset();
|
||||
|
||||
if (m_is_initialized) {
|
||||
ast_manager & m = get_manager();
|
||||
dec_ref_map_values(m, m_conversions);
|
||||
|
|
Loading…
Reference in a new issue