mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
2b190039d5
|
@ -1346,16 +1346,16 @@ class PythonInstallComponent(Component):
|
|||
Component.__init__(self, name, None, [])
|
||||
|
||||
def main_component(self):
|
||||
return is_python_install_enabled()
|
||||
return False
|
||||
|
||||
def install_deps(self, out):
|
||||
if not self.main_component():
|
||||
return
|
||||
if not is_python_install_enabled():
|
||||
return
|
||||
pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
|
||||
MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
|
||||
|
||||
def mk_install(self, out):
|
||||
if not self.main_component():
|
||||
if not is_python_install_enabled():
|
||||
return
|
||||
MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
|
||||
if sys.version >= "3":
|
||||
|
@ -1374,7 +1374,7 @@ class PythonInstallComponent(Component):
|
|||
out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
|
||||
|
||||
def mk_uninstall(self, out):
|
||||
if not self.main_component():
|
||||
if not is_python_install_enabled():
|
||||
return
|
||||
pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
|
||||
MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3')))
|
||||
|
|
|
@ -441,8 +441,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_max(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_max(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
|
|
@ -813,16 +813,26 @@ end = struct
|
|||
let s = Z3native.get_sort (context_gno ctx) no in
|
||||
let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in
|
||||
if (Z3native.is_algebraic_number (context_gno ctx) no) then
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
else
|
||||
if (Z3native.is_numeral_ast (context_gno ctx) no) then
|
||||
if (sk == INT_SORT || sk == REAL_SORT || sk == BV_SORT ||
|
||||
sk == FLOATING_POINT_SORT || sk == ROUNDING_MODE_SORT) then
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
else
|
||||
raise (Z3native.Exception "Unsupported numeral object")
|
||||
else
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
if (Z3native.is_numeral_ast (context_gno ctx) no) then
|
||||
match sk with
|
||||
| REAL_SORT
|
||||
| BOOL_SORT
|
||||
| ARRAY_SORT
|
||||
| BV_SORT
|
||||
| ROUNDING_MODE_SORT
|
||||
| RELATION_SORT
|
||||
| UNINTERPRETED_SORT
|
||||
| FLOATING_POINT_SORT
|
||||
| INT_SORT
|
||||
| DATATYPE_SORT
|
||||
| FINITE_DOMAIN_SORT ->
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
| _ ->
|
||||
raise (Z3native.Exception "Unsupported numeral object")
|
||||
else
|
||||
Expr(z3_native_object_of_ast_ptr ctx no)
|
||||
|
||||
let expr_of_ast a =
|
||||
let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in
|
||||
|
|
|
@ -43,14 +43,14 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
void Z3_API Z3_optimize_inc_ref(Z3_context c,Z3_optimize d);
|
||||
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
|
||||
|
||||
/**
|
||||
\brief Decrement the reference counter of the given optimize context.
|
||||
|
||||
def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
void Z3_API Z3_optimize_dec_ref(Z3_context c,Z3_optimize d);
|
||||
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
|
||||
|
||||
/**
|
||||
\brief Assert hard constraint to the optimization context.
|
||||
|
@ -102,7 +102,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d);
|
||||
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
|
||||
|
||||
/**
|
||||
\brief Backtrack one level.
|
||||
|
@ -113,7 +113,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d);
|
||||
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
|
||||
|
||||
/**
|
||||
\brief Check consistency and produce optimal values.
|
||||
|
@ -132,7 +132,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) ))
|
||||
*/
|
||||
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c,Z3_optimize d);
|
||||
Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
|
||||
|
||||
/**
|
||||
\brief Retrieve the model for the last #Z3_optimize_check
|
||||
|
@ -195,9 +195,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_optimize_to_string(
|
||||
Z3_context c,
|
||||
Z3_optimize o);
|
||||
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
|
||||
|
||||
|
||||
/**
|
||||
|
@ -212,7 +210,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
|
||||
*/
|
||||
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d);
|
||||
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
||||
|
|
|
@ -20,6 +20,7 @@ Notes:
|
|||
#include"seq_rewriter.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
#include"ast_pp.h"
|
||||
#include"ast_util.h"
|
||||
|
||||
|
||||
br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
|
@ -187,6 +188,21 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
|
||||
return BR_DONE;
|
||||
}
|
||||
// check if subsequence of a is in b.
|
||||
ptr_vector<expr> as, bs;
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
bool found = false;
|
||||
for (unsigned i = 0; !found && i < bs.size(); ++i) {
|
||||
if (as.size() > bs.size() - i) break;
|
||||
unsigned j = 0;
|
||||
for (; j < as.size() && as[j] == bs[i+j]; ++j) {};
|
||||
found = j == as.size();
|
||||
}
|
||||
if (found) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
@ -261,6 +277,7 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
}
|
||||
|
||||
br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
||||
TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";);
|
||||
std::string s1, s2;
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
bool isc2 = m_util.str.is_string(b, s2);
|
||||
|
@ -276,24 +293,177 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
expr* a1 = m_util.str.get_leftmost_concat(a);
|
||||
expr* b1 = m_util.str.get_leftmost_concat(b);
|
||||
isc1 = m_util.str.is_string(a1, s1);
|
||||
isc2 = m_util.str.is_string(b1, s2);
|
||||
ptr_vector<expr> as, bs;
|
||||
|
||||
if (a1 != b1 && isc1 && isc2) {
|
||||
if (s1.length() <= s2.length()) {
|
||||
if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) {
|
||||
if (a == a1) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
SASSERT(as.size() > 1);
|
||||
s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length());
|
||||
bs[0] = m_util.str.mk_string(s2);
|
||||
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
|
||||
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
else {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) {
|
||||
if (b == b1) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
SASSERT(bs.size() > 1);
|
||||
s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length());
|
||||
as[0] = m_util.str.mk_string(s1);
|
||||
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
|
||||
m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
else {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (a1 != b1) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
unsigned i = 0;
|
||||
for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {};
|
||||
if (i == as.size()) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (i == bs.size()) {
|
||||
expr_ref_vector es(m());
|
||||
for (unsigned j = i; j < as.size(); ++j) {
|
||||
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j]));
|
||||
}
|
||||
result = mk_and(es);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
if (i > 0) {
|
||||
a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
|
||||
b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i);
|
||||
result = m_util.str.mk_prefix(a, b);
|
||||
return BR_DONE;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
|
||||
std::string s1, s2;
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
if (isc1 && m_util.str.is_string(b, s2)) {
|
||||
bool suffix = s1.length() <= s2.length();
|
||||
for (unsigned i = 0; i < s1.length() && suffix; ++i) {
|
||||
suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
|
||||
}
|
||||
result = m().mk_bool_val(suffix);
|
||||
if (a == b) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
std::string s1, s2;
|
||||
if (m_util.str.is_empty(a)) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.str.is_empty(b)) {
|
||||
result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
// concatenation is left-associative, so a2, b2 are not concatenations
|
||||
expr* a1, *a2, *b1, *b2;
|
||||
if (m_util.str.is_concat(a, a1, a2) &&
|
||||
m_util.str.is_concat(b, b1, b2) && a2 == b2) {
|
||||
result = m_util.str.mk_suffix(a1, b1);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
if (m_util.str.is_concat(b, b1, b2) && b2 == a) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
bool isc1 = false;
|
||||
bool isc2 = false;
|
||||
|
||||
if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
|
||||
isc1 = true;
|
||||
}
|
||||
else if (m_util.str.is_string(a, s1)) {
|
||||
isc1 = true;
|
||||
a2 = a;
|
||||
a1 = 0;
|
||||
}
|
||||
|
||||
if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) {
|
||||
isc2 = true;
|
||||
}
|
||||
else if (m_util.str.is_string(b, s2)) {
|
||||
isc2 = true;
|
||||
b2 = b;
|
||||
b1 = 0;
|
||||
}
|
||||
if (isc1 && isc2) {
|
||||
if (s1.length() == s2.length()) {
|
||||
SASSERT(s1 != s2);
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (s1.length() < s2.length()) {
|
||||
bool suffix = true;
|
||||
for (unsigned i = 0; i < s1.length(); ++i) {
|
||||
suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1];
|
||||
}
|
||||
if (suffix && a1 == 0) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (suffix) {
|
||||
s2 = std::string(s2.c_str(), s2.length()-s1.length());
|
||||
b2 = m_util.str.mk_string(s2);
|
||||
result = m_util.str.mk_suffix(a1, b1?m_util.str.mk_concat(b1, b2):b2);
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(s1.length() > s2.length());
|
||||
if (b1 == 0) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
bool suffix = true;
|
||||
for (unsigned i = 0; i < s2.length(); ++i) {
|
||||
suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1];
|
||||
}
|
||||
if (suffix) {
|
||||
s1 = std::string(s1.c_str(), s1.length()-s2.length());
|
||||
a2 = m_util.str.mk_string(s1);
|
||||
result = m_util.str.mk_suffix(a1?m_util.str.mk_concat(a1, a2):a2, b1);
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
|
@ -288,9 +288,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
ast_manager& m = *m_manager;
|
||||
sort_ref rng(m);
|
||||
switch(k) {
|
||||
case OP_SEQ_UNIT:
|
||||
case OP_SEQ_EMPTY:
|
||||
match(*m_sigs[k], arity, domain, range, rng);
|
||||
if (rng == m_string) {
|
||||
parameter param(symbol(""));
|
||||
return mk_func_decl(OP_STRING_CONST, 1, ¶m, 0, 0, m_string);
|
||||
}
|
||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
||||
|
||||
case OP_SEQ_UNIT:
|
||||
case OP_RE_PLUS:
|
||||
case OP_RE_STAR:
|
||||
case OP_RE_OPTION:
|
||||
|
|
|
@ -163,13 +163,19 @@ public:
|
|||
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); }
|
||||
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)); }
|
||||
app* mk_string(symbol const& s);
|
||||
app* mk_string(char const* s) { return mk_string(symbol(s)); }
|
||||
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
|
||||
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
|
||||
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); }
|
||||
app* mk_length(expr* a) { 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_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, 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); }
|
||||
app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
|
||||
|
||||
|
||||
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
|
||||
|
||||
|
@ -180,7 +186,9 @@ public:
|
|||
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
|
||||
}
|
||||
|
||||
bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && strcmp(s.bare_str(),"") == 0); }
|
||||
bool is_empty(expr const* n) const { symbol s;
|
||||
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
|
||||
}
|
||||
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
|
||||
bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
|
||||
bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
|
||||
|
@ -209,6 +217,7 @@ public:
|
|||
MATCH_BINARY(is_in_re);
|
||||
|
||||
void get_concat(expr* e, ptr_vector<expr>& es) const;
|
||||
expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }
|
||||
};
|
||||
|
||||
class re {
|
||||
|
|
|
@ -289,9 +289,9 @@ namespace smt {
|
|||
void arith_eq_adapter::restart_eh() {
|
||||
context & ctx = get_context();
|
||||
TRACE("arith_eq_adapter", tout << "restart\n";);
|
||||
svector<enode_pair> tmp(m_restart_pairs);
|
||||
svector<enode_pair>::iterator it = tmp.begin();
|
||||
svector<enode_pair>::iterator end = tmp.end();
|
||||
enode_pair_vector tmp(m_restart_pairs);
|
||||
enode_pair_vector::iterator it = tmp.begin();
|
||||
enode_pair_vector::iterator end = tmp.end();
|
||||
m_restart_pairs.reset();
|
||||
for (; it != end && !ctx.inconsistent(); ++it) {
|
||||
TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" <<
|
||||
|
|
|
@ -68,7 +68,7 @@ namespace smt {
|
|||
arith_simplifier_plugin * m_as;
|
||||
|
||||
already_processed m_already_processed;
|
||||
svector<enode_pair> m_restart_pairs;
|
||||
enode_pair_vector m_restart_pairs;
|
||||
svector<parameter> m_proof_hint;
|
||||
|
||||
context & get_context() const { return m_owner.get_context(); }
|
||||
|
|
|
@ -45,6 +45,7 @@ namespace smt {
|
|||
class enode;
|
||||
typedef ptr_vector<enode> enode_vector;
|
||||
typedef std::pair<enode *, enode *> enode_pair;
|
||||
typedef svector<enode_pair> enode_pair_vector;
|
||||
|
||||
class context;
|
||||
|
||||
|
|
|
@ -712,7 +712,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, svector<enode_pair> & todo) {
|
||||
void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo) {
|
||||
SASSERT(r->get_root() == r);
|
||||
SASSERT(is_select(sel));
|
||||
if (!get_context().is_relevant(r)) {
|
||||
|
@ -751,7 +751,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void theory_array_base::propagate_selects_to_store_parents(enode * r, svector<enode_pair> & todo) {
|
||||
void theory_array_base::propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo) {
|
||||
select_set * sel_set = get_select_set(r);
|
||||
select_set::iterator it2 = sel_set->begin();
|
||||
select_set::iterator end2 = sel_set->end();
|
||||
|
@ -763,9 +763,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
void theory_array_base::propagate_selects() {
|
||||
svector<enode_pair> todo;
|
||||
ptr_vector<enode>::const_iterator it = m_selects_domain.begin();
|
||||
ptr_vector<enode>::const_iterator end = m_selects_domain.end();
|
||||
enode_pair_vector todo;
|
||||
enode_vector::const_iterator it = m_selects_domain.begin();
|
||||
enode_vector::const_iterator end = m_selects_domain.end();
|
||||
for (; it != end; ++it) {
|
||||
enode * r = *it;
|
||||
propagate_selects_to_store_parents(r, todo);
|
||||
|
|
|
@ -58,8 +58,8 @@ namespace smt {
|
|||
unsigned get_dimension(sort* s) const;
|
||||
|
||||
ptr_vector<enode> m_axiom1_todo;
|
||||
svector<std::pair<enode*, enode*> > m_axiom2_todo;
|
||||
svector<std::pair<enode*, enode*> > m_extensionality_todo;
|
||||
enode_pair_vector m_axiom2_todo;
|
||||
enode_pair_vector m_extensionality_todo;
|
||||
|
||||
void assert_axiom(unsigned num_lits, literal * lits);
|
||||
void assert_axiom(literal l1, literal l2);
|
||||
|
@ -181,8 +181,8 @@ namespace smt {
|
|||
bool is_unspecified_default_ok() const;
|
||||
void collect_defaults();
|
||||
void collect_selects();
|
||||
void propagate_select_to_store_parents(enode * r, enode * sel, svector<enode_pair> & todo);
|
||||
void propagate_selects_to_store_parents(enode * r, svector<enode_pair> & todo);
|
||||
void propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo);
|
||||
void propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo);
|
||||
void propagate_selects();
|
||||
select_set * get_select_set(enode * n);
|
||||
virtual void finalize_model(model_generator & m);
|
||||
|
|
|
@ -438,8 +438,8 @@ namespace smt {
|
|||
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, 0, m_used_eqs.size(), m_used_eqs.c_ptr())));
|
||||
TRACE("occurs_check",
|
||||
tout << "occurs_check: true\n";
|
||||
svector<enode_pair>::const_iterator it = m_used_eqs.begin();
|
||||
svector<enode_pair>::const_iterator end = m_used_eqs.end();
|
||||
enode_pair_vector::const_iterator it = m_used_eqs.begin();
|
||||
enode_pair_vector::const_iterator end = m_used_eqs.end();
|
||||
for(; it != end; ++it) {
|
||||
enode_pair const & p = *it;
|
||||
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
|
||||
|
@ -675,7 +675,7 @@ namespace smt {
|
|||
CTRACE("datatype", d->m_recognizers.empty(), ctx.display(tout););
|
||||
SASSERT(!d->m_recognizers.empty());
|
||||
literal_vector lits;
|
||||
svector<enode_pair> eqs;
|
||||
enode_pair_vector eqs;
|
||||
ptr_vector<enode>::const_iterator it = d->m_recognizers.begin();
|
||||
ptr_vector<enode>::const_iterator end = d->m_recognizers.end();
|
||||
for (unsigned idx = 0; it != end; ++it, ++idx) {
|
||||
|
|
|
@ -74,7 +74,7 @@ namespace smt {
|
|||
void sign_recognizer_conflict(enode * c, enode * r);
|
||||
|
||||
ptr_vector<enode> m_to_unmark;
|
||||
svector<enode_pair> m_used_eqs;
|
||||
enode_pair_vector m_used_eqs;
|
||||
enode * m_main;
|
||||
bool occurs_check(enode * n);
|
||||
bool occurs_check_core(enode * n);
|
||||
|
|
306
src/smt/theory_seq.cpp
Normal file
306
src/smt/theory_seq.cpp
Normal file
|
@ -0,0 +1,306 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_seq.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Native theory solver for sequences.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-6-12
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "value_factory.h"
|
||||
#include "smt_context.h"
|
||||
#include "smt_model_generator.h"
|
||||
#include "theory_seq.h"
|
||||
|
||||
using namespace smt;
|
||||
|
||||
theory_seq::theory_seq(ast_manager& m):
|
||||
theory(m.mk_family_id("seq")),
|
||||
m_axioms_head(0),
|
||||
m_axioms(m),
|
||||
m_ineqs(m),
|
||||
m_used(false),
|
||||
m_rewrite(m),
|
||||
m_util(m),
|
||||
m_autil(m),
|
||||
m_trail_stack(*this),
|
||||
m_find(*this) {}
|
||||
|
||||
final_check_status theory_seq::final_check_eh() {
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
final_check_status st = check_ineqs();
|
||||
if (st == FC_CONTINUE) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
return m_used?FC_GIVEUP:FC_DONE;
|
||||
}
|
||||
|
||||
final_check_status theory_seq::check_ineqs() {
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
enode_pair_vector eqs;
|
||||
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
|
||||
expr_ref a(m_ineqs[i].get(), m);
|
||||
expr_ref b = canonize(a, eqs);
|
||||
if (m.is_true(b)) {
|
||||
ctx.internalize(a, false);
|
||||
literal lit(ctx.get_literal(a));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.assign(
|
||||
lit,
|
||||
ctx.mk_justification(
|
||||
ext_theory_propagation_justification(
|
||||
get_id(), ctx.get_region(), 0, 0, eqs.size(), eqs.c_ptr(), lit)));
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
}
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
final_check_status theory_seq::simplify_eqs() {
|
||||
bool simplified = false;
|
||||
for (unsigned i = 0; i < get_num_vars(); ++i) {
|
||||
theory_var v = m_find.find(i);
|
||||
if (v != i) continue;
|
||||
|
||||
}
|
||||
if (simplified) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
final_check_status theory_seq::add_axioms() {
|
||||
for (unsigned i = 0; i < get_num_vars(); ++i) {
|
||||
|
||||
// add axioms for len(x) when x = a ++ b
|
||||
}
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
bool theory_seq::internalize_atom(app* a, bool) {
|
||||
return internalize_term(a);
|
||||
}
|
||||
|
||||
bool theory_seq::internalize_term(app* term) {
|
||||
m_used = true;
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
unsigned num_args = term->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
ctx.internalize(term->get_arg(i), false);
|
||||
}
|
||||
if (ctx.e_internalized(term)) {
|
||||
return true;
|
||||
}
|
||||
enode * e = ctx.mk_enode(term, false, m.is_bool(term), true);
|
||||
if (m.is_bool(term)) {
|
||||
bool_var bv = ctx.mk_bool_var(term);
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
ctx.set_enode_flag(bv, true);
|
||||
}
|
||||
else {
|
||||
theory_var v = mk_var(e);
|
||||
ctx.attach_th_var(e, this, v);
|
||||
}
|
||||
// assert basic axioms
|
||||
if (!m_used) { m_trail_stack.push(value_trail<theory_seq,bool>(m_used)); m_used = true; }
|
||||
return true;
|
||||
}
|
||||
|
||||
theory_var theory_seq::mk_var(enode* n) {
|
||||
theory_var r = theory::mk_var(n);
|
||||
VERIFY(r == m_find.mk_var());
|
||||
return r;
|
||||
}
|
||||
|
||||
bool theory_seq::can_propagate() {
|
||||
return m_axioms_head < m_axioms.size();
|
||||
}
|
||||
|
||||
expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) {
|
||||
eqs.reset();
|
||||
expr_ref result = expand(e, eqs);
|
||||
m_rewrite(result);
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
expr* e1, *e2;
|
||||
SASSERT(ctx.e_internalized(e));
|
||||
enode* n = ctx.get_enode(e);
|
||||
enode* start = n;
|
||||
do {
|
||||
e = n->get_owner();
|
||||
if (m_util.str.is_concat(e, e1, e2)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m);
|
||||
}
|
||||
if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(e, m);
|
||||
}
|
||||
if (m.is_eq(e, e1, e2)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m);
|
||||
}
|
||||
if (m_util.str.is_prefix(e, e1, e2)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m);
|
||||
}
|
||||
if (m_util.str.is_suffix(e, e1, e2)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m);
|
||||
}
|
||||
if (m_util.str.is_contains(e, e1, e2)) {
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m);
|
||||
}
|
||||
#if 0
|
||||
if (m_util.str.is_unit(e)) {
|
||||
// TBD: canonize the element.
|
||||
if (start != n) eqs.push_back(enode_pair(start, n));
|
||||
return expr_ref(e, m);
|
||||
}
|
||||
#endif
|
||||
n = n->get_next();
|
||||
}
|
||||
while (n != start);
|
||||
return expr_ref(n->get_root()->get_owner(), m);
|
||||
}
|
||||
|
||||
void theory_seq::propagate() {
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
|
||||
expr_ref e(m);
|
||||
e = m_axioms[m_axioms_head].get();
|
||||
assert_axiom(e);
|
||||
++m_axioms_head;
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::create_axiom(expr_ref& e) {
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
|
||||
m_axioms.push_back(e);
|
||||
}
|
||||
|
||||
void theory_seq::assert_axiom(expr_ref& e) {
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
if (m.is_true(e)) return;
|
||||
TRACE("seq", tout << "asserting " << e << "\n";);
|
||||
ctx.internalize(e, false);
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
|
||||
}
|
||||
|
||||
expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) {
|
||||
ast_manager& m = get_manager();
|
||||
expr_ref result(m);
|
||||
sort* s = m.get_sort(e1);
|
||||
SASSERT(s == m.get_sort(e2));
|
||||
sort* ss[2] = { s, s };
|
||||
result = m.mk_app(m.mk_func_decl(symbol("#prefix_eq"), 2, ss, s), e1, e2);
|
||||
return result;
|
||||
}
|
||||
|
||||
void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
|
||||
context& ctx = get_context();
|
||||
ctx.internalize(e1, false);
|
||||
enode* n1 = ctx.get_enode(e1);
|
||||
enode* n2 = ctx.get_enode(e2);
|
||||
literal lit(v);
|
||||
ctx.assign_eq(n1, n2, eq_justification(
|
||||
alloc(ext_theory_eq_propagation_justification,
|
||||
get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)));
|
||||
}
|
||||
|
||||
void theory_seq::assign_eq(bool_var v, bool is_true) {
|
||||
context & ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
|
||||
enode* n = ctx.bool_var2enode(v);
|
||||
app* e = n->get_owner();
|
||||
if (is_true) {
|
||||
expr* e1, *e2;
|
||||
expr_ref f(m);
|
||||
if (m_util.str.is_prefix(e, e1, e2)) {
|
||||
f = mk_skolem("#prefix_eq", e1, e2);
|
||||
f = m_util.str.mk_concat(e1, f);
|
||||
propagate_eq(v, f, e2);
|
||||
}
|
||||
else if (m_util.str.is_suffix(e, e1, e2)) {
|
||||
f = mk_skolem("#suffix_eq", e1, e2);
|
||||
f = m_util.str.mk_concat(f, e1);
|
||||
propagate_eq(v, f, e2);
|
||||
}
|
||||
else if (m_util.str.is_contains(e, e1, e2)) {
|
||||
expr_ref f1 = mk_skolem("#contains_eq1", e1, e2);
|
||||
expr_ref f2 = mk_skolem("#contains_eq2", e1, e2);
|
||||
f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2);
|
||||
propagate_eq(v, f, e2);
|
||||
}
|
||||
else if (m_util.str.is_in_re(e, e1, e2)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
else {
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
|
||||
m_ineqs.push_back(e);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
|
||||
m_find.merge(v1, v2);
|
||||
}
|
||||
|
||||
void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
|
||||
ast_manager& m = get_manager();
|
||||
expr* e1 = get_enode(v1)->get_owner();
|
||||
expr* e2 = get_enode(v2)->get_owner();
|
||||
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
|
||||
m_ineqs.push_back(m.mk_eq(e1, e2));
|
||||
}
|
||||
|
||||
void theory_seq::push_scope_eh() {
|
||||
theory::push_scope_eh();
|
||||
m_trail_stack.push_scope();
|
||||
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
|
||||
}
|
||||
|
||||
void theory_seq::pop_scope_eh(unsigned num_scopes) {
|
||||
m_trail_stack.pop_scope(num_scopes);
|
||||
theory::pop_scope_eh(num_scopes);
|
||||
}
|
||||
|
||||
void theory_seq::restart_eh() {
|
||||
|
||||
}
|
||||
|
||||
void theory_seq::relevant_eh(app* n) {
|
||||
ast_manager& m = get_manager();
|
||||
if (m_util.str.is_length(n)) {
|
||||
expr_ref e(m);
|
||||
e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n);
|
||||
create_axiom(e);
|
||||
}
|
||||
}
|
91
src/smt/theory_seq.h
Normal file
91
src/smt/theory_seq.h
Normal file
|
@ -0,0 +1,91 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_seq.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Native theory solver for sequences.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-6-12
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef THEORY_SEQ_H_
|
||||
#define THEORY_SEQ_H_
|
||||
|
||||
#include "smt_theory.h"
|
||||
#include "seq_decl_plugin.h"
|
||||
#include "theory_seq_empty.h"
|
||||
#include "th_rewriter.h"
|
||||
#include "union_find.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class theory_seq : public theory {
|
||||
typedef union_find<theory_seq> th_union_find;
|
||||
typedef trail_stack<theory_seq> th_trail_stack;
|
||||
struct stats {
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(stats)); }
|
||||
unsigned m_num_splits;
|
||||
};
|
||||
expr_ref_vector m_axioms;
|
||||
expr_ref_vector m_ineqs;
|
||||
unsigned m_axioms_head;
|
||||
bool m_used;
|
||||
th_rewriter m_rewrite;
|
||||
seq_util m_util;
|
||||
arith_util m_autil;
|
||||
th_trail_stack m_trail_stack;
|
||||
th_union_find m_find;
|
||||
stats m_stats;
|
||||
|
||||
virtual final_check_status final_check_eh();
|
||||
virtual bool internalize_atom(app*, bool);
|
||||
virtual bool internalize_term(app*);
|
||||
virtual void new_eq_eh(theory_var, theory_var);
|
||||
virtual void new_diseq_eh(theory_var, theory_var);
|
||||
virtual void assign_eq(bool_var v, bool is_true);
|
||||
virtual bool can_propagate();
|
||||
virtual void propagate();
|
||||
virtual void push_scope_eh();
|
||||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
virtual void restart_eh();
|
||||
virtual void relevant_eh(app* n);
|
||||
virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq, new_ctx->get_manager()); }
|
||||
virtual char const * get_name() const { return "seq"; }
|
||||
virtual theory_var mk_var(enode* n);
|
||||
|
||||
final_check_status check_ineqs();
|
||||
final_check_status simplify_eqs();
|
||||
final_check_status add_axioms();
|
||||
|
||||
void assert_axiom(expr_ref& e);
|
||||
void create_axiom(expr_ref& e);
|
||||
expr_ref canonize(expr* e, enode_pair_vector& eqs);
|
||||
expr_ref expand(expr* e, enode_pair_vector& eqs);
|
||||
|
||||
void propagate_eq(bool_var v, expr* e1, expr* e2);
|
||||
expr_ref mk_skolem(char const* name, expr* e1, expr* e2);
|
||||
public:
|
||||
theory_seq(ast_manager& m);
|
||||
virtual void init_model(model_generator & mg) {
|
||||
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
|
||||
}
|
||||
|
||||
th_trail_stack & get_trail_stack() { return m_trail_stack; }
|
||||
virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
|
||||
static 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);
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
#endif /* THEORY_SEQ_H_ */
|
||||
|
Loading…
Reference in a new issue