mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch '4tXJ7f-fix_build'
This commit is contained in:
commit
ad9127690d
|
@ -71,6 +71,7 @@ VERBOSE=True
|
|||
DEBUG_MODE=False
|
||||
SHOW_CPPS = True
|
||||
VS_X64 = False
|
||||
VS_ARM = False
|
||||
LINUX_X64 = True
|
||||
ONLY_MAKEFILES = False
|
||||
Z3PY_SRC_DIR=None
|
||||
|
@ -99,6 +100,7 @@ USE_OMP=True
|
|||
FPMATH="Default"
|
||||
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
|
||||
|
||||
|
||||
def check_output(cmd):
|
||||
out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
|
||||
if out != None:
|
||||
|
@ -1557,6 +1559,8 @@ class DotNetDLLComponent(Component):
|
|||
if IS_WINDOWS:
|
||||
if VS_X64:
|
||||
cscCmdLine.extend(['/platform:x64'])
|
||||
elif VS_ARM:
|
||||
cscCmdLine.extend(['/platform:arm'])
|
||||
else:
|
||||
cscCmdLine.extend(['/platform:x86'])
|
||||
else:
|
||||
|
@ -1997,6 +2001,8 @@ class DotNetExampleComponent(ExampleComponent):
|
|||
out.write('\t%s /out:%s /reference:%s /debug:full /reference:System.Numerics.dll' % (CSC, exefile, dll))
|
||||
if VS_X64:
|
||||
out.write(' /platform:x64')
|
||||
elif VS_ARM:
|
||||
out.write(' /platform:arm')
|
||||
else:
|
||||
out.write(' /platform:x86')
|
||||
for csfile in get_cs_files(self.ex_dir):
|
||||
|
@ -2186,18 +2192,21 @@ def mk_config():
|
|||
'AR_FLAGS=/nologo\n'
|
||||
'LINK_FLAGS=/nologo /MDd\n'
|
||||
'SLINK_FLAGS=/nologo /LDd\n')
|
||||
if not VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
else:
|
||||
if VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
elif VS_ARM:
|
||||
print("ARM on VS is unsupported")
|
||||
exit(1)
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
else:
|
||||
# Windows Release mode
|
||||
LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
|
||||
|
@ -2209,18 +2218,23 @@ def mk_config():
|
|||
% LTCG)
|
||||
if TRACE:
|
||||
extra_opt = '%s /D _TRACE ' % extra_opt
|
||||
if not VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG))
|
||||
else:
|
||||
if VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
|
||||
'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG))
|
||||
elif VS_ARM:
|
||||
print("ARM on VS is unsupported")
|
||||
exit(1)
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt))
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG))
|
||||
|
||||
|
||||
|
||||
# End of Windows VS config.mk
|
||||
if is_verbose():
|
||||
|
@ -2446,6 +2460,9 @@ def mk_makefile():
|
|||
if VS_X64:
|
||||
print(" platform: x64\n")
|
||||
print("To build Z3, open a [Visual Studio x64 Command Prompt], then")
|
||||
elif VS_ARM:
|
||||
print(" platform: ARM\n")
|
||||
print("To build Z3, open a [Visual Studio ARM Command Prompt], then")
|
||||
else:
|
||||
print(" platform: x86")
|
||||
print("To build Z3, open a [Visual Studio Command Prompt], then")
|
||||
|
|
|
@ -8824,13 +8824,13 @@ def _check_fp_args(a, b):
|
|||
_z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression")
|
||||
|
||||
def fpLT(a, b, ctx=None):
|
||||
"""Create the Z3 floating-point expression `other <= self`.
|
||||
"""Create the Z3 floating-point expression `other < self`.
|
||||
|
||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||
>>> fpLT(x, y)
|
||||
x < y
|
||||
>>> (x <= y).sexpr()
|
||||
'(fp.leq x y)'
|
||||
>>> (x < y).sexpr()
|
||||
'(fp.lt x y)'
|
||||
"""
|
||||
return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
|
||||
|
||||
|
@ -8846,7 +8846,7 @@ def fpLEQ(a, b, ctx=None):
|
|||
return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
|
||||
|
||||
def fpGT(a, b, ctx=None):
|
||||
"""Create the Z3 floating-point expression `other <= self`.
|
||||
"""Create the Z3 floating-point expression `other > self`.
|
||||
|
||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||
>>> fpGT(x, y)
|
||||
|
@ -8857,11 +8857,9 @@ def fpGT(a, b, ctx=None):
|
|||
return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
|
||||
|
||||
def fpGEQ(a, b, ctx=None):
|
||||
"""Create the Z3 floating-point expression `other <= self`.
|
||||
"""Create the Z3 floating-point expression `other >= self`.
|
||||
|
||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||
>>> x + y
|
||||
x + y
|
||||
>>> fpGEQ(x, y)
|
||||
x >= y
|
||||
>>> (x >= y).sexpr()
|
||||
|
@ -8870,7 +8868,7 @@ def fpGEQ(a, b, ctx=None):
|
|||
return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
|
||||
|
||||
def fpEQ(a, b, ctx=None):
|
||||
"""Create the Z3 floating-point expression `other <= self`.
|
||||
"""Create the Z3 floating-point expression `fpEQ(other, self)`.
|
||||
|
||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||
>>> fpEQ(x, y)
|
||||
|
@ -8881,7 +8879,7 @@ def fpEQ(a, b, ctx=None):
|
|||
return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
|
||||
|
||||
def fpNEQ(a, b, ctx=None):
|
||||
"""Create the Z3 floating-point expression `other <= self`.
|
||||
"""Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
|
||||
|
||||
>>> x, y = FPs('x y', FPSort(8, 24))
|
||||
>>> fpNEQ(x, y)
|
||||
|
|
|
@ -30,6 +30,7 @@ Revision History:
|
|||
#include"for_each_ast.h"
|
||||
#include"decl_collector.h"
|
||||
#include"smt2_util.h"
|
||||
#include"seq_decl_plugin.h"
|
||||
|
||||
// ---------------------------------------
|
||||
// smt_renaming
|
||||
|
@ -160,6 +161,7 @@ class smt_printer {
|
|||
unsigned m_num_lets;
|
||||
arith_util m_autil;
|
||||
bv_util m_bvutil;
|
||||
seq_util m_sutil;
|
||||
family_id m_basic_fid;
|
||||
family_id m_bv_fid;
|
||||
family_id m_arith_fid;
|
||||
|
@ -247,6 +249,10 @@ class smt_printer {
|
|||
}
|
||||
|
||||
if (m_is_smt2) {
|
||||
if (is_sort_symbol && sym == symbol("String")) {
|
||||
m_out << "String";
|
||||
return;
|
||||
}
|
||||
if (is_sort_symbol && sym != symbol("BitVec")) {
|
||||
m_out << "(" << sym << " ";
|
||||
}
|
||||
|
@ -397,6 +403,7 @@ class smt_printer {
|
|||
bool is_int, pos;
|
||||
buffer<symbol> names;
|
||||
unsigned bv_size;
|
||||
zstring s;
|
||||
unsigned num_args = n->get_num_args();
|
||||
func_decl* decl = n->get_decl();
|
||||
if (m_autil.is_numeral(n, val, is_int)) {
|
||||
|
@ -415,6 +422,19 @@ class smt_printer {
|
|||
display_rational(val, is_int);
|
||||
}
|
||||
}
|
||||
else if (m_sutil.str.is_string(n, s)) {
|
||||
std::string encs = s.encode();
|
||||
m_out << "\"";
|
||||
for (unsigned i = 0; i < encs.length(); ++i) {
|
||||
if (encs[i] == '\"') {
|
||||
m_out << "\"\"";
|
||||
}
|
||||
else {
|
||||
m_out << encs[i];
|
||||
}
|
||||
}
|
||||
m_out << "\"";
|
||||
}
|
||||
else if (m_bvutil.is_numeral(n, val, bv_size)) {
|
||||
if (m_is_smt2) {
|
||||
m_out << "(_ bv" << val << " " << bv_size << ")";
|
||||
|
@ -797,6 +817,7 @@ public:
|
|||
m_num_lets(0),
|
||||
m_autil(m),
|
||||
m_bvutil(m),
|
||||
m_sutil(m),
|
||||
m_logic(logic),
|
||||
m_AUFLIRA("AUFLIRA"),
|
||||
// It's much easier to read those testcases with that.
|
||||
|
|
|
@ -25,6 +25,8 @@ Notes:
|
|||
#include"automaton.h"
|
||||
#include"well_sorted.h"
|
||||
#include"var_subst.h"
|
||||
#include"symbolic_automata_def.h"
|
||||
|
||||
|
||||
expr_ref sym_expr::accept(expr* e) {
|
||||
ast_manager& m = m_t.get_manager();
|
||||
|
@ -37,6 +39,7 @@ expr_ref sym_expr::accept(expr* e) {
|
|||
}
|
||||
case t_char:
|
||||
SASSERT(m.get_sort(e) == m.get_sort(m_t));
|
||||
SASSERT(m.get_sort(e) == m_sort);
|
||||
result = m.mk_eq(e, m_t);
|
||||
break;
|
||||
case t_range: {
|
||||
|
@ -67,8 +70,114 @@ struct display_expr1 {
|
|||
}
|
||||
};
|
||||
|
||||
class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
|
||||
ast_manager& m;
|
||||
expr_solver& m_solver;
|
||||
typedef sym_expr* T;
|
||||
public:
|
||||
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
|
||||
m(m), m_solver(s) {}
|
||||
|
||||
virtual T mk_false() {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
|
||||
}
|
||||
virtual T mk_true() {
|
||||
expr_ref fml(m.mk_true(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort());
|
||||
}
|
||||
virtual T mk_and(T x, T y) {
|
||||
if (x->is_char() && y->is_char()) {
|
||||
if (x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
if (m.are_distinct(x->get_char(), y->get_char())) {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
}
|
||||
var_ref v(m.mk_var(0, x->get_sort()), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_true(fml1)) return y;
|
||||
if (m.is_true(fml2)) return x;
|
||||
expr_ref fml(m.mk_and(fml1, fml2), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
virtual T mk_or(T x, T y) {
|
||||
if (x->is_char() && y->is_char() &&
|
||||
x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
var_ref v(m.mk_var(0, x->get_sort()), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_false(fml1)) return y;
|
||||
if (m.is_false(fml2)) return x;
|
||||
expr_ref fml(m.mk_or(fml1, fml2), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
|
||||
virtual T mk_and(unsigned sz, T const* ts) {
|
||||
switch (sz) {
|
||||
case 0: return mk_true();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_and(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
virtual T mk_or(unsigned sz, T const* ts) {
|
||||
switch (sz) {
|
||||
case 0: return mk_false();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_or(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
virtual lbool is_sat(T x) {
|
||||
if (x->is_char()) {
|
||||
return l_true;
|
||||
}
|
||||
if (x->is_range()) {
|
||||
// TBD check lower is below upper.
|
||||
}
|
||||
expr_ref v(m.mk_fresh_const("x", x->get_sort()), m);
|
||||
expr_ref fml = x->accept(v);
|
||||
if (m.is_true(fml)) {
|
||||
return l_true;
|
||||
}
|
||||
if (m.is_false(fml)) {
|
||||
return l_false;
|
||||
}
|
||||
return m_solver.check_sat(fml);
|
||||
}
|
||||
virtual T mk_not(T x) {
|
||||
var_ref v(m.mk_var(0, x->get_sort()), m);
|
||||
expr_ref fml(m.mk_not(x->accept(v)), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
};
|
||||
|
||||
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
|
||||
|
||||
re2automaton::~re2automaton() {}
|
||||
|
||||
void re2automaton::set_solver(expr_solver* solver) {
|
||||
m_solver = solver;
|
||||
m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
|
||||
m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
|
||||
}
|
||||
|
||||
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {}
|
||||
|
||||
eautomaton* re2automaton::operator()(expr* e) {
|
||||
eautomaton* r = re2aut(e);
|
||||
|
@ -136,7 +245,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
expr_ref _start(bv.mk_numeral(start, nb), m);
|
||||
expr_ref _stop(bv.mk_numeral(stop, nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
|
||||
|
@ -145,13 +254,14 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _ch(bv.mk_numeral(s1[0], nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
|
||||
expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
|
||||
sort* s = m.get_sort(e2);
|
||||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else {
|
||||
|
@ -187,14 +297,15 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
}
|
||||
else if (u.re.is_full(e)) {
|
||||
expr_ref tt(m.mk_true(), m);
|
||||
sym_expr* _true = sym_expr::mk_pred(tt);
|
||||
sort* seq_s, *char_s;
|
||||
VERIFY (u.is_re(m.get_sort(e), seq_s));
|
||||
VERIFY (u.is_seq(seq_s, char_s));
|
||||
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
|
||||
return eautomaton::mk_loop(sm, _true);
|
||||
}
|
||||
#if 0
|
||||
else if (u.re.is_intersect(e, e1, e2)) {
|
||||
// maybe later
|
||||
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
|
||||
return m_sa->mk_product(*a, *b);
|
||||
}
|
||||
#endif
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
@ -437,7 +548,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
|
|||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
bool all_values = true;
|
||||
|
||||
|
||||
if (bs.empty()) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; all_values && i < bs.size(); ++i) {
|
||||
all_values = m().is_value(bs[i].get());
|
||||
}
|
||||
|
@ -459,6 +575,39 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
unsigned lenA = 0, lenB = 0;
|
||||
bool lA = min_length(as.size(), as.c_ptr(), lenA);
|
||||
if (lA) {
|
||||
bool lB = min_length(bs.size(), bs.c_ptr(), lenB);
|
||||
if (lenB > lenA) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (as.empty()) {
|
||||
result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
unsigned offs = 0;
|
||||
unsigned sz = as.size();
|
||||
expr* b0 = bs[0].get();
|
||||
expr* bL = bs[bs.size()-1].get();
|
||||
for (; offs < as.size() && m().are_distinct(b0, as[offs].get()); ++offs) {};
|
||||
for (; sz > offs && m().are_distinct(bL, as[sz-1].get()); --sz) {}
|
||||
if (offs == sz) {
|
||||
result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (offs > 0 || sz < as.size()) {
|
||||
SASSERT(sz > offs);
|
||||
result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include"params.h"
|
||||
#include"lbool.h"
|
||||
#include"automaton.h"
|
||||
#include"symbolic_automata.h"
|
||||
|
||||
class sym_expr {
|
||||
enum ty {
|
||||
|
@ -33,21 +34,24 @@ class sym_expr {
|
|||
t_range
|
||||
};
|
||||
ty m_ty;
|
||||
sort* m_sort;
|
||||
expr_ref m_t;
|
||||
expr_ref m_s;
|
||||
unsigned m_ref;
|
||||
sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {}
|
||||
sym_expr(ty ty, expr_ref& t, expr_ref& s, sort* srt) : m_ty(ty), m_sort(srt), 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, t_char, t, t); }
|
||||
static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t.get_manager().get_sort(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); }
|
||||
static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s); }
|
||||
static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, lo.get_manager().get_sort(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_ty == t_char; }
|
||||
bool is_pred() const { return !is_char(); }
|
||||
bool is_range() const { return m_ty == t_range; }
|
||||
sort* get_sort() const { return m_sort; }
|
||||
expr* get_char() const { SASSERT(is_char()); return m_t; }
|
||||
|
||||
};
|
||||
|
@ -58,17 +62,31 @@ public:
|
|||
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
|
||||
};
|
||||
|
||||
class expr_solver {
|
||||
public:
|
||||
virtual ~expr_solver() {}
|
||||
virtual lbool check_sat(expr* e) = 0;
|
||||
};
|
||||
|
||||
typedef automaton<sym_expr, sym_expr_manager> eautomaton;
|
||||
class re2automaton {
|
||||
typedef boolean_algebra<sym_expr*> boolean_algebra_t;
|
||||
typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
|
||||
ast_manager& m;
|
||||
sym_expr_manager sm;
|
||||
seq_util u;
|
||||
bv_util bv;
|
||||
scoped_ptr<expr_solver> m_solver;
|
||||
scoped_ptr<boolean_algebra_t> m_ba;
|
||||
scoped_ptr<symbolic_automata_t> m_sa;
|
||||
|
||||
eautomaton* re2aut(expr* e);
|
||||
eautomaton* seq2aut(expr* e);
|
||||
public:
|
||||
public:
|
||||
re2automaton(ast_manager& m);
|
||||
~re2automaton();
|
||||
eautomaton* operator()(expr* e);
|
||||
void set_solver(expr_solver* solver);
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
@ -222,16 +222,16 @@ public:
|
|||
str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
|
||||
|
||||
sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, ¶m); }
|
||||
sort* mk_string_sort() { return m.mk_sort(m_fid, _STRING_SORT, 0, 0); }
|
||||
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
|
||||
sort* mk_string_sort() const { return m.mk_sort(m_fid, _STRING_SORT, 0, 0); }
|
||||
app* mk_empty(sort* s) const { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
|
||||
app* mk_string(zstring const& s);
|
||||
app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
|
||||
app* mk_char(char ch);
|
||||
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
|
||||
app* mk_concat(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
|
||||
app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); }
|
||||
expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
|
||||
expr* mk_concat(expr_ref_vector const& es) { return mk_concat(es.size(), es.c_ptr()); }
|
||||
app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
|
||||
expr* mk_concat(unsigned n, expr* const* es) const { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
|
||||
expr* mk_concat(expr_ref_vector const& es) const { return mk_concat(es.size(), es.c_ptr()); }
|
||||
app* mk_length(expr* a) const { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
|
||||
app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
|
||||
app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
|
||||
app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
|
||||
|
|
|
@ -178,15 +178,19 @@ public:
|
|||
return alloc(automaton, a.m, a.init(), final, mvs);
|
||||
}
|
||||
|
||||
automaton* clone() const {
|
||||
return clone(*this);
|
||||
}
|
||||
|
||||
// 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);
|
||||
return b.clone();
|
||||
}
|
||||
if (b.is_empty()) {
|
||||
return clone(a);
|
||||
return a.clone();
|
||||
}
|
||||
moves mvs;
|
||||
unsigned_vector final;
|
||||
|
@ -213,7 +217,7 @@ public:
|
|||
mvs.push_back(move(m, 0, a.init() + offset));
|
||||
}
|
||||
if (a.is_empty()) {
|
||||
return clone(a);
|
||||
return a.clone();
|
||||
}
|
||||
|
||||
mvs.push_back(move(m, init, a.final_state() + offset));
|
||||
|
@ -227,16 +231,16 @@ public:
|
|||
SASSERT(&a.m == &b.m);
|
||||
M& m = a.m;
|
||||
if (a.is_empty()) {
|
||||
return clone(a);
|
||||
return a.clone();
|
||||
}
|
||||
if (b.is_empty()) {
|
||||
return clone(b);
|
||||
return b.clone();
|
||||
}
|
||||
if (a.is_epsilon()) {
|
||||
return clone(b);
|
||||
return b.clone();
|
||||
}
|
||||
if (b.is_epsilon()) {
|
||||
return clone(a);
|
||||
return a.clone();
|
||||
}
|
||||
|
||||
moves mvs;
|
||||
|
@ -458,6 +462,7 @@ public:
|
|||
}
|
||||
|
||||
unsigned init() const { return m_init; }
|
||||
unsigned_vector const& final_states() const { return m_final_states; }
|
||||
unsigned in_degree(unsigned state) const { return m_delta_inv[state].size(); }
|
||||
unsigned out_degree(unsigned state) const { return m_delta[state].size(); }
|
||||
move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; }
|
||||
|
|
46
src/math/automata/boolean_algebra.h
Normal file
46
src/math/automata/boolean_algebra.h
Normal file
|
@ -0,0 +1,46 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
boolean_algebra.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Boolean Algebra, a la Margus Veanes Automata library.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2016-2-27
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef BOOLEAN_ALGEBRA_H_
|
||||
#define BOOLEAN_ALGEBRA_H_
|
||||
|
||||
#include "util.h"
|
||||
|
||||
template<class T>
|
||||
class positive_boolean_algebra {
|
||||
public:
|
||||
virtual T mk_false() = 0;
|
||||
virtual T mk_true() = 0;
|
||||
virtual T mk_and(T x, T y) = 0;
|
||||
virtual T mk_or(T x, T y) = 0;
|
||||
virtual T mk_and(unsigned sz, T const* ts) = 0;
|
||||
virtual T mk_or(unsigned sz, T const* ts) = 0;
|
||||
virtual lbool is_sat(T x) = 0;
|
||||
};
|
||||
|
||||
template<class T>
|
||||
class boolean_algebra : public positive_boolean_algebra<T> {
|
||||
public:
|
||||
virtual T mk_not(T x) = 0;
|
||||
//virtual lbool are_equivalent(T x, T y) = 0;
|
||||
//virtual T simplify(T x) = 0;
|
||||
};
|
||||
|
||||
#endif
|
108
src/math/automata/symbolic_automata.h
Normal file
108
src/math/automata/symbolic_automata.h
Normal file
|
@ -0,0 +1,108 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
symbolic_automata.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2016-02-27.
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef SYMBOLIC_AUTOMATA_H_
|
||||
#define SYMBOLIC_AUTOMATA_H_
|
||||
|
||||
|
||||
#include "automaton.h"
|
||||
#include "boolean_algebra.h"
|
||||
|
||||
|
||||
template<class T, class M = default_value_manager<T> >
|
||||
class symbolic_automata {
|
||||
typedef automaton<T, M> automaton_t;
|
||||
typedef boolean_algebra<T*> ba_t;
|
||||
typedef typename automaton_t::move move_t;
|
||||
typedef vector<move_t> moves_t;
|
||||
typedef obj_ref<T, M> ref_t;
|
||||
typedef ref_vector<T, M> refs_t;
|
||||
|
||||
M& m;
|
||||
ba_t& m_ba;
|
||||
|
||||
|
||||
class block {
|
||||
uint_set m_set;
|
||||
unsigned m_rep;
|
||||
bool m_rep_chosen;
|
||||
public:
|
||||
|
||||
block(): m_rep(0), m_rep_chosen(false) {}
|
||||
|
||||
block(uint_set const& s):
|
||||
m_set(s),
|
||||
m_rep(0),
|
||||
m_rep_chosen(false) {
|
||||
}
|
||||
|
||||
block(unsigned_vector const& vs) {
|
||||
for (unsigned i = 0; i < vs.size(); ++i) {
|
||||
m_set.insert(vs[i]);
|
||||
}
|
||||
m_rep_chosen = false;
|
||||
m_rep = 0;
|
||||
}
|
||||
|
||||
block& operator=(block const& b) {
|
||||
m_set = b.m_set;
|
||||
m_rep = 0;
|
||||
m_rep_chosen = false;
|
||||
return *this;
|
||||
}
|
||||
|
||||
unsigned get_representative() {
|
||||
if (!m_rep_chosen) {
|
||||
uint_set::iterator it = m_set.begin();
|
||||
if (m_set.end() != it) {
|
||||
m_rep = *it;
|
||||
}
|
||||
m_rep_chosen = true;
|
||||
}
|
||||
return m_rep;
|
||||
}
|
||||
|
||||
void insert(unsigned i) { m_set.insert(i); }
|
||||
bool contains(unsigned i) const { return m_set.contains(i); }
|
||||
bool is_empty() const { return m_set.empty(); }
|
||||
unsigned size() const { return m_set.num_elems(); }
|
||||
void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; }
|
||||
void clear() { m_set.reset(); m_rep_chosen = false; }
|
||||
uint_set::iterator begin() const { return m_set.begin(); }
|
||||
uint_set::iterator end() const { return m_set.end(); }
|
||||
};
|
||||
|
||||
void add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W);
|
||||
|
||||
public:
|
||||
symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
|
||||
automaton_t* mk_determinstic(automaton_t& a);
|
||||
automaton_t* mk_complement(automaton_t& a);
|
||||
automaton_t* remove_epsilons(automaton_t& a);
|
||||
automaton_t* mk_total(automaton_t& a);
|
||||
automaton_t* mk_minimize(automaton_t& a);
|
||||
automaton_t* mk_minimize_total(automaton_t& a);
|
||||
automaton_t* mk_difference(automaton_t& a, automaton_t& b);
|
||||
automaton_t* mk_product(automaton_t& a, automaton_t& b);
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif
|
371
src/math/automata/symbolic_automata_def.h
Normal file
371
src/math/automata/symbolic_automata_def.h
Normal file
|
@ -0,0 +1,371 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
symbolic_automata_def.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2016-02-27.
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef SYMBOLIC_AUTOMATA_DEF_H_
|
||||
#define SYMBOLIC_AUTOMATA_DEF_H_
|
||||
|
||||
|
||||
#include "symbolic_automata.h"
|
||||
#include "hashtable.h"
|
||||
|
||||
typedef std::pair<unsigned, unsigned> unsigned_pair;
|
||||
|
||||
|
||||
|
||||
template<class T, class M>
|
||||
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) {
|
||||
unsigned dead_state = a.num_states();
|
||||
moves_t mvs, new_mvs;
|
||||
for (unsigned i = 0; i < dead_state; ++i) {
|
||||
mvs.reset();
|
||||
a.get_moves_from(i, mvs, true);
|
||||
refs_t vs(m);
|
||||
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
vs.push_back(mvs[j].t());
|
||||
}
|
||||
ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
|
||||
lbool is_sat = m_ba.is_sat(cond);
|
||||
if (is_sat == l_undef) {
|
||||
return 0;
|
||||
}
|
||||
if (is_sat == l_true) {
|
||||
new_mvs.push_back(move_t(m, i, dead_state, cond));
|
||||
}
|
||||
}
|
||||
if (new_mvs.empty()) {
|
||||
return a.clone();
|
||||
}
|
||||
new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true()));
|
||||
|
||||
// TBD private: automaton_t::append_moves(0, a, new_mvs);
|
||||
|
||||
return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs);
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize(automaton_t& a) {
|
||||
if (a.is_empty()) {
|
||||
return a.clone();
|
||||
}
|
||||
|
||||
if (a.is_epsilon()) {
|
||||
return a.clone();
|
||||
}
|
||||
// SASSERT(a.is_deterministic());
|
||||
|
||||
scoped_ptr<automaton_t> fa = mk_total(a);
|
||||
if (!fa) {
|
||||
return 0;
|
||||
}
|
||||
return mk_minimize_total(*fa.get());
|
||||
}
|
||||
|
||||
|
||||
template<class T, class M>
|
||||
void symbolic_automata<T, M>::add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W) {
|
||||
block& p0 = pblocks[p0_index];
|
||||
if (p1.size() < p0.size()) {
|
||||
unsigned p1_index = pblocks.size();
|
||||
pblocks.push_back(p1);
|
||||
for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) {
|
||||
p0.remove(*it);
|
||||
blocks[*it] = p1_index;
|
||||
}
|
||||
if (W.contains(p0_index)) {
|
||||
W.push_back(p1_index);
|
||||
}
|
||||
else if (p0.size() <= p1.size()) {
|
||||
W.push_back(p0_index);
|
||||
}
|
||||
else {
|
||||
W.push_back(p1_index);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize_total(automaton_t& a) {
|
||||
vector<block> pblocks;
|
||||
unsigned_vector blocks;
|
||||
unsigned_vector non_final;
|
||||
for (unsigned i = 0; i < a.num_states(); ++i) {
|
||||
if (!a.is_final_state(i)) {
|
||||
non_final.push_back(i);
|
||||
blocks.push_back(1);
|
||||
}
|
||||
else {
|
||||
blocks.push_back(0);
|
||||
}
|
||||
}
|
||||
pblocks.push_back(block(a.final_states())); // 0 |-> final states
|
||||
pblocks.push_back(block(non_final)); // 1 |-> non-final states
|
||||
|
||||
unsigned_vector W;
|
||||
W.push_back(pblocks[0].size() > pblocks[1].size() ? 1 : 0);
|
||||
|
||||
refs_t trail(m);
|
||||
u_map<T*> gamma;
|
||||
moves_t mvs;
|
||||
while (!W.empty()) {
|
||||
block R(pblocks[W.back()]);
|
||||
W.pop_back();
|
||||
gamma.reset();
|
||||
uint_set::iterator it = R.begin(), end = R.end();
|
||||
for (; it != end; ++it) {
|
||||
unsigned dst = *it;
|
||||
mvs.reset();
|
||||
a.get_moves_to(dst, mvs);
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
unsigned src = mvs[i].src();
|
||||
if (pblocks[src].size() > 1) {
|
||||
T* t = mvs[i].t();
|
||||
T* t1;
|
||||
if (gamma.find(src, t1)) {
|
||||
t = m_ba.mk_or(t, t1);
|
||||
trail.push_back(t);
|
||||
}
|
||||
gamma.insert(src, t);
|
||||
}
|
||||
}
|
||||
}
|
||||
uint_set relevant1;
|
||||
typedef typename u_map<T*>::iterator gamma_iterator;
|
||||
gamma_iterator gend = gamma.end();
|
||||
for (gamma_iterator git = gamma.begin(); git != gend; ++git) {
|
||||
unsigned p0A_index = blocks[git->m_key];
|
||||
if (relevant1.contains(p0A_index)) {
|
||||
continue;
|
||||
}
|
||||
relevant1.insert(p0A_index);
|
||||
block& p0A = pblocks[p0A_index];
|
||||
block p1;
|
||||
for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
|
||||
if (p0A.contains(it->m_key)) p1.insert(it->m_key);
|
||||
}
|
||||
|
||||
add_block(p1, p0A_index, blocks, pblocks, W);
|
||||
|
||||
bool iterate = true;
|
||||
while (iterate) {
|
||||
iterate = false;
|
||||
uint_set relevant2;
|
||||
for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
|
||||
unsigned p0B_index = blocks[it->m_key];
|
||||
if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) {
|
||||
continue;
|
||||
}
|
||||
relevant2.insert(p0B_index);
|
||||
block const& p0B = pblocks[p0B_index];
|
||||
uint_set::iterator bi = p0B.begin(), be = p0B.end();
|
||||
|
||||
block p1;
|
||||
p1.insert(*bi);
|
||||
bool split_found = false;
|
||||
ref_t psi(gamma[*bi], m);
|
||||
++bi;
|
||||
for (; bi != be; ++bi) {
|
||||
unsigned q = *bi;
|
||||
ref_t phi(gamma[q], m);
|
||||
if (split_found) {
|
||||
ref_t phi_and_psi(m_ba.mk_and(phi, psi), m);
|
||||
switch (m_ba.is_sat(phi_and_psi)) {
|
||||
case l_true:
|
||||
p1.insert(q);
|
||||
break;
|
||||
case l_undef:
|
||||
return 0;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
else {
|
||||
ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m);
|
||||
lbool is_sat = m_ba.is_sat(psi_min_phi);
|
||||
if (is_sat == l_undef) {
|
||||
return 0;
|
||||
}
|
||||
if (is_sat == l_true) {
|
||||
psi = psi_min_phi;
|
||||
split_found = true;
|
||||
continue;
|
||||
}
|
||||
// psi is a subset of phi
|
||||
ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m);
|
||||
is_sat = m_ba.is_sat(phi_min_psi);
|
||||
if (is_sat == l_undef) {
|
||||
return 0;
|
||||
}
|
||||
else if (is_sat == l_false) {
|
||||
p1.insert(q); // psi and phi are equivalent
|
||||
}
|
||||
else {
|
||||
p1.clear();
|
||||
p1.insert(q);
|
||||
psi = phi_min_psi;
|
||||
split_found = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (p1.size() < p0B.size() && p0B.size() > 2) iterate = true;
|
||||
add_block(p1, p0B_index, blocks, pblocks, W);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
unsigned new_init = pblocks[blocks[a.init()]].get_representative();
|
||||
|
||||
// set moves
|
||||
map<unsigned_pair, T*, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > conds;
|
||||
svector<unsigned_pair> keys;
|
||||
moves_t new_moves;
|
||||
|
||||
for (unsigned i = 0; i < a.num_states(); ++i) {
|
||||
unsigned src = pblocks[blocks[i]].get_representative();
|
||||
typename automaton_t::moves const& mvs = a.get_moves_from(i);
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative();
|
||||
unsigned_pair st(src, dst);
|
||||
T* t = 0;
|
||||
if (conds.find(st, t)) {
|
||||
t = m_ba.mk_or(t, mvs[j].t());
|
||||
trail.push_back(t);
|
||||
conds.insert(st, t);
|
||||
}
|
||||
else {
|
||||
conds.insert(st, mvs[j].t());
|
||||
keys.push_back(st);
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < keys.size(); ++i) {
|
||||
unsigned_pair st = keys[i];
|
||||
new_moves.push_back(move_t(m, st.first, st.second, conds[st]));
|
||||
}
|
||||
// set final states.
|
||||
unsigned_vector new_final;
|
||||
uint_set new_final_set;
|
||||
for (unsigned i = 0; i < a.final_states().size(); ++i) {
|
||||
unsigned f = pblocks[blocks[a.final_states()[i]]].get_representative();
|
||||
if (!new_final_set.contains(f)) {
|
||||
new_final_set.insert(f);
|
||||
new_final.push_back(f);
|
||||
}
|
||||
}
|
||||
|
||||
return alloc(automaton_t, m, new_init, new_final, new_moves);
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
|
||||
map<unsigned_pair, unsigned, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > state_ids;
|
||||
unsigned_pair init_pair(a.init(), b.init());
|
||||
svector<unsigned_pair> todo;
|
||||
todo.push_back(init_pair);
|
||||
state_ids.insert(init_pair, 0);
|
||||
moves_t mvs;
|
||||
unsigned_vector final;
|
||||
if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
|
||||
final.push_back(0);
|
||||
}
|
||||
if (false) {
|
||||
mk_minimize(a);
|
||||
}
|
||||
unsigned n = 1;
|
||||
moves_t mvsA, mvsB;
|
||||
while (!todo.empty()) {
|
||||
unsigned_pair curr_pair = todo.back();
|
||||
todo.pop_back();
|
||||
unsigned src = state_ids[curr_pair];
|
||||
mvsA.reset(); mvsB.reset();
|
||||
a.get_moves_from(curr_pair.first, mvsA, true);
|
||||
b.get_moves_from(curr_pair.second, mvsB, true);
|
||||
for (unsigned i = 0; i < mvsA.size(); ++i) {
|
||||
for (unsigned j = 0; j < mvsB.size(); ++j) {
|
||||
ref_t ab(m_ba.mk_and(mvsA[i].t(), mvsB[j].t()), m);
|
||||
lbool is_sat = m_ba.is_sat(ab);
|
||||
if (is_sat == l_false) {
|
||||
continue;
|
||||
}
|
||||
else if (is_sat == l_undef) {
|
||||
return 0;
|
||||
}
|
||||
unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst());
|
||||
unsigned tgt;
|
||||
if (!state_ids.find(tgt_pair, tgt)) {
|
||||
tgt = n++;
|
||||
state_ids.insert(tgt_pair, tgt);
|
||||
todo.push_back(tgt_pair);
|
||||
if (a.is_final_state(tgt_pair.first) && b.is_final_state(tgt_pair.second)) {
|
||||
final.push_back(tgt);
|
||||
}
|
||||
}
|
||||
mvs.push_back(move_t(m, src, tgt, ab));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (final.empty()) {
|
||||
return alloc(automaton_t, m);
|
||||
}
|
||||
vector<moves_t> inv(n, moves_t());
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
move_t const& mv = mvs[i];
|
||||
inv[mv.dst()].push_back(move_t(m, mv.dst(), mv.src(), mv.t()));
|
||||
}
|
||||
|
||||
svector<bool> back_reachable(n, false);
|
||||
for (unsigned i = 0; i < final.size(); ++i) {
|
||||
back_reachable[final[i]] = true;
|
||||
}
|
||||
|
||||
unsigned_vector stack(final);
|
||||
while (!stack.empty()) {
|
||||
unsigned state = stack.back();
|
||||
stack.pop_back();
|
||||
moves_t const& mv = inv[state];
|
||||
for (unsigned i = 0; i < mv.size(); ++i) {
|
||||
state = mv[i].dst();
|
||||
if (!back_reachable[state]) {
|
||||
back_reachable[state] = true;
|
||||
stack.push_back(state);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
moves_t mvs1;
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
move_t const& mv = mvs[i];
|
||||
if (back_reachable[mv.dst()]) {
|
||||
mvs1.push_back(mv);
|
||||
}
|
||||
}
|
||||
if (mvs1.empty()) {
|
||||
return alloc(automaton_t, m);
|
||||
}
|
||||
else {
|
||||
return alloc(automaton_t, m, 0, final, mvs1);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
#endif
|
|
@ -435,11 +435,7 @@ namespace datalog {
|
|||
void destroy() {
|
||||
SASSERT(this);
|
||||
this->~base_ancestor();
|
||||
#if _DEBUG
|
||||
memory::deallocate(__FILE__, __LINE__, this);
|
||||
#else
|
||||
memory::deallocate(this);
|
||||
#endif
|
||||
}
|
||||
public:
|
||||
/**
|
||||
|
|
|
@ -425,7 +425,7 @@ private:
|
|||
DEBUG_CODE(
|
||||
for (unsigned i = 0; i < m_fmls.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
VERIFY(m_model->eval(m_fmls[i].get(), tmp));
|
||||
VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));
|
||||
CTRACE("sat", !m.is_true(tmp),
|
||||
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
|
||||
<< " to " << tmp << "\n";
|
||||
|
|
|
@ -99,22 +99,29 @@ namespace smt {
|
|||
This method may update m_antecedents, m_todo_js and m_todo_eqs.
|
||||
*/
|
||||
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
|
||||
ast_manager& m = get_manager();
|
||||
SASSERT(m_antecedents);
|
||||
TRACE("conflict_detail", tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
|
||||
switch (js.get_kind()) {
|
||||
case eq_justification::AXIOM: tout << " axiom\n"; break;
|
||||
case eq_justification::EQUATION:
|
||||
tout << " was asserted\nliteral: "; m_ctx.display_literal(tout, js.get_literal()); tout << "\n";
|
||||
break;
|
||||
case eq_justification::JUSTIFICATION: tout << " justification\n"; break;
|
||||
case eq_justification::CONGRUENCE: tout << " congruence\n"; break;
|
||||
default: break;
|
||||
});
|
||||
|
||||
switch(js.get_kind()) {
|
||||
case eq_justification::AXIOM:
|
||||
TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " axiom\n";);
|
||||
break;
|
||||
case eq_justification::EQUATION:
|
||||
TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " was asserted\n"
|
||||
<< "literal: "; m_ctx.display_literal(tout, js.get_literal()); tout << "\n";);
|
||||
m_antecedents->push_back(js.get_literal());
|
||||
break;
|
||||
case eq_justification::JUSTIFICATION:
|
||||
TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " justification\n";);
|
||||
mark_justification(js.get_justification());
|
||||
break;
|
||||
case eq_justification::CONGRUENCE: {
|
||||
TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " congruence\n";);
|
||||
CTRACE("dyn_ack_target", !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";);
|
||||
m_dyn_ack_manager.used_cg_eh(lhs->get_owner(), rhs->get_owner());
|
||||
unsigned num_args = lhs->get_num_args();
|
||||
|
@ -206,7 +213,6 @@ namespace smt {
|
|||
justification_vector::iterator it = m_todo_js.begin() + old_js_qhead;
|
||||
justification_vector::iterator end = m_todo_js.end();
|
||||
for (; it != end; ++it) {
|
||||
TRACE("conflict_detail", tout << "unmarking: " << *it << "\n";);
|
||||
(*it)->unset_mark();
|
||||
}
|
||||
m_todo_js.shrink(old_js_qhead);
|
||||
|
@ -371,11 +377,9 @@ namespace smt {
|
|||
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
|
||||
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
|
||||
tout << "js.kind: " << js.get_kind() << "\n";
|
||||
tout << "consequent: " << consequent << "\n";
|
||||
for (unsigned i = 0; i < m_assigned_literals.size(); ++i) {
|
||||
tout << m_assigned_literals[i] << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << "consequent: " << consequent << ": ";
|
||||
m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
|
||||
m_ctx.display(tout, js); tout << "\n";
|
||||
);
|
||||
|
||||
// m_conflict_lvl can be smaller than m_ctx.get_search_level() when:
|
||||
|
@ -416,12 +420,12 @@ namespace smt {
|
|||
|
||||
TRACE("conflict",
|
||||
tout << "before minimization:\n";
|
||||
m_ctx.display_literals(tout, m_lemma.size(), m_lemma.c_ptr());
|
||||
m_ctx.display_literals(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
TRACE("conflict_verbose",
|
||||
tout << "before minimization:\n";
|
||||
m_ctx.display_literals_verbose(tout, m_lemma.size(), m_lemma.c_ptr());
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
if (m_params.m_minimize_lemmas)
|
||||
|
@ -429,12 +433,16 @@ namespace smt {
|
|||
|
||||
TRACE("conflict",
|
||||
tout << "after minimization:\n";
|
||||
m_ctx.display_literals(tout, m_lemma.size(), m_lemma.c_ptr());
|
||||
m_ctx.display_literals(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
TRACE("conflict_verbose",
|
||||
tout << "after minimization:\n";
|
||||
m_ctx.display_literals_verbose(tout, m_lemma.size(), m_lemma.c_ptr());
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
TRACE("conflict_bug",
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
|
@ -1423,7 +1431,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
end_unsat_core:
|
||||
TRACE("unsat_core", tout << "assumptions:\n"; m_ctx.display_literals(tout, m_assumptions.size(), m_assumptions.c_ptr()); tout << "\n";);
|
||||
TRACE("unsat_core", tout << "assumptions:\n"; m_ctx.display_literals(tout, m_assumptions); tout << "\n";);
|
||||
reset_unmark_and_justifications(0, 0);
|
||||
}
|
||||
|
||||
|
|
|
@ -114,7 +114,6 @@ namespace smt {
|
|||
|
||||
void mark_justification(justification * js) {
|
||||
if (!js->is_marked()) {
|
||||
TRACE("conflict_detail", tout << "marking: " << js << "\n";);
|
||||
js->set_mark();
|
||||
m_todo_js.push_back(js);
|
||||
}
|
||||
|
@ -126,7 +125,7 @@ namespace smt {
|
|||
std::swap(n1, n2);
|
||||
enode_pair p(n1, n2);
|
||||
if (m_already_processed_eqs.insert_if_not_there(p)) {
|
||||
TRACE("conflict_detail", tout << "marking eq #" << p.first->get_owner_id() << " = #" <<
|
||||
TRACE("conflict_detail_verbose", tout << "marking eq #" << p.first->get_owner_id() << " = #" <<
|
||||
p.second->get_owner_id() << "\n";);
|
||||
m_todo_eqs.push_back(p);
|
||||
SASSERT(m_already_processed_eqs.contains(p));
|
||||
|
@ -168,9 +167,8 @@ namespace smt {
|
|||
void eq_justification2literals(enode * lhs, enode * rhs, eq_justification js);
|
||||
void eq_branch2literals(enode * n1, enode * n2);
|
||||
void eq2literals(enode * n1, enode * n2);
|
||||
void justification2literals_core(justification * js, literal_vector & result);
|
||||
void justification2literals_core(justification * js, literal_vector & result) ;
|
||||
void unmark_justifications(unsigned old_js_qhead);
|
||||
void justification2literals(justification * js, literal_vector & result);
|
||||
|
||||
literal_vector m_tmp_literal_vector;
|
||||
|
||||
|
@ -256,6 +254,9 @@ namespace smt {
|
|||
literal_vector::const_iterator end_unsat_core() const {
|
||||
return m_assumptions.end();
|
||||
}
|
||||
|
||||
void justification2literals(justification * js, literal_vector & result);
|
||||
|
||||
};
|
||||
|
||||
inline void mark_literals(conflict_resolution & cr, unsigned sz, literal const * ls) {
|
||||
|
|
|
@ -295,7 +295,7 @@ namespace smt {
|
|||
|
||||
void context::assign_core(literal l, b_justification j, bool decision) {
|
||||
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
|
||||
display_literal(tout, l); tout << " level: " << m_scope_lvl << "\n";
|
||||
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
|
||||
display(tout, j););
|
||||
SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
|
||||
m_assigned_literals.push_back(l);
|
||||
|
|
|
@ -1176,8 +1176,18 @@ namespace smt {
|
|||
|
||||
void display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const;
|
||||
|
||||
void display_literals(std::ostream & out, literal_vector const& lits) const {
|
||||
display_literals(out, lits.size(), lits.c_ptr());
|
||||
}
|
||||
|
||||
void display_literal_verbose(std::ostream & out, literal lit) const;
|
||||
|
||||
void display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;
|
||||
|
||||
void display_literals_verbose(std::ostream & out, literal_vector const& lits) const {
|
||||
display_literals_verbose(out, lits.size(), lits.c_ptr());
|
||||
}
|
||||
|
||||
void display_watch_list(std::ostream & out, literal l) const;
|
||||
|
||||
void display_watch_lists(std::ostream & out) const;
|
||||
|
|
|
@ -96,6 +96,10 @@ namespace smt {
|
|||
display_compact(out, num_lits, lits, m_bool_var2expr.c_ptr());
|
||||
}
|
||||
|
||||
void context::display_literal_verbose(std::ostream & out, literal lit) const {
|
||||
display_literals_verbose(out, 1, &lit);
|
||||
}
|
||||
|
||||
void context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
|
||||
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n");
|
||||
}
|
||||
|
@ -599,12 +603,16 @@ namespace smt {
|
|||
case b_justification::CLAUSE: {
|
||||
clause * cls = j.get_clause();
|
||||
out << "clause ";
|
||||
display_literals(out, cls->get_num_literals(), cls->begin_literals());
|
||||
if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
|
||||
break;
|
||||
}
|
||||
case b_justification::JUSTIFICATION:
|
||||
out << "justification";
|
||||
case b_justification::JUSTIFICATION: {
|
||||
out << "justification ";
|
||||
literal_vector lits;
|
||||
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
|
||||
display_literals_verbose(out, lits.size(), lits.c_ptr());
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
|
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include "theory_seq.h"
|
||||
#include "ast_trail.h"
|
||||
#include "theory_arith.h"
|
||||
#include "smt_kernel.h"
|
||||
|
||||
using namespace smt;
|
||||
|
||||
|
@ -36,6 +37,21 @@ struct display_expr {
|
|||
}
|
||||
};
|
||||
|
||||
class seq_expr_solver : public expr_solver {
|
||||
kernel m_kernel;
|
||||
public:
|
||||
seq_expr_solver(ast_manager& m, smt_params& fp):
|
||||
m_kernel(m, fp)
|
||||
{}
|
||||
|
||||
virtual lbool check_sat(expr* e) {
|
||||
m_kernel.push();
|
||||
m_kernel.assert_expr(e);
|
||||
lbool r = m_kernel.check();
|
||||
m_kernel.pop(1);
|
||||
return r;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
void theory_seq::solution_map::update(expr* e, expr* r, dependency* d) {
|
||||
|
@ -182,6 +198,7 @@ theory_seq::theory_seq(ast_manager& m):
|
|||
m(m),
|
||||
m_rep(m, m_dm),
|
||||
m_eq_id(0),
|
||||
m_find(*this),
|
||||
m_factory(0),
|
||||
m_exclude(m),
|
||||
m_axioms(m),
|
||||
|
@ -198,28 +215,31 @@ theory_seq::theory_seq(ast_manager& m):
|
|||
m_new_solution(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";
|
||||
m_contains_right = "seq.contains.right";
|
||||
m_accept = "aut.accept";
|
||||
m_reject = "aut.reject";
|
||||
m_prefix = "seq.p.suffix";
|
||||
m_suffix = "seq.s.prefix";
|
||||
m_accept = "aut.accept";
|
||||
m_reject = "aut.reject";
|
||||
m_tail = "seq.tail";
|
||||
m_nth = "seq.nth";
|
||||
m_seq_first = "seq.first";
|
||||
m_seq_last = "seq.last";
|
||||
m_indexof_left = "seq.indexof.left";
|
||||
m_indexof_right = "seq.indexof.right";
|
||||
m_indexof_left = "seq.idx.left";
|
||||
m_indexof_right = "seq.idx.right";
|
||||
m_aut_step = "aut.step";
|
||||
m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l
|
||||
m_post = "seq.post"; // (seq.post s l): suffix of string s of length l
|
||||
m_eq = "seq.eq";
|
||||
|
||||
}
|
||||
|
||||
theory_seq::~theory_seq() {
|
||||
m_trail_stack.reset();
|
||||
}
|
||||
|
||||
void theory_seq::init(context* ctx) {
|
||||
theory::init(ctx);
|
||||
m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
|
||||
}
|
||||
|
||||
final_check_status theory_seq::final_check_eh() {
|
||||
TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
|
||||
|
@ -258,6 +278,11 @@ final_check_status theory_seq::final_check_eh() {
|
|||
TRACE("seq", tout << ">>propagate_automata\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (check_contains()) {
|
||||
++m_stats.m_propagate_contains;
|
||||
TRACE("seq", tout << ">>propagate_contains\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (is_solved()) {
|
||||
TRACE("seq", tout << ">>is_solved\n";);
|
||||
return FC_DONE;
|
||||
|
@ -288,7 +313,7 @@ bool theory_seq::branch_variable() {
|
|||
unsigned id = e.id();
|
||||
|
||||
s = find_branch_start(2*id);
|
||||
TRACE("seq", tout << s << " " << 2*id << ": " << e.ls() << " = " << e.rs() << "\n";);
|
||||
TRACE("seq", tout << s << " " << 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) {
|
||||
|
@ -337,15 +362,15 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
|
|||
return false;
|
||||
}
|
||||
|
||||
TRACE("seq", tout << mk_pp(l, m) << ": " << get_context().get_scope_level() << " - start:" << start << "\n";);
|
||||
|
||||
expr_ref v0(m);
|
||||
v0 = m_util.str.mk_empty(m.get_sort(l));
|
||||
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));
|
||||
}
|
||||
for (; start < rs.size(); ++start) {
|
||||
unsigned j = start;
|
||||
|
@ -370,14 +395,31 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
|
|||
all_units &= m_util.str.is_unit(rs[j]);
|
||||
}
|
||||
if (all_units) {
|
||||
context& ctx = get_context();
|
||||
literal_vector lits;
|
||||
lits.push_back(~mk_eq_empty(l));
|
||||
for (unsigned i = 0; i < rs.size(); ++i) {
|
||||
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));
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
switch (ctx.get_assignment(lits[i])) {
|
||||
case l_true: break;
|
||||
case l_false: start = 0; return true;
|
||||
case l_undef: ctx.force_phase(~lits[i]); start = 0; return true;
|
||||
}
|
||||
}
|
||||
set_conflict(dep, lits);
|
||||
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
|
||||
TRACE("seq",
|
||||
tout << "start: " << start << "\n";
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
ctx.display_literal_verbose(tout << lits[i] << ": ", lits[i]);
|
||||
tout << "\n";
|
||||
ctx.display(tout, ctx.get_justification(lits[i].var()));
|
||||
tout << "\n";
|
||||
});
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
@ -429,10 +471,19 @@ lbool theory_seq::assume_equality(expr* l, expr* r) {
|
|||
if (n1->get_root() == n2->get_root()) {
|
||||
return l_true;
|
||||
}
|
||||
if (ctx.is_diseq(n1, n2)) {
|
||||
return l_false;
|
||||
}
|
||||
if (false && ctx.is_diseq_slow(n1, n2)) {
|
||||
return l_false;
|
||||
}
|
||||
ctx.mark_as_relevant(n1);
|
||||
ctx.mark_as_relevant(n2);
|
||||
ctx.assume_eq(n1, n2);
|
||||
return l_undef;
|
||||
if (!ctx.assume_eq(n1, n2)) {
|
||||
return l_false;
|
||||
}
|
||||
return ctx.get_assignment(mk_eq(l, r, false));
|
||||
//return l_undef;
|
||||
}
|
||||
|
||||
|
||||
|
@ -483,29 +534,50 @@ bool theory_seq::propagate_length_coherence(expr* e) {
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool theory_seq::check_length_coherence(expr* e) {
|
||||
if (is_var(e) && m_rep.is_root(e)) {
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
|
||||
expr_ref head(m), tail(m);
|
||||
if (!propagate_length_coherence(e) &&
|
||||
l_false == assume_equality(e, emp)) {
|
||||
if (!check_length_coherence0(e)) {
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
|
||||
expr_ref head(m), tail(m);
|
||||
// e = emp \/ e = unit(head.elem(e))*tail(e)
|
||||
mk_decompose(e, head, tail);
|
||||
expr_ref conc = mk_concat(head, tail);
|
||||
propagate_is_conc(e, conc);
|
||||
assume_equality(tail, emp);
|
||||
}
|
||||
else if (!get_context().at_base_level()) {
|
||||
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
if (propagate_is_conc(e, conc)) {
|
||||
assume_equality(tail, emp);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::check_length_coherence0(expr* e) {
|
||||
if (is_var(e) && m_rep.is_root(e)) {
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
|
||||
if (propagate_length_coherence(e) ||
|
||||
l_false != assume_equality(e, emp)) {
|
||||
if (!get_context().at_base_level()) {
|
||||
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool theory_seq::check_length_coherence() {
|
||||
|
||||
obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
|
||||
#if 1
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
if (check_length_coherence0(e)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
it = m_length.begin();
|
||||
#endif
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
if (check_length_coherence(e)) {
|
||||
|
@ -533,7 +605,6 @@ bool theory_seq::fixed_length(expr* e) {
|
|||
}
|
||||
if (is_skolem(m_tail, e) || is_skolem(m_seq_first, e) ||
|
||||
is_skolem(m_indexof_left, e) || is_skolem(m_indexof_right, e) ||
|
||||
is_skolem(m_contains_left, e) || is_skolem(m_contains_right, e) ||
|
||||
m_fixed.contains(e)) {
|
||||
return false;
|
||||
}
|
||||
|
@ -543,7 +614,6 @@ bool theory_seq::fixed_length(expr* e) {
|
|||
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
|
||||
m_fixed.insert(e);
|
||||
|
||||
|
||||
unsigned _lo = lo.get_unsigned();
|
||||
expr_ref seq(e, m), head(m), tail(m);
|
||||
expr_ref_vector elems(m);
|
||||
|
@ -571,14 +641,19 @@ void theory_seq::propagate_non_empty(literal lit, expr* s) {
|
|||
propagate_lit(0, 1, &lit, ~mk_eq_empty(s));
|
||||
}
|
||||
|
||||
void theory_seq::propagate_is_conc(expr* e, expr* conc) {
|
||||
bool theory_seq::propagate_is_conc(expr* e, expr* conc) {
|
||||
TRACE("seq", tout << mk_pp(conc, m) << " is non-empty\n";);
|
||||
context& ctx = get_context();
|
||||
literal lit = ~mk_eq_empty(e);
|
||||
SASSERT(ctx.get_assignment(lit) == l_true);
|
||||
propagate_lit(0, 1, &lit, mk_eq(e, conc, false));
|
||||
expr_ref e1(e, m), e2(conc, m);
|
||||
new_eq_eh(m_dm.mk_leaf(assumption(lit)), ctx.get_enode(e1), ctx.get_enode(e2));
|
||||
if (ctx.get_assignment(lit) == l_true) {
|
||||
propagate_lit(0, 1, &lit, mk_eq(e, conc, false));
|
||||
expr_ref e1(e, m), e2(conc, m);
|
||||
new_eq_eh(m_dm.mk_leaf(assumption(lit)), ctx.get_enode(e1), ctx.get_enode(e2));
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool theory_seq::is_nth(expr* e) const {
|
||||
|
@ -718,6 +793,23 @@ bool theory_seq::check_extensionality() {
|
|||
return true;
|
||||
}
|
||||
|
||||
/*
|
||||
\brief check negated contains constriants.
|
||||
*/
|
||||
bool theory_seq::check_contains() {
|
||||
context & ctx = get_context();
|
||||
for (unsigned i = 0; !ctx.inconsistent() && i < m_ncs.size(); ++i) {
|
||||
if (solve_nc(i)) {
|
||||
if (i + 1 != m_ncs.size()) {
|
||||
nc n = m_ncs[m_ncs.size()-1];
|
||||
m_ncs.set(i, n);
|
||||
--i;
|
||||
}
|
||||
m_ncs.pop_back();
|
||||
}
|
||||
}
|
||||
return m_new_propagation || ctx.inconsistent();
|
||||
}
|
||||
/*
|
||||
- Eqs = 0
|
||||
- Diseqs evaluate to false
|
||||
|
@ -763,20 +855,31 @@ void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
|
|||
|
||||
|
||||
void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits, literal lit) {
|
||||
if (lit == true_literal) return;
|
||||
|
||||
context& ctx = get_context();
|
||||
ctx.mark_as_relevant(lit);
|
||||
literal_vector lits(n, _lits);
|
||||
|
||||
if (lit == false_literal) {
|
||||
set_conflict(dep, lits);
|
||||
return;
|
||||
}
|
||||
|
||||
ctx.mark_as_relevant(lit);
|
||||
enode_pair_vector eqs;
|
||||
linearize(dep, eqs, lits);
|
||||
TRACE("seq", ctx.display_detailed_literal(tout, lit);
|
||||
tout << " <- "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); if (!lits.empty()) tout << "\n"; display_deps(tout, dep););
|
||||
TRACE("seq",
|
||||
tout << "assert:";
|
||||
ctx.display_detailed_literal(tout, lit);
|
||||
tout << " <- "; ctx.display_literals_verbose(tout, lits);
|
||||
if (!lits.empty()) tout << "\n"; display_deps(tout, dep););
|
||||
justification* js =
|
||||
ctx.mk_justification(
|
||||
ext_theory_propagation_justification(
|
||||
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit));
|
||||
|
||||
m_new_propagation = true;
|
||||
ctx.assign(lit, js);
|
||||
ctx.assign(lit, js);
|
||||
}
|
||||
|
||||
void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
|
||||
|
@ -784,7 +887,7 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
|
|||
enode_pair_vector eqs;
|
||||
literal_vector lits(_lits);
|
||||
linearize(dep, eqs, lits);
|
||||
TRACE("seq", display_deps(tout, lits, eqs););
|
||||
TRACE("seq", display_deps(tout << "assert conflict:", lits, eqs););
|
||||
m_new_propagation = true;
|
||||
ctx.set_conflict(
|
||||
ctx.mk_justification(
|
||||
|
@ -801,8 +904,8 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
|
|||
enode_pair_vector eqs;
|
||||
linearize(dep, eqs, lits);
|
||||
TRACE("seq",
|
||||
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- \n";
|
||||
display_deps(tout, dep);
|
||||
tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
|
||||
display_deps(tout, dep);
|
||||
);
|
||||
|
||||
justification* js = ctx.mk_justification(
|
||||
|
@ -860,6 +963,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
|
|||
// no-op
|
||||
}
|
||||
else if (m_util.is_seq(li) || m_util.is_re(li)) {
|
||||
TRACE("seq", tout << "inserting " << li << " = " << ri << "\n";);
|
||||
m_eqs.push_back(mk_eqdep(li, ri, deps));
|
||||
}
|
||||
else {
|
||||
|
@ -1017,6 +1121,7 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
|
|||
return true;
|
||||
}
|
||||
if (!ctx.inconsistent() && change) {
|
||||
TRACE("seq", tout << "inserting equality\n";);
|
||||
m_eqs.push_back(eq(m_eq_id++, ls, rs, deps));
|
||||
return true;
|
||||
}
|
||||
|
@ -1485,6 +1590,30 @@ bool theory_seq::solve_ne(unsigned idx) {
|
|||
return updated;
|
||||
}
|
||||
|
||||
bool theory_seq::solve_nc(unsigned idx) {
|
||||
context& ctx = get_context();
|
||||
nc const& n = m_ncs[idx];
|
||||
|
||||
dependency* deps = n.deps();
|
||||
expr_ref c = canonize(n.contains(), deps);
|
||||
|
||||
CTRACE("seq", c != n.contains(), tout << n.contains() << " => " << c << "\n";);
|
||||
|
||||
if (m.is_true(c)) {
|
||||
literal_vector lits;
|
||||
set_conflict(deps, lits);
|
||||
return true;
|
||||
}
|
||||
if (m.is_false(c)) {
|
||||
return true;
|
||||
}
|
||||
if (c != n.contains()) {
|
||||
m_ncs.push_back(nc(c, deps));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
|
||||
cell* c = alloc(cell, p, e, d);
|
||||
m_all_cells.push_back(c);
|
||||
|
@ -1748,6 +1877,20 @@ void theory_seq::display(std::ostream & out) const {
|
|||
out << "Exclusions:\n";
|
||||
m_exclude.display(out);
|
||||
}
|
||||
|
||||
if (!m_length.empty()) {
|
||||
obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
rational lo(-1), hi(-1);
|
||||
lower_bound(e, lo);
|
||||
upper_bound(e, hi);
|
||||
if (lo.is_pos() || !hi.is_minus_one()) {
|
||||
out << mk_pp(e, m) << " [" << lo << ":" << hi << "]\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void theory_seq::display_equations(std::ostream& out) const {
|
||||
|
@ -1974,6 +2117,7 @@ theory_var theory_seq::mk_var(enode* n) {
|
|||
}
|
||||
else {
|
||||
theory_var v = theory::mk_var(n);
|
||||
m_find.mk_var();
|
||||
get_context().attach_th_var(n, this, v);
|
||||
get_context().mark_as_relevant(n);
|
||||
return v;
|
||||
|
@ -2033,7 +2177,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
|
|||
return result;
|
||||
}
|
||||
expr* e = m_rep.find(e0, deps);
|
||||
expr* e1, *e2;
|
||||
expr* e1, *e2, *e3;
|
||||
if (m_util.str.is_concat(e, e1, e2)) {
|
||||
result = mk_concat(expand(e1, deps), expand(e2, deps));
|
||||
}
|
||||
|
@ -2052,6 +2196,12 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
|
|||
else if (m_util.str.is_unit(e, e1)) {
|
||||
result = m_util.str.mk_unit(expand(e1, deps));
|
||||
}
|
||||
else if (m_util.str.is_index(e, e1, e2)) {
|
||||
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0));
|
||||
}
|
||||
else if (m_util.str.is_index(e, e1, e2, e3)) {
|
||||
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3);
|
||||
}
|
||||
else {
|
||||
result = e;
|
||||
}
|
||||
|
@ -2180,7 +2330,6 @@ void theory_seq::add_indexof_axiom(expr* i) {
|
|||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref xsy(m);
|
||||
|
||||
|
||||
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
|
||||
expr_ref x = mk_skolem(m_indexof_left, t, s);
|
||||
expr_ref y = mk_skolem(m_indexof_right, t, s);
|
||||
|
@ -2356,7 +2505,7 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
|
|||
propagate_lit(0, 1, &lit, lits[1]);
|
||||
}
|
||||
else {
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
}
|
||||
}
|
||||
|
@ -2389,7 +2538,7 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
|
|||
}
|
||||
}
|
||||
|
||||
bool theory_seq::lower_bound(expr* _e, rational& lo) {
|
||||
bool theory_seq::lower_bound(expr* _e, rational& lo) const {
|
||||
context& ctx = get_context();
|
||||
expr_ref e(m_util.str.mk_length(_e), m);
|
||||
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
|
||||
|
@ -2398,7 +2547,7 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) {
|
|||
return m_autil.is_numeral(_lo, lo) && lo.is_int();
|
||||
}
|
||||
|
||||
bool theory_seq::upper_bound(expr* _e, rational& hi) {
|
||||
bool theory_seq::upper_bound(expr* _e, rational& hi) const {
|
||||
context& ctx = get_context();
|
||||
expr_ref e(m_util.str.mk_length(_e), m);
|
||||
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
|
||||
|
@ -2407,7 +2556,7 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) {
|
|||
return m_autil.is_numeral(_hi, hi) && hi.is_int();
|
||||
}
|
||||
|
||||
bool theory_seq::get_length(expr* e, rational& val) {
|
||||
bool theory_seq::get_length(expr* e, rational& val) const {
|
||||
context& ctx = get_context();
|
||||
theory* th = ctx.get_theory(m_autil.get_family_id());
|
||||
if (!th) return false;
|
||||
|
@ -2677,7 +2826,7 @@ literal theory_seq::mk_seq_eq(expr* a, expr* b) {
|
|||
return mk_literal(mk_skolem(m_eq, a, b, 0, m.mk_bool_sort()));
|
||||
}
|
||||
|
||||
literal theory_seq::mk_eq_empty(expr* _e) {
|
||||
literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
|
||||
context& ctx = get_context();
|
||||
expr_ref e(_e, m);
|
||||
SASSERT(m_util.is_seq(e));
|
||||
|
@ -2699,7 +2848,7 @@ literal theory_seq::mk_eq_empty(expr* _e) {
|
|||
emp = m_util.str.mk_empty(m.get_sort(e));
|
||||
|
||||
literal lit = mk_eq(e, emp, false);
|
||||
ctx.force_phase(lit);
|
||||
ctx.force_phase(phase?lit:~lit);
|
||||
ctx.mark_as_relevant(lit);
|
||||
return lit;
|
||||
}
|
||||
|
@ -2713,7 +2862,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
|
|||
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); }
|
||||
if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); }
|
||||
TRACE("seq", ctx.display_literals_verbose(tout << "axiom: ", lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
TRACE("seq", ctx.display_literals_verbose(tout << "assert: ", lits); tout << "\n";);
|
||||
m_new_propagation = true;
|
||||
++m_stats.m_add_axiom;
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
|
@ -2770,8 +2919,8 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
|
|||
new_eq_eh(deps, n1, n2);
|
||||
}
|
||||
TRACE("seq",
|
||||
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
|
||||
tout << " => " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
|
||||
tout << "assert: " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << " <- \n";
|
||||
if (!lits.empty()) { ctx.display_literals_verbose(tout, lits); tout << "\n"; });
|
||||
justification* js =
|
||||
ctx.mk_justification(
|
||||
ext_theory_eq_propagation_justification(
|
||||
|
@ -2798,7 +2947,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
}
|
||||
else {
|
||||
#if 0
|
||||
propagate_not_prefix(e);
|
||||
propagate_not_prefix2(e);
|
||||
#else
|
||||
propagate_non_empty(lit, e1);
|
||||
if (add_prefix2prefix(e, change)) {
|
||||
|
@ -2836,17 +2985,22 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
}
|
||||
else if (m_util.str.is_contains(e, e1, e2)) {
|
||||
if (is_true) {
|
||||
expr_ref f1 = mk_skolem(m_contains_left, e1, e2);
|
||||
expr_ref f2 = mk_skolem(m_contains_right, e1, e2);
|
||||
expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
|
||||
expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
|
||||
f = mk_concat(f1, e2, f2);
|
||||
propagate_eq(lit, f, e1, true);
|
||||
}
|
||||
else if (!canonizes(false, e)) {
|
||||
propagate_non_empty(lit, e2);
|
||||
#if 1
|
||||
dependency* dep = m_dm.mk_leaf(assumption(lit));
|
||||
m_ncs.push_back(nc(expr_ref(e, m), dep));
|
||||
#else
|
||||
propagate_lit(0, 1, &lit, ~mk_literal(m_util.str.mk_prefix(e2, e1)));
|
||||
if (add_contains2contains(e, change)) {
|
||||
add_atom(e);
|
||||
}
|
||||
#endif
|
||||
}
|
||||
}
|
||||
else if (is_accept(e)) {
|
||||
|
@ -2898,6 +3052,12 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
|
|||
|
||||
void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
|
||||
if (n1 != n2 && m_util.is_seq(n1->get_owner())) {
|
||||
theory_var v1 = n1->get_th_var(get_id());
|
||||
theory_var v2 = n2->get_th_var(get_id());
|
||||
if (m_find.find(v1) == m_find.find(v2)) {
|
||||
return;
|
||||
}
|
||||
m_find.merge(v1, v2);
|
||||
expr_ref o1(n1->get_owner(), m);
|
||||
expr_ref o2(n2->get_owner(), m);
|
||||
TRACE("seq", tout << o1 << " = " << o2 << "\n";);
|
||||
|
@ -2916,7 +3076,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
|
|||
expr_ref eq(m.mk_eq(e1, e2), m);
|
||||
m_rewrite(eq);
|
||||
if (!m.is_false(eq)) {
|
||||
TRACE("seq", tout << "new disequality: " << eq << "\n";);
|
||||
TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);
|
||||
|
||||
literal lit = mk_eq(e1, e2, false);
|
||||
|
||||
|
@ -2975,6 +3135,7 @@ void theory_seq::push_scope_eh() {
|
|||
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
|
||||
m_eqs.push_scope();
|
||||
m_nqs.push_scope();
|
||||
m_ncs.push_scope();
|
||||
m_atoms_lim.push_back(m_atoms.size());
|
||||
}
|
||||
|
||||
|
@ -2987,6 +3148,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) {
|
|||
m_exclude.pop_scope(num_scopes);
|
||||
m_eqs.pop_scope(num_scopes);
|
||||
m_nqs.pop_scope(num_scopes);
|
||||
m_ncs.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();
|
||||
|
@ -3191,7 +3353,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
|
|||
if (has_undef) {
|
||||
return true;
|
||||
}
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
SASSERT(ctx.get_assignment(lits[i]) == l_false);
|
||||
lits[i].neg();
|
||||
|
@ -3341,6 +3503,32 @@ void theory_seq::propagate_not_prefix(expr* e) {
|
|||
add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
|
||||
}
|
||||
|
||||
/*
|
||||
!prefix(e1,e2) => len(e1) > 0
|
||||
!prefix(e1,e2) => len(e1) > len(e2) or e2 = pre(e2,len(e1))post(e2,len(e2)-len(e1)) & pre(e2, len(e1)) != e1
|
||||
*/
|
||||
|
||||
void theory_seq::propagate_not_prefix2(expr* e) {
|
||||
context& ctx = get_context();
|
||||
expr* e1, *e2;
|
||||
VERIFY(m_util.str.is_prefix(e, e1, e2));
|
||||
literal lit = ctx.get_literal(e);
|
||||
SASSERT(ctx.get_assignment(lit) == l_false);
|
||||
if (canonizes(false, e)) {
|
||||
return;
|
||||
}
|
||||
propagate_non_empty(~lit, e1);
|
||||
expr_ref len_e1(m_util.str.mk_length(e1), m);
|
||||
expr_ref len_e2(m_util.str.mk_length(e2), m);
|
||||
expr_ref len_e2_e1(mk_sub(len_e2, len_e1), m);
|
||||
expr_ref x = mk_skolem(m_pre, e2, len_e1);
|
||||
expr_ref y = mk_skolem(m_post, e2, len_e2_e1);
|
||||
literal e2_ge_e1 = mk_literal(m_autil.mk_ge(len_e2_e1, m_autil.mk_int(0)));
|
||||
add_axiom(lit, ~e2_ge_e1, mk_seq_eq(e2, mk_concat(x, y)));
|
||||
add_axiom(lit, ~e2_ge_e1, mk_eq(m_util.str.mk_length(x), len_e1, false));
|
||||
add_axiom(lit, ~e2_ge_e1, ~mk_eq(e1, x, false));
|
||||
}
|
||||
|
||||
/*
|
||||
!suffix(e1,e2) => e1 != ""
|
||||
!suffix(e1,e2) => e2 = "" or e1 = ycx & (e2 = zdx & c != d or x = e2)
|
||||
|
@ -3391,7 +3579,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
|
|||
switch (ctx.get_assignment(e2_is_emp)) {
|
||||
case l_true:
|
||||
TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e2, m) << " = empty\n";
|
||||
ctx.display_literals_verbose(tout, 1, &e2_is_emp); tout << "\n"; );
|
||||
ctx.display_literal_verbose(tout, e2_is_emp); tout << "\n"; );
|
||||
return false; // done
|
||||
case l_undef:
|
||||
// ctx.force_phase(e2_is_emp);
|
||||
|
@ -3405,7 +3593,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
|
|||
conc = mk_concat(head2, tail2);
|
||||
propagate_eq(~e2_is_emp, e2, conc, true);
|
||||
|
||||
literal e1_is_emp = mk_eq_empty(e1);
|
||||
literal e1_is_emp = mk_eq_empty(e1, false);
|
||||
switch (ctx.get_assignment(e1_is_emp)) {
|
||||
case l_true:
|
||||
TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " != empty\n";);
|
||||
|
|
|
@ -28,6 +28,7 @@ Revision History:
|
|||
#include "scoped_ptr_vector.h"
|
||||
#include "automaton.h"
|
||||
#include "seq_rewriter.h"
|
||||
#include "union_find.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -44,6 +45,7 @@ namespace smt {
|
|||
typedef trail_stack<theory_seq> th_trail_stack;
|
||||
typedef std::pair<expr*, dependency*> expr_dep;
|
||||
typedef obj_map<expr, expr_dep> eqdep_map_t;
|
||||
typedef union_find<theory_seq> th_union_find;
|
||||
|
||||
class seq_value_proc;
|
||||
|
||||
|
@ -191,6 +193,27 @@ namespace smt {
|
|||
expr_ref const& r() const { return m_r; }
|
||||
};
|
||||
|
||||
class nc {
|
||||
expr_ref m_contains;
|
||||
dependency* m_dep;
|
||||
public:
|
||||
nc(expr_ref const& c, dependency* dep):
|
||||
m_contains(c),
|
||||
m_dep(dep) {}
|
||||
nc(nc const& other):
|
||||
m_contains(other.m_contains),
|
||||
m_dep(other.m_dep) {}
|
||||
nc& operator=(nc const& other) {
|
||||
if (this != &other) {
|
||||
m_contains = other.m_contains;
|
||||
m_dep = other.m_dep;
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
dependency* deps() const { return m_dep; }
|
||||
expr_ref const& contains() const { return m_contains; }
|
||||
};
|
||||
|
||||
class apply {
|
||||
public:
|
||||
virtual ~apply() {}
|
||||
|
@ -263,13 +286,16 @@ namespace smt {
|
|||
unsigned m_add_axiom;
|
||||
unsigned m_extensionality;
|
||||
unsigned m_fixed_length;
|
||||
unsigned m_propagate_contains;
|
||||
};
|
||||
ast_manager& m;
|
||||
dependency_manager m_dm;
|
||||
solution_map m_rep; // unification representative.
|
||||
scoped_vector<eq> m_eqs; // set of current equations.
|
||||
scoped_vector<ne> m_nqs; // set of current disequalities.
|
||||
unsigned m_eq_id;
|
||||
scoped_vector<nc> m_ncs; // set of non-contains constraints.
|
||||
unsigned m_eq_id;
|
||||
th_union_find m_find;
|
||||
|
||||
seq_factory* m_factory; // value factory
|
||||
exclusion_table m_exclude; // set of asserted disequalities.
|
||||
|
@ -286,7 +312,7 @@ namespace smt {
|
|||
arith_util m_autil;
|
||||
th_trail_stack m_trail_stack;
|
||||
stats m_stats;
|
||||
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
|
||||
symbol m_prefix, m_suffix, m_accept, m_reject;
|
||||
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
|
||||
symbol m_pre, m_post, m_eq;
|
||||
ptr_vector<expr> m_todo;
|
||||
|
@ -306,6 +332,7 @@ namespace smt {
|
|||
|
||||
obj_hashtable<expr> m_fixed; // string variables that are fixed length.
|
||||
|
||||
virtual void init(context* ctx);
|
||||
virtual final_check_status final_check_eh();
|
||||
virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
|
||||
virtual bool internalize_term(app*);
|
||||
|
@ -335,12 +362,14 @@ namespace smt {
|
|||
bool split_variable(); // split a variable
|
||||
bool is_solved();
|
||||
bool check_length_coherence();
|
||||
bool check_length_coherence0(expr* e);
|
||||
bool check_length_coherence(expr* e);
|
||||
bool fixed_length();
|
||||
bool fixed_length(expr* e);
|
||||
bool propagate_length_coherence(expr* e);
|
||||
|
||||
bool check_extensionality();
|
||||
bool check_contains();
|
||||
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);
|
||||
|
@ -362,6 +391,7 @@ namespace smt {
|
|||
expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
|
||||
bool solve_nqs(unsigned i);
|
||||
bool solve_ne(unsigned i);
|
||||
bool solve_nc(unsigned i);
|
||||
|
||||
struct cell {
|
||||
cell* m_parent;
|
||||
|
@ -441,7 +471,7 @@ namespace smt {
|
|||
void add_at_axiom(expr* n);
|
||||
void add_in_re_axiom(expr* n);
|
||||
literal mk_literal(expr* n);
|
||||
literal mk_eq_empty(expr* n);
|
||||
literal mk_eq_empty(expr* n, bool phase = true);
|
||||
literal mk_seq_eq(expr* a, expr* b);
|
||||
void tightest_prefix(expr* s, expr* x);
|
||||
expr_ref mk_sub(expr* a, expr* b);
|
||||
|
@ -452,9 +482,9 @@ namespace smt {
|
|||
|
||||
|
||||
// arithmetic integration
|
||||
bool lower_bound(expr* s, rational& lo);
|
||||
bool upper_bound(expr* s, rational& hi);
|
||||
bool get_length(expr* s, rational& val);
|
||||
bool lower_bound(expr* s, rational& lo) const;
|
||||
bool upper_bound(expr* s, rational& hi) const;
|
||||
bool get_length(expr* s, rational& val) const;
|
||||
|
||||
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
|
||||
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
|
||||
|
@ -489,11 +519,12 @@ namespace smt {
|
|||
bool add_suffix2suffix(expr* e, bool& change);
|
||||
bool add_contains2contains(expr* e, bool& change);
|
||||
void propagate_not_prefix(expr* e);
|
||||
void propagate_not_prefix2(expr* e);
|
||||
void propagate_not_suffix(expr* e);
|
||||
void ensure_nth(literal lit, expr* s, expr* idx);
|
||||
bool canonizes(bool sign, expr* e);
|
||||
void propagate_non_empty(literal lit, expr* s);
|
||||
void propagate_is_conc(expr* e, expr* conc);
|
||||
bool propagate_is_conc(expr* e, expr* conc);
|
||||
void propagate_acc_rej_length(literal lit, expr* acc_rej);
|
||||
bool propagate_automata();
|
||||
void add_atom(expr* e);
|
||||
|
@ -512,6 +543,11 @@ namespace smt {
|
|||
// model building
|
||||
app* mk_value(app* a);
|
||||
|
||||
th_trail_stack& get_trail_stack() { return m_trail_stack; }
|
||||
void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
|
||||
void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
|
||||
void unmerge_eh(theory_var v1, theory_var v2) {}
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
@ -20,9 +20,11 @@ Author:
|
|||
#include "ctx_simplify_tactic.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
#include "ast_pp.h"
|
||||
#include <climits>
|
||||
|
||||
static rational uMaxInt(unsigned sz) {
|
||||
return rational::power_of_two(sz) - rational::one();
|
||||
static uint64 uMaxInt(unsigned sz) {
|
||||
SASSERT(sz <= 64);
|
||||
return ULLONG_MAX >> (64u - sz);
|
||||
}
|
||||
|
||||
namespace {
|
||||
|
@ -30,31 +32,32 @@ namespace {
|
|||
struct interval {
|
||||
// l < h: [l, h]
|
||||
// l > h: [0, h] U [l, UMAX_INT]
|
||||
rational l, h;
|
||||
uint64 l, h;
|
||||
unsigned sz;
|
||||
bool tight;
|
||||
|
||||
explicit interval() : l(0), h(0), sz(0), tight(false) {}
|
||||
interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
|
||||
interval() {}
|
||||
interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
|
||||
// canonicalize full set
|
||||
if (is_wrapped() && l == h + rational::one()) {
|
||||
this->l = rational::zero();
|
||||
if (is_wrapped() && l == h + 1) {
|
||||
this->l = 0;
|
||||
this->h = uMaxInt(sz);
|
||||
}
|
||||
SASSERT(invariant());
|
||||
}
|
||||
|
||||
bool invariant() const {
|
||||
return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
|
||||
(!is_wrapped() || l != h+rational::one());
|
||||
return l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
|
||||
(!is_wrapped() || l != h+1);
|
||||
}
|
||||
|
||||
bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
|
||||
bool is_full() const { return l == 0 && h == uMaxInt(sz); }
|
||||
bool is_wrapped() const { return l > h; }
|
||||
bool is_singleton() const { return l == h; }
|
||||
|
||||
bool operator==(const interval& b) const {
|
||||
SASSERT(sz == b.sz);
|
||||
return l == b.l && h == b.h;
|
||||
return l == b.l && h == b.h && tight == b.tight;
|
||||
}
|
||||
bool operator!=(const interval& b) const { return !(*this == b); }
|
||||
|
||||
|
@ -79,7 +82,7 @@ struct interval {
|
|||
|
||||
/// return false if intersection is unsat
|
||||
bool intersect(const interval& b, interval& result) const {
|
||||
if (is_full() || (l == b.l && h == b.h)) {
|
||||
if (is_full() || *this == b) {
|
||||
result = b;
|
||||
return true;
|
||||
}
|
||||
|
@ -128,18 +131,18 @@ struct interval {
|
|||
/// return false if negation is empty
|
||||
bool negate(interval& result) const {
|
||||
if (!tight) {
|
||||
result = interval(rational::zero(), uMaxInt(sz), true);
|
||||
result = interval(0, uMaxInt(sz), true);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (is_full())
|
||||
return false;
|
||||
if (l.is_zero()) {
|
||||
result = interval(h + rational::one(), uMaxInt(sz), sz);
|
||||
if (l == 0) {
|
||||
result = interval(h + 1, uMaxInt(sz), sz);
|
||||
} else if (uMaxInt(sz) == h) {
|
||||
result = interval(rational::zero(), l - rational::one(), sz);
|
||||
result = interval(0, l - 1, sz);
|
||||
} else {
|
||||
result = interval(h + rational::one(), l - rational::one(), sz);
|
||||
result = interval(h + 1, l - 1, sz);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -151,59 +154,76 @@ std::ostream& operator<<(std::ostream& o, const interval& I) {
|
|||
}
|
||||
|
||||
|
||||
struct undo_bound {
|
||||
expr* e;
|
||||
interval b;
|
||||
bool fresh;
|
||||
undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {}
|
||||
};
|
||||
|
||||
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
||||
typedef obj_map<expr, interval> map;
|
||||
typedef obj_map<expr, bool> expr_set;
|
||||
typedef obj_map<expr, unsigned> expr_cnt;
|
||||
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
bool m_propagate_eq;
|
||||
bv_util m_bv;
|
||||
vector<map> m_scopes;
|
||||
map *m_bound;
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
bool m_propagate_eq;
|
||||
bv_util m_bv;
|
||||
vector<undo_bound> m_scopes;
|
||||
map m_bound;
|
||||
svector<expr_set*> m_expr_vars;
|
||||
svector<expr_cnt*> m_bound_exprs;
|
||||
|
||||
bool is_bound(expr *e, expr*& v, interval& b) {
|
||||
if (!m.is_bool(e))
|
||||
return false;
|
||||
bool is_number(expr *e, uint64& n, unsigned& sz) const {
|
||||
rational r;
|
||||
if (m_bv.is_numeral(e, r, sz) && sz <= 64) {
|
||||
n = r.get_uint64();
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
rational n;
|
||||
bool is_bound(expr *e, expr*& v, interval& b) const {
|
||||
uint64 n;
|
||||
expr *lhs, *rhs;
|
||||
unsigned sz;
|
||||
|
||||
if (m_bv.is_bv_ule(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C
|
||||
if (is_number(lhs, n, sz)) { // C ule x <=> x uge C
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, uMaxInt(sz), sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) { // x ule C
|
||||
b = interval(rational::zero(), n, sz, true);
|
||||
if (is_number(rhs, n, sz)) { // x ule C
|
||||
b = interval(0, n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m_bv.is_bv_sle(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C
|
||||
if (is_number(lhs, n, sz)) { // C sle x <=> x sge C
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true);
|
||||
b = interval(n, (1ull << (sz-1)) - 1, sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) { // x sle C
|
||||
b = interval(rational::power_of_two(sz-1), n, sz, true);
|
||||
if (is_number(rhs, n, sz)) { // x sle C
|
||||
b = interval(1ull << (sz-1), n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
}
|
||||
} else if (m.is_eq(e, lhs, rhs)) {
|
||||
if (m_bv.is_numeral(lhs, n, sz)) {
|
||||
if (is_number(lhs, n, sz)) {
|
||||
if (m_bv.is_numeral(rhs))
|
||||
return false;
|
||||
b = interval(n, n, sz, true);
|
||||
v = rhs;
|
||||
return true;
|
||||
}
|
||||
if (m_bv.is_numeral(rhs, n, sz)) {
|
||||
if (is_number(rhs, n, sz)) {
|
||||
b = interval(n, n, sz, true);
|
||||
v = lhs;
|
||||
return true;
|
||||
|
@ -212,14 +232,65 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
|
|||
return false;
|
||||
}
|
||||
|
||||
public:
|
||||
expr_set* get_expr_vars(expr* t) {
|
||||
unsigned id = t->get_id();
|
||||
m_expr_vars.reserve(id + 1);
|
||||
expr_set*& entry = m_expr_vars[id];
|
||||
if (entry)
|
||||
return entry;
|
||||
|
||||
bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
|
||||
m_scopes.push_back(map());
|
||||
m_bound = &m_scopes.back();
|
||||
updt_params(p);
|
||||
expr_set* set = alloc(expr_set);
|
||||
entry = set;
|
||||
|
||||
if (!m_bv.is_numeral(t))
|
||||
set->insert(t, true);
|
||||
|
||||
if (!is_app(t))
|
||||
return set;
|
||||
|
||||
app* a = to_app(t);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr_set* set_arg = get_expr_vars(a->get_arg(i));
|
||||
for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
|
||||
set->insert(I->m_key, true);
|
||||
}
|
||||
}
|
||||
return set;
|
||||
}
|
||||
|
||||
expr_cnt* get_expr_bounds(expr* t) {
|
||||
unsigned id = t->get_id();
|
||||
m_bound_exprs.reserve(id + 1);
|
||||
expr_cnt*& entry = m_bound_exprs[id];
|
||||
if (entry)
|
||||
return entry;
|
||||
|
||||
expr_cnt* set = alloc(expr_cnt);
|
||||
entry = set;
|
||||
|
||||
if (!is_app(t))
|
||||
return set;
|
||||
|
||||
interval b;
|
||||
expr* e;
|
||||
if (is_bound(t, e, b)) {
|
||||
set->insert_if_not_there2(e, 0)->get_data().m_value++;
|
||||
}
|
||||
|
||||
app* a = to_app(t);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr_cnt* set_arg = get_expr_bounds(a->get_arg(i));
|
||||
for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
|
||||
set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value;
|
||||
}
|
||||
}
|
||||
return set;
|
||||
}
|
||||
|
||||
public:
|
||||
bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_propagate_eq = p.get_bool("propagate_eq", false);
|
||||
|
@ -229,7 +300,14 @@ public:
|
|||
r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities");
|
||||
}
|
||||
|
||||
virtual ~bv_bounds_simplifier() {}
|
||||
virtual ~bv_bounds_simplifier() {
|
||||
for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) {
|
||||
dealloc(m_expr_vars[i]);
|
||||
}
|
||||
for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) {
|
||||
dealloc(m_bound_exprs[i]);
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool assert_expr(expr * t, bool sign) {
|
||||
while (m.is_not(t, t)) {
|
||||
|
@ -243,20 +321,38 @@ public:
|
|||
if (sign)
|
||||
VERIFY(b.negate(b));
|
||||
|
||||
push();
|
||||
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
|
||||
interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value;
|
||||
return r.intersect(b, r);
|
||||
map::obj_map_entry* e = m_bound.find_core(t1);
|
||||
if (e) {
|
||||
interval& old = e->get_data().m_value;
|
||||
interval intr;
|
||||
if (!old.intersect(b, intr))
|
||||
return false;
|
||||
if (old == intr)
|
||||
return true;
|
||||
m_scopes.insert(undo_bound(t1, old, false));
|
||||
old = intr;
|
||||
} else {
|
||||
m_bound.insert(t1, b);
|
||||
m_scopes.insert(undo_bound(t1, interval(), true));
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual bool simplify(expr* t, expr_ref& result) {
|
||||
expr* t1;
|
||||
interval b, ctx, intr;
|
||||
result = 0;
|
||||
bool sign = false;
|
||||
interval b;
|
||||
|
||||
if (m_bound.find(t, b) && b.is_singleton()) {
|
||||
result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t));
|
||||
return true;
|
||||
}
|
||||
|
||||
if (!m.is_bool(t))
|
||||
return false;
|
||||
|
||||
bool sign = false;
|
||||
while (m.is_not(t, t)) {
|
||||
sign = !sign;
|
||||
}
|
||||
|
@ -272,16 +368,20 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
if (m_bound->find(t1, ctx)) {
|
||||
interval ctx, intr;
|
||||
result = 0;
|
||||
|
||||
if (b.is_full() && b.tight) {
|
||||
result = m.mk_true();
|
||||
} else if (m_bound.find(t1, ctx)) {
|
||||
if (ctx.implies(b)) {
|
||||
result = m.mk_true();
|
||||
} else if (!b.intersect(ctx, intr)) {
|
||||
result = m.mk_false();
|
||||
} else if (m_propagate_eq && intr.l == intr.h) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
|
||||
} else if (m_propagate_eq && intr.is_singleton()) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
|
||||
m.get_sort(t1)));
|
||||
}
|
||||
} else if (b.is_full() && b.tight) {
|
||||
result = m.mk_true();
|
||||
}
|
||||
|
||||
CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
|
||||
|
@ -290,19 +390,53 @@ public:
|
|||
return result != 0;
|
||||
}
|
||||
|
||||
virtual void push() {
|
||||
TRACE("bv", tout << "push\n";);
|
||||
unsigned sz = m_scopes.size();
|
||||
m_scopes.resize(sz + 1);
|
||||
m_bound = &m_scopes.back();
|
||||
m_bound->~map();
|
||||
new (m_bound) map(m_scopes[sz - 1]);
|
||||
virtual bool may_simplify(expr* t) {
|
||||
if (m_bv.is_numeral(t))
|
||||
return false;
|
||||
|
||||
while (m.is_not(t, t));
|
||||
|
||||
expr_set* used_exprs = get_expr_vars(t);
|
||||
for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) {
|
||||
if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
|
||||
return true;
|
||||
}
|
||||
|
||||
expr* t1;
|
||||
interval b;
|
||||
// skip common case: single bound constraint without any context for simplification
|
||||
if (is_bound(t, t1, b)) {
|
||||
return b.is_full() || m_bound.contains(t1);
|
||||
}
|
||||
|
||||
expr_cnt* bounds = get_expr_bounds(t);
|
||||
for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) {
|
||||
if (I->m_value > 1 || m_bound.contains(I->m_key))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual void pop(unsigned num_scopes) {
|
||||
TRACE("bv", tout << "pop: " << num_scopes << "\n";);
|
||||
m_scopes.shrink(m_scopes.size() - num_scopes);
|
||||
m_bound = &m_scopes.back();
|
||||
if (m_scopes.empty())
|
||||
return;
|
||||
unsigned target = m_scopes.size() - num_scopes;
|
||||
if (target == 0) {
|
||||
m_bound.reset();
|
||||
m_scopes.reset();
|
||||
return;
|
||||
}
|
||||
for (unsigned i = m_scopes.size()-1; i >= target; --i) {
|
||||
undo_bound& undo = m_scopes[i];
|
||||
SASSERT(m_bound.contains(undo.e));
|
||||
if (undo.fresh) {
|
||||
m_bound.erase(undo.e);
|
||||
} else {
|
||||
m_bound.insert(undo.e, undo.b);
|
||||
}
|
||||
}
|
||||
m_scopes.shrink(target);
|
||||
}
|
||||
|
||||
virtual simplifier * translate(ast_manager & m) {
|
||||
|
@ -310,7 +444,7 @@ public:
|
|||
}
|
||||
|
||||
virtual unsigned scope_level() const {
|
||||
return m_scopes.size() - 1;
|
||||
return m_scopes.size();
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -36,7 +36,7 @@ public:
|
|||
virtual ~ctx_propagate_assertions() {}
|
||||
virtual bool assert_expr(expr * t, bool sign);
|
||||
virtual bool simplify(expr* t, expr_ref& result);
|
||||
virtual void push();
|
||||
void push();
|
||||
virtual void pop(unsigned num_scopes);
|
||||
virtual unsigned scope_level() const { return m_scopes.size(); }
|
||||
virtual simplifier * translate(ast_manager & m);
|
||||
|
@ -260,10 +260,6 @@ struct ctx_simplify_tactic::imp {
|
|||
return m_simp->scope_level();
|
||||
}
|
||||
|
||||
void push() {
|
||||
m_simp->push();
|
||||
}
|
||||
|
||||
void restore_cache(unsigned lvl) {
|
||||
if (lvl >= m_cache_undo.size())
|
||||
return;
|
||||
|
@ -331,17 +327,13 @@ struct ctx_simplify_tactic::imp {
|
|||
|
||||
void simplify(expr * t, expr_ref & r) {
|
||||
r = 0;
|
||||
if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t)) {
|
||||
if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t) || !m_simp->may_simplify(t)) {
|
||||
r = t;
|
||||
return;
|
||||
}
|
||||
checkpoint();
|
||||
TRACE("ctx_simplify_tactic_detail", tout << "processing: " << mk_bounded_pp(t, m) << "\n";);
|
||||
if (m_simp->simplify(t, r)) {
|
||||
SASSERT(r.get() != 0);
|
||||
return;
|
||||
}
|
||||
if (is_cached(t, r)) {
|
||||
if (is_cached(t, r) || m_simp->simplify(t, r)) {
|
||||
SASSERT(r.get() != 0);
|
||||
return;
|
||||
}
|
||||
|
|
|
@ -30,7 +30,7 @@ public:
|
|||
virtual ~simplifier() {}
|
||||
virtual bool assert_expr(expr * t, bool sign) = 0;
|
||||
virtual bool simplify(expr* t, expr_ref& result) = 0;
|
||||
virtual void push() = 0;
|
||||
virtual bool may_simplify(expr* t) { return true; }
|
||||
virtual void pop(unsigned num_scopes) = 0;
|
||||
virtual simplifier * translate(ast_manager & m) = 0;
|
||||
virtual unsigned scope_level() const = 0;
|
||||
|
|
|
@ -198,7 +198,7 @@ void memory::display_i_max_usage(std::ostream & os) {
|
|||
<< "\n";
|
||||
}
|
||||
|
||||
#if _DEBUG
|
||||
#if Z3DEBUG
|
||||
void memory::deallocate(char const * file, int line, void * p) {
|
||||
deallocate(p);
|
||||
TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););
|
||||
|
|
|
@ -60,7 +60,7 @@ public:
|
|||
static void deallocate(void* p);
|
||||
static ALLOC_ATTR void* allocate(size_t s);
|
||||
static ALLOC_ATTR void* reallocate(void *p, size_t s);
|
||||
#if _DEBUG
|
||||
#if Z3DEBUG
|
||||
static void deallocate(char const* file, int line, void* p);
|
||||
static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue