mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into lackr

Browse source
This commit is contained in:
Mikolas Janota 2016-01-13 12:10:36 +00:00
commit 094d357b07
20 changed files with 509 additions and 183 deletions
Download patch file Download diff file Expand all files Collapse all files

98
scripts/mk_util.py
View file

@ -460,7 +460,7 @@ def find_ocaml_find():
print ("Testing %s..." % OCAMLFIND)
r = exec_cmd([OCAMLFIND, 'printconf'])
if r != 0:
OCAMLFIND=''
OCAMLFIND = ''
def find_ml_lib():
global OCAML_LIB
@ -630,6 +630,7 @@ def display_help(exit_code):
print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)")
print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)")
print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)")
print(" OCAMLFIND Ocaml find tool (only relevant with --ml)")
print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)")
print(" OCAML_LIB Ocaml library directory (only relevant with --ml)")
print(" CSC C# Compiler (only relevant if .NET bindings are enabled)")
@ -1753,6 +1754,42 @@ class MLComponent(Component):
self.stubs = "z3native_stubs"
self.sub_dir = os.path.join('api', 'ml')
self.destdir = ""
self.ldconf = ""
# Calling _init_ocamlfind_paths() is postponed to later because
# OCAMLFIND hasn't been checked yet.
def _install_bindings(self):
# FIXME: Depending on global state is gross. We can't pre-compute this
# in the constructor because we haven't tested for ocamlfind yet
return OCAMLFIND != ''
def _init_ocamlfind_paths(self):
"""
Initialises self.destdir and self.ldconf
Do not call this from the MLComponent constructor because OCAMLFIND
has not been checked at that point
"""
if self.destdir != "" and self.ldconf != "":
# Initialisation already done
return
# Use Ocamlfind to get the default destdir and ldconf path
self.destdir = check_output([OCAMLFIND, 'printconf', 'destdir'])
if self.destdir == "":
raise MKException('Failed to get OCaml destdir')
if not os.path.isdir(self.destdir):
raise MKException('The destdir reported by {ocamlfind} ({destdir}) does not exist'.format(ocamlfind=OCAMLFIND, destdir=self.destdir))
self.ldconf = check_output([OCAMLFIND, 'printconf', 'ldconf'])
if self.ldconf == "":
raise MKException('Failed to get OCaml ldconf path')
def final_info(self):
if not self._install_bindings():
print("WARNING: Could not find ocamlfind utility. OCaml bindings will not be installed")
def mk_makefile(self, out):
if is_ml_enabled():
src_dir = self.to_src_dir
@ -1832,7 +1869,7 @@ class MLComponent(Component):
out.write('\n')
def mk_install_deps(self, out):
if is_ml_enabled() and OCAMLFIND != '':
if is_ml_enabled() and self._install_bindings():
out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ')
out.write(os.path.join(self.sub_dir, 'META '))
out.write(os.path.join(self.sub_dir, 'z3ml.cma '))
@ -1840,8 +1877,22 @@ class MLComponent(Component):
out.write(os.path.join(self.sub_dir, 'z3ml.cmxs '))
def mk_install(self, out):
if is_ml_enabled() and OCAMLFIND != '':
out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META'))))
if is_ml_enabled() and self._install_bindings():
self._init_ocamlfind_paths()
in_prefix = self.destdir.startswith(PREFIX)
maybe_stripped_destdir = strip_path_prefix(self.destdir, PREFIX)
# Note that when doing a staged install with DESTDIR that modifying
# OCaml's ``ld.conf`` may fail. Therefore packagers will need to
# make their packages modify it manually at package install time
# as opposed to ``make install`` time.
MakeRuleCmd.make_install_directory(out,
maybe_stripped_destdir,
in_prefix=in_prefix)
out.write('\t@{ocamlfind} install -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3 {metafile}'.format(
ldconf=self.ldconf,
ocamlfind=OCAMLFIND,
ocaml_destdir=self.destdir,
metafile=os.path.join(self.sub_dir, 'META')))
for m in self.modules:
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
@ -1859,8 +1910,12 @@ class MLComponent(Component):
out.write('\n')
def mk_uninstall(self, out):
if is_ml_enabled() and OCAMLFIND != '':
out.write('\t@%s remove Z3\n' % (OCAMLFIND))
if is_ml_enabled() and self._install_bindings():
self._init_ocamlfind_paths()
out.write('\t@{ocamlfind} remove -ldconf $(DESTDIR){ldconf} -destdir $(DESTDIR){ocaml_destdir} Z3\n'.format(
ldconf=self.ldconf,
ocamlfind=OCAMLFIND,
ocaml_destdir=self.destdir))
def main_component(self):
return is_ml_enabled()
@ -2175,6 +2230,7 @@ def mk_config():
print('Java Compiler: %s' % JAVAC)
if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Find tool: %s' % OCAMLFIND)
print('OCaml Native: %s' % OCAMLOPT)
print('OCaml Library: %s' % OCAML_LIB)
else:
@ -2310,6 +2366,7 @@ def mk_config():
print('Java Compiler: %s' % JAVAC)
if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Find tool: %s' % OCAMLFIND)
print('OCaml Native: %s' % OCAMLOPT)
print('OCaml Library: %s' % OCAML_LIB)
if is_dotnet_enabled():
@ -3535,6 +3592,15 @@ class MakeRuleCmd(object):
# Note: DESTDIR is to support staged installs
return "$(DESTDIR)$(PREFIX)/"
@classmethod
def _is_str(cls, obj):
if sys.version_info.major > 2:
# Python 3 or newer. Strings are always unicode and of type str
return isinstance(obj, str)
else:
# Python 2. Has byte-string and unicode representation, allow both
return isinstance(obj, str) or isinstance(obj, unicode)
@classmethod
def _install_root(cls, path, in_prefix, out, is_install=True):
if not in_prefix:
@ -3553,9 +3619,9 @@ class MakeRuleCmd(object):
@classmethod
def install_files(cls, out, src_pattern, dest, in_prefix=True):
assert len(dest) > 0
assert isinstance(src_pattern, str)
assert cls._is_str(src_pattern)
assert not ' ' in src_pattern
assert isinstance(dest, str)
assert cls._is_str(dest)
assert not ' ' in dest
assert not os.path.isabs(src_pattern)
install_root = cls._install_root(dest, in_prefix, out)
@ -3568,7 +3634,7 @@ class MakeRuleCmd(object):
@classmethod
def remove_installed_files(cls, out, pattern, in_prefix=True):
assert len(pattern) > 0
assert isinstance(pattern, str)
assert cls._is_str(pattern)
assert not ' ' in pattern
install_root = cls._install_root(pattern, in_prefix, out, is_install=False)
@ -3579,7 +3645,7 @@ class MakeRuleCmd(object):
@classmethod
def make_install_directory(cls, out, dir, in_prefix=True):
assert len(dir) > 0
assert isinstance(dir, str)
assert cls._is_str(dir)
assert not ' ' in dir
install_root = cls._install_root(dir, in_prefix, out)
@ -3593,8 +3659,8 @@ class MakeRuleCmd(object):
Returns True iff ``temp_path`` is a path prefix
of ``target_as_abs``
"""
assert isinstance(temp_path, str)
assert isinstance(target_as_abs, str)
assert cls._is_str(temp_path)
assert cls._is_str(target_as_abs)
assert len(temp_path) > 0
assert len(target_as_abs) > 0
assert os.path.isabs(temp_path)
@ -3610,8 +3676,8 @@ class MakeRuleCmd(object):
@classmethod
def create_relative_symbolic_link(cls, out, target, link_name):
assert isinstance(target, str)
assert isinstance(link_name, str)
assert cls._is_str(target)
assert cls._is_str(link_name)
assert len(target) > 0
assert len(link_name) > 0
assert not os.path.isabs(target)
@ -3648,8 +3714,8 @@ class MakeRuleCmd(object):
@classmethod
def create_symbolic_link(cls, out, target, link_name):
assert isinstance(target, str)
assert isinstance(link_name, str)
assert cls._is_str(target)
assert cls._is_str(link_name)
assert not os.path.isabs(target)
cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(

8
src/api/api_fpa.cpp
View file

@ -943,7 +943,7 @@ extern "C" {
return "";
}
scoped_mpf val(mpfm);
app * a = to_app(e);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val);
if (!r || !mpfm.is_regular(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG)
@ -981,7 +981,7 @@ extern "C" {
return 0;
}
scoped_mpf val(mpfm);
app * a = to_app(e);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val);
const mpz & z = mpfm.sig(val);
if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) {
@ -1012,7 +1012,7 @@ extern "C" {
return "";
}
scoped_mpf val(mpfm);
app * a = to_app(e);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val);
if (!r || !mpfm.is_regular(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
@ -1044,7 +1044,7 @@ extern "C" {
return 0;
}
scoped_mpf val(mpfm);
app * a = to_app(e);
// app * a = to_app(e);
bool r = plugin->is_numeral(e, val);
if (!r || !mpfm.is_regular(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG);

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

@ -9320,8 +9320,10 @@ def Union(*args):
args = _get_args(args)
sz = len(args)
if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.")
_z3_assert(sz > 0, "At least one argument expected.")
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
if sz == 1:
return args[0]
ctx = args[0].ctx
v = (Ast * sz)()
for i in range(sz):

1
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -1171,7 +1171,6 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
template<typename Cfg>
bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
unsigned nb = 0;
unsigned case_size = 1;
unsigned circuit_size = sz*sz*5;
for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {

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

@ -24,26 +24,42 @@ Notes:
#include"uint_set.h"
#include"automaton.h"
#include"well_sorted.h"
#include"var_subst.h"
expr_ref sym_expr::accept(expr* e) {
ast_manager& m = m_t.get_manager();
expr_ref result(m);
if (m_is_pred) {
var_subst subst(m);
subst(m_t, 1, &e, result);
}
else {
result = m.mk_eq(e, m_t);
}
return result;
}
std::ostream& sym_expr::display(std::ostream& out) const {
return out << m_t;
}
struct display_expr1 {
ast_manager& m;
display_expr1(ast_manager& m): m(m) {}
std::ostream& display(std::ostream& out, expr* e) const {
return out << mk_pp(e, m);
std::ostream& display(std::ostream& out, sym_expr* e) const {
return e->display(out);
}
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {}
eautomaton* re2automaton::operator()(expr* e) {
eautomaton* r = re2aut(e);
if (r) {
//display_expr1 disp(m);
//r->display(std::cout, disp);
display_expr1 disp(m);
r->compress();
//r->display(std::cout, disp);
TRACE("seq", r->display(tout, disp););
}
return r;
}
@ -53,6 +69,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr* e1, *e2;
scoped_ptr<eautomaton> a, b;
unsigned lo, hi;
zstring s1, s2;
if (u.re.is_to_re(e, e1)) {
return seq2aut(e1);
}
@ -76,17 +94,45 @@ eautomaton* re2automaton::re2aut(expr* e) {
a = eautomaton::mk_opt(*a);
return a.detach();
}
else if (u.re.is_range(e)) {
else if (u.re.is_range(e, e1, e2)) {
if (u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
s1.length() == 1 && s2.length() == 1) {
unsigned start = s1[0];
unsigned stop = s2[0];
unsigned nb = s1.num_bits();
sort_ref s(bv.mk_sort(nb), m);
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));
return a.detach();
}
else {
TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
}
}
else if (u.re.is_loop(e)) {
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
b = eautomaton::mk_epsilon(sm);
while (hi > lo) {
scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
b = eautomaton::mk_union(*eps, *c);
--hi;
}
while (lo > 0) {
b = eautomaton::mk_concat(*a, *b);
--lo;
}
return b.detach();
}
#if 0
else if (u.re.is_intersect(e, e1, e2)) {
}
else if (u.re.is_empty(e)) {
return alloc(eautomaton, m);
}
else if (u.re.is_full(e)) {
}
else if (u.re.is_intersect(e, e1, e2)) {
}
#endif
@ -103,10 +149,10 @@ eautomaton* re2automaton::seq2aut(expr* e) {
return eautomaton::mk_concat(*a, *b);
}
else if (u.str.is_unit(e, e1)) {
return alloc(eautomaton, m, e1);
return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
}
else if (u.str.is_empty(e)) {
return eautomaton::mk_epsilon(m);
return eautomaton::mk_epsilon(sm);
}
else if (u.str.is_string(e, s)) {
unsigned init = 0;
@ -115,9 +161,9 @@ eautomaton* re2automaton::seq2aut(expr* e) {
final.push_back(s.length());
for (unsigned k = 0; k < s.length(); ++k) {
// reference count?
mvs.push_back(eautomaton::move(m, k, k+1, u.str.mk_char(s, k)));
mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
}
return alloc(eautomaton, m, init, final, mvs);
return alloc(eautomaton, sm, init, final, mvs);
}
return 0;
}
@ -210,8 +256,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STRING_STOI:
SASSERT(num_args == 1);
return mk_str_stoi(args[0], result);
case OP_REGEXP_LOOP:
return BR_FAILED;
case _OP_STRING_CONCAT:
case _OP_STRING_PREFIX:
case _OP_STRING_SUFFIX:
@ -653,7 +697,37 @@ void seq_rewriter::add_next(u_map<expr*>& next, unsigned idx, expr* cond) {
}
}
bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
seq.reset();
unsigned state = aut.init();
uint_set visited;
eautomaton::moves mvs;
aut.get_moves_from(state, mvs, true);
while (!aut.is_final_state(state)) {
if (mvs.size() != 1) {
return false;
}
if (visited.contains(state)) {
return false;
}
if (aut.is_final_state(mvs[0].src())) {
return false;
}
visited.insert(state);
sym_expr* t = mvs[0].t();
if (!t || !t->is_char()) {
return false;
}
seq.push_back(m_util.str.mk_unit(t->get_char()));
state = mvs[0].dst();
mvs.reset();
aut.get_moves_from(state, mvs, true);
}
return mvs.empty();
}
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
seq.reset();
zstring s;
ptr_vector<expr> todo;
expr *e1, *e2;
@ -688,63 +762,80 @@ 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) {
scoped_ptr<eautomaton> aut;
expr_ref_vector seq(m());
if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) {
expr_ref_vector trail(m());
u_map<expr*> maps[2];
bool select_map = false;
expr_ref ch(m()), cond(m());
eautomaton::moves mvs;
maps[0].insert(aut->init(), m().mk_true());
// is_accepted(a, aut) & some state in frontier is final.
if (!(aut = m_re2aut(b))) {
return BR_FAILED;
}
for (unsigned i = 0; i < seq.size(); ++i) {
u_map<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map];
select_map = !select_map;
ch = seq[i].get();
next.reset();
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
for (; it != end; ++it) {
mvs.reset();
unsigned state = it->m_key;
expr* acc = it->m_value;
aut->get_moves_from(state, mvs, false);
for (unsigned j = 0; j < mvs.size(); ++j) {
eautomaton::move const& mv = mvs[j];
if (m().is_value(mv.t()) && m().is_value(ch)) {
if (mv.t() == ch) {
add_next(next, mv.dst(), acc);
}
else {
continue;
}
}
else {
cond = m().mk_eq(mv.t(), ch);
if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
add_next(next, mv.dst(), cond);
}
}
}
if (is_sequence(*aut, seq)) {
TRACE("seq", tout << seq << "\n";);
if (seq.empty()) {
result = m().mk_eq(a, m_util.str.mk_empty(m().get_sort(a)));
}
u_map<expr*> const& frontier = maps[select_map];
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
expr_ref_vector ors(m());
for (; it != end; ++it) {
unsigned_vector states;
bool has_final = false;
aut->get_epsilon_closure(it->m_key, states);
for (unsigned i = 0; i < states.size() && !has_final; ++i) {
has_final = aut->is_final_state(states[i]);
}
if (has_final) {
ors.push_back(it->m_value);
}
else {
result = m().mk_eq(a, m_util.str.mk_concat(seq));
}
result = mk_or(ors);
return BR_REWRITE_FULL;
}
return BR_FAILED;
if (!is_sequence(a, seq)) {
return BR_FAILED;
}
expr_ref_vector trail(m());
u_map<expr*> maps[2];
bool select_map = false;
expr_ref ch(m()), cond(m());
eautomaton::moves mvs;
maps[0].insert(aut->init(), m().mk_true());
// is_accepted(a, aut) & some state in frontier is final.
for (unsigned i = 0; i < seq.size(); ++i) {
u_map<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map];
select_map = !select_map;
ch = seq[i].get();
next.reset();
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
for (; it != end; ++it) {
mvs.reset();
unsigned state = it->m_key;
expr* acc = it->m_value;
aut->get_moves_from(state, mvs, false);
for (unsigned j = 0; j < mvs.size(); ++j) {
eautomaton::move const& mv = mvs[j];
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, mv.dst(), acc);
}
else {
continue;
}
}
else {
cond = mv.t()->accept(ch);
if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
add_next(next, mv.dst(), cond);
}
}
}
}
u_map<expr*> const& frontier = maps[select_map];
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
expr_ref_vector ors(m());
for (; it != end; ++it) {
unsigned_vector states;
bool has_final = false;
aut->get_epsilon_closure(it->m_key, states);
for (unsigned i = 0; i < states.size() && !has_final; ++i) {
has_final = aut->is_final_state(states[i]);
}
if (has_final) {
ors.push_back(it->m_value);
}
}
result = mk_or(ors);
return BR_REWRITE_FULL;
}
br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
return BR_FAILED;
@ -823,8 +914,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
sort* s;
VERIFY(m_util.is_re(a, s));
sort_ref seq(m_util.str.mk_seq(s), m());
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a);
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
return BR_REWRITE1;
}
@ -848,7 +938,6 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
expr* a, *b;
zstring s;
bool lchange = false;
SASSERT(lhs.empty());
// solve from back
@ -1237,6 +1326,13 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
found = !rpos.contains(j) && l[i] == r[j];
}
if (!found) {
#if 0
std::cout << mk_pp(l[i], m()) << " not found in ";
for (unsigned j = 0; j < szr; ++j) {
std::cout << mk_pp(r[j], m()) << " ";
}
std::cout << "\n";
#endif
return false;
}
SASSERT(0 < j && j <= szr);

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

@ -26,11 +26,37 @@ Notes:
#include"lbool.h"
#include"automaton.h"
class sym_expr {
bool m_is_pred;
expr_ref m_t;
unsigned m_ref;
sym_expr(bool is_pred, expr_ref& t) : m_is_pred(is_pred), m_t(t), 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); }
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; }
expr* get_char() const { SASSERT(is_char()); return m_t; }
typedef automaton<expr, ast_manager> eautomaton;
};
class sym_expr_manager {
public:
void inc_ref(sym_expr* s) { if (s) s->inc_ref(); }
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
};
typedef automaton<sym_expr, sym_expr_manager> eautomaton;
class re2automaton {
ast_manager& m;
seq_util u;
sym_expr_manager sm;
seq_util u;
bv_util bv;
eautomaton* re2aut(expr* e);
eautomaton* seq2aut(expr* e);
public:
@ -44,6 +70,7 @@ class re2automaton {
class seq_rewriter {
seq_util m_util;
arith_util m_autil;
re2automaton m_re2aut;
expr_ref_vector m_es, m_lhs, m_rhs;
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
@ -75,11 +102,12 @@ class seq_rewriter {
void add_next(u_map<expr*>& next, unsigned idx, expr* cond);
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
bool is_epsilon(expr* e) const;
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) {
m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m) {
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }

92
src/ast/seq_decl_plugin.cpp
View file

@ -22,12 +22,46 @@ Revision History:
#include "ast_pp.h"
#include <sstream>
static bool is_hex_digit(char ch, unsigned& d) {
if ('0' <= ch && ch <= '9') {
d = ch - '0';
return true;
}
if ('A' <= ch && ch <= 'F') {
d = 10 + ch - 'A';
return true;
}
return false;
}
static bool is_escape_char(char const *& s, unsigned& result) {
unsigned d1, d2;
if (*s == '\\' && *(s + 1) == 'x' &&
is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) {
result = d1*16 + d2;
s += 4;
return true;
}
if (*s == '\\' && *(s + 1) == '\\') {
result = '\\';
s += 2;
return true;
}
return false;
}
zstring::zstring(encoding enc): m_encoding(enc) {}
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
while (*s) {
m_buffer.push_back(*s);
++s;
unsigned ch;
if (is_escape_char(s, ch)) {
m_buffer.push_back(ch);
}
else {
m_buffer.push_back(*s);
++s;
}
}
}
@ -80,9 +114,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
return result;
}
static const char esc_table[32][3] =
{ "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
"^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
static const char esc_table[32][6] =
{ "\\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);
@ -91,7 +126,7 @@ std::string zstring::encode() const {
unsigned char ch = m_buffer[i];
if (0 <= ch && ch < 32) {
strm << esc_table[ch];
}
}
else if (ch == 127) {
strm << "^?";
}
@ -250,7 +285,13 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
if (!is_match) {
std::ostringstream strm;
strm << "Sort of function '" << sig.m_name << "' ";
strm << "does not match the declared type";
strm << "does not match the declared type. Given domain: ";
for (unsigned i = 0; i < dsz; ++i) {
strm << mk_pp(dom[i], m) << " ";
}
if (range) {
strm << " and range: " << mk_pp(range, m);
}
m.raise_exception(strm.str().c_str());
}
range_out = apply_binding(binding, sig.m_range);
@ -277,7 +318,19 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
if (!is_match) {
std::ostringstream strm;
strm << "Sort of polymorphic function '" << sig.m_name << "' ";
strm << "does not match the declared type";
strm << "does not match the declared type. ";
strm << "\nGiven domain: ";
for (unsigned i = 0; i < dsz; ++i) {
strm << mk_pp(dom[i], m) << " ";
}
if (range) {
strm << " and range: " << mk_pp(range, m);
}
strm << "\nExpected domain: ";
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) {
@ -319,7 +372,8 @@ void seq_decl_plugin::init() {
parameter paramA(A);
parameter paramS(strT);
sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);
parameter paramSA(seqA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramSA);
sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, &paramS);
sort* boolT = m.mk_bool_sort();
sort* intT = arith_util(m).mk_int();
@ -356,7 +410,7 @@ void seq_decl_plugin::init() {
m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA);
m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA);
m_sigs[OP_RE_LOOP] = alloc(psig, m, "re-loop", 1, 1, &reA, reA);
m_sigs[OP_RE_LOOP] = alloc(psig, m, "re.loop", 1, 1, &reA, reA);
m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
@ -367,7 +421,6 @@ void seq_decl_plugin::init() {
m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT);
m_sigs[_OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT);
m_sigs[_OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
@ -411,7 +464,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
m.raise_exception("invalid regex sort, parameter is not a sort");
}
sort * s = to_sort(parameters[0].get_ast());
return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
}
case _STRING_SORT:
@ -472,7 +524,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_RE_OF_PRED:
case OP_STRING_ITOS:
case OP_STRING_STOI:
case OP_REGEXP_LOOP:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
@ -670,3 +721,18 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
es.push_back(e);
}
}
bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) {
if (is_loop(n)) {
app const* a = to_app(n);
SASSERT(a->get_num_args() == 1);
SASSERT(a->get_decl()->get_num_parameters() == 2);
body = a->get_arg(0);
lo = a->get_decl()->get_parameter(0).get_int();
hi = a->get_decl()->get_parameter(1).get_int();
return true;
}
else {
return false;
}
}

13
src/ast/seq_decl_plugin.h
View file

@ -63,7 +63,6 @@ enum seq_op_kind {
OP_STRING_CONST,
OP_STRING_ITOS,
OP_STRING_STOI,
OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments?
// internal only operators. Converted to SEQ variants.
_OP_STRING_STRREPL,
_OP_STRING_CONCAT,
@ -99,6 +98,7 @@ public:
zstring& operator=(zstring const& other);
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;
unsigned length() const { return m_buffer.size(); }
unsigned operator[](unsigned i) const { return m_buffer[i]; }
@ -299,20 +299,23 @@ public:
bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); }
bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
bool is_intersection(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); }
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); }
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); }
bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); }
bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); }
bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); }
bool is_full(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_SET); }
MATCH_UNARY(is_to_re);
MATCH_BINARY(is_concat);
MATCH_BINARY(is_union);
MATCH_BINARY(is_inter);
MATCH_BINARY(is_intersection);
MATCH_BINARY(is_range);
MATCH_UNARY(is_star);
MATCH_UNARY(is_plus);
MATCH_UNARY(is_opt);
bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
};
str str;

38
src/math/automata/automaton.h
View file

@ -151,7 +151,7 @@ public:
m_final_states(other.m_final_states)
{}
// create the automaton that accepts the empty string only.
// create the automaton that accepts the empty string/sequence only.
static automaton* mk_epsilon(M& m) {
moves mvs;
unsigned_vector final;
@ -168,10 +168,24 @@ public:
return alloc(automaton, m, 0, final, mvs);
}
static automaton* clone(automaton const& a) {
moves mvs;
unsigned_vector final;
append_moves(0, a, mvs);
append_final(0, a, final);
return alloc(automaton, a.m, a.init(), final, mvs);
}
// create the sum of disjoint automata
static automaton* mk_union(automaton const& a, automaton const& b) {
SASSERT(&a.m == &b.m);
M& m = a.m;
if (a.is_empty()) {
return clone(b);
}
if (b.is_empty()) {
return clone(a);
}
moves mvs;
unsigned_vector final;
unsigned offset1 = 1;
@ -196,6 +210,10 @@ public:
init = 0;
mvs.push_back(move(m, 0, a.init() + offset));
}
if (a.is_empty()) {
return clone(a);
}
mvs.push_back(move(m, init, a.final_state() + offset));
append_moves(offset, a, mvs);
append_final(offset, a, final);
@ -206,6 +224,19 @@ public:
static automaton* mk_concat(automaton const& a, automaton const& b) {
SASSERT(&a.m == &b.m);
M& m = a.m;
if (a.is_empty()) {
return clone(a);
}
if (b.is_empty()) {
return clone(b);
}
if (a.is_epsilon()) {
return clone(b);
}
if (b.is_epsilon()) {
return clone(a);
}
moves mvs;
unsigned_vector final;
unsigned init = 0;
@ -295,6 +326,10 @@ public:
// src - e -> dst - ET -> Dst1 => src - ET -> Dst1 if in_degree(dst) = 1, src != dst
// Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst
//
// Some missing:
// src - et -> dst - E -> Dst1 => src - et -> Dst1 if in_degree(dst) = 1
// Src - ET -> dst - e -> dst1 => Src - ET -> dst1 if out_degree(dst) = 1,
//
void compress() {
for (unsigned i = 0; i < m_delta.size(); ++i) {
for (unsigned j = 0; j < m_delta[i].size(); ++j) {
@ -446,6 +481,7 @@ public:
}
bool is_empty() const { return m_final_states.empty(); }
bool is_epsilon() const { return m_final_states.size() == 1 && m_final_states.back() == init() && m_delta.empty(); }
unsigned final_state() const { return m_final_states[0]; }
bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); }
unsigned num_states() const { return m_delta.size(); }

1
src/model/func_interp.cpp
View file

@ -169,6 +169,7 @@ void func_interp::insert_new_entry(expr * const * args, expr * r) {
for (unsigned i = 0; i < m_arity; i++) {
tout << mk_ismt2_pp(args[i], m_manager) << "\n";
}
tout << "Old: " << mk_ismt2_pp(get_entry(args)->get_result(), m_manager) << "\n";
);
SASSERT(get_entry(args) == 0);
func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r);

21
src/muz/base/dl_engine_base.h
View file

@ -44,7 +44,26 @@ namespace datalog {
virtual expr_ref get_answer() = 0;
virtual lbool query(expr* q) = 0;
virtual lbool query(unsigned num_rels, func_decl*const* rels) { return l_undef; }
virtual lbool query(unsigned num_rels, func_decl*const* rels) {
if (num_rels != 1) return l_undef;
expr_ref q(m);
expr_ref_vector args(m);
sort_ref_vector sorts(m);
svector<symbol> names;
func_decl* r = rels[0];
for (unsigned i = 0; i < r->get_arity(); ++i) {
args.push_back(m.mk_var(i, r->get_domain(i)));
sorts.push_back(r->get_domain(i));
names.push_back(symbol(i));
}
sorts.reverse();
names.reverse();
q = m.mk_app(r, args.size(), args.c_ptr());
if (!args.empty()) {
q = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), q);
}
return query(q);
}
virtual void reset_statistics() {}
virtual void display_profile(std::ostream& out) const {}

8
src/muz/fp/dl_cmds.cpp
View file

@ -268,10 +268,10 @@ public:
print_certificate(ctx);
break;
case l_undef:
if(dlctx.get_status() == datalog::BOUNDED){
ctx.regular_stream() << "bounded\n";
print_certificate(ctx);
break;
if (dlctx.get_status() == datalog::BOUNDED){
ctx.regular_stream() << "bounded\n";
print_certificate(ctx);
break;
}
ctx.regular_stream() << "unknown\n";
switch(dlctx.get_status()) {

4
src/parsers/smt2/smt2parser.cpp
View file

@ -399,7 +399,7 @@ namespace smt2 {
void check_keyword(char const * msg) { if (!curr_is_keyword()) throw parser_exception(msg); }
void check_string(char const * msg) { if (!curr_is_string()) throw parser_exception(msg); }
void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
void check_int_or_float(char const * msg) { if (!curr_is_int() || !curr_is_float()) throw parser_exception(msg); }
void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); }
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
void error(unsigned line, unsigned pos, char const * msg) {
@ -2341,7 +2341,7 @@ namespace smt2 {
break;
}
case CPK_NUMERAL:
check_int("invalid command argument, numeral expected");
check_int_or_float("invalid command argument, numeral expected");
m_curr_cmd->set_next_arg(m_ctx, curr_numeral());
next();
break;

1
src/smt/theory_arith.h
View file

@ -547,6 +547,7 @@ namespace smt {
ptr_vector<expr> m_todo;
bool is_int_expr(expr* e);
bool is_int(theory_var v) const { return m_data[v].m_is_int; }
bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
bool is_real(theory_var v) const { return !is_int(v); }
bool get_implied_old_value(theory_var v, inf_numeral & r) const;
inf_numeral const & get_implied_value(theory_var v) const;

10
src/smt/theory_arith_core.h
View file

@ -66,6 +66,9 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::is_int_expr(expr* e) {
#if 0
return m_util.is_int(e);
#else
if (m_util.is_int(e)) return true;
if (is_uninterp(e)) return false;
m_todo.reset();
@ -93,6 +96,7 @@ namespace smt {
}
}
return true;
#endif
}
@ -3073,7 +3077,7 @@ namespace smt {
theory_var num = get_num_vars();
bool refine = false;
for (theory_var v = 0; v < num; v++) {
if (is_int(v))
if (is_int_src(v))
continue;
if (!get_context().is_shared(get_enode(v)))
continue;
@ -3084,7 +3088,7 @@ namespace smt {
rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
theory_var v2;
if (mapping.find(value, v2)) {
SASSERT(!is_int(v2));
SASSERT(!is_int_src(v2));
if (get_value(v) != get_value(v2)) {
// v and v2 are not known to be equal.
// The choice of m_epsilon is making them equal.
@ -3126,7 +3130,7 @@ namespace smt {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v))));
}
// -----------------------------------

16
src/smt/theory_arith_eq.h
View file

@ -43,7 +43,7 @@ namespace smt {
CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v););
SASSERT(lower_bound(v).is_rational());
numeral const & val = lower_bound(v).get_rational();
value_sort_pair key(val, is_int(v));
value_sort_pair key(val, is_int_src(v));
theory_var v2;
if (m_fixed_var_table.find(key, v2)) {
if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
@ -51,7 +51,7 @@ namespace smt {
// The table m_fixed_var_table is not restored during backtrack. So, it may
// contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
// the same sort of v. The following test was missing in a previous version of Z3.
if (!is_equal(v, v2) && is_int(v) == is_int(v2)) {
if (!is_equal(v, v2) && is_int_src(v) == is_int_src(v2)) {
antecedents ante(*this);
//
@ -226,7 +226,7 @@ namespace smt {
if (y == null_theory_var) {
// x is an implied fixed var at k.
value_sort_pair key(k, is_int(x));
value_sort_pair key(k, is_int_src(x));
theory_var x2;
if (m_fixed_var_table.find(key, x2) &&
x2 < static_cast<int>(get_num_vars()) &&
@ -238,7 +238,7 @@ namespace smt {
// So, we must check whether x2 is really equal to k (previous test)
// AND has the same sort of x.
// The following test was missing in a previous version of Z3.
is_int(x) == is_int(x2) &&
is_int_src(x) == is_int_src(x2) &&
!is_equal(x, x2)) {
antecedents ante(*this);
@ -254,7 +254,7 @@ namespace smt {
}
}
if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) {
if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
// found equality x = y
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
@ -294,7 +294,7 @@ namespace smt {
}
if (new_eq) {
if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
if (!is_equal(x, x2) && is_int_src(x) == is_int_src(x2)) {
SASSERT(y == y2 && k == k2);
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
@ -323,12 +323,12 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
// I doesn't make sense to propagate an equality (to the core) of variables of different sort.
SASSERT(is_int(x) == is_int(y));
// Ignore equality if variables are already known to be equal.
if (is_equal(x, y))
return;
// I doesn't make sense to propagate an equality (to the core) of variables of different sort.
if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) {
TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";);
return;
}
context & ctx = get_context();

64
src/smt/theory_seq.cpp
View file

@ -31,8 +31,8 @@ using namespace smt;
struct display_expr {
ast_manager& m;
display_expr(ast_manager& m): m(m) {}
std::ostream& display(std::ostream& out, expr* e) const {
return out << mk_pp(e, m);
std::ostream& display(std::ostream& out, sym_expr* e) const {
return e->display(out);
}
};
@ -165,11 +165,12 @@ theory_seq::theory_seq(ast_manager& m):
m_util(m),
m_autil(m),
m_trail_stack(*this),
m_atoms_qhead(0),
m_ls(m), m_rs(m),
m_lhs(m), m_rhs(m),
m_atoms_qhead(0),
m_new_solution(false),
m_new_propagation(false) {
m_new_propagation(false),
m_mk_aut(m) {
m_prefix = "seq.prefix.suffix";
m_suffix = "seq.suffix.prefix";
m_contains_left = "seq.contains.left";
@ -194,7 +195,6 @@ theory_seq::~theory_seq() {
final_check_status theory_seq::final_check_eh() {
context & ctx = get_context();
TRACE("seq", display(tout););
if (simplify_and_solve_eqs()) {
++m_stats.m_solve_eqs;
@ -760,7 +760,6 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
if (l == r) {
return false;
}
context& ctx = get_context();
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";);
m_new_solution = true;
m_rep.update(l, r, deps);
@ -933,7 +932,6 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
}
bool theory_seq::solve_nqs(unsigned i) {
bool change = false;
context & ctx = get_context();
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
if (solve_ne(i)) {
@ -1179,7 +1177,9 @@ void theory_seq::display(std::ostream & out) const {
for (; it != end; ++it) {
out << mk_pp(it->m_key, m) << "\n";
display_expr disp(m);
it->m_value->display(out, disp);
if (it->m_value) {
it->m_value->display(out, disp);
}
}
}
if (!m_rep.empty()) {
@ -1262,7 +1262,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
m_factory = alloc(seq_factory, get_manager(), get_family_id());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
@ -1288,7 +1288,6 @@ public:
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == m_dependencies.size());
ast_manager& m = mg.get_manager();
if (values.empty()) {
return th.mk_value(n);
}
@ -1326,7 +1325,10 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
if (concats.size() > 1) {
for (unsigned i = 0; i < concats.size(); ++i) {
sv->add_dependency(ctx.get_enode(concats[i]));
expr* e = concats[i];
if (!m_util.str.is_string(e)) {
sv->add_dependency(ctx.get_enode(e));
}
}
}
else if (m_util.str.is_unit(e, e1)) {
@ -1362,7 +1364,8 @@ app* theory_seq::mk_value(app* e) {
unsigned sz;
if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
unsigned v = val.get_unsigned();
if ((0 <= v && v < 7) || (14 <= v && v < 32) || v == 127) {
if (false && ((v < 7) || (14 <= v && v < 32) || v == 127)) {
// disabled: use escape characters.
result = m_util.str.mk_unit(result);
}
else {
@ -1817,7 +1820,6 @@ enode* theory_seq::ensure_enode(expr* e) {
}
static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
ast_manager& m = ctx.get_manager();
theory* th = ctx.get_theory(afid);
if (th && ctx.e_internalized(e)) {
return dynamic_cast<theory_mi_arith*>(th);
@ -1957,11 +1959,10 @@ void theory_seq::add_at_axiom(expr* e) {
void theory_seq::propagate_step(literal lit, expr* step) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(lit) == l_true);
expr* re, *t, *s, *idx, *i, *j;
VERIFY(is_step(step, s, idx, re, i, j, t));
expr_ref nth = mk_nth(s, idx);
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(t, m) << " = " << nth << "\n";);
propagate_eq(lit, t, nth);
expr* re, *acc, *s, *idx, *i, *j;
VERIFY(is_step(step, s, idx, re, i, j, acc));
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
propagate_lit(0, 1, &lit, mk_literal(acc));
rational lo;
rational _idx;
if (lower_bound(s, lo) && lo.is_unsigned() && m_autil.is_numeral(idx, _idx) && lo >= _idx) {
@ -2255,15 +2256,14 @@ eautomaton* theory_seq::get_automaton(expr* re) {
if (m_re2aut.find(re, result)) {
return result;
}
result = re2automaton(m)(re);
result = m_mk_aut(re);
if (result) {
display_expr disp(m);
TRACE("seq", result->display(tout, disp););
}
if (result) {
m_automata.push_back(result);
m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
}
m_automata.push_back(result);
m_trail_stack.push(push_back_vector<theory_seq, scoped_ptr_vector<eautomaton> >(m_automata));
m_re2aut.insert(re, result);
m_trail_stack.push(insert_obj_map<theory_seq, expr, eautomaton*>(m_re2aut, re));
return result;
@ -2286,10 +2286,11 @@ bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, exp
s = to_app(e)->get_arg(0);
idx = to_app(e)->get_arg(1);
re = to_app(e)->get_arg(2);
TRACE("seq", tout << mk_pp(re, m) << "\n";);
VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
SASSERT(r.is_unsigned());
i = r.get_unsigned();
aut = m_re2aut[re];
aut = get_automaton(re);
return true;
}
else {
@ -2316,12 +2317,13 @@ bool theory_seq::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, exp
}
}
expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) {
expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* acc) {
SASSERT(m.is_bool(acc));
expr_ref_vector args(m);
args.push_back(s).push_back(idx).push_back(re);
args.push_back(m_autil.mk_int(i));
args.push_back(m_autil.mk_int(j));
args.push_back(t);
args.push_back(acc);
return expr_ref(m_util.mk_skolem(m_aut_step, args.size(), args.c_ptr(), m.mk_bool_sort()), m);
}
@ -2395,7 +2397,9 @@ bool theory_seq::add_accept2step(expr* acc) {
for (unsigned i = 0; i < mvs.size(); ++i) {
unsigned j = (i + start) % mvs.size();
eautomaton::move mv = mvs[j];
step = mk_step(e, idx, re, src, mv.dst(), mv.t());
expr_ref nth = mk_nth(e, idx);
expr_ref acc = mv.t()->accept(nth);
step = mk_step(e, idx, re, src, mv.dst(), acc);
lits.push_back(mk_literal(step));
switch (ctx.get_assignment(lits.back())) {
case l_true:
@ -2438,8 +2442,8 @@ bool theory_seq::add_accept2step(expr* acc) {
bool theory_seq::add_step2accept(expr* step) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(step) == l_true);
expr* re, *t, *s, *idx, *i, *j;
VERIFY(is_step(step, s, idx, re, i, j, t));
expr* re, *_acc, *s, *idx, *i, *j;
VERIFY(is_step(step, s, idx, re, i, j, _acc));
literal acc1 = mk_accept(s, idx, re, i);
switch (ctx.get_assignment(acc1)) {
case l_false:
@ -2513,7 +2517,7 @@ bool theory_seq::add_reject2reject(expr* rej) {
bool has_undef = false;
for (unsigned i = 0; i < mvs.size(); ++i) {
eautomaton::move const& mv = mvs[i];
literal eq = mk_eq(nth, mv.t(), false);
literal eq = mk_literal(mv.t()->accept(nth));
switch (ctx.get_assignment(eq)) {
case l_false:
case l_true:

3
src/smt/theory_seq.h
View file

@ -278,6 +278,7 @@ namespace smt {
unsigned m_atoms_qhead;
bool m_new_solution; // new solution added
bool m_new_propagation; // new propagation to core
re2automaton m_mk_aut;
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
@ -411,7 +412,7 @@ namespace smt {
return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
}
bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* acc);
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);

8
src/smt/theory_seq_empty.h
View file

@ -26,23 +26,19 @@ namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
ast_manager& m;
proto_model& m_model;
seq_util u;
symbol_set m_strings;
unsigned m_next;
char m_char;
std::string m_unique_delim;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid, proto_model & md):
seq_factory(ast_manager & m, family_id fid):
value_factory(m, fid),
m(m),
m_model(md),
u(m),
m_next(0),
m_char(0),
m_unique_delim("!"),
m_trail(m)
{
@ -129,7 +125,7 @@ namespace smt {
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
virtual void init_model(model_generator & mg) {
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id()));
}
};

24
src/util/mpf.cpp
View file

@ -245,26 +245,30 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
m_mpz_manager.set(exp, exponent);
// Normalize such that 1.0 <= sig < 2.0
if (m_mpq_manager.ge(sig, mpq(2))) {
if (m_mpq_manager.lt(sig, 1)) {
m_mpq_manager.inv(sig);
unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
if (!m_mpq_manager.is_power_of_two(sig, pp)) pp++;
scoped_mpz p2(m_mpz_manager);
m_mpq_manager.power(2, pp, p2);
m_mpq_manager.div(sig, p2, sig);
m_mpz_manager.sub(exp, mpz(pp), exp);
m_mpq_manager.inv(sig);
}
else if (m_mpq_manager.ge(sig, 2)) {
unsigned int pp = m_mpq_manager.prev_power_of_two(sig);
scoped_mpz p2(m_mpz_manager);
m_mpq_manager.power(2, pp, p2);
m_mpq_manager.div(sig, p2, sig);
m_mpz_manager.add(exp, mpz(pp), exp);
}
SASSERT(m_mpq_manager.lt(sig, mpq(2)));
while (m_mpq_manager.lt(sig, 1)) {
m_mpq_manager.mul(sig, 2, sig);
m_mpz_manager.dec(exp);
}
// Check that 1.0 <= sig < 2.0
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
TRACE("mpf_dbg", tout << "Normalized: sig = " << m_mpq_manager.to_string(sig) <<
" exp = " << m_mpz_manager.to_string(exp) << std::endl;);
// Check that 1.0 <= sig < 2.0
SASSERT((m_mpq_manager.le(1, sig) && m_mpq_manager.lt(sig, 2)));
scoped_mpz p(m_mpq_manager);
scoped_mpq t(m_mpq_manager), sq(m_mpq_manager);
m_mpz_manager.power(2, sbits + 3 - 1, p);