mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 06:00:53 +00:00
Code Activity

remove theory_str and classes that are only used by it

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-07 21:05:12 -07:00
parent 2ac1b24121
commit fcd3a70c92
34 changed files with 14 additions and 14974 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -39,7 +39,6 @@ add_subdirectory(math/polynomial)
add_subdirectory(math/dd)
add_subdirectory(math/hilbert)
add_subdirectory(math/simplex)
add_subdirectory(math/automata)
add_subdirectory(math/interval)
add_subdirectory(math/realclosure)
add_subdirectory(math/subpaving)

1
src/api/api_ast.cpp
View file

@ -800,7 +800,6 @@ extern "C" {
unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p);
m_rw.set_solver(alloc(api::seq_expr_solver, m, p));
expr_ref result(m);
cancel_eh<reslimit> eh(m.limit());
api::context::set_interruptable si(*(mk_c(c)), eh);

17
src/api/api_context.h
View file

@ -57,23 +57,6 @@ namespace smt2 {
namespace api {
class seq_expr_solver : public expr_solver {
ast_manager& m;
params_ref const& p;
solver_ref s;
public:
seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
lbool check_sat(expr* e) override {
if (!s) {
s = mk_smt_solver(m, p, symbol("ALL"));
}
s->push();
s->assert_expr(e);
lbool r = s->check_sat();
s->pop(1);
return r;
}
};
class context : public tactic_manager {

3
src/api/api_model.cpp
View file

@ -160,9 +160,6 @@ extern "C" {
model * _m = to_model_ref(m);
params_ref p;
ast_manager& mgr = mk_c(c)->m();
if (!_m->has_solver()) {
_m->set_solver(alloc(api::seq_expr_solver, mgr, p));
}
expr_ref result(mgr);
model::scoped_model_completion _scm(*_m, model_completion);
result = (*_m)(to_expr(t));

1
src/ast/rewriter/CMakeLists.txt
View file

@ -46,7 +46,6 @@ z3_add_component(rewriter
COMPONENT_DEPENDENCIES
ast
params
automata
interval
polynomial
)

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

@ -29,8 +29,6 @@ Authors:
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "params/seq_rewriter_params.hpp"
#include "math/automata/automaton.h"
#include "math/automata/symbolic_automata_def.h"
expr_ref sym_expr::accept(expr* e) {
@ -83,320 +81,6 @@ struct display_expr1 {
}
};
class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
ast_manager& m;
expr_solver& m_solver;
expr_ref m_var;
typedef sym_expr* T;
public:
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
m(m), m_solver(s), m_var(m) {}
T mk_false() override {
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
}
T mk_true() override {
expr_ref fml(m.mk_true(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort());
}
T mk_and(T x, T y) override {
seq_util u(m);
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());
}
}
unsigned lo1, hi1, lo2, hi2;
if (x->is_range() && y->is_range() &&
u.is_const_char(x->get_lo(), lo1) && u.is_const_char(x->get_hi(), hi1) &&
u.is_const_char(y->get_lo(), lo2) && u.is_const_char(y->get_hi(), hi2)) {
lo1 = std::max(lo1, lo2);
hi1 = std::min(hi1, hi2);
if (lo1 > hi1) {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->get_sort());
}
expr_ref _start(u.mk_char(lo1), m);
expr_ref _stop(u.mk_char(hi1), m);
return sym_expr::mk_range(_start, _stop);
}
sort* s = x->get_sort();
if (m.is_bool(s)) s = y->get_sort();
var_ref v(m.mk_var(0, s), 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;
}
if (fml1 == fml2) {
return x;
}
if (is_complement(fml1, fml2)) {
expr_ref ff(m.mk_false(), m);
return sym_expr::mk_pred(ff, x->get_sort());
}
expr_ref fml(m);
bool_rewriter br(m);
br.mk_and(fml1, fml2, fml);
return sym_expr::mk_pred(fml, x->get_sort());
}
bool is_complement(expr* f1, expr* f2) {
expr* f = nullptr;
return
(m.is_not(f1, f) && f == f2) ||
(m.is_not(f2, f) && f == f1);
}
T mk_or(T x, T y) override {
if (x->is_char() && y->is_char() &&
x->get_char() == y->get_char()) {
return x;
}
if (x == y) 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;
bool_rewriter br(m);
expr_ref fml(m);
br.mk_or(fml1, fml2, fml);
return sym_expr::mk_pred(fml, x->get_sort());
}
T mk_and(unsigned sz, T const* ts) override {
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;
}
}
}
T mk_or(unsigned sz, T const* ts) override {
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;
}
}
}
lbool is_sat(T x) override {
unsigned lo, hi;
seq_util u(m);
if (x->is_char()) {
return l_true;
}
if (x->is_range() && u.is_const_char(x->get_lo(), lo) && u.is_const_char(x->get_hi(), hi)) {
return (lo <= hi) ? l_true : l_false;
}
if (x->is_not() && x->get_arg()->is_range() && u.is_const_char(x->get_arg()->get_lo(), lo) && 0 < lo) {
return l_true;
}
if (!m_var || m_var->get_sort() != x->get_sort()) {
m_var = m.mk_fresh_const("x", x->get_sort());
}
expr_ref fml = x->accept(m_var);
if (m.is_true(fml)) {
return l_true;
}
if (m.is_false(fml)) {
return l_false;
}
return m_solver.check_sat(fml);
}
T mk_not(T x) override {
return sym_expr::mk_not(m, x);
}
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
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());
}
eautomaton* re2automaton::mk_product(eautomaton* a1, eautomaton* a2) {
return m_sa->mk_product(*a1, *a2);
}
eautomaton* re2automaton::operator()(expr* e) {
eautomaton* r = re2aut(e);
if (r) {
r->compress();
bool_rewriter br(m);
TRACE(seq, display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
}
return r;
}
bool re2automaton::is_unit_char(expr* e, expr_ref& ch) {
zstring s;
expr* c = nullptr;
if (u.str.is_string(e, s) && s.length() == 1) {
ch = u.mk_char(s[0]);
return true;
}
if (u.str.is_unit(e, c)) {
ch = c;
return true;
}
return false;
}
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr *e0, *e1, *e2;
scoped_ptr<eautomaton> a, b;
unsigned lo, hi;
zstring s1, s2;
if (u.re.is_to_re(e, e1)) {
return seq2aut(e1);
}
else if (u.re.is_concat(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
return eautomaton::mk_concat(*a, *b);
}
else if (u.re.is_union(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
return eautomaton::mk_union(*a, *b);
}
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
a->add_final_to_init_moves();
a->add_init_to_final_states();
return a.detach();
}
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
a->add_final_to_init_moves();
return a.detach();
}
else if (u.re.is_opt(e, e1) && (a = re2aut(e1))) {
a = eautomaton::mk_opt(*a);
return a.detach();
}
else if (u.re.is_range(e, e1, e2)) {
expr_ref _start(m), _stop(m);
if (is_unit_char(e1, _start) &&
is_unit_char(e2, _stop)) {
TRACE(seq, tout << "Range: " << _start << " " << _stop << "\n";);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
return a.detach();
}
else {
// if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
return alloc(eautomaton, sm);
}
}
else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
return m_sa->mk_complement(*a);
}
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
b = eautomaton::mk_epsilon(sm);
while (hi > lo) {
scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
b = eautomaton::mk_union(*eps, *c);
--hi;
}
while (lo > 0) {
b = eautomaton::mk_concat(*a, *b);
--lo;
}
return b.detach();
}
else if (u.re.is_loop(e, e1, lo) && (a = re2aut(e1))) {
b = eautomaton::clone(*a);
b->add_final_to_init_moves();
b->add_init_to_final_states();
while (lo > 0) {
b = eautomaton::mk_concat(*a, *b);
--lo;
}
return b.detach();
}
else if (u.re.is_empty(e)) {
return alloc(eautomaton, sm);
}
else if (u.re.is_full_seq(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(e->get_sort(), 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);
}
else if (u.re.is_full_char(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(e->get_sort(), seq_s));
VERIFY (u.is_seq(seq_s, char_s));
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
a = alloc(eautomaton, sm, _true);
return a.detach();
}
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
eautomaton* r = m_sa->mk_product(*a, *b);
TRACE(seq, display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
return r;
}
else {
TRACE(seq, tout << "not handled " << mk_pp(e, m) << "\n";);
}
return nullptr;
}
eautomaton* re2automaton::seq2aut(expr* e) {
SASSERT(u.is_seq(e));
zstring s;
expr* e1, *e2;
scoped_ptr<eautomaton> a, b;
if (u.str.is_concat(e, e1, e2) && (a = seq2aut(e1)) && (b = seq2aut(e2))) {
return eautomaton::mk_concat(*a, *b);
}
else if (u.str.is_unit(e, e1)) {
return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
}
else if (u.str.is_empty(e)) {
return eautomaton::mk_epsilon(sm);
}
else if (u.str.is_string(e, s)) {
unsigned init = 0;
eautomaton::moves mvs;
unsigned_vector final;
final.push_back(s.length());
for (unsigned k = 0; k < s.length(); ++k) {
// reference count?
mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
}
return alloc(eautomaton, sm, init, final, mvs);
}
return nullptr;
}
void seq_rewriter::updt_params(params_ref const & p) {
seq_rewriter_params sp(p);
@ -2721,46 +2405,6 @@ void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned
}
bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
seq.reset();
unsigned state = aut.init();
uint_set visited;
eautomaton::moves mvs;
unsigned_vector states;
aut.get_epsilon_closure(state, states);
bool has_final = false;
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
aut.get_moves_from(state, mvs, true);
while (!has_final) {
if (mvs.size() != 1) {
return false;
}
if (visited.contains(state)) {
return false;
}
if (aut.is_final_state(mvs[0].src())) {
return false;
}
visited.insert(state);
sym_expr* t = mvs[0].t();
if (!t || !t->is_char()) {
return false;
}
seq.push_back(str().mk_unit(t->get_char()));
state = mvs[0].dst();
mvs.reset();
aut.get_moves_from(state, mvs, true);
states.reset();
has_final = false;
aut.get_epsilon_closure(state, states);
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
}
return mvs.empty();
}
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
seq.reset();

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

@ -26,8 +26,6 @@ Notes:
#include "util/params.h"
#include "util/lbool.h"
#include "util/sign.h"
#include "math/automata/automaton.h"
#include "math/automata/symbolic_automata.h"
inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& es) {
@ -81,33 +79,15 @@ public:
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
};
#if 0
class expr_solver {
public:
virtual ~expr_solver() = default;
virtual lbool check_sat(expr* e) = 0;
};
#endif
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;
scoped_ptr<expr_solver> m_solver;
scoped_ptr<boolean_algebra_t> m_ba;
scoped_ptr<symbolic_automata_t> m_sa;
bool is_unit_char(expr* e, expr_ref& ch);
eautomaton* re2aut(expr* e);
eautomaton* seq2aut(expr* e);
public:
re2automaton(ast_manager& m);
eautomaton* operator()(expr* e);
void set_solver(expr_solver* solver);
bool has_solver() const { return m_solver; }
eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
};
/**
\brief Cheap rewrite rules for seq constraints
@ -150,7 +130,7 @@ class seq_rewriter {
seq_util m_util;
arith_util m_autil;
bool_rewriter m_br;
re2automaton m_re2aut;
// re2automaton m_re2aut;
op_cache m_op_cache;
expr_ref_vector m_es, m_lhs, m_rhs;
bool m_coalesce_chars;
@ -340,7 +320,7 @@ class seq_rewriter {
void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
// bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
@ -360,7 +340,8 @@ class seq_rewriter {
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_br(m, p), m_re2aut(m), m_op_cache(m), m_es(m),
m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
}
ast_manager & m() const { return m_util.get_manager(); }
@ -371,8 +352,6 @@ public:
void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
bool has_solver() { return m_re2aut.has_solver(); }
bool coalesce_chars() const { return m_coalesce_chars; }

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

@ -933,9 +933,6 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
return m_cfg.mk_eq(a, b);
}
void set_solver(expr_solver* solver) {
m_cfg.m_seq_rw.set_solver(solver);
}
};
th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@ -1057,10 +1054,6 @@ expr_ref th_rewriter::mk_eq(expr* a, expr* b) {
return m_imp->mk_eq(a, b);
}
void th_rewriter::set_solver(expr_solver* solver) {
m_imp->set_solver(solver);
}
bool th_rewriter::reduce_quantifier(quantifier * old_q,
expr * new_body,

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

@ -74,7 +74,6 @@ public:
expr_dependency * get_used_dependencies();
void reset_used_dependencies();
void set_solver(expr_solver* solver);
};

19
src/cmd_context/cmd_context.h
View file

@ -575,22 +575,3 @@ public:
std::ostream & operator<<(std::ostream & out, cmd_context::status st);
class th_solver : public expr_solver {
cmd_context& m_ctx;
params_ref m_params;
ref<solver> m_solver;
public:
th_solver(cmd_context& ctx): m_ctx(ctx) {}
lbool check_sat(expr* e) override {
if (!m_solver) {
m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
}
m_solver->push();
m_solver->assert_expr(e);
lbool r = m_solver->check_sat(0,nullptr);
m_solver->pop(1);
return r;
}
};

1
src/cmd_context/eval_cmd.cpp
View file

@ -75,7 +75,6 @@ public:
unsigned rlimit = m_params.get_uint("rlimit", 0);
// md->compress();
model_evaluator ev(*(md.get()), m_params);
ev.set_solver(alloc(th_solver, ctx));
cancel_eh<reslimit> eh(ctx.m().limit());
{
scoped_ctrl_c ctrlc(eh);

2
src/cmd_context/simplify_cmd.cpp
View file

@ -69,8 +69,6 @@ public:
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
th_solver solver(ctx);
s.set_solver(alloc(th_solver, ctx));
unsigned cache_sz;
unsigned num_steps = 0;
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);

6
src/math/automata/CMakeLists.txt
View file

@ -1,6 +0,0 @@
z3_add_component(automata
SOURCES
automaton.cpp
COMPONENT_DEPENDENCIES
util
)

23
src/math/automata/automaton.cpp
View file

@ -1,23 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
automaton.cpp
Abstract:
Symbolic Automaton, a la Margus Veanes Automata library.
Author:
Nikolaj Bjorner (nbjorner) 2015-12-23.
Revision History:
--*/
#include "math/automata/automaton.h"
template class automaton<unsigned>;

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

@ -1,751 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
automaton.h
Abstract:
Symbolic Automaton, a la Margus Veanes Automata library.
Author:
Nikolaj Bjorner (nbjorner) 2015-12-23.
Revision History:
--*/
#pragma once
#include "util/util.h"
#include "util/vector.h"
#include "util/uint_set.h"
#include "util/trace.h"
template<class T>
class default_value_manager {
public:
void inc_ref(T* t) {}
void dec_ref(T* t) {}
};
template<class T, class M = default_value_manager<T> >
class automaton {
public:
class move {
M& m;
T* m_t;
unsigned m_src;
unsigned m_dst;
public:
move(M& m, unsigned s, unsigned d, T* t = nullptr): m(m), m_t(t), m_src(s), m_dst(d) {
if (t) m.inc_ref(t);
}
~move() {
if (m_t) m.dec_ref(m_t);
}
move(move const& other): m(other.m), m_t(other.m_t), m_src(other.m_src), m_dst(other.m_dst) {
if (m_t) m.inc_ref(m_t);
}
move(move &&other) noexcept : m(other.m), m_t(nullptr), m_src(other.m_src), m_dst(other.m_dst) {
std::swap(m_t, other.m_t);
}
move& operator=(move const& other) {
SASSERT(&m == &other.m);
T* t = other.m_t;
if (t) m.inc_ref(t);
if (m_t) m.dec_ref(m_t);
m_t = t;
m_src = other.m_src;
m_dst = other.m_dst;
return *this;
}
unsigned dst() const { return m_dst; }
unsigned src() const { return m_src; }
T* t() const { return m_t; }
bool is_epsilon() const { return m_t == nullptr; }
};
typedef vector<move> moves;
private:
M& m;
vector<moves> m_delta;
vector<moves> m_delta_inv;
unsigned m_init;
uint_set m_final_set;
unsigned_vector m_final_states;
// local data-structures
mutable uint_set m_visited;
mutable unsigned_vector m_todo;
struct default_display {
std::ostream& display(std::ostream& out, T* t) {
return out << t;
}
};
public:
// The empty automaton:
automaton(M& m):
m(m),
m_init(0)
{
m_delta.push_back(moves());
m_delta_inv.push_back(moves());
}
// create an automaton from initial state, final states, and moves
automaton(M& m, unsigned init, unsigned_vector const& final, moves const& mvs): m(m) {
m_init = init;
m_delta.push_back(moves());
m_delta_inv.push_back(moves());
for (unsigned f : final) {
add_to_final_states(f);
}
for (move const& mv : mvs) {
unsigned n = std::max(mv.src(), mv.dst());
if (n >= m_delta.size()) {
m_delta.resize(n+1, moves());
m_delta_inv.resize(n+1, moves());
}
add(mv);
}
}
// create an automaton that accepts a sequence.
automaton(M& m, ptr_vector<T> const& seq):
m(m),
m_init(0) {
m_delta.resize(seq.size()+1, moves());
m_delta_inv.resize(seq.size()+1, moves());
for (unsigned i = 0; i < seq.size(); ++i) {
m_delta[i].push_back(move(m, i, i + 1, seq[i]));
m_delta[i + 1].push_back(move(m, i, i + 1, seq[i]));
}
add_to_final_states(seq.size());
}
// The automaton that accepts t
automaton(M& m, T* t):
m(m),
m_init(0) {
m_delta.resize(2, moves());
m_delta_inv.resize(2, moves());
add_to_final_states(1);
add(move(m, 0, 1, t));
}
automaton(automaton const& other):
m(other.m),
m_delta(other.m_delta),
m_delta_inv(other.m_delta_inv),
m_init(other.m_init),
m_final_set(other.m_final_set),
m_final_states(other.m_final_states)
{}
// create the automaton that accepts the empty string/sequence only.
static automaton* mk_epsilon(M& m) {
moves mvs;
unsigned_vector final;
final.push_back(0);
return alloc(automaton, m, 0, final, mvs);
}
// create the automaton with a single state on condition t.
static automaton* mk_loop(M& m, T* t) {
moves mvs;
unsigned_vector final;
final.push_back(0);
mvs.push_back(move(m, 0, 0, t));
return alloc(automaton, m, 0, final, mvs);
}
static automaton* clone(automaton const& a) {
moves mvs;
unsigned_vector final;
append_moves(0, a, mvs);
append_final(0, a, final);
return alloc(automaton, a.m, a.init(), final, mvs);
}
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 b.clone();
}
if (b.is_empty()) {
return a.clone();
}
moves mvs;
unsigned_vector final;
unsigned offset1 = 1;
unsigned offset2 = a.num_states() + 1;
mvs.push_back(move(m, 0, a.init() + offset1));
mvs.push_back(move(m, 0, b.init() + offset2));
append_moves(offset1, a, mvs);
append_moves(offset2, b, mvs);
append_final(offset1, a, final);
append_final(offset2, b, final);
return alloc(automaton, m, 0, final, mvs);
}
static automaton* mk_opt(automaton const& a) {
M& m = a.m;
moves mvs;
unsigned_vector final;
unsigned offset = 0;
unsigned init = a.init();
if (!a.initial_state_is_source()) {
offset = 1;
init = 0;
mvs.push_back(move(m, 0, a.init() + offset));
}
if (a.is_empty()) {
return a.clone();
}
mvs.push_back(move(m, init, a.final_state() + offset));
append_moves(offset, a, mvs);
append_final(offset, a, final);
return alloc(automaton, m, init, final, mvs);
}
// concatenate accepting languages
static automaton* mk_concat(automaton const& a, automaton const& b) {
SASSERT(&a.m == &b.m);
M& m = a.m;
if (a.is_empty()) {
return a.clone();
}
if (b.is_empty()) {
return b.clone();
}
if (a.is_epsilon()) {
return b.clone();
}
if (b.is_epsilon()) {
return a.clone();
}
moves mvs;
unsigned_vector final;
unsigned init = 0;
unsigned offset1 = 1;
unsigned offset2 = a.num_states() + offset1;
mvs.push_back(move(m, 0, a.init() + offset1));
append_moves(offset1, a, mvs);
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
mvs.push_back(move(m, a.m_final_states[i] + offset1, b.init() + offset2));
}
append_moves(offset2, b, mvs);
append_final(offset2, b, final);
return alloc(automaton, m, init, final, mvs);
}
static automaton* mk_reverse(automaton const& a) {
M& m = a.m;
if (a.is_empty()) {
return alloc(automaton, m);
}
moves mvs;
for (unsigned i = 0; i < a.m_delta.size(); ++i) {
moves const& mvs1 = a.m_delta[i];
for (unsigned j = 0; j < mvs1.size(); ++j) {
move const& mv = mvs1[j];
mvs.push_back(move(m, mv.dst(), mv.src(), mv.t()));
}
}
unsigned_vector final;
unsigned init;
final.push_back(a.init());
if (a.m_final_states.size() == 1) {
init = a.m_final_states[0];
}
else {
init = a.num_states();
for (unsigned st : a.m_final_states) {
mvs.push_back(move(m, init, st));
}
}
return alloc(automaton, m, init, final, mvs);
}
void add_to_final_states(unsigned s) {
if (!is_final_state(s)) {
m_final_set.insert(s);
m_final_states.push_back(s);
}
}
void remove_from_final_states(unsigned s) {
if (is_final_state(s)) {
m_final_set.remove(s);
m_final_states.erase(s);
}
}
bool is_sink_state(unsigned s) const {
if (is_final_state(s)) return false;
moves mvs;
get_moves_from(s, mvs);
for (move const& m : mvs) {
if (s != m.dst()) return false;
}
return true;
}
void add_init_to_final_states() {
add_to_final_states(init());
}
void add_final_to_init_moves() {
for (unsigned i = 0; i < m_final_states.size(); ++i) {
unsigned state = m_final_states[i];
bool found = false;
moves const& mvs = m_delta[state];
for (unsigned j = 0; found && j < mvs.size(); ++j) {
found = (mvs[j].dst() == m_init) && mvs[j].is_epsilon();
}
if (!found && state != m_init) {
add(move(m, state, m_init));
}
}
}
// remove epsilon transitions
// src - e -> dst
// in_degree(src) = 1, final(src) => final(dst), src0 != src
// src0 - t -> src - e -> dst => src0 - t -> dst
// out_degree(dst) = 1, final(dst) => final(src), dst != dst1
// src - e -> dst - t -> dst1 => src - t -> dst1
// Generalized:
// Src - E -> dst - t -> dst1 => Src - t -> dst1 if dst is final => each Src is final
//
// src - e -> dst - ET -> Dst1 => src - ET -> Dst1 if in_degree(dst) = 1, src != dst
// Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst
//
// Some missing:
// src - et -> dst - E -> Dst1 => src - et -> Dst1 if in_degree(dst) = 1
// Src - ET -> dst - e -> dst1 => Src - ET -> dst1 if out_degree(dst) = 1,
//
void compress() {
SASSERT(!m_delta.empty());
TRACE(seq, display(tout););
for (unsigned i = 0; i < m_delta.size(); ++i) {
for (unsigned j = 0; j < m_delta[i].size(); ++j) {
move const& mv = m_delta[i][j];
unsigned src = mv.src();
unsigned dst = mv.dst();
SASSERT(src == i);
if (mv.is_epsilon()) {
if (src == dst) {
// just remove this edge.
}
else if (1 == in_degree(src) && 1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
move const& mv0 = m_delta_inv[src][0];
unsigned src0 = mv0.src();
T* t = mv0.t();
SASSERT(mv0.dst() == src);
if (src0 == src) {
continue;
}
add(move(m, src0, dst, t));
remove(src0, src, t);
}
else if (1 == out_degree(dst) && 1 == in_degree(dst) && init() != dst && (!is_final_state(dst) || is_final_state(src))) {
move const& mv1 = m_delta[dst][0];
unsigned dst1 = mv1.dst();
T* t = mv1.t();
SASSERT(mv1.src() == dst);
if (dst1 == dst) {
continue;
}
add(move(m, src, dst1, t));
remove(dst, dst1, t);
}
else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
moves const& mvs = m_delta[dst];
moves mvs1;
for (move const& mv : mvs) {
mvs1.push_back(move(m, src, mv.dst(), mv.t()));
}
for (move const& mv : mvs1) {
remove(dst, mv.dst(), mv.t());
add(mv);
}
}
//
// Src - E -> dst - et -> dst1 => Src - et -> dst1 if out_degree(dst) = 1, src != dst
//
else if (1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
move const& mv = m_delta[dst][0];
unsigned dst1 = mv.dst();
T* t = mv.t();
unsigned_vector src0s;
moves const& mvs = m_delta_inv[dst];
moves mvs1;
for (move const& mv1 : mvs) {
SASSERT(mv1.is_epsilon());
mvs1.push_back(move(m, mv1.src(), dst1, t));
}
for (move const& mv1 : mvs1) {
remove(mv1.src(), dst, nullptr);
add(mv1);
}
remove(dst, dst1, t);
--j;
continue;
}
//
// Src1 - ET -> src - e -> dst => Src1 - ET -> dst if out_degree(src) = 1, src != init()
//
else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
moves const& mvs = m_delta_inv[src];
moves mvs1;
for (move const& mv : mvs) {
mvs1.push_back(move(m, mv.src(), dst, mv.t()));
}
for (move const& mv : mvs1) {
remove(mv.src(), src, mv.t());
add(mv);
}
}
else if (1 == out_degree(src) && (is_final_state(src) || !is_final_state(dst))) {
moves const& mvs = m_delta[dst];
moves mvs1;
for (move const& mv : mvs) {
mvs1.push_back(move(m, src, mv.dst(), mv.t()));
}
for (move const& mv : mvs1) {
add(mv);
}
}
else {
TRACE(seq, tout << "epsilon not removed " << out_degree(src) << " " << is_final_state(src) << " " << is_final_state(dst) << "\n";);
continue;
}
remove(src, dst, nullptr);
--j;
}
}
}
SASSERT(!m_delta.empty());
while (true) {
SASSERT(!m_delta.empty());
unsigned src = m_delta.size() - 1;
if (in_degree(src) == 0 && init() != src) {
remove_from_final_states(src);
m_delta.pop_back();
}
else {
break;
}
}
sinkify_dead_states();
TRACE(seq, display(tout););
}
bool is_sequence(unsigned& length) const {
if (is_final_state(m_init) && (out_degree(m_init) == 0 || (out_degree(m_init) == 1 && is_loop_state(m_init)))) {
length = 0;
return true;
}
if (is_empty() || in_degree(m_init) != 0 || out_degree(m_init) != 1) {
return false;
}
length = 1;
unsigned s = get_move_from(m_init).dst();
while (!is_final_state(s)) {
if (out_degree(s) != 1 || in_degree(s) != 1) {
return false;
}
s = get_move_from(s).dst();
++length;
}
return out_degree(s) == 0 || (out_degree(s) == 1 && is_loop_state(s));
}
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]; }
move const& get_move_to(unsigned state) const { SASSERT(m_delta_inv[state].size() == 1); return m_delta_inv[state][0]; }
moves const& get_moves_from(unsigned state) const { return m_delta[state]; }
moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
bool is_final_configuration(uint_set const& s) const {
for (unsigned i : s) {
if (is_final_state(i))
return true;
}
return false;
}
bool is_epsilon_free() const {
for (moves const& mvs : m_delta) {
for (move const & m : mvs) {
if (!m.t()) return false;
}
}
return true;
}
bool all_epsilon_in(unsigned s) {
moves const& mvs = m_delta_inv[s];
for (move const& m : mvs) {
if (m.t()) return false;
}
return true;
}
bool is_empty() const { return m_final_states.empty(); }
bool is_epsilon() const { return m_final_states.size() == 1 && m_final_states.back() == init() && m_delta.empty(); }
unsigned final_state() const { return m_final_states[0]; }
bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); }
unsigned num_states() const { return m_delta.size(); }
bool is_loop_state(unsigned s) const {
moves mvs;
get_moves_from(s, mvs);
for (move const& m : mvs) {
if (s == m.dst()) return true;
}
return false;
}
unsigned move_count() const {
unsigned result = 0;
for (moves const& mvs : m_delta) result += mvs.size();
return result;
}
void get_epsilon_closure(unsigned state, unsigned_vector& states) {
get_epsilon_closure(state, m_delta, states);
}
void get_inv_epsilon_closure(unsigned state, unsigned_vector& states) {
get_epsilon_closure(state, m_delta_inv, states);
}
void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
get_moves(state, m_delta, mvs, epsilon_closure);
}
void get_moves_from_states(uint_set const& states, moves& mvs, bool epsilon_closure = true) const {
for (unsigned i : states) {
moves curr;
get_moves(i, m_delta, curr, epsilon_closure);
mvs.append(curr);
}
}
void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
get_moves(state, m_delta_inv, mvs, epsilon_closure);
}
template<class D>
std::ostream& display(std::ostream& out, D& displayer = D()) const {
out << "init: " << init() << "\n";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
out << i << " -> " << mv.dst() << " ";
if (mv.t()) {
out << "if ";
displayer.display(out, mv.t());
}
out << "\n";
}
}
return out;
}
private:
std::ostream& display(std::ostream& out) const {
out << "init: " << init() << "\n";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
out << i << " -> " << mv.dst() << " ";
if (mv.t()) {
out << "if *** ";
}
out << "\n";
}
}
return out;
}
void sinkify_dead_states() {
uint_set dead_states;
for (unsigned i = 0; i < m_delta.size(); ++i) {
if (!m_final_states.contains(i)) {
dead_states.insert(i);
}
}
bool change = true;
unsigned_vector to_remove;
while (change) {
change = false;
to_remove.reset();
for (unsigned s : dead_states) {
moves const& mvs = m_delta[s];
for (move const& mv : mvs) {
if (!dead_states.contains(mv.dst())) {
to_remove.push_back(s);
break;
}
}
}
change = !to_remove.empty();
for (unsigned s : to_remove) {
dead_states.remove(s);
}
to_remove.reset();
}
TRACE(seq, tout << "remove: " << dead_states << "\n";
tout << "final: " << m_final_states << "\n";
);
for (unsigned s : dead_states) {
CTRACE(seq, !m_delta[s].empty(), tout << "live state " << s << "\n";);
m_delta[s].reset();
}
}
#if 0
void remove_dead_states() {
unsigned_vector remap;
for (unsigned i = 0; i < m_delta.size(); ++i) {
}
}
#endif
void add(move const& mv) {
if (!is_duplicate_cheap(mv)) {
m_delta[mv.src()].push_back(mv);
m_delta_inv[mv.dst()].push_back(mv);
}
}
bool is_duplicate_cheap(move const& mv) const {
if (m_delta[mv.src()].empty()) return false;
move const& mv0 = m_delta[mv.src()].back();
return mv0.src() == mv.src() && mv0.dst() == mv.dst() && mv0.t() == mv.t();
}
unsigned find_move(unsigned src, unsigned dst, T* t, moves const& mvs) {
for (unsigned i = 0; i < mvs.size(); ++i) {
move const& mv = mvs[i];
if (mv.src() == src && mv.dst() == dst && t == mv.t()) {
return i;
}
}
UNREACHABLE();
return UINT_MAX;
}
void remove(unsigned src, unsigned dst, T* t, moves& mvs) {
remove(find_move(src, dst, t, mvs), mvs);
}
void remove(unsigned src, unsigned dst, T* t) {
remove(src, dst, t, m_delta[src]);
remove(src, dst, t, m_delta_inv[dst]);
}
void remove(unsigned index, moves& mvs) {
mvs[index] = mvs.back();
mvs.pop_back();
}
mutable unsigned_vector m_states1, m_states2;
void get_moves(unsigned state, vector<moves> const& delta, moves& mvs, bool epsilon_closure) const {
m_states1.reset();
m_states2.reset();
get_epsilon_closure(state, delta, m_states1);
for (unsigned i = 0; i < m_states1.size(); ++i) {
state = m_states1[i];
moves const& mv1 = delta[state];
for (unsigned j = 0; j < mv1.size(); ++j) {
move const& mv = mv1[j];
if (!mv.is_epsilon()) {
if (epsilon_closure) {
m_states2.reset();
get_epsilon_closure(mv.dst(), delta, m_states2);
for (unsigned k = 0; k < m_states2.size(); ++k) {
mvs.push_back(move(m, state, m_states2[k], mv.t()));
}
}
else {
mvs.push_back(move(m, state, mv.dst(), mv.t()));
}
}
}
}
}
void get_epsilon_closure(unsigned state, vector<moves> const& delta, unsigned_vector& states) const {
m_todo.push_back(state);
m_visited.insert(state);
while (!m_todo.empty()) {
state = m_todo.back();
states.push_back(state);
m_todo.pop_back();
moves const& mvs = delta[state];
for (unsigned i = 0; i < mvs.size(); ++i) {
unsigned tgt = mvs[i].dst();
if (mvs[i].is_epsilon() && !m_visited.contains(tgt)) {
m_visited.insert(tgt);
m_todo.push_back(tgt);
}
}
}
m_visited.reset();
SASSERT(m_todo.empty());
}
static void append_moves(unsigned offset, automaton const& a, moves& mvs) {
for (unsigned i = 0; i < a.num_states(); ++i) {
moves const& mvs1 = a.m_delta[i];
for (unsigned j = 0; j < mvs1.size(); ++j) {
move const& mv = mvs1[j];
mvs.push_back(move(a.m, mv.src() + offset, mv.dst() + offset, mv.t()));
}
}
}
static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
for (unsigned s : a.m_final_states) {
final.push_back(s+offset);
}
}
};
typedef automaton<unsigned> uautomaton;

43
src/math/automata/boolean_algebra.h
View file

@ -1,43 +0,0 @@
/*++
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:
--*/
#pragma once
#include "util/util.h"
template<class T>
class positive_boolean_algebra {
public:
virtual ~positive_boolean_algebra() = default;
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;
};

152
src/math/automata/symbolic_automata.h
View file

@ -1,152 +0,0 @@
/*++
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:
--*/
#pragma once
#include "math/automata/automaton.h"
#include "math/automata/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;
typedef std::pair<unsigned, unsigned> unsigned_pair;
template<class V> class u2_map : public map<unsigned_pair, V, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > {};
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);
private:
automaton_t* mk_determinstic_param(automaton_t& a, bool flip_acceptance);
vector<std::pair<vector<bool>, ref_t> > generate_min_terms(vector<ref_t> &constraints) {
vector<std::pair<vector<bool>, ref_t> > min_terms;
ref_t curr_pred(m_ba.mk_true(), m);
vector<bool> curr_bv;
generate_min_terms_rec(constraints, min_terms, 0, curr_bv, curr_pred);
return min_terms;
}
void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t> > &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
lbool is_sat = m_ba.is_sat(curr_pred);
if (is_sat == l_undef)
throw default_exception("incomplete theory: unable to generate min-terms");
if (is_sat != l_true) {
return;
}
if (i == constraints.size()) {
min_terms.push_back(std::pair<vector<bool>, ref_t>(curr_bv, curr_pred));
}
else {
//true case
curr_bv.push_back(true);
ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
curr_bv.pop_back();
//false case
curr_bv.push_back(false);
ref_t neg(m_ba.mk_not(constraints[i]), m);
ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
curr_bv.pop_back();
}
}
};

490
src/math/automata/symbolic_automata_def.h
View file

@ -1,490 +0,0 @@
/*++
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:
--*/
#pragma once
#include "math/automata/symbolic_automata.h"
#include "util/hashtable.h"
#include "util/vector.h"
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.data())), m);
lbool is_sat = m_ba.is_sat(cond);
if (is_sat == l_undef) {
return nullptr;
}
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 nullptr;
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 nullptr;
}
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 nullptr;
}
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
u2_map<T*> 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_determinstic(automaton_t& a) {
return mk_determinstic_param(a);
}
template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_complement(automaton_t& a) {
return mk_determinstic_param(a, true);
}
template<class T, class M>
typename symbolic_automata<T, M>::automaton_t*
symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance) {
vector<std::pair<vector<bool>, ref_t> > min_terms;
vector<ref_t> predicates;
map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id; // set of states to unique id
vector<uint_set> id2s; // unique id to set of b-states
uint_set set;
unsigned_vector vector;
moves_t new_mvs; // moves in the resulting automaton
unsigned_vector new_final_states; // new final states
unsigned p_state_id = 0; // next state identifier
TRACE(seq, tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);
// adds non-final states of a to final if flipping and final otherwise
unsigned_vector init_states;
a.get_epsilon_closure(a.init(), init_states);
for (unsigned s : init_states) {
set.insert(s);
}
if (a.is_final_configuration(set) != flip_acceptance) {
new_final_states.push_back(p_state_id);
}
s2id.insert(set, p_state_id++); // the index to the initial state is 0
id2s.push_back(set);
::vector<uint_set> todo; //States to visit
todo.push_back(set);
uint_set state;
moves_t mvsA;
new_mvs.reset();
// or just make todo a vector whose indices coincide with state_id.
while (!todo.empty()) {
uint_set state = todo.back();
unsigned state_id = s2id[state];
todo.pop_back();
mvsA.reset();
min_terms.reset();
predicates.reset();
a.get_moves_from_states(state, mvsA);
for (unsigned j = 0; j < mvsA.size(); ++j) {
ref_t mv_guard(mvsA[j].t(),m);
predicates.push_back(mv_guard);
}
min_terms = generate_min_terms(predicates);
for (unsigned j = 0; j < min_terms.size(); ++j) {
set = uint_set();
for (unsigned i = 0; i < mvsA.size(); ++i) {
if (min_terms[j].first[i])
set.insert(mvsA[i].dst());
}
bool is_new = !s2id.contains(set);
if (is_new) {
TRACE(seq, tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);
if (a.is_final_configuration(set) != flip_acceptance) {
new_final_states.push_back(p_state_id);
}
s2id.insert(set, p_state_id++);
id2s.push_back(set);
todo.push_back(set);
}
new_mvs.push_back(move_t(m, state_id, s2id[set], min_terms[j].second));
}
}
if (new_final_states.empty()) {
return alloc(automaton_t, m);
}
return alloc(automaton_t, m, 0, new_final_states, new_mvs);
}
template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
u2_map<unsigned> pair2id;
unsigned_pair init_pair(a.init(), b.init());
svector<unsigned_pair> todo;
todo.push_back(init_pair);
pair2id.insert(init_pair, 0);
moves_t mvs;
unsigned_vector final;
unsigned_vector a_init, b_init;
a.get_epsilon_closure(a.init(), a_init);
bool a_init_is_final = false, b_init_is_final = false;
for (unsigned ia : a_init) {
if (a.is_final_state(ia)) {
a_init_is_final = true;
b.get_epsilon_closure(b.init(), b_init);
for (unsigned ib : b_init) {
if (b.is_final_state(ib)) {
b_init_is_final = true;
final.push_back(0);
break;
}
}
break;
}
}
unsigned n = 1;
moves_t mvsA, mvsB;
while (!todo.empty()) {
unsigned_pair curr_pair = todo.back();
todo.pop_back();
unsigned src = pair2id[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 nullptr;
}
unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst());
unsigned tgt;
if (!pair2id.find(tgt_pair, tgt)) {
tgt = n++;
pair2id.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()));
}
bool_vector back_reachable(n, false);
for (unsigned f : final) {
back_reachable[f] = 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()) {
if (a_init_is_final && b_init_is_final) {
// special case: automaton has no moves, but the initial state is final on both sides
// this results in the automaton which accepts the empty sequence and nothing else
final.clear();
final.push_back(0);
return alloc(automaton_t, m, 0, final, mvs1);
} else {
return alloc(automaton_t, m);
}
}
else {
return alloc(automaton_t, m, 0, final, mvs1);
}
}
template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_difference(automaton_t& a, automaton_t& b) {
return mk_product(a,mk_complement(b));
}

7
src/model/model.cpp
View file

@ -572,13 +572,6 @@ expr_ref model::operator()(expr* t) {
return m_mev(t);
}
void model::set_solver(expr_solver* s) {
m_mev.set_solver(s);
}
bool model::has_solver() {
return m_mev.has_solver();
}
expr_ref_vector model::operator()(expr_ref_vector const& ts) {
expr_ref_vector rs(m);

2
src/model/model.h
View file

@ -110,8 +110,6 @@ public:
bool is_false(expr_ref_vector const& ts);
bool are_equal(expr* s, expr* t);
void reset_eval_cache();
bool has_solver();
void set_solver(expr_solver* solver);
void add_rec_funs();
class scoped_model_completion {

8
src/model/model_evaluator.cpp
View file

@ -864,14 +864,6 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
return eval(tmp, r, model_completion);
}
void model_evaluator::set_solver(expr_solver* solver) {
m_imp->m_cfg.m_seq_rw.set_solver(solver);
}
bool model_evaluator::has_solver() {
return m_imp->m_cfg.m_seq_rw.has_solver();
}
model_core const & model_evaluator::get_model() const {
return m_imp->cfg().m_model;
}

4
src/model/model_evaluator.h
View file

@ -57,10 +57,6 @@ public:
bool is_true(expr_ref_vector const& ts);
bool are_equal(expr* s, expr* t);
void set_solver(expr_solver* solver);
bool has_solver();
/**
* best effort evaluator of extensional array equality.
*/

3
src/params/CMakeLists.txt
View file

@ -10,8 +10,7 @@ z3_add_component(params
theory_array_params.cpp
theory_bv_params.cpp
theory_pb_params.cpp
theory_seq_params.cpp
theory_str_params.cpp
theory_seq_params.cpp
COMPONENT_DEPENDENCIES
util
ast

2
src/params/smt_params.cpp
View file

@ -80,7 +80,6 @@ void smt_params::updt_params(params_ref const & p) {
theory_pb_params::updt_params(p);
// theory_array_params::updt_params(p);
theory_datatype_params::updt_params(p);
theory_str_params::updt_params(p);
updt_local_params(p);
}
@ -100,7 +99,6 @@ void smt_params::display(std::ostream & out) const {
theory_bv_params::display(out);
theory_pb_params::display(out);
theory_datatype_params::display(out);
theory_str_params::display(out);
DISPLAY_PARAM(m_display_proof);
DISPLAY_PARAM(m_display_dot_proof);

2
src/params/smt_params.h
View file

@ -24,7 +24,6 @@ Revision History:
#include "params/theory_arith_params.h"
#include "params/theory_array_params.h"
#include "params/theory_bv_params.h"
#include "params/theory_str_params.h"
#include "params/theory_seq_params.h"
#include "params/theory_pb_params.h"
#include "params/theory_datatype_params.h"
@ -79,7 +78,6 @@ struct smt_params : public preprocessor_params,
public theory_arith_params,
public theory_array_params,
public theory_bv_params,
public theory_str_params,
public theory_seq_params,
public theory_pb_params,
public theory_datatype_params {

57
src/params/theory_str_params.cpp
View file

@ -1,57 +0,0 @@
/*++
Module Name:
theory_str_params.cpp
Abstract:
Parameters for string theory plugin
Author:
Murphy Berzish (mtrberzi) 2016-12-13
Revision History:
--*/
#include "params/theory_str_params.h"
#include "params/smt_params_helper.hpp"
void theory_str_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_StrongArrangements = p.str_strong_arrangements();
m_AggressiveLengthTesting = p.str_aggressive_length_testing();
m_AggressiveValueTesting = p.str_aggressive_value_testing();
m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
m_StringConstantCache = p.str_string_constant_cache();
m_OverlapTheoryAwarePriority = p.str_overlap_priority();
m_RegexAutomata_DifficultyThreshold = p.str_regex_automata_difficulty_threshold();
m_RegexAutomata_IntersectionDifficultyThreshold = p.str_regex_automata_intersection_difficulty_threshold();
m_RegexAutomata_FailedAutomatonThreshold = p.str_regex_automata_failed_automaton_threshold();
m_RegexAutomata_FailedIntersectionThreshold = p.str_regex_automata_failed_intersection_threshold();
m_RegexAutomata_LengthAttemptThreshold = p.str_regex_automata_length_attempt_threshold();
m_FixedLengthRefinement = p.str_fixed_length_refinement();
m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
void theory_str_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_StrongArrangements);
DISPLAY_PARAM(m_AggressiveLengthTesting);
DISPLAY_PARAM(m_AggressiveValueTesting);
DISPLAY_PARAM(m_AggressiveUnrollTesting);
DISPLAY_PARAM(m_UseFastLengthTesterCache);
DISPLAY_PARAM(m_UseFastValueTesterCache);
DISPLAY_PARAM(m_StringConstantCache);
DISPLAY_PARAM(m_OverlapTheoryAwarePriority);
DISPLAY_PARAM(m_RegexAutomata_DifficultyThreshold);
DISPLAY_PARAM(m_RegexAutomata_IntersectionDifficultyThreshold);
DISPLAY_PARAM(m_RegexAutomata_FailedAutomatonThreshold);
DISPLAY_PARAM(m_RegexAutomata_FailedIntersectionThreshold);
DISPLAY_PARAM(m_RegexAutomata_LengthAttemptThreshold);
DISPLAY_PARAM(m_FixedLengthNaiveCounterexamples);
}

122
src/params/theory_str_params.h
View file

@ -1,122 +0,0 @@
/*++
Module Name:
theory_str_params.h
Abstract:
Parameters for string theory plugin
Author:
Murphy Berzish (mtrberzi) 2016-12-13
Revision History:
--*/
#pragma once
#include "util/params.h"
struct theory_str_params {
/*
* If AssertStrongerArrangements is set to true,
* the implications that would normally be asserted during arrangement generation
* will instead be asserted as equivalences.
* This is a stronger version of the standard axiom.
* The Z3str2 axioms can be simulated by setting this to false.
*/
bool m_StrongArrangements = true;
/*
* If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
* to prioritize trying concrete length options over choosing the "more" option.
*/
bool m_AggressiveLengthTesting = false;
/*
* Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
* to prioritize trying concrete value options over choosing the "more" option.
*/
bool m_AggressiveValueTesting = false;
/*
* If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
* to prioritize trying concrete unroll counts over choosing the "more" option.
*/
bool m_AggressiveUnrollTesting = true;
/*
* If UseFastLengthTesterCache is set to true,
* length tester terms will not be generated from scratch each time they are needed,
* but will be saved in a map and looked up.
*/
bool m_UseFastLengthTesterCache = false;
/*
* If UseFastValueTesterCache is set to true,
* value tester terms will not be generated from scratch each time they are needed,
* but will be saved in a map and looked up.
*/
bool m_UseFastValueTesterCache = true;
/*
* If StringConstantCache is set to true,
* all string constants in theory_str generated from anywhere will be cached and saved.
*/
bool m_StringConstantCache = true;
double m_OverlapTheoryAwarePriority = -0.1;
/*
* RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3
* will not eagerly construct an automaton for a regular expression term.
*/
unsigned m_RegexAutomata_DifficultyThreshold = 1000;
/*
* RegexAutomata_IntersectionDifficultyThreshold is the lowest difficulty above which Z3str3
* will not eagerly intersect automata to check unsatisfiability.
*/
unsigned m_RegexAutomata_IntersectionDifficultyThreshold = 1000;
/*
* RegexAutomata_FailedAutomatonThreshold is the number of failed attempts to build an automaton
* after which a full automaton (i.e. with no length information) will be built regardless of difficulty.
*/
unsigned m_RegexAutomata_FailedAutomatonThreshold = 10;
/*
* RegexAutomaton_FailedIntersectionThreshold is the number of failed attempts to perform automaton
* intersection after which intersection will always be performed regardless of difficulty.
*/
unsigned m_RegexAutomata_FailedIntersectionThreshold = 10;
/*
* RegexAutomaton_LengthAttemptThreshold is the number of attempts to satisfy length/path constraints
* before which we begin checking unsatisfiability of a regex term.
*/
unsigned m_RegexAutomata_LengthAttemptThreshold = 10;
/*
* If FixedLengthRefinement is true and the fixed-length equation solver is enabled,
* Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive
* reductions to fixed-length formulas.
*/
bool m_FixedLengthRefinement = false;
/*
* If FixedLengthNaiveCounterexamples is true and the fixed-length equation solver is enabled,
* Z3str3 will only construct simple counterexamples to block unsatisfiable length assignments
* instead of attempting to learn more complex lessons.
*/
bool m_FixedLengthNaiveCounterexamples = true;
theory_str_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};

5
src/smt/CMakeLists.txt
View file

@ -68,10 +68,7 @@ z3_add_component(smt
theory_recfun.cpp
theory_seq.cpp
theory_sls.cpp
theory_special_relations.cpp
theory_str.cpp
theory_str_mc.cpp
theory_str_regex.cpp
theory_special_relations.cpp
theory_user_propagator.cpp
theory_utvpi.cpp
theory_wmaxsat.cpp

27
src/smt/smt_setup.cpp
View file

@ -39,7 +39,6 @@ Revision History:
#include "smt/theory_sls.h"
#include "smt/theory_pb.h"
#include "smt/theory_fpa.h"
#include "smt/theory_str.h"
#include "smt/theory_polymorphism.h"
namespace smt {
@ -561,10 +560,7 @@ namespace smt {
}
void setup::setup_QF_S() {
if (m_params.m_string_solver == "z3str3") {
setup_str();
}
else if (m_params.m_string_solver == "seq") {
if (m_params.m_string_solver == "seq") {
setup_unknown();
}
else if (m_params.m_string_solver == "char") {
@ -582,7 +578,7 @@ namespace smt {
// don't register any solver.
}
else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
throw default_exception("invalid parameter for smt.string_solver, valid options are 'seq', 'auto'");
}
}
@ -748,10 +744,7 @@ namespace smt {
void setup::setup_seq_str(static_features const & st) {
// check params for what to do here when it's ambiguous
if (m_params.m_string_solver == "z3str3") {
setup_str();
}
else if (m_params.m_string_solver == "seq") {
if (m_params.m_string_solver == "seq") {
setup_seq();
}
else if (m_params.m_string_solver == "empty") {
@ -760,16 +753,11 @@ namespace smt {
else if (m_params.m_string_solver == "none") {
// don't register any solver.
}
else if (m_params.m_string_solver == "auto") {
if (st.m_has_seq_non_str) {
else if (m_params.m_string_solver == "auto") {
setup_seq();
}
else {
setup_str();
}
}
else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
throw default_exception("invalid parameter for smt.string_solver, valid options are 'seq', 'auto'");
}
}
@ -787,11 +775,6 @@ namespace smt {
m_context.register_plugin(alloc(theory_fpa, m_context));
}
void setup::setup_str() {
setup_arith();
m_context.register_plugin(alloc(theory_str, m_context, m_manager, m_params));
}
void setup::setup_seq() {
m_context.register_plugin(alloc(smt::theory_seq, m_context));
setup_char();

1
src/smt/smt_setup.h
View file

@ -108,7 +108,6 @@ namespace smt {
void setup_mi_arith();
void setup_lra_arith();
void setup_fpa();
void setup_str();
void setup_relevancy(static_features& st);
public:

8985
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

779
src/smt/theory_str.h
View file

@ -1,779 +0,0 @@
/*++
Module Name:
theory_str.h
Abstract:
String Theory Plugin
Author:
Murphy Berzish and Yunhui Zheng
Revision History:
--*/
#pragma once
#include "util/trail.h"
#include "util/union_find.h"
#include "util/scoped_ptr_vector.h"
#include "util/hashtable.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/seq_decl_plugin.h"
#include "model/value_factory.h"
#include "smt/smt_theory.h"
#include "params/theory_str_params.h"
#include "smt/smt_model_generator.h"
#include "smt/smt_arith_value.h"
#include "smt/smt_kernel.h"
#include<set>
#include<stack>
#include<vector>
#include<map>
#include<functional>
namespace smt {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
typedef int_hashtable<int_hash, default_eq<int> > integer_set;
class str_value_factory : public value_factory {
seq_util u;
symbol_set m_strings;
std::string delim;
unsigned m_next;
public:
str_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
u(m), delim("!"), m_next(0) {}
expr * get_some_value(sort * s) override {
return u.str.mk_string("some value");
}
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
v1 = u.str.mk_string("value 1");
v2 = u.str.mk_string("value 2");
return true;
}
expr * get_fresh_value(sort * s) override {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << delim << std::hex << (m_next++) << std::dec << delim;
std::string s(strm.str());
symbol sym(s);
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);
return u.str.mk_string(s);
}
}
sort* seq = nullptr;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
TRACE(t_str, tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
UNREACHABLE(); return nullptr;
}
void register_value(expr * n) override { /* Ignore */ }
};
// NSB: added operator[] and contains to obj_pair_hashtable
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail {
obj_map<expr, ptr_vector<expr> > & target;
expr * entry;
public:
binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
target(target), entry(entry) {}
void undo() override {
TRACE(t_str_binary_search, tout << "in binary_search_trail::undo()" << std::endl;);
if (target.contains(entry)) {
if (!target[entry].empty()) {
target[entry].pop_back();
} else {
TRACE(t_str_binary_search, tout << "WARNING: attempt to remove length tester from an empty stack" << std::endl;);
}
} else {
TRACE(t_str_binary_search, tout << "WARNING: attempt to access length tester map via invalid key" << std::endl;);
}
}
};
class regex_automaton_under_assumptions {
protected:
expr * re_term;
eautomaton * aut;
bool polarity;
bool assume_lower_bound;
rational lower_bound;
bool assume_upper_bound;
rational upper_bound;
public:
regex_automaton_under_assumptions() :
re_term(nullptr), aut(nullptr), polarity(false),
assume_lower_bound(false), assume_upper_bound(false) {}
regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) :
re_term(re_term), aut(aut), polarity(polarity),
assume_lower_bound(false), assume_upper_bound(false) {}
void set_lower_bound(rational & lb) {
lower_bound = lb;
assume_lower_bound = true;
}
void unset_lower_bound() {
assume_lower_bound = false;
}
void set_upper_bound(rational & ub) {
upper_bound = ub;
assume_upper_bound = true;
}
void unset_upper_bound() {
assume_upper_bound = false;
}
bool get_lower_bound(rational & lb) const {
if (assume_lower_bound) {
lb = lower_bound;
return true;
} else {
return false;
}
}
bool get_upper_bound(rational & ub) const {
if (assume_upper_bound) {
ub = upper_bound;
return true;
} else {
return false;
}
}
eautomaton * get_automaton() const { return aut; }
expr * get_regex_term() const { return re_term; }
bool get_polarity() const { return polarity; }
};
class char_union_find {
unsigned_vector m_find;
unsigned_vector m_size;
unsigned_vector m_next;
integer_set char_const_set;
u_map<svector<expr*> > m_justification; // representative -> list of formulas justifying EQC
void ensure_size(unsigned v) {
while (v >= get_num_vars()) {
mk_var();
}
}
public:
unsigned mk_var() {
unsigned r = m_find.size();
m_find.push_back(r);
m_size.push_back(1);
m_next.push_back(r);
return r;
}
unsigned get_num_vars() const { return m_find.size(); }
void mark_as_char_const(unsigned r) {
char_const_set.insert((int)r);
}
bool is_char_const(unsigned r) {
return char_const_set.contains((int)r);
}
unsigned find(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
while (true) {
unsigned new_v = m_find[v];
if (new_v == v)
return v;
v = new_v;
}
}
unsigned next(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
return m_next[v];
}
bool is_root(unsigned v) const {
return v >= get_num_vars() || m_find[v] == v;
}
svector<expr*> get_justification(unsigned v) {
unsigned r = find(v);
svector<expr*> retval;
if (m_justification.find(r, retval)) {
return retval;
} else {
return svector<expr*>();
}
}
void merge(unsigned v1, unsigned v2, expr * justification) {
unsigned r1 = find(v1);
unsigned r2 = find(v2);
if (r1 == r2)
return;
ensure_size(v1);
ensure_size(v2);
// swap r1 and r2 if:
// 1. EQC of r1 is bigger than EQC of r2
// 2. r1 is a character constant and r2 is not.
// this maintains the invariant that if a character constant is in an eqc then it is the root of that eqc
if (m_size[r1] > m_size[r2] || (is_char_const(r1) && !is_char_const(r2))) {
std::swap(r1, r2);
}
m_find[r1] = r2;
m_size[r2] += m_size[r1];
std::swap(m_next[r1], m_next[r2]);
if (m_justification.contains(r1)) {
// add r1's justifications to r2
if (!m_justification.contains(r2)) {
m_justification.insert(r2, m_justification[r1]);
} else {
m_justification[r2].append(m_justification[r1]);
}
m_justification.remove(r1);
}
if (justification != nullptr) {
if (!m_justification.contains(r2)) {
m_justification.insert(r2, svector<expr*>());
}
m_justification[r2].push_back(justification);
}
}
void reset() {
m_find.reset();
m_next.reset();
m_size.reset();
char_const_set.reset();
m_justification.reset();
}
};
class theory_str : public theory {
struct T_cut
{
int level;
obj_map<expr, int> vars;
T_cut() {
level = -100;
}
};
typedef union_find<theory_str> th_union_find;
typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
struct zstring_hash_proc {
unsigned operator()(zstring const & s) const {
auto str = s.encode();
return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17);
}
};
typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(stats)); }
unsigned m_refine_eq;
unsigned m_refine_neq;
unsigned m_refine_f;
unsigned m_refine_nf;
unsigned m_solved_by;
unsigned m_fixed_length_iterations;
};
protected:
theory_str_params const & m_params;
/*
* Setting EagerStringConstantLengthAssertions to true allows some methods,
* in particular internalize_term(), to add
* length assertions about relevant string constants.
* Note that currently this should always be set to 'true', or else *no* length assertions
* will be made about string constants.
*/
bool opt_EagerStringConstantLengthAssertions;
/*
* If VerifyFinalCheckProgress is set to true, continuing after final check is invoked
* without asserting any new axioms is considered a bug and will throw an exception.
*/
bool opt_VerifyFinalCheckProgress;
/*
* This constant controls how eagerly we expand unrolls in unbounded regex membership tests.
*/
int opt_LCMUnrollStep;
/*
* If NoQuickReturn_IntegerTheory is set to true,
* integer theory integration checks that assert axioms
* will not return from the function after asserting their axioms.
* The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect.
*/
bool opt_NoQuickReturn_IntegerTheory;
/*
* If DisableIntegerTheoryIntegration is set to true,
* ALL calls to the integer theory integration methods
* (get_arith_value, get_len_value, lower_bound, upper_bound)
* will ignore what the arithmetic solver believes about length terms,
* and will return no information.
*
* This reduces performance significantly, but can be useful to enable
* if it is suspected that string-integer integration, or the arithmetic solver itself,
* might have a bug.
*
* The default behaviour of Z3str2 is to set this to 'false'.
*/
bool opt_DisableIntegerTheoryIntegration;
/*
* If DeferEQCConsistencyCheck is set to true,
* expensive calls to new_eq_check() will be deferred until final check,
* at which time the consistency of *all* string equivalence classes will be validated.
*/
bool opt_DeferEQCConsistencyCheck;
/*
* If CheckVariableScope is set to true,
* pop_scope_eh() and final_check_eh() will run extra checks
* to determine whether the current assignment
* contains references to any internal variables that are no longer in scope.
*/
bool opt_CheckVariableScope;
/*
* If ConcatOverlapAvoid is set to true,
* the check to simplify Concat = Concat in handle_equality() will
* avoid simplifying wrt. pairs of Concat terms that will immediately
* result in an overlap. (false = Z3str2 behaviour)
*/
bool opt_ConcatOverlapAvoid;
bool search_started;
arith_util m_autil;
seq_util u;
int sLevel;
bool finalCheckProgressIndicator;
expr_ref_vector m_trail; // trail for generated terms
str_value_factory * m_factory;
re2automaton m_mk_aut;
// Unique identifier appended to unused variables to ensure that model construction
// does not introduce equalities when they weren't enforced.
unsigned m_unused_id;
const char* newOverlapStr = "!!NewOverlapAssumption!!";
// terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms;
ptr_vector<enode> m_basicstr_axiom_todo;
ptr_vector<enode> m_concat_axiom_todo;
ptr_vector<enode> m_string_constant_length_todo;
ptr_vector<enode> m_concat_eval_todo;
expr_ref_vector m_delayed_assertions_todo;
// enode lists for library-aware/high-level string terms (e.g. substr, contains)
ptr_vector<enode> m_library_aware_axiom_todo;
// list of axioms that are re-asserted every time the scope is popped
expr_ref_vector m_persisted_axioms;
expr_ref_vector m_persisted_axiom_todo;
// hashtable of all exprs for which we've already set up term-specific axioms --
// this prevents infinite recursive descent with respect to axioms that
// include an occurrence of the term for which axioms are being generated
obj_hashtable<expr> axiomatized_terms;
// hashtable of all top-level exprs for which set_up_axioms() has been called
obj_hashtable<expr> existing_toplevel_exprs;
int tmpStringVarCount;
int tmpXorVarCount;
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
scoped_ptr_vector<T_cut> m_cut_allocs;
expr_ref m_theoryStrOverlapAssumption_term;
obj_hashtable<expr> variable_set;
obj_hashtable<expr> internal_variable_set;
std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
expr_ref_vector contains_map;
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
// regex automata
scoped_ptr_vector<eautomaton> m_automata;
ptr_vector<eautomaton> regex_automata;
obj_hashtable<expr> regex_terms;
obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]
obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries
// keep track of the last lower/upper bound we saw for each string term
// so we don't perform duplicate work
obj_map<expr, rational> regex_last_lower_bound;
obj_map<expr, rational> regex_last_upper_bound;
// each counter maps a (str.in.re) expression to an integer.
// use helper functions regex_inc_counter() and regex_get_counter() to access
obj_map<expr, unsigned> regex_length_attempt_count;
obj_map<expr, unsigned> regex_fail_count;
obj_map<expr, unsigned> regex_intersection_fail_count;
obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i
obj_pair_map<expr, expr, expr*> concat_astNode_map;
// all (str.to-int) and (int.to-str) terms
expr_ref_vector string_int_conversion_terms;
obj_hashtable<expr> string_int_axioms;
string_map stringConstantCache;
unsigned long totalCacheAccessCount;
unsigned long cacheHitCount;
unsigned long cacheMissCount;
unsigned m_fresh_id;
// cache mapping each string S to Length(S)
obj_map<expr, app*> length_ast_map;
trail_stack m_trail_stack;
trail_stack m_library_aware_trail_stack;
th_union_find m_find;
theory_var get_var(expr * n) const;
expr * get_eqc_next(expr * n);
app * get_ast(theory_var i);
// fixed length model construction
expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver*
expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these
obj_map<expr, rational> fixed_length_used_len_terms; // constraints used in generating fixed length model
obj_map<expr, expr_ref_vector* > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver*
obj_map<expr, expr_ref_vector* > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver*
obj_map<expr, std::tuple<rational, expr*, expr*>> fixed_length_lesson; //keep track of information for the lesson
unsigned preprocessing_iteration_count; // number of attempts we've made to solve by preprocessing length information
obj_map<expr, zstring> candidate_model;
stats m_stats;
protected:
void reset_internal_data_structures();
void assert_axiom(expr * e);
void assert_implication(expr * premise, expr * conclusion);
expr * rewrite_implication(expr * premise, expr * conclusion);
// Use the rewriter to simplify an axiom, then assert it.
void assert_axiom_rw(expr * e);
expr * mk_string(zstring const& str);
expr * mk_string(const char * str);
app * mk_strlen(expr * e);
expr * mk_concat(expr * n1, expr * n2);
expr * mk_concat_const_str(expr * n1, expr * n2);
app * mk_contains(expr * haystack, expr * needle);
app * mk_indexof(expr * haystack, expr * needle);
app * mk_fresh_const(char const* name, sort* s);
literal mk_literal(expr* _e);
app * mk_int(int n);
app * mk_int(rational & q);
void check_and_init_cut_var(expr * node);
void add_cut_info_one_node(expr * baseNode, int slevel, expr * node);
void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode);
bool has_self_cut(expr * n1, expr * n2);
// for ConcatOverlapAvoid
bool will_result_in_overlap(expr * lhs, expr * rhs);
void track_variable_scope(expr * var);
app * mk_str_var(std::string name);
app * mk_int_var(std::string name);
app_ref mk_nonempty_str_var();
app * mk_internal_xor_var();
void add_nonempty_constraint(expr * s);
void instantiate_concat_axiom(enode * cat);
void try_eval_concat(enode * cat);
void instantiate_basic_string_axioms(enode * str);
void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
// for count abstraction and refinement
expr* refine(expr* lhs, expr* rhs, rational offset);
expr* refine_eq(expr* lhs, expr* rhs, unsigned offset);
expr* refine_dis(expr* lhs, expr* rhs);
expr* refine_function(expr* f);
bool flatten(expr* ex, expr_ref_vector & flat);
rational get_refine_length(expr* ex, expr_ref_vector& extra_deps);
void instantiate_axiom_CharAt(enode * e);
void instantiate_axiom_prefixof(enode * e);
void instantiate_axiom_suffixof(enode * e);
void instantiate_axiom_Contains(enode * e);
void instantiate_axiom_Indexof(enode * e);
void instantiate_axiom_Indexof_extended(enode * e);
void instantiate_axiom_LastIndexof(enode * e);
void instantiate_axiom_Substr(enode * e);
void instantiate_axiom_Replace(enode * e);
void instantiate_axiom_str_to_int(enode * e);
void instantiate_axiom_int_to_str(enode * e);
void instantiate_axiom_is_digit(enode * e);
void instantiate_axiom_str_to_code(enode * e);
void instantiate_axiom_str_from_code(enode * e);
void add_persisted_axiom(expr * a);
expr * mk_RegexIn(expr * str, expr * regexp);
void instantiate_axiom_RegexIn(enode * e);
// regex automata and length-aware regex
bool solve_regex_automata();
unsigned estimate_regex_complexity(expr * re);
unsigned estimate_regex_complexity_under_complement(expr * re);
unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);
bool check_regex_length_linearity(expr * re);
bool check_regex_length_linearity_helper(expr * re, bool already_star);
expr_ref infer_all_regex_lengths(expr * lenVar, expr * re, expr_ref_vector & freeVariables);
void check_subterm_lengths(expr * re, integer_set & lens);
void find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut);
bool refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound);
bool refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound);
expr_ref generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints);
void aut_path_add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
expr_ref aut_path_rewrite_constraint(expr * cond, expr * ch_var);
void regex_inc_counter(obj_map<expr, unsigned> & counter_map, expr * key);
unsigned regex_get_counter(obj_map<expr, unsigned> & counter_map, expr * key);
void set_up_axioms(expr * ex);
void handle_equality(expr * lhs, expr * rhs);
app * mk_value_helper(app * n);
expr * get_eqc_value(expr * n, bool & hasEqcValue);
bool get_string_constant_eqc(expr * n, zstring & stringVal);
expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
bool in_same_eqc(expr * n1, expr * n2);
expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
bool is_var(expr * e) const;
bool get_arith_value(expr* e, rational& val) const;
bool get_len_value(expr* e, rational& val);
bool lower_bound(expr* _e, rational& lo);
bool upper_bound(expr* _e, rational& hi);
bool can_two_nodes_eq(expr * n1, expr * n2);
bool can_concat_eq_str(expr * concat, zstring& str);
bool can_concat_eq_concat(expr * concat1, expr * concat2);
bool check_concat_len_in_eqc(expr * concat);
void check_eqc_empty_string(expr * lhs, expr * rhs);
void check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs);
bool check_length_consistency(expr * n1, expr * n2);
bool check_length_const_string(expr * n1, expr * constStr);
bool check_length_eq_var_concat(expr * n1, expr * n2);
bool check_length_concat_concat(expr * n1, expr * n2);
bool check_length_concat_var(expr * concat, expr * var);
bool check_length_var_var(expr * var1, expr * var2);
void check_contain_in_new_eq(expr * n1, expr * n2);
void check_contain_by_eqc_val(expr * varNode, expr * constNode);
void check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass);
void check_contain_by_eq_nodes(expr * n1, expr * n2);
bool in_contain_idx_map(expr * n);
void compute_contains(std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
void get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
bool is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec);
void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
expr * simplify_concat(expr * node);
void simplify_parent(expr * nn, expr * eq_str);
void simplify_concat_equality(expr * lhs, expr * rhs);
void solve_concat_eq_str(expr * concat, expr * str);
void infer_len_concat_equality(expr * nn1, expr * nn2);
bool infer_len_concat(expr * n, rational & nLen);
void infer_len_concat_arg(expr * n, rational len);
bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2);
bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type1(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type2(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type3(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type4(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
void print_cut_var(expr * node, std::ofstream & xout);
void generate_mutual_exclusion(expr_ref_vector & exprs);
void add_theory_aware_branching_info(expr * term, double priority, lbool phase);
bool new_eq_check(expr * lhs, expr * rhs);
void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
void check_consistency_prefix(expr * e, bool is_true);
void check_consistency_suffix(expr * e, bool is_true);
void check_consistency_contains(expr * e, bool is_true);
int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
void trace_ctx_dep(std::ofstream & tout,
std::map<expr*, expr*> & aliasIndexMap,
std::map<expr*, expr*> & var_eq_constStr_map,
std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
std::map<expr*, expr*> & concat_eq_constStr_map,
std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map);
bool term_appears_as_subterm(expr * needle, expr * haystack);
void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,
std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
void classify_ast_by_type_in_positive_context(std::map<expr*, int> & varMap,
std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node);
expr * getMostLeftNodeInConcat(expr * node);
expr * getMostRightNodeInConcat(expr * node);
void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
void get_concats_in_eqc(expr * n, std::set<expr*> & concats);
void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
expr * eval_concat(expr * n1, expr * n2);
bool finalcheck_str2int(app * a);
bool finalcheck_int2str(app * a);
bool string_integer_conversion_valid(zstring str, rational& converted) const;
lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
expr_ref_vector& free_variables,
obj_map<expr, zstring> &model, expr_ref_vector &cex);
bool fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term, expr_ref_vector & term_chars, expr_ref & cex);
bool fixed_length_get_len_value(expr * e, rational & val);
bool fixed_length_reduce_eq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
bool fixed_length_reduce_diseq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
bool fixed_length_reduce_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_negative_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_negative_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity);
void dump_assignments();
void check_variable_scope();
void recursive_check_variable_scope(expr * ex);
void collect_var_concat(expr * node, std::set<expr*> & varSet, std::set<expr*> & concatSet);
bool propagate_length(std::set<expr*> & varSet, std::set<expr*> & concatSet, std::map<expr*, int> & exprLenMap);
void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
bool propagate_length_within_eqc(expr * var);
const rational NEQ = rational(-1); // negative word equation lesson
const rational PFUN = rational(-2); // positive function lesson
const rational NFUN = rational(-3); // negative function lesson
// TESTING
void refresh_theory_var(expr * e);
public:
theory_str(context& ctx, ast_manager & m, theory_str_params const & params);
~theory_str() override;
char const * get_name() const override { return "seq"; }
void init() override;
void display(std::ostream & out) const override;
void collect_statistics(::statistics & st) const override;
bool overlapping_variables_detected() const { return loopDetected; }
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) {}
protected:
bool internalize_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app * term) override;
virtual enode* ensure_enode(expr* e);
theory_var mk_var(enode * n) override;
void new_eq_eh(theory_var, theory_var) override;
void new_diseq_eh(theory_var, theory_var) override;
theory* mk_fresh(context* c) override { return alloc(theory_str, *c, c->get_manager(), m_params); }
void init_search_eh() override;
void add_theory_assumptions(expr_ref_vector & assumptions) override;
lbool validate_unsat_core(expr_ref_vector & unsat_core) override;
void relevant_eh(app * n) override;
void assign_eh(bool_var v, bool is_true) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
void reset_eh() override;
bool can_propagate() override;
void propagate() override;
final_check_status final_check_eh() override;
virtual void attach_new_th_var(enode * n);
void init_model(model_generator & m) override;
model_value_proc * mk_value(enode * n, model_generator & mg) override;
void finalize_model(model_generator & mg) override;
};
};

1549
src/smt/theory_str_mc.cpp
View file

File diff suppressed because it is too large Load diff

1526
src/smt/theory_str_regex.cpp
View file

File diff suppressed because it is too large Load diff