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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-01-04 22:35:08 -08:00
commit b079ff1dae
55 changed files with 5500 additions and 885 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -16,11 +16,12 @@ def init_project_def():
add_lib('nlsat', ['polynomial', 'sat'])
add_lib('hilbert', ['util'], 'math/hilbert')
add_lib('simplex', ['util'], 'math/simplex')
add_lib('automata', ['util'], 'math/automata')
add_lib('interval', ['util'], 'math/interval')
add_lib('realclosure', ['interval'], 'math/realclosure')
add_lib('subpaving', ['interval'], 'math/subpaving')
add_lib('ast', ['util', 'polynomial'])
add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
add_lib('rewriter', ['ast', 'polynomial', 'automata'], 'ast/rewriter')
add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
add_lib('model', ['rewriter'])
add_lib('tactic', ['ast', 'model'])

2
scripts/update_api.py
View file

@ -1079,7 +1079,7 @@ def def_API(name, result, params):
def mk_bindings():
exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n")
for key, val in API2Id.items():
exe_c.write(" in.register_cmd(%s, exec_%s);\n" % (key, val))
exe_c.write(" in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val))
exe_c.write("}\n")
def ml_method_name(name):

34
src/api/api_ast.cpp
View file

@ -641,6 +641,12 @@ extern "C" {
else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) {
return Z3_ROUNDING_MODE_SORT;
}
else if (fid == mk_c(c)->get_seq_fid() && k == SEQ_SORT) {
return Z3_SEQ_SORT;
}
else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
return Z3_RE_SORT;
}
else {
return Z3_UNKNOWN_SORT;
}
@ -776,6 +782,8 @@ extern "C" {
SET_ERROR_CODE(Z3_SORT_ERROR);
RETURN_Z3(of_expr(0));
}
SASSERT(from[i]->get_ref_count() > 0);
SASSERT(to[i]->get_ref_count() > 0);
}
expr_safe_replace subst(m);
for (unsigned i = 0; i < num_exprs; i++) {
@ -1106,6 +1114,32 @@ extern "C" {
}
}
if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
default:
return Z3_OP_UNINTERPRETED;
}
}
if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;

2
src/api/api_context.cpp
View file

@ -73,6 +73,7 @@ namespace api {
m_datalog_util(m()),
m_fpa_util(m()),
m_dtutil(m()),
m_sutil(m()),
m_last_result(m()),
m_ast_trail(m()),
m_replay_stack(),
@ -97,6 +98,7 @@ namespace api {
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
m_fpa_fid = m().mk_family_id("fpa");
m_seq_fid = m().mk_family_id("seq");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {

5
src/api/api_context.h
View file

@ -25,6 +25,7 @@ Revision History:
#include"api_util.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"fpa_decl_plugin.h"
@ -58,6 +59,7 @@ namespace api {
datalog::dl_decl_util m_datalog_util;
fpa_util m_fpa_util;
datatype_util m_dtutil;
seq_util m_sutil;
// Support for old solver API
smt_params m_fparams;
@ -78,6 +80,7 @@ namespace api {
family_id m_datalog_fid;
family_id m_pb_fid;
family_id m_fpa_fid;
family_id m_seq_fid;
datatype_decl_plugin * m_dt_plugin;
std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world.
@ -121,6 +124,7 @@ namespace api {
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
fpa_util & fpautil() { return m_fpa_util; }
datatype_util& dtutil() { return m_dtutil; }
seq_util& sutil() { return m_sutil; }
family_id get_basic_fid() const { return m_basic_fid; }
family_id get_array_fid() const { return m_array_fid; }
family_id get_arith_fid() const { return m_arith_fid; }
@ -129,6 +133,7 @@ namespace api {
family_id get_datalog_fid() const { return m_datalog_fid; }
family_id get_pb_fid() const { return m_pb_fid; }
family_id get_fpa_fid() const { return m_fpa_fid; }
family_id get_seq_fid() const { return m_seq_fid; }
datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
Z3_error_code get_error_code() const { return m_error_code; }

151
src/api/api_seq.cpp Normal file
View file

@ -0,0 +1,151 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
api_seq.cpp
Abstract:
API for sequences and regular expressions.
Author:
Nikolaj Bjorner (nbjorner) 2016-01-02.
Revision History:
--*/
#include<iostream>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"api_util.h"
#include"ast_pp.h"
extern "C" {
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort domain) {
Z3_TRY;
LOG_Z3_mk_seq_sort(c, domain);
RESET_ERROR_CODE();
sort * ty = mk_c(c)->sutil().str.mk_seq(to_sort(domain));
mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(ty));
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort domain) {
Z3_TRY;
LOG_Z3_mk_re_sort(c, domain);
RESET_ERROR_CODE();
sort * ty = mk_c(c)->sutil().re.mk_re(to_sort(domain));
mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(ty));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string str) {
Z3_TRY;
LOG_Z3_mk_string(c, str);
RESET_ERROR_CODE();
zstring s(str, zstring::ascii);
app* a = mk_c(c)->sutil().str.mk_string(s);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_string_sort(c);
RESET_ERROR_CODE();
sort* ty = mk_c(c)->sutil().str.mk_string_sort();
mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(ty));
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_seq_sort(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_seq(to_sort(s));
return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_re_sort(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_re(to_sort(s));
return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_string_sort(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().is_string(to_sort(s));
return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_string(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->sutil().str.is_string(to_expr(s));
return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_get_string(c, s);
RESET_ERROR_CODE();
zstring str;
if (!mk_c(c)->sutil().str.is_string(to_expr(s), str)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
std::string result = str.encode();
return mk_c(c)->mk_external_string(result);
Z3_CATCH_RETURN("");
}
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) {
Z3_TRY;
LOG_Z3_mk_seq_empty(c, seq);
RESET_ERROR_CODE();
app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP);
MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP);
MK_BINARY(Z3_mk_seq_prefix, mk_c(c)->get_seq_fid(), OP_SEQ_PREFIX, SKIP);
MK_BINARY(Z3_mk_seq_suffix, mk_c(c)->get_seq_fid(), OP_SEQ_SUFFIX, SKIP);
MK_BINARY(Z3_mk_seq_contains, mk_c(c)->get_seq_fid(), OP_SEQ_CONTAINS, SKIP);
MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);
MK_TERNARY(Z3_mk_seq_index, mk_c(c)->get_seq_fid(), OP_SEQ_INDEX, SKIP);
MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);
MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
};

17
src/api/api_util.h
View file

@ -135,6 +135,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \
MK_BINARY_BODY(NAME, FID, OP, EXTRA_CODE); \
}
#define MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE) \
Z3_TRY; \
RESET_ERROR_CODE(); \
EXTRA_CODE; \
expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \
ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args); \
mk_c(c)->save_ast_trail(a); \
check_sorts(c, a); \
RETURN_Z3(of_ast(a)); \
Z3_CATCH_RETURN(0);
#define MK_TERNARY(NAME, FID, OP, EXTRA_CODE) \
Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3) { \
LOG_ ## NAME(c, n1, n2, n3); \
MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE); \
}
#define MK_NARY(NAME, FID, OP, EXTRA_CODE) \
Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
Z3_TRY; \

184
src/api/c++/z3++.h
View file

@ -205,6 +205,18 @@ namespace z3 {
\brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz.
*/
sort bv_sort(unsigned sz);
/**
\brief Return the sort for ASCII strings.
*/
sort string_sort();
/**
\brief Return a sequence sort over base sort \c s.
*/
sort seq_sort(sort& s);
/**
\brief Return a regular expression sort over sequences \c seq_sort.
*/
sort re_sort(sort& seq_sort);
/**
\brief Return an array sort for arrays from \c d to \c r.
@ -261,6 +273,9 @@ namespace z3 {
expr bv_val(__uint64 n, unsigned sz);
expr bv_val(char const * n, unsigned sz);
expr string_val(char const* s);
expr string_val(std::string const& s);
expr num_val(int n, sort const & s);
/**
@ -425,6 +440,14 @@ namespace z3 {
\brief Return true if this sort is a Relation sort.
*/
bool is_relation() const { return sort_kind() == Z3_RELATION_SORT; }
/**
\brief Return true if this sort is a Sequence sort.
*/
bool is_seq() const { return sort_kind() == Z3_SEQ_SORT; }
/**
\brief Return true if this sort is a regular expression sort.
*/
bool is_re() const { return sort_kind() == Z3_RE_SORT; }
/**
\brief Return true if this sort is a Finite domain sort.
*/
@ -532,6 +555,15 @@ namespace z3 {
\brief Return true if this is a Relation expression.
*/
bool is_relation() const { return get_sort().is_relation(); }
/**
\brief Return true if this is a sequence expression.
*/
bool is_seq() const { return get_sort().is_seq(); }
/**
\brief Return true if this is a regular expression.
*/
bool is_re() const { return get_sort().is_re(); }
/**
\brief Return true if this is a Finite-domain expression.
@ -663,6 +695,7 @@ namespace z3 {
friend expr distinct(expr_vector const& args);
friend expr concat(expr const& a, expr const& b);
friend expr concat(expr_vector const& args);
friend expr operator==(expr const & a, expr const & b);
friend expr operator==(expr const & a, int b);
@ -728,10 +761,50 @@ namespace z3 {
friend expr operator|(int a, expr const & b);
friend expr operator~(expr const & a);
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
/**
\brief sequence and regular expression operations.
+ is overloaeded as sequence concatenation and regular expression union.
concat is overloaded to handle sequences and regular expressions
*/
expr extract(expr const& offset, expr const& length) const {
check_context(*this, offset); check_context(offset, length);
Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
}
expr replace(expr const& src, expr const& dst) const {
check_context(*this, src); check_context(src, dst);
Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
check_error();
return expr(ctx(), r);
}
expr unit() const {
Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
check_error();
return expr(ctx(), r);
}
expr contains(expr const& s) {
check_context(*this, s);
Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
check_error();
return expr(ctx(), r);
}
expr at(expr const& index) const {
check_context(*this, index);
Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
check_error();
return expr(ctx(), r);
}
expr length() const {
Z3_ast r = Z3_mk_seq_length(ctx(), *this);
check_error();
return expr(ctx(), r);
}
/**
\brief Return a simplified version of this expression.
*/
@ -835,6 +908,13 @@ namespace z3 {
else if (a.is_bv() && b.is_bv()) {
r = Z3_mk_bvadd(a.ctx(), a, b);
}
else if (a.is_seq() && b.is_seq()) {
return concat(a, b);
}
else if (a.is_re() && b.is_re()) {
Z3_ast _args[2] = { a, b };
r = Z3_mk_re_union(a.ctx(), 2, _args);
}
else {
// operator is not supported by given arguments.
assert(false);
@ -1219,11 +1299,48 @@ namespace z3 {
inline expr concat(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
Z3_ast r;
if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
Z3_ast _args[2] = { a, b };
r = Z3_mk_seq_concat(a.ctx(), 2, _args);
}
else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
Z3_ast _args[2] = { a, b };
r = Z3_mk_re_concat(a.ctx(), 2, _args);
}
else {
r = Z3_mk_concat(a.ctx(), a, b);
}
a.ctx().check_error();
return expr(a.ctx(), r);
}
inline expr concat(expr_vector const& args) {
Z3_ast r;
assert(args.size() > 0);
if (args.size() == 1) {
return args[0];
}
context& ctx = args[0].ctx();
array<Z3_ast> _args(args);
if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
}
else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
}
else {
r = _args[args.size()-1];
for (unsigned i = args.size()-1; i > 0; ) {
--i;
r = Z3_mk_concat(ctx, _args[i], r);
ctx.check_error();
}
}
ctx.check_error();
return expr(ctx, r);
}
class func_entry : public object {
Z3_func_entry m_entry;
void init(Z3_func_entry e) {
@ -1762,6 +1879,10 @@ namespace z3 {
inline sort context::int_sort() { Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }
inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
array<Z3_symbol> _enum_names(n);
@ -1885,6 +2006,9 @@ namespace z3 {
inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }
inline expr context::num_val(int n, sort const & s) { Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr func_decl::operator()(unsigned n, expr const * args) const {
@ -2017,6 +2141,62 @@ namespace z3 {
d.check_error();
return expr(d.ctx(), r);
}
// sequence and regular expression operations.
// union is +
// concat is overloaded to handle sequences and regular expressions
inline expr empty(sort const& s) {
Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
s.check_error();
return expr(s.ctx(), r);
}
inline expr suffixof(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
inline expr prefixof(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
a.check_error();
return expr(a.ctx(), r);
}
inline expr indexof(expr const& s, expr const& substr, expr const& offset) {
check_context(s, substr); check_context(s, offset);
Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
s.check_error();
return expr(s.ctx(), r);
}
inline expr to_re(expr const& s) {
Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
s.check_error();
return expr(s.ctx(), r);
}
inline expr in_re(expr const& s, expr const& re) {
check_context(s, re);
Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
s.check_error();
return expr(s.ctx(), r);
}
inline expr plus(expr const& re) {
Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
re.check_error();
return expr(re.ctx(), r);
}
inline expr option(expr const& re) {
Z3_ast r = Z3_mk_re_option(re.ctx(), re);
re.check_error();
return expr(re.ctx(), r);
}
inline expr star(expr const& re) {
Z3_ast r = Z3_mk_re_star(re.ctx(), re);
re.check_error();
return expr(re.ctx(), r);
}
inline expr interpolant(expr const& a) {
return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
}

281
src/api/dotnet/Context.cs
View file

@ -125,6 +125,7 @@ namespace Microsoft.Z3
private BoolSort m_boolSort = null;
private IntSort m_intSort = null;
private RealSort m_realSort = null;
private SeqSort m_stringSort = null;
/// <summary>
/// Retrieves the Boolean sort of the context.
@ -163,6 +164,20 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Retrieves the String sort of the context.
/// </summary>
public SeqSort StringSort
{
get
{
Contract.Ensures(Contract.Result<SeqSort>() != null);
if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx));
return m_stringSort;
}
}
/// <summary>
/// Create a new Boolean sort.
/// </summary>
@ -223,6 +238,27 @@ namespace Microsoft.Z3
return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size));
}
/// <summary>
/// Create a new sequence sort.
/// </summary>
public SeqSort MkSeqSort(Sort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<SeqSort>() != null);
return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject));
}
/// <summary>
/// Create a new regular expression sort.
/// </summary>
public ReSort MkReSort(SeqSort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<ReSort>() != null);
return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject));
}
/// <summary>
/// Create a new array sort.
/// </summary>
@ -2286,6 +2322,230 @@ namespace Microsoft.Z3
#endregion
#region Sequence, string and regular expresions
/// <summary>
/// Create the empty sequence.
/// </summary>
public SeqExpr MkEmptySeq(Sort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject));
}
/// <summary>
/// Create the singleton sequence.
/// </summary>
public SeqExpr MkUnit(Expr elem)
{
Contract.Requires(elem != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject));
}
/// <summary>
/// Create a string constant.
/// </summary>
public SeqExpr MkString(string s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
}
/// <summary>
/// Concatentate sequences.
/// </summary>
public SeqExpr MkConcat(params SeqExpr[] t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<SeqExpr>() != null);
CheckContextMatch(t);
return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Retrieve the length of a given sequence.
/// </summary>
public IntExpr MkLength(SeqExpr s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject));
}
/// <summary>
/// Check for sequence prefix.
/// </summary>
public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
{
Contract.Requires(s1 != null);
Contract.Requires(s2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(s1, s2);
return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject));
}
/// <summary>
/// Check for sequence suffix.
/// </summary>
public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
{
Contract.Requires(s1 != null);
Contract.Requires(s2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(s1, s2);
return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject));
}
/// <summary>
/// Check for sequence containment of s2 in s1.
/// </summary>
public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
{
Contract.Requires(s1 != null);
Contract.Requires(s2 != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(s1, s2);
return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject));
}
/// <summary>
/// Retrieve sequence of length one at index.
/// </summary>
public SeqExpr MkAt(SeqExpr s, IntExpr index)
{
Contract.Requires(s != null);
Contract.Requires(index != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
CheckContextMatch(s, index);
return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject));
}
/// <summary>
/// Extract subsequence.
/// </summary>
public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
{
Contract.Requires(s != null);
Contract.Requires(offset != null);
Contract.Requires(length != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
CheckContextMatch(s, offset, length);
return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject));
}
/// <summary>
/// Extract index of sub-string starting at offset.
/// </summary>
public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
{
Contract.Requires(s != null);
Contract.Requires(offset != null);
Contract.Requires(substr != null);
Contract.Ensures(Contract.Result<IntExpr>() != null);
CheckContextMatch(s, substr, offset);
return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject));
}
/// <summary>
/// Replace the first occurrence of src by dst in s.
/// </summary>
public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
{
Contract.Requires(s != null);
Contract.Requires(src != null);
Contract.Requires(dst != null);
Contract.Ensures(Contract.Result<SeqExpr>() != null);
CheckContextMatch(s, src, dst);
return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject));
}
/// <summary>
/// Convert a regular expression that accepts sequence s.
/// </summary>
public ReExpr MkToRe(SeqExpr s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject));
}
/// <summary>
/// Check for regular expression membership.
/// </summary>
public BoolExpr MkInRe(SeqExpr s, ReExpr re)
{
Contract.Requires(s != null);
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<BoolExpr>() != null);
CheckContextMatch(s, re);
return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject));
}
/// <summary>
/// Take the Kleene star of a regular expression.
/// </summary>
public ReExpr MkStar(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject));
}
/// <summary>
/// Take the Kleene plus of a regular expression.
/// </summary>
public ReExpr MPlus(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject));
}
/// <summary>
/// Create the optional regular expression.
/// </summary>
public ReExpr MOption(ReExpr re)
{
Contract.Requires(re != null);
Contract.Ensures(Contract.Result<ReExpr>() != null);
return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject));
}
/// <summary>
/// Create the concatenation of regular languages.
/// </summary>
public ReExpr MkConcat(params ReExpr[] t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ReExpr>() != null);
CheckContextMatch(t);
return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create the union of regular languages.
/// </summary>
public ReExpr MkUnion(params ReExpr[] t)
{
Contract.Requires(t != null);
Contract.Requires(Contract.ForAll(t, a => a != null));
Contract.Ensures(Contract.Result<ReExpr>() != null);
CheckContextMatch(t);
return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
#endregion
#region Pseudo-Boolean constraints
/// <summary>
@ -4448,6 +4708,26 @@ namespace Microsoft.Z3
throw new Z3Exception("Context mismatch");
}
[Pure]
internal void CheckContextMatch(Z3Object other1, Z3Object other2)
{
Contract.Requires(other1 != null);
Contract.Requires(other2 != null);
CheckContextMatch(other1);
CheckContextMatch(other2);
}
[Pure]
internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
{
Contract.Requires(other1 != null);
Contract.Requires(other2 != null);
Contract.Requires(other3 != null);
CheckContextMatch(other1);
CheckContextMatch(other2);
CheckContextMatch(other3);
}
[Pure]
internal void CheckContextMatch(Z3Object[] arr)
{
@ -4628,6 +4908,7 @@ namespace Microsoft.Z3
m_boolSort = null;
m_intSort = null;
m_realSort = null;
m_stringSort = null;
}
#endregion
}

2
src/api/dotnet/Expr.cs
View file

@ -1826,6 +1826,8 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
case Z3_sort_kind.Z3_RE_SORT: return new ReExpr(ctx, obj);
case Z3_sort_kind.Z3_SEQ_SORT: return new SeqExpr(ctx, obj);
}
return new Expr(ctx, obj);

42
src/api/dotnet/ReExpr.cs Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (<c>) 2016 Microsoft Corporation
Module Name:
ReExpr.cs
Abstract:
Z3 Managed API: Regular Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Regular expression expressions
/// </summary>
public class ReExpr : Expr
{
#region Internal
/// <summary> Constructor for ReExpr </summary>
internal ReExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

43
src/api/dotnet/ReSort.cs Normal file
View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
ReSort.cs
Abstract:
Z3 Managed API: Regular expression Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A regular expression sort
/// </summary>
public class ReSort : Sort
{
#region Internal
internal ReSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal ReSort(Context ctx)
: base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
}

42
src/api/dotnet/SeqExpr.cs Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (<c>) 2016 Microsoft Corporation
Module Name:
SeqExpr.cs
Abstract:
Z3 Managed API: Sequence Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Sequence expressions
/// </summary>
public class SeqExpr : Expr
{
#region Internal
/// <summary> Constructor for SeqExpr </summary>
internal SeqExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

43
src/api/dotnet/SeqSort.cs Normal file
View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
SeqSort.cs
Abstract:
Z3 Managed API: Sequence Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A Sequence sort
/// </summary>
public class SeqSort : Sort
{
#region Internal
internal SeqSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal SeqSort(Context ctx)
: base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
}

2
src/api/dotnet/Sort.cs
View file

@ -147,6 +147,8 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
case Z3_sort_kind.Z3_SEQ_SORT: return new SeqSort(ctx, obj);
case Z3_sort_kind.Z3_RE_SORT: return new ReSort(ctx, obj);
default:
throw new Z3Exception("Unknown sort kind");
}

229
src/api/java/Context.java
View file

@ -103,6 +103,7 @@ public class Context extends IDisposable
private BoolSort m_boolSort = null;
private IntSort m_intSort = null;
private RealSort m_realSort = null;
private SeqSort m_stringSort = null;
/**
* Retrieves the Boolean sort of the context.
@ -142,6 +143,16 @@ public class Context extends IDisposable
return new BoolSort(this);
}
/**
* Retrieves the Integer sort of the context.
**/
public SeqSort getStringSort()
{
if (m_stringSort == null)
m_stringSort = mkStringSort();
return m_stringSort;
}
/**
* Create a new uninterpreted sort.
**/
@ -193,6 +204,31 @@ public class Context extends IDisposable
return new ArraySort(this, domain, range);
}
/**
* Create a new string sort
**/
public SeqSort mkStringSort()
{
return new SeqSort(this, Native.mkStringSort(nCtx()));
}
/**
* Create a new sequence sort
**/
public SeqSort mkSeqSort(Sort s)
{
return new SeqSort(this, Native.mkSeqSort(nCtx(), s.getNativeObject()));
}
/**
* Create a new regular expression sort
**/
public ReSort mkReSort(Sort s)
{
return new ReSort(this, Native.mkReSort(nCtx(), s.getNativeObject()));
}
/**
* Create a new tuple sort.
**/
@ -1849,6 +1885,184 @@ public class Context extends IDisposable
arg2.getNativeObject()));
}
/**
* Sequences, Strings and regular expressions.
*/
/**
* Create the empty sequence.
*/
public SeqExpr MkEmptySeq(Sort s)
{
checkContextMatch(s);
return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
}
/**
* Create the singleton sequence.
*/
public SeqExpr MkUnit(Expr elem)
{
checkContextMatch(elem);
return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
}
/**
* Create a string constant.
*/
public SeqExpr MkString(String s)
{
return new SeqExpr(this, Native.mkString(nCtx(), s));
}
/**
* Concatentate sequences.
*/
public SeqExpr MkConcat(SeqExpr... t)
{
checkContextMatch(t);
return new SeqExpr(this, Native.mkSeqConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
}
/**
* Retrieve the length of a given sequence.
*/
public IntExpr MkLength(SeqExpr s)
{
checkContextMatch(s);
return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
}
/**
* Check for sequence prefix.
*/
public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Check for sequence suffix.
*/
public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Check for sequence containment of s2 in s1.
*/
public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Retrieve sequence of length one at index.
*/
public SeqExpr MkAt(SeqExpr s, IntExpr index)
{
checkContextMatch(s, index);
return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
}
/**
* Extract subsequence.
*/
public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
{
checkContextMatch(s, offset, length);
return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
}
/**
* Extract index of sub-string starting at offset.
*/
public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
{
checkContextMatch(s, substr, offset);
return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
}
/**
* Replace the first occurrence of src by dst in s.
*/
public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
{
checkContextMatch(s, src, dst);
return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
}
/**
* Convert a regular expression that accepts sequence s.
*/
public ReExpr MkToRe(SeqExpr s)
{
checkContextMatch(s);
return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
}
/**
* Check for regular expression membership.
*/
public BoolExpr MkInRe(SeqExpr s, ReExpr re)
{
checkContextMatch(s, re);
return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
}
/**
* Take the Kleene star of a regular expression.
*/
public ReExpr MkStar(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));
}
/**
* Take the Kleene plus of a regular expression.
*/
public ReExpr MPlus(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
}
/**
* Create the optional regular expression.
*/
public ReExpr MOption(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));
}
/**
* Create the concatenation of regular languages.
*/
public ReExpr MkConcat(ReExpr... t)
{
checkContextMatch(t);
return new ReExpr(this, Native.mkReConcat(nCtx(), (int)t.length, AST.arrayToNative(t)));
}
/**
* Create the union of regular languages.
*/
public ReExpr MkUnion(ReExpr... t)
{
checkContextMatch(t);
return new ReExpr(this, Native.mkReUnion(nCtx(), (int)t.length, AST.arrayToNative(t)));
}
/**
* Create a Term of a given sort.
* @param v A string representing the term value in decimal notation. If the given sort is a real, then the
@ -3683,6 +3897,19 @@ public class Context extends IDisposable
throw new Z3Exception("Context mismatch");
}
void checkContextMatch(Z3Object other1, Z3Object other2)
{
checkContextMatch(other1);
checkContextMatch(other2);
}
void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3)
{
checkContextMatch(other1);
checkContextMatch(other2);
checkContextMatch(other3);
}
void checkContextMatch(Z3Object[] arr)
{
if (arr != null)
@ -3822,6 +4049,7 @@ public class Context extends IDisposable
m_Params_DRQ.clear(this);
m_Probe_DRQ.clear(this);
m_Solver_DRQ.clear(this);
m_Optimize_DRQ.clear(this);
m_Statistics_DRQ.clear(this);
m_Tactic_DRQ.clear(this);
m_Fixedpoint_DRQ.clear(this);
@ -3829,6 +4057,7 @@ public class Context extends IDisposable
m_boolSort = null;
m_intSort = null;
m_realSort = null;
m_stringSort = null;
synchronized (creation_lock) {
if (m_refCount.get() == 0 && m_ctx != 0) {

4
src/api/java/Expr.java
View file

@ -2186,6 +2186,10 @@ public class Expr extends AST
return new FPRMExpr(ctx, obj);
case Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainExpr(ctx, obj);
case Z3_SEQ_SORT:
return new SeqExpr(ctx, obj);
case Z3_RE_SORT:
return new ReExpr(ctx, obj);
default: ;
}

4
src/api/java/Sort.java
View file

@ -141,6 +141,10 @@ public class Sort extends AST
return new FPSort(ctx, obj);
case Z3_ROUNDING_MODE_SORT:
return new FPRMSort(ctx, obj);
case Z3_SEQ_SORT:
return new SeqSort(ctx, obj);
case Z3_RE_SORT:
return new ReSort(ctx, obj);
default:
throw new Z3Exception("Unknown sort kind");
}

59
src/api/ml/z3.ml
View file

@ -87,6 +87,8 @@ struct
(z3obj_sno res ctx no) ;
(z3obj_create res) ;
res
end
open Internal
@ -833,6 +835,13 @@ end = struct
let o = Z3native.mk_app (context_gno ctx) (AST.ptr_of_ast fa) (List.length args) (expr_lton args) in
expr_of_ptr ctx o
let apply1 ctx f t = expr_of_ptr ctx (f (context_gno ctx) (gno t)) in
let apply2 ctx f t1 t2 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2)) in
let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) in
let simplify ( x : expr ) ( p : Params.params option ) = match p with
| None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x))
| Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp))
@ -854,13 +863,13 @@ end = struct
if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then
raise (Z3native.Exception "Number of arguments does not match")
else
expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))
expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args))
let substitute ( x : expr ) from to_ =
if (List.length from) <> (List.length to_) then
raise (Z3native.Exception "Argument sizes do not match")
else
expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_))
expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_))
let substitute_one ( x : expr ) from to_ =
substitute ( x : expr ) [ from ] [ to_ ]
@ -872,7 +881,7 @@ end = struct
if (Expr.gc x) == to_ctx then
x
else
expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx))
expr_of_ptr to_ctx (Z3native.translate (gnc x) (gno x) (context_gno to_ctx))
let to_string ( x : expr ) = Z3native.ast_to_string (gnc x) (gno x)
@ -933,34 +942,33 @@ struct
let mk_val ( ctx : context ) ( value : bool ) =
if value then mk_true ctx else mk_false ctx
let mk_not ( ctx : context ) ( a : expr ) =
expr_of_ptr ctx (Z3native.mk_not (context_gno ctx) (gno a))
let mk_not ( ctx : context ) ( a : expr ) = apply1 ctx Z3native.mk_not a
let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
expr_of_ptr ctx (Z3native.mk_ite (context_gno ctx) (gno t1) (gno t2) (gno t3))
let mk_ite ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
apply3 ctx Z3native.mk_ite t1 t2 t3
let mk_iff ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
expr_of_ptr ctx (Z3native.mk_iff (context_gno ctx) (gno t1) (gno t2))
apply2 ctx Z3native.mk_iff t1 t2
let mk_implies ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
expr_of_ptr ctx (Z3native.mk_implies (context_gno ctx) (gno t1) (gno t2))
apply2 ctx Z3native.mk_implies t1 t2
let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
expr_of_ptr ctx (Z3native.mk_xor (context_gno ctx) (gno t1) (gno t2))
apply2 ctx Z3native.mk_xor t1 t2
let mk_and ( ctx : context ) ( args : expr list ) =
let f x = (Expr.gno (x)) in
expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args)))
expr_of_ptr ctx (Z3native.mk_and (context_gno ctx) (List.length args) (Array.of_list (List.map f args)))
let mk_or ( ctx : context ) ( args : expr list ) =
let f x = (Expr.gno (x)) in
expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
expr_of_ptr ctx (Z3native.mk_or (context_gno ctx) (List.length args) (Array.of_list(List.map f args)))
let mk_eq ( ctx : context ) ( x : expr ) ( y : expr ) =
expr_of_ptr ctx (Z3native.mk_eq (context_gno ctx) (Expr.gno x) (Expr.gno y))
apply2 ctx Z3native.mk_eq x y
let mk_distinct ( ctx : context ) ( args : expr list ) =
expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
expr_of_ptr ctx (Z3native.mk_distinct (context_gno ctx) (List.length args) (expr_lton args))
let get_bool_value ( x : expr ) = lbool_of_int (Z3native.get_bool_value (gnc x) (gno x))
@ -1066,10 +1074,10 @@ struct
mk_list f n
let get_body ( x : quantifier ) =
expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x))
apply1 (gc x) Z3native.get_quantifier_body x
let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) =
expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
let mk_pattern ( ctx : context ) ( terms : expr list ) =
if (List.length terms) == 0 then
@ -1194,23 +1202,23 @@ struct
mk_const ctx (Symbol.mk_string ctx name) domain range
let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) =
expr_of_ptr ctx (Z3native.mk_select (context_gno ctx) (Expr.gno a) (Expr.gno i))
apply2 ctx Z3native.mk_select a i
let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) =
expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (Expr.gno a) (Expr.gno i) (Expr.gno v))
apply3 ctx Z3native.mk_store a i v
let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) =
expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) =
let m x = (Expr.gno x) in
expr_of_ptr ctx (Z3native.mk_map (context_gno ctx) (FuncDecl.gno f) (List.length args) (Array.of_list (List.map m args)))
let mk_term_array ( ctx : context ) ( arg : expr ) =
expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg))
apply1 ctx Z3native.mk_array_default arg
let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) =
expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
apply2 ctx Z3native.mk_array_ext arg1 arg2
end
@ -1233,13 +1241,14 @@ struct
expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain))
let mk_set_add ( ctx : context ) ( set : expr ) ( element : expr ) =
expr_of_ptr ctx (Z3native.mk_set_add (context_gno ctx) (Expr.gno set) (Expr.gno element))
apply2 ctx Z3native.mk_set_add set element
let mk_del ( ctx : context ) ( set : expr ) ( element : expr ) =
expr_of_ptr ctx (Z3native.mk_set_del (context_gno ctx) (Expr.gno set) (Expr.gno element))
apply2 Z3native.mk_set_del set element
let mk_union ( ctx : context ) ( args : expr list ) =
expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args))
let r = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) in
r
let mk_intersection ( ctx : context ) ( args : expr list ) =
expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args))

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

@ -930,6 +930,10 @@ def _to_expr_ref(a, ctx):
return FiniteDomainRef(a, ctx)
if sk == Z3_ROUNDING_MODE_SORT:
return FPRMRef(a, ctx)
if sk == Z3_SEQ_SORT:
return SeqRef(a, ctx)
if sk == Z3_RE_SORT:
return ReRef(a, ctx)
return ExprRef(a, ctx)
def _coerce_expr_merge(s, a):
@ -3562,24 +3566,56 @@ def Concat(*args):
121
"""
args = _get_args(args)
sz = len(args)
if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.")
ctx = args[0].ctx
if is_seq(args[0]):
if __debug__:
_z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
if is_re(args[0]):
if __debug__:
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
if __debug__:
_z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
_z3_assert(len(args) >= 2, "At least two arguments expected.")
ctx = args[0].ctx
r = args[0]
for i in range(len(args) - 1):
for i in range(sz - 1):
r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
return r
def Extract(high, low, a):
"""Create a Z3 bit-vector extraction expression.
"""Create a Z3 bit-vector extraction expression, or create a string extraction expression.
>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)
>>> simplify(Extract(StringVal("abcd"),2,1))
"c"
"""
if isinstance(high, str):
high = StringVal(high)
if is_seq(high):
s = high
offset = _py2expr(low, high.ctx)
length = _py2expr(a, high.ctx)
if __debug__:
_z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers")
return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
if __debug__:
_z3_assert(low <= high, "First argument must be greater than or equal to second argument")
_z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
@ -7781,7 +7817,7 @@ def binary_interpolant(a,b,p=None,ctx=None):
solver that determines satisfiability.
x = Int('x')
print binary_interpolant(x<0,x>2)
print(binary_interpolant(x<0,x>2))
Not(x >= 0)
"""
f = And(Interpolant(a),b)
@ -7821,6 +7857,7 @@ def sequence_interpolant(v,p=None,ctx=None):
f = And(Interpolant(f),v[i])
return tree_interpolant(f,p,ctx)
#########################################
#
# Floating-Point Arithmetic
@ -8901,3 +8938,339 @@ def fpToIEEEBV(x):
if __debug__:
_z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx)
#########################################
#
# Strings, Sequences and Regular expressions
#
#########################################
class SeqSortRef(SortRef):
"""Sequence sort."""
def is_string(self):
"""Determine if sort is a string
>>> s = StringSort()
>>> s.is_string()
True
>>> s = SeqSort(IntSort())
>>> s.is_string()
False
"""
return Z3_is_string_sort(self.ctx_ref(), self.ast)
def StringSort(ctx=None):
"""Create a string sort
>>> s = StringSort()
>>> print(s)
String
"""
ctx = _get_ctx(ctx)
return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
def SeqSort(s):
"""Create a sequence sort over elements provided in the argument
>>> s = SeqSort(IntSort())
>>> s == Unit(IntVal(1)).sort()
True
"""
return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
class SeqRef(ExprRef):
"""Sequence expression."""
def sort(self):
return SeqSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def __add__(self, other):
return Concat(self, other)
def __getitem__(self, i):
return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
def is_string(self):
return Z3_is_string_sort(self.ctx_ref(), Z3_get_sort(self.ctx_ref(), self.as_ast()))
def is_string_value(self):
return Z3_is_string(self.ctx_ref(), self.as_ast())
def as_string(self):
"""Return a string representation of sequence expression."""
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def _coerce_seq(s, ctx=None):
if isinstance(s, str):
ctx = _get_ctx(ctx)
s = StringVal(s, ctx)
return s
def _get_ctx2(a, b, ctx=None):
if is_expr(a):
return a.ctx
if is_expr(b):
return b.ctx
if ctx is None:
ctx = main_ctx()
return ctx
def is_seq(a):
"""Return `True` if `a` is a Z3 sequence expression.
>>> print (is_seq(Unit(IntVal(0))))
True
>>> print (is_seq(StringVal("abc")))
True
"""
return isinstance(a, SeqRef)
def is_string(a):
"""Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
True
"""
return isinstance(a, SeqRef) and a.is_string()
def is_string_value(a):
"""return 'True' if 'a' is a Z3 string constant expression.
>>> print (is_string_value(StringVal("a")))
True
>>> print (is_string_value(StringVal("a") + StringVal("b")))
False
"""
return isinstance(a, SeqRef) and a.is_string_value()
def StringVal(s, ctx=None):
"""create a string expression"""
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
def String(name, ctx=None):
"""Return a string constant named `name`. If `ctx=None`, then the global context is used.
>>> x = String('x')
"""
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
def Strings(names, ctx=None):
"""Return a tuple of String constants. """
ctx = _get_ctx(ctx)
if isinstance(names, str):
names = names.split(" ")
return [String(name, ctx) for name in names]
def Empty(s):
"""Create the empty sequence of the given sort
>>> e = Empty(StringSort())
>>> print(e)
""
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
seq.empty
"""
return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
def Unit(a):
"""Create a singleton sequence"""
return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
def PrefixOf(a, b):
"""Check if 'a' is a prefix of 'b'
>>> s1 = PrefixOf("ab", "abc")
>>> simplify(s1)
True
>>> s2 = PrefixOf("bc", "abc")
>>> simplify(s2)
False
"""
ctx = _get_ctx2(a, b)
a = _coerce_seq(a, ctx)
b = _coerce_seq(b, ctx)
return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def SuffixOf(a, b):
"""Check if 'a' is a suffix of 'b'
>>> s1 = SuffixOf("ab", "abc")
>>> simplify(s1)
False
>>> s2 = SuffixOf("bc", "abc")
>>> simplify(s2)
True
"""
ctx = _get_ctx2(a, b)
a = _coerce_seq(a, ctx)
b = _coerce_seq(b, ctx)
return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def Contains(a, b):
"""Check if 'a' contains 'b'
>>> s1 = Contains("abc", "ab")
>>> simplify(s1)
True
>>> s2 = Contains("abc", "bc")
>>> simplify(s2)
True
>>> x, y, z = Strings('x y z')
>>> s3 = Contains(Concat(x,y,z), y)
>>> simplify(s3)
True
"""
ctx = _get_ctx2(a, b)
a = _coerce_seq(a, ctx)
b = _coerce_seq(b, ctx)
return BoolRef(Z3_mk_seq_contains(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def Replace(s, src, dst):
"""Replace the first occurrence of 'src' by 'dst' in 's'
>>> r = Replace("aaa", "a", "b")
>>> simplify(r)
"baa"
"""
ctx = _get_ctx2(dst, s)
if ctx is None and is_expr(src):
ctx = src.ctx
src = _coerce_seq(src, ctx)
dst = _coerce_seq(dst, ctx)
s = _coerce_seq(s, ctx)
return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
def IndexOf(s, substr):
return IndexOf(s, substr, IntVal(0))
def IndexOf(s, substr, offset):
"""Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4
"""
ctx = None
if is_expr(offset):
ctx = offset.ctx
ctx = _get_ctx2(s, substr, ctx)
s = _coerce_seq(s, ctx)
substr = _coerce_seq(substr, ctx)
if isinstance(offset, int):
offset = IntVal(offset, ctx)
return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
def Length(s):
"""Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
"""
s = _coerce_seq(s)
return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
def Re(s, ctx=None):
"""The regular expression that accepts sequence 's'
>>> s1 = Re("ab")
>>> s2 = Re(StringVal("ab"))
>>> s3 = Re(Unit(BoolVal(True)))
"""
s = _coerce_seq(s, ctx)
return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
## Regular expressions
class ReSortRef(SortRef):
"""Regular expression sort."""
def ReSort(s):
if is_ast(s):
return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx)
if s is None or isinstance(s, Context):
ctx = _get_ctx(s)
return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx)
raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument")
class ReRef(ExprRef):
"""Regular expressions."""
def __add__(self, other):
return Union(self, other)
def is_re(s):
return isinstance(s, ReRef)
def InRe(s, re):
"""Create regular expression membership test
>>> re = Union(Re("a"),Re("b"))
>>> print (simplify(InRe("a", re)))
True
>>> print (simplify(InRe("b", re)))
True
>>> print (simplify(InRe("c", re)))
False
"""
s = _coerce_seq(s, re.ctx)
return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
def Union(*args):
"""Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> print (simplify(InRe("d", re)))
False
"""
args = _get_args(args)
sz = len(args)
if __debug__:
_z3_assert(sz >= 2, "At least two arguments expected.")
_z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
ctx = args[0].ctx
v = (Ast * sz)()
for i in range(sz):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
def Plus(re):
"""Create the regular expression accepting one or more repetitions of argument.
>>> re = Plus(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
False
"""
return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
def Option(re):
"""Create the regular expression that optionally accepts the argument.
>>> re = Option(Re("a"))
>>> print(simplify(InRe("a", re)))
True
>>> print(simplify(InRe("", re)))
True
>>> print(simplify(InRe("aa", re)))
False
"""
return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
def Star(re):
"""Create the regular expression accepting zero or more repetitions of argument.
>>> re = Star(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
True
"""
return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)

5
src/api/python/z3printer.py
View file

@ -570,6 +570,9 @@ class Formatter:
def pp_algebraic(self, a):
return to_format(a.as_decimal(self.precision))
def pp_string(self, a):
return to_format(a.as_string())
def pp_bv(self, a):
return to_format(a.as_string())
@ -875,6 +878,8 @@ class Formatter:
return self.pp_fp_value(a)
elif z3.is_fp(a):
return self.pp_fp(a, d, xs)
elif z3.is_string_value(a):
return self.pp_string(a)
elif z3.is_const(a):
return self.pp_const(a)
else:

242
src/api/z3_api.h
View file

@ -161,6 +161,8 @@ typedef enum
Z3_FINITE_DOMAIN_SORT,
Z3_FLOATING_POINT_SORT,
Z3_ROUNDING_MODE_SORT,
Z3_SEQ_SORT,
Z3_RE_SORT,
Z3_UNKNOWN_SORT = 1000
} Z3_sort_kind;
@ -1098,7 +1100,7 @@ typedef enum {
Z3_OP_PR_TH_LEMMA,
Z3_OP_PR_HYPER_RESOLVE,
// Sequences
// Relational algebra
Z3_OP_RA_STORE = 0x600,
Z3_OP_RA_EMPTY,
Z3_OP_RA_IS_EMPTY,
@ -1115,6 +1117,28 @@ typedef enum {
Z3_OP_FD_CONSTANT,
Z3_OP_FD_LT,
// Sequences
Z3_OP_SEQ_UNIT,
Z3_OP_SEQ_EMPTY,
Z3_OP_SEQ_CONCAT,
Z3_OP_SEQ_PREFIX,
Z3_OP_SEQ_SUFFIX,
Z3_OP_SEQ_CONTAINS,
Z3_OP_SEQ_EXTRACT,
Z3_OP_SEQ_REPLACE,
Z3_OP_SEQ_AT,
Z3_OP_SEQ_LENGTH,
Z3_OP_SEQ_INDEX,
Z3_OP_SEQ_TO_RE,
Z3_OP_SEQ_IN_RE,
// regular expressions
Z3_OP_RE_PLUS,
Z3_OP_RE_STAR,
Z3_OP_RE_OPTION,
Z3_OP_RE_CONCAT,
Z3_OP_RE_UNION,
// Auxiliary
Z3_OP_LABEL = 0x700,
Z3_OP_LABEL_LIT,
@ -3093,6 +3117,222 @@ extern "C" {
/*@}*/
/** @name Sequences and regular expressions */
/*@{*/
/**
\brief Create a sequence sort out of the sort for the elements.
def_API('Z3_mk_seq_sort', SORT, (_in(CONTEXT), _in(SORT)))
*/
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s);
/**
\brief Check if \c s is a sequence sort.
def_API('Z3_is_seq_sort', BOOL, (_in(CONTEXT), _in(SORT)))
*/
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s);
/**
\brief Create a regular expression sort out of a sequence sort.
def_API('Z3_mk_re_sort', SORT, (_in(CONTEXT), _in(SORT)))
*/
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq);
/**
\brief Check if \c s is a regular expression sort.
def_API('Z3_is_re_sort', BOOL, (_in(CONTEXT), _in(SORT)))
*/
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s);
/**
\brief Create a sort for 8 bit strings.
This function creates a sort for ASCII strings.
Each character is 8 bits.
def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), ))
*/
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
/**
\brief Check if \c s is a string sort.
def_API('Z3_is_string_sort', BOOL, (_in(CONTEXT), _in(SORT)))
*/
Z3_bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s);
/**
\brief Create a string constant out of the string that is passed in
def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING)))
*/
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s);
/**
\brief Determine if \c s is a string constant.
def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
/**
\brief Retrieve the string constant stored in \c s.
\pre Z3_is_string(c, s)
def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s);
/**
\brief Create an empty sequence of the sequence sort \c seq.
\pre s is a sequence sort.
def_API('Z3_mk_seq_empty' ,AST ,(_in(CONTEXT), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq);
/**
\brief Create a unit sequence of \c a.
def_API('Z3_mk_seq_unit' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a);
/**
\brief Concatenate sequences.
\pre n > 0
def_API('Z3_mk_seq_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
*/
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]);
/**
\brief Check if \c prefix is a prefix of \c s.
\pre prefix and s are the same sequence sorts.
def_API('Z3_mk_seq_prefix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s);
/**
\brief Check if \c suffix is a suffix of \c s.
\pre \c suffix and \c s are the same sequence sorts.
def_API('Z3_mk_seq_suffix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s);
/**
\brief Check if \c container contains \c containee.
\pre \c container and \c containee are the same sequence sorts.
def_API('Z3_mk_seq_contains' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee);
/**
\brief Extract subsequence starting at \c offset of \c length.
def_API('Z3_mk_seq_extract' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length);
/**
\brief Replace the first occurrence of \c src with \c dst in \c s.
def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
/**
\brief Retrieve from \s the unit sequence positioned at position \c index.
def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index);
/**
\brief Return the length of the sequence \c s.
def_API('Z3_mk_seq_length' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s);
/**
\brief Return index of first occurrence of \c substr in \c s starting from offset \c offset.
If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well.
The function is under-specified if \c offset is negative or larger than the length of \c s.
def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
/**
\brief Create a regular expression that accepts the sequence \c seq.
def_API('Z3_mk_seq_to_re' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq);
/**
\brief Check if \c seq is in the language generated by the regular expression \c re.
def_API('Z3_mk_seq_in_re' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re);
/**
\brief Create the regular language \c re+.
def_API('Z3_mk_re_plus' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re);
/**
\brief Create the regular language \c re*.
def_API('Z3_mk_re_star' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re);
/**
\brief Create the regular language \c [re].
def_API('Z3_mk_re_option' ,AST ,(_in(CONTEXT), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re);
/**
\brief Create the union of the regular languages.
\pre n > 0
def_API('Z3_mk_re_union' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
*/
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]);
/**
\brief Create the concatenation of the regular languages.
\pre n > 0
def_API('Z3_mk_re_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST)))
*/
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]);
/*@}*/
/** @name Quantifiers */
/*@{*/
/**

10
src/api/z3_replayer.cpp
View file

@ -46,6 +46,7 @@ struct z3_replayer::imp {
size_t m_ptr;
size_t_map<void *> m_heap;
svector<z3_replayer_cmd> m_cmds;
vector<std::string> m_cmds_names;
enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
@ -509,6 +510,7 @@ struct z3_replayer::imp {
if (idx >= m_cmds.size())
throw z3_replayer_exception("invalid command");
try {
TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";);
m_cmds[idx](m_owner);
}
catch (z3_error & ex) {
@ -672,9 +674,11 @@ struct z3_replayer::imp {
m_result = obj;
}
void register_cmd(unsigned id, z3_replayer_cmd cmd) {
void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
m_cmds.reserve(id+1, 0);
m_cmds_names.reserve(id+1, "");
m_cmds[id] = cmd;
m_cmds_names[id] = name;
}
void reset() {
@ -786,8 +790,8 @@ void z3_replayer::store_result(void * obj) {
return m_imp->store_result(obj);
}
void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd) {
return m_imp->register_cmd(id, cmd);
void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
return m_imp->register_cmd(id, cmd, name);
}
void z3_replayer::parse() {

2
src/api/z3_replayer.h
View file

@ -62,7 +62,7 @@ public:
void ** get_obj_addr(unsigned pos);
void store_result(void * obj);
void register_cmd(unsigned id, z3_replayer_cmd cmd);
void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name);
};
#endif

1
src/ast/ast.cpp
View file

@ -1656,6 +1656,7 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
// increment reference counters

5
src/ast/rewriter/bit_blaster/bit_blaster_tpl.h
View file

@ -121,8 +121,11 @@ public:
void mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
void mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
bool mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); }
void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits);
};

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

@ -38,7 +38,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
template<typename Cfg>
bool bit_blaster_tpl<Cfg>::is_numeral(unsigned sz, expr * const * bits) const {
for (unsigned i = 0; i < sz; i++)
if (!m().is_true(bits[i]) && !m().is_false(bits[i]))
if (!is_bool_const(bits[i]))
return false;
return true;
}
@ -158,30 +158,24 @@ void bit_blaster_tpl<Cfg>::mk_subtracter(unsigned sz, expr * const * a_bits, exp
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
SASSERT(sz > 0);
if (!m_use_bcm) {
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_b))
std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) {
mk_neg(sz, a_bits, out_bits);
return;
}
if (is_numeral(sz, a_bits, n_a)) {
n_a *= n_b;
num2bits(n_a, sz, out_bits);
return;
}
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_b))
std::swap(a_bits, b_bits);
if (is_minus_one(sz, b_bits)) {
mk_neg(sz, a_bits, out_bits);
return;
}
else {
numeral n_a, n_b;
if (is_numeral(sz, a_bits, n_a)) {
mk_const_multiplier(sz, a_bits, b_bits, out_bits);
return;
} else if (is_numeral(sz, b_bits, n_b)) {
mk_const_multiplier(sz, b_bits, a_bits, out_bits);
return;
}
if (is_numeral(sz, a_bits, n_a)) {
n_a *= n_b;
num2bits(n_a, sz, out_bits);
return;
}
if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
return;
}
if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
return;
}
if (!m_use_wtm) {
@ -1171,13 +1165,74 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
}
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
DEBUG_CODE({
numeral x;
SASSERT(is_numeral(sz, a_bits, x));
SASSERT(out_bits.empty());
});
bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
unsigned nb = 0;
unsigned case_size = 1;
unsigned circuit_size = sz*sz*5;
for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
if (!is_bool_const(a_bits[i])) {
case_size *= 2;
}
if (!is_bool_const(b_bits[i])) {
case_size *= 2;
}
}
if (case_size >= circuit_size) {
return false;
}
SASSERT(out_bits.empty());
ptr_buffer<expr, 128> na_bits;
na_bits.append(sz, a_bits);
ptr_buffer<expr, 128> nb_bits;
nb_bits.append(sz, b_bits);
mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits);
return false;
}
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;
if (is_a && i == sz) { is_a = false; i = 0; }
while (!is_a && i < sz && is_bool_const(b_bits[i])) ++i;
if (i < sz) {
expr_ref_vector out1(m()), out2(m());
expr_ref x(m());
x = is_a?a_bits[i]:b_bits[i];
if (is_a) a_bits[i] = m().mk_true(); else b_bits[i] = m().mk_true();
mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out1);
if (is_a) a_bits[i] = m().mk_false(); else b_bits[i] = m().mk_false();
mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);
if (is_a) a_bits[i] = x; else b_bits[i] = x;
SASSERT(out_bits.empty());
for (unsigned j = 0; j < sz; ++j) {
out_bits.push_back(m().mk_ite(x, out1[j].get(), out2[j].get()));
}
}
else {
numeral n_a, n_b;
SASSERT(i == sz && !is_a);
VERIFY(is_numeral(sz, a_bits.c_ptr(), n_a));
VERIFY(is_numeral(sz, b_bits.c_ptr(), n_b));
n_a *= n_b;
num2bits(n_a, sz, out_bits);
}
}
template<typename Cfg>
bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
numeral n_a;
if (!is_numeral(sz, a_bits, n_a)) {
return false;
}
SASSERT(out_bits.empty());
if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
return true;
}
if (!m_use_bcm) {
return false;
}
expr_ref_vector minus_b_bits(m()), tmp(m());
mk_neg(sz, b_bits, minus_b_bits);
@ -1255,4 +1310,6 @@ void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
return true;
}

118
src/ast/rewriter/bv_rewriter.cpp
View file

@ -1968,7 +1968,63 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
}
#include "ast_pp.h"
bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
std::swap(lhs, rhs);
}
if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
return false;
}
unsigned sz = to_app(rhs)->get_num_args();
expr_ref t1(m()), t2(m());
t1 = to_app(rhs)->get_arg(0);
if (sz > 2) {
t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
}
else {
SASSERT(sz == 2);
t2 = to_app(rhs)->get_arg(1);
}
mk_t1_add_t2_eq_c(t1, t2, lhs, result);
return true;
}
bool bv_rewriter::is_add_mul_const(expr* e) const {
if (!m_util.is_bv_add(e)) {
return false;
}
unsigned num = to_app(e)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(e)->get_arg(i);
expr * c2, * x2;
if (m_util.is_numeral(arg))
continue;
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
continue;
return false;
}
return true;
}
bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
return
m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs))) ||
m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)));
}
bool bv_rewriter::has_numeral(app* a) const {
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (is_numeral(a->get_arg(i))) {
return true;
}
}
return false;
}
br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
expr * c, * x;
numeral c_val, c_inv_val;
unsigned sz;
@ -2001,24 +2057,30 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
// c * x = t_1 + ... + t_n
// and t_i's have non-unary coefficients (this condition is used to make sure we are actually reducing the number of multipliers).
if (m_util.is_bv_add(rhs)) {
if (is_add_mul_const(rhs)) {
// Potential problem: this simplification may increase the number of adders by reducing the amount of sharing.
unsigned num = to_app(rhs)->get_num_args();
unsigned i;
for (i = 0; i < num; i++) {
expr * arg = to_app(rhs)->get_arg(i);
expr * c2, * x2;
if (m_util.is_numeral(arg))
continue;
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
continue;
break;
}
if (i == num) {
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
return BR_REWRITE2;
result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
return BR_REWRITE2;
}
}
if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
unsigned sz = to_app(rhs)->get_num_args();
unsigned i = 0;
expr* c2, *x2;
numeral c2_val, c2_inv_val;
bool found = false;
for (; !found && i < sz; ++i) {
expr* arg = to_app(rhs)->get_arg(i);
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
m_util.mult_inverse(c2_val, sz, c2_inv_val)) {
found = true;
}
}
if (found) {
result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz),
m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
return BR_REWRITE3;
}
}
return BR_FAILED;
}
@ -2065,9 +2127,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return st;
}
expr_ref new_lhs(m());
expr_ref new_rhs(m());
if (m_util.is_bv_add(lhs) || m_util.is_bv_mul(lhs) || m_util.is_bv_add(rhs) || m_util.is_bv_mul(rhs)) {
expr_ref new_lhs(m());
expr_ref new_rhs(m());
st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
if (st != BR_FAILED) {
if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
@ -2080,28 +2143,27 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
new_rhs = rhs;
}
lhs = new_lhs;
rhs = new_rhs;
// Try to rewrite t1 + t2 = c --> t1 = c - t2
// Reason: it is much cheaper to bit-blast.
expr * t1, * t2;
if (m_util.is_bv_add(new_lhs, t1, t2) && is_numeral(new_rhs)) {
mk_t1_add_t2_eq_c(t1, t2, new_rhs, result);
if (isolate_term(lhs, rhs, result)) {
return BR_REWRITE2;
}
if (m_util.is_bv_add(new_rhs, t1, t2) && is_numeral(new_lhs)) {
mk_t1_add_t2_eq_c(t1, t2, new_lhs, result);
return BR_REWRITE2;
if (is_concat_target(lhs, rhs)) {
return mk_eq_concat(lhs, rhs, result);
}
if (st != BR_FAILED) {
result = m().mk_eq(new_lhs, new_rhs);
result = m().mk_eq(lhs, rhs);
return BR_DONE;
}
}
if ((m_util.is_concat(lhs) && is_concat_split_target(rhs)) ||
(m_util.is_concat(rhs) && is_concat_split_target(lhs)))
if (is_concat_target(lhs, rhs)) {
return mk_eq_concat(lhs, rhs, result);
}
if (swapped) {
result = m().mk_eq(lhs, rhs);
return BR_DONE;

4
src/ast/rewriter/bv_rewriter.h
View file

@ -137,6 +137,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool is_concat_split_target(expr * t) const;
br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result);
bool is_add_mul_const(expr* e) const;
bool isolate_term(expr* lhs, expr* rhs, expr_ref & result);
bool has_numeral(app* e) const;
bool is_concat_target(expr* lhs, expr* rhs) const;
void updt_local_params(params_ref const & p);

15
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -20,9 +20,11 @@ Revision History:
#include "expr_safe_replace.h"
#include "rewriter.h"
#include "ast_pp.h"
void expr_safe_replace::insert(expr* src, expr* dst) {
SASSERT(m.get_sort(src) == m.get_sort(dst));
m_src.push_back(src);
m_dst.push_back(dst);
m_subst.insert(src, dst);
@ -30,7 +32,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_todo.push_back(e);
expr* a, *b, *d;
expr* a, *b;
while (!m_todo.empty()) {
a = m_todo.back();
@ -39,7 +41,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
}
else if (m_subst.find(a, b)) {
m_cache.insert(a, b);
m_todo.pop_back();
m_todo.pop_back();
}
else if (is_var(a)) {
m_cache.insert(a, a);
@ -51,18 +53,21 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) {
if (m_cache.find(c->get_arg(i), d)) {
expr* d = 0, *arg = c->get_arg(i);
if (m_cache.find(arg, d)) {
m_args.push_back(d);
arg_differs |= c->get_arg(i) != d;
arg_differs |= arg != d;
SASSERT(m.get_sort(arg) == m.get_sort(d));
}
else {
m_todo.push_back(c->get_arg(i));
m_todo.push_back(arg);
}
}
if (m_args.size() == n) {
if (arg_differs) {
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
m_refs.push_back(b);
SASSERT(m.get_sort(a) == m.get_sort(b));
} else {
b = a;
}

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

@ -22,30 +22,144 @@ Notes:
#include"ast_pp.h"
#include"ast_util.h"
#include"uint_set.h"
#include"automaton.h"
#include"well_sorted.h"
struct display_expr1 {
ast_manager& m;
display_expr1(ast_manager& m): m(m) {}
std::ostream& display(std::ostream& out, expr* e) const {
return out << mk_pp(e, m);
}
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
eautomaton* re2automaton::operator()(expr* e) {
eautomaton* r = re2aut(e);
if (r) {
//display_expr1 disp(m);
//r->display(std::cout, disp);
r->compress();
//r->display(std::cout, disp);
}
return r;
}
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr* e1, *e2;
scoped_ptr<eautomaton> a, b;
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)) {
}
else if (u.re.is_loop(e)) {
}
#if 0
else if (u.re.is_intersect(e, e1, e2)) {
}
else if (u.re.is_empty(e)) {
}
#endif
return 0;
}
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, m, e1);
}
else if (u.str.is_empty(e)) {
return eautomaton::mk_epsilon(m);
}
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(m, k, k+1, u.str.mk_char(s, k)));
}
return alloc(eautomaton, m, init, final, mvs);
}
return 0;
}
br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid());
switch(f->get_decl_kind()) {
case OP_SEQ_UNIT:
case OP_SEQ_EMPTY:
case OP_RE_PLUS:
case OP_RE_STAR:
case OP_RE_OPTION:
case OP_RE_RANGE:
case OP_RE_CONCAT:
case OP_RE_UNION:
case OP_RE_INTERSECT:
case OP_RE_LOOP:
case OP_RE_EMPTY_SET:
case OP_RE_FULL_SET:
case OP_RE_OF_PRED:
case _OP_SEQ_SKOLEM:
return BR_FAILED;
case OP_SEQ_EMPTY:
return BR_FAILED;
case OP_RE_PLUS:
SASSERT(num_args == 1);
return mk_re_plus(args[0], result);
case OP_RE_STAR:
SASSERT(num_args == 1);
return mk_re_star(args[0], result);
case OP_RE_OPTION:
SASSERT(num_args == 1);
return mk_re_opt(args[0], result);
case OP_RE_CONCAT:
SASSERT(num_args == 2);
return mk_re_concat(args[0], args[1], result);
case OP_RE_UNION:
SASSERT(num_args == 2);
return mk_re_union(args[0], args[1], result);
case OP_RE_RANGE:
return BR_FAILED;
case OP_RE_INTERSECT:
return BR_FAILED;
case OP_RE_LOOP:
return BR_FAILED;
case OP_RE_EMPTY_SET:
return BR_FAILED;
case OP_RE_FULL_SET:
return BR_FAILED;
case OP_RE_OF_PRED:
return BR_FAILED;
case _OP_SEQ_SKOLEM:
return BR_FAILED;
case OP_SEQ_CONCAT:
if (num_args == 1) {
result = args[0];
@ -83,10 +197,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 3);
return mk_seq_replace(args[0], args[1], args[2], result);
case OP_SEQ_TO_RE:
return BR_FAILED;
SASSERT(num_args == 1);
return mk_str_to_regexp(args[0], result);
case OP_SEQ_IN_RE:
return BR_FAILED;
SASSERT(num_args == 2);
return mk_str_in_regexp(args[0], args[1], result);
case OP_STRING_CONST:
return BR_FAILED;
case OP_STRING_ITOS:
@ -129,8 +244,8 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
result = m_util.str.mk_string(s1 + s2);
return BR_DONE;
}
if (m_util.str.is_concat(b, c, d)) {
result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
if (m_util.str.is_concat(a, c, d)) {
result = m_util.str.mk_concat(c, m_util.str.mk_concat(d, b));
return BR_REWRITE2;
}
if (m_util.str.is_empty(a)) {
@ -141,11 +256,15 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
result = a;
return BR_DONE;
}
if (m_util.str.is_concat(a, c, d) &&
m_util.str.is_string(d, s1) && isc2) {
// TBD concatenation is right-associative
if (isc2 && m_util.str.is_concat(a, c, d) && m_util.str.is_string(d, s1)) {
result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
return BR_DONE;
}
if (isc1 && m_util.str.is_concat(b, c, d) && m_util.str.is_string(c, s2)) {
result = m_util.str.mk_concat(m_util.str.mk_string(s1 + s2), d);
return BR_DONE;
}
return BR_FAILED;
}
@ -156,17 +275,17 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
unsigned len = 0;
unsigned j = 0;
for (unsigned i = 0; i < m_es.size(); ++i) {
if (m_util.str.is_string(m_es[i], b)) {
if (m_util.str.is_string(m_es[i].get(), b)) {
len += b.length();
}
else if (m_util.str.is_unit(m_es[i])) {
else if (m_util.str.is_unit(m_es[i].get())) {
len += 1;
}
else if (m_util.str.is_empty(m_es[i])) {
else if (m_util.str.is_empty(m_es[i].get())) {
// skip
}
else {
m_es[j] = m_es[i];
m_es[j] = m_es[i].get();
++j;
}
}
@ -177,7 +296,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
if (j != m_es.size() || j != 1) {
expr_ref_vector es(m());
for (unsigned i = 0; i < j; ++i) {
es.push_back(m_util.str.mk_length(m_es[i]));
es.push_back(m_util.str.mk_length(m_es[i].get()));
}
if (len != 0) {
es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
@ -207,20 +326,31 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
return BR_DONE;
}
// check if subsequence of b is in a.
ptr_vector<expr> as, bs;
expr_ref_vector as(m()), bs(m());
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
bool all_values = true;
for (unsigned i = 0; all_values && i < bs.size(); ++i) {
all_values = m().is_value(bs[i].get());
}
bool found = false;
for (unsigned i = 0; !found && i < as.size(); ++i) {
if (bs.size() > as.size() - i) break;
all_values &= m().is_value(as[i].get());
unsigned j = 0;
for (; j < bs.size() && as[j+i] == bs[j]; ++j) {};
for (; j < bs.size() && as[j+i].get() == bs[j].get(); ++j) {};
found = j == bs.size();
}
if (found) {
result = m().mk_true();
return BR_DONE;
}
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}
@ -292,7 +422,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
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;
expr_ref_vector as(m()), bs(m());
if (a1 != b1 && isc1 && isc2) {
if (s1.length() <= s2.length()) {
@ -342,15 +472,26 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
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) {};
bool all_values = true;
for (; i < as.size() && i < bs.size(); ++i) {
all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
if (as[i].get() != bs[i].get()) {
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
break;
}
};
if (i == as.size()) {
result = m().mk_true();
return BR_DONE;
}
SASSERT(i < as.size());
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]));
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(es);
return BR_REWRITE3;
@ -380,20 +521,10 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
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;
expr* a1, *a2, *b1, *b2;
if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
isc1 = true;
}
@ -453,6 +584,37 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
}
}
}
expr_ref_vector as(m()), bs(m());
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
bool change = false;
while (as.size() > 0 && bs.size() > 0 && as.back() == bs.back()) {
as.pop_back();
bs.pop_back();
change = true;
}
if (as.size() > 0 && bs.size() > 0 && m().is_value(as.back()) && m().is_value(bs.back())) {
result = m().mk_false();
return BR_DONE;
}
if (change) {
// suffix("", bs) <- true
if (as.empty()) {
result = m().mk_true();
return BR_DONE;
}
// suffix(as, "") iff as = ""
if (bs.empty()) {
for (unsigned j = 0; j < as.size(); ++j) {
bs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(bs);
return BR_REWRITE3;
}
result = m_util.str.mk_suffix(m_util.str.mk_concat(as.size(), as.c_ptr()),
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
return BR_DONE;
}
return BR_FAILED;
}
@ -480,26 +642,190 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
}
return BR_FAILED;
}
void seq_rewriter::add_next(u_map<expr*>& next, unsigned idx, expr* cond) {
expr* acc;
if (m().is_true(cond) || !next.find(idx, acc)) {
next.insert(idx, cond);
}
else {
next.insert(idx, m().mk_or(cond, acc));
}
}
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
zstring s;
ptr_vector<expr> todo;
expr *e1, *e2;
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
todo.pop_back();
if (m_util.str.is_string(e, s)) {
for (unsigned i = s.length(); i > 0; ) {
--i;
seq.push_back(m_util.str.mk_char(s, i));
}
}
else if (m_util.str.is_empty(e)) {
continue;
}
else if (m_util.str.is_unit(e)) {
seq.push_back(e);
}
else if (m_util.str.is_concat(e, e1, e2)) {
todo.push_back(e1);
todo.push_back(e2);
}
else {
return false;
}
}
seq.reverse();
return true;
}
br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
scoped_ptr<eautomaton> aut;
expr_ref_vector seq(m());
if (is_sequence(a, seq) && (aut = re2automaton(m())(b))) {
expr_ref_vector trail(m());
u_map<expr*> maps[2];
bool select_map = false;
expr_ref ch(m()), cond(m());
eautomaton::moves mvs;
maps[0].insert(aut->init(), m().mk_true());
// is_accepted(a, aut) & some state in frontier is final.
for (unsigned i = 0; i < seq.size(); ++i) {
u_map<expr*>& frontier = maps[select_map];
u_map<expr*>& next = maps[!select_map];
select_map = !select_map;
ch = seq[i].get();
next.reset();
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
for (; it != end; ++it) {
mvs.reset();
unsigned state = it->m_key;
expr* acc = it->m_value;
aut->get_moves_from(state, mvs, false);
for (unsigned j = 0; j < mvs.size(); ++j) {
eautomaton::move const& mv = mvs[j];
if (m().is_value(mv.t()) && m().is_value(ch)) {
if (mv.t() == ch) {
add_next(next, mv.dst(), acc);
}
else {
continue;
}
}
else {
cond = m().mk_eq(mv.t(), ch);
if (!m().is_true(acc)) cond = m().mk_and(acc, cond);
add_next(next, mv.dst(), cond);
}
}
}
}
u_map<expr*> const& frontier = maps[select_map];
u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
expr_ref_vector ors(m());
for (; it != end; ++it) {
unsigned_vector states;
bool has_final = false;
aut->get_epsilon_closure(it->m_key, states);
for (unsigned i = 0; i < states.size() && !has_final; ++i) {
has_final = aut->is_final_state(states[i]);
}
if (has_final) {
ors.push_back(it->m_value);
}
}
result = mk_or(ors);
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
if (is_epsilon(a)) {
result = b;
return BR_DONE;
}
if (is_epsilon(b)) {
result = a;
return BR_DONE;
}
return BR_FAILED;
}
/*
(a + a) = a
(a + eps) = a
(eps + a) = a
*/
br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
if (a == b) {
result = a;
return BR_DONE;
}
if (m_util.re.is_star(a) && is_epsilon(b)) {
result = a;
return BR_DONE;
}
if (m_util.re.is_star(b) && is_epsilon(a)) {
result = b;
return BR_DONE;
}
return BR_FAILED;
}
/*
a** = a*
(a* + b)* = (a + b)*
(a + b*)* = (a + b)*
(a*b*)* = (a + b)*
*/
br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
expr* b, *c, *b1, *c1;
if (m_util.re.is_star(a)) {
result = a;
return BR_DONE;
}
if (m_util.re.is_union(a, b, c)) {
if (m_util.re.is_star(b, b1)) {
result = m_util.re.mk_star(m_util.re.mk_union(b1, c));
return BR_REWRITE2;
}
if (m_util.re.is_star(c, c1)) {
result = m_util.re.mk_star(m_util.re.mk_union(b, c1));
return BR_REWRITE2;
}
}
if (m_util.re.is_concat(a, b, c) &&
m_util.re.is_star(b, b1) && m_util.re.is_star(c, c1)) {
result = m_util.re.mk_star(m_util.re.mk_union(b1, c1));
return BR_REWRITE2;
}
return BR_FAILED;
}
/*
a+ = aa*
*/
br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
return BR_FAILED;
// result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
// return BR_REWRITE2;
}
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
return BR_FAILED;
sort* s;
VERIFY(m_util.is_re(a, s));
sort_ref seq(m_util.str.mk_seq(s), m());
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(seq)), a);
return BR_REWRITE1;
}
br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
@ -518,38 +844,33 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
return BR_REWRITE3;
}
bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs) {
expr* a, *b;
zstring s;
bool change = false;
expr_ref_vector trail(m());
m_lhs.reset();
m_rhs.reset();
m_util.str.get_concat(l, m_lhs);
m_util.str.get_concat(r, m_rhs);
// solve from back
while (true) {
while (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) {
m_rhs.pop_back();
while (!rs.empty() && m_util.str.is_empty(rs.back())) {
rs.pop_back();
change = true;
}
while (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) {
m_lhs.pop_back();
while (!ls.empty() && m_util.str.is_empty(ls.back())) {
ls.pop_back();
change = true;
}
if (m_lhs.empty() || m_rhs.empty()) {
if (ls.empty() || rs.empty()) {
break;
}
expr* l = m_lhs.back();
expr* r = m_rhs.back();
expr* l = ls.back();
expr* r = rs.back();
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
std::swap(m_lhs, m_rhs);
ls.swap(rs);
}
if (l == r) {
m_lhs.pop_back();
m_rhs.pop_back();
ls.pop_back();
rs.pop_back();
}
else if(m_util.str.is_unit(l, a) &&
m_util.str.is_unit(r, b)) {
@ -558,8 +879,8 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
}
lhs.push_back(a);
rhs.push_back(b);
m_lhs.pop_back();
m_rhs.pop_back();
ls.pop_back();
rs.pop_back();
}
else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
SASSERT(s.length() > 0);
@ -568,14 +889,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
SASSERT(m().get_sort(ch) == m().get_sort(a));
lhs.push_back(ch);
rhs.push_back(a);
m_lhs.pop_back();
ls.pop_back();
if (s.length() == 1) {
m_rhs.pop_back();
rs.pop_back();
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
m_rhs[m_rhs.size()-1] = s2;
trail.push_back(s2);
rs[rs.size()-1] = s2;
}
}
else {
@ -587,22 +907,22 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
// solve from front
unsigned head1 = 0, head2 = 0;
while (true) {
while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) {
while (head1 < ls.size() && m_util.str.is_empty(ls[head1].get())) {
++head1;
}
while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) {
while (head2 < rs.size() && m_util.str.is_empty(rs[head2].get())) {
++head2;
}
if (head1 == m_lhs.size() || head2 == m_rhs.size()) {
if (head1 == ls.size() || head2 == rs.size()) {
break;
}
SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
SASSERT(head1 < ls.size() && head2 < rs.size());
expr* l = m_lhs[head1];
expr* r = m_rhs[head2];
expr* l = ls[head1].get();
expr* r = rs[head2].get();
if (m_util.str.is_unit(r) && m_util.str.is_string(l)) {
std::swap(l, r);
std::swap(m_lhs, m_rhs);
ls.swap(rs);
}
if (l == r) {
++head1;
@ -624,14 +944,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
SASSERT(m().get_sort(ch) == m().get_sort(a));
lhs.push_back(ch);
rhs.push_back(a);
m_lhs.pop_back();
ls.pop_back();
if (s.length() == 1) {
m_rhs.pop_back();
rs.pop_back();
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
m_rhs[m_rhs.size()-1] = s2;
trail.push_back(s2);
rs[rs.size()-1] = s2;
}
}
else {
@ -641,10 +960,10 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
}
// reduce strings
zstring s1, s2;
while (head1 < m_lhs.size() &&
head2 < m_rhs.size() &&
m_util.str.is_string(m_lhs[head1], s1) &&
m_util.str.is_string(m_rhs[head2], s2)) {
while (head1 < ls.size() &&
head2 < rs.size() &&
m_util.str.is_string(ls[head1].get(), s1) &&
m_util.str.is_string(rs[head2].get(), s2)) {
unsigned l = std::min(s1.length(), s2.length());
for (unsigned i = 0; i < l; ++i) {
if (s1[i] != s2[i]) {
@ -655,68 +974,88 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
++head1;
}
else {
m_lhs[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
trail.push_back(m_lhs[head1]);
ls[head1] = m_util.str.mk_string(s1.extract(l, s1.length()-l));
}
if (l == s2.length()) {
++head2;
}
else {
m_rhs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
trail.push_back(m_rhs[head2]);
rs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l));
}
change = true;
}
while (head1 < m_lhs.size() &&
head2 < m_rhs.size() &&
m_util.str.is_string(m_lhs.back(), s1) &&
m_util.str.is_string(m_rhs.back(), s2)) {
while (head1 < ls.size() &&
head2 < rs.size() &&
m_util.str.is_string(ls.back(), s1) &&
m_util.str.is_string(rs.back(), s2)) {
unsigned l = std::min(s1.length(), s2.length());
for (unsigned i = 0; i < l; ++i) {
if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) {
return false;
}
}
m_lhs.pop_back();
m_rhs.pop_back();
ls.pop_back();
rs.pop_back();
if (l < s1.length()) {
m_lhs.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
trail.push_back(m_lhs.back());
ls.push_back(m_util.str.mk_string(s1.extract(0, s1.length()-l)));
}
if (l < s2.length()) {
m_rhs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
trail.push_back(m_rhs.back());
}
rs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l)));
}
change = true;
}
bool is_sat;
unsigned szl = m_lhs.size() - head1, szr = m_rhs.size() - head2;
expr* const* ls = m_lhs.c_ptr() + head1, * const*rs = m_rhs.c_ptr() + head2;
if (length_constrained(szl, ls, szr, rs, lhs, rhs, is_sat)) {
unsigned szl = ls.size() - head1, szr = rs.size() - head2;
expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset();
return is_sat;
}
if (is_subsequence(szl, ls, szr, rs, lhs, rhs, is_sat)) {
if (is_subsequence(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset();
return is_sat;
}
if (szl == 0 && szr == 0) {
return true;
}
if (szl == 0 && szr == 0) {
ls.reset(); rs.reset();
return true;
}
else if (!change) {
lhs.push_back(l);
rhs.push_back(r);
// skip
SASSERT(lhs.empty());
}
else {
// could solve if either side is fixed size.
SASSERT(szl > 0 && szr > 0);
lhs.push_back(m_util.str.mk_concat(szl, ls));
rhs.push_back(m_util.str.mk_concat(szr, rs));
lhs.push_back(m_util.str.mk_concat(szl, ls.c_ptr() + head1));
rhs.push_back(m_util.str.mk_concat(szr, rs.c_ptr() + head2));
ls.reset();
rs.reset();
}
SASSERT(lhs.empty() || ls.empty());
return true;
}
bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) {
m_lhs.reset();
m_rhs.reset();
m_util.str.get_concat(l, m_lhs);
m_util.str.get_concat(r, m_rhs);
if (reduce_eq(m_lhs, m_rhs, lhs, rhs)) {
SASSERT(lhs.size() == rhs.size());
if (lhs.empty()) {
lhs.push_back(l);
rhs.push_back(r);
}
return true;
}
else {
TRACE("seq", tout << mk_pp(l, m()) << " != " << mk_pp(r, m()) << "\n";);
return false;
}
}
expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
SASSERT(n > 0);
ptr_vector<expr> bs;
@ -812,6 +1151,11 @@ bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr
return false;
}
bool seq_rewriter::is_epsilon(expr* e) const {
expr* e1;
return m_util.re.is_to_re(e, e1) && m_util.str.is_empty(e1);
}
bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
is_sat = true;

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

@ -24,15 +24,27 @@ Notes:
#include"rewriter_types.h"
#include"params.h"
#include"lbool.h"
#include"automaton.h"
typedef automaton<expr, ast_manager> eautomaton;
class re2automaton {
ast_manager& m;
seq_util u;
eautomaton* re2aut(expr* e);
eautomaton* seq2aut(expr* e);
public:
re2automaton(ast_manager& m);
eautomaton* operator()(expr* e);
};
/**
\brief Cheap rewrite rules for seq constraints
*/
class seq_rewriter {
seq_util m_util;
arith_util m_autil;
ptr_vector<expr> m_es, m_lhs, m_rhs;
expr_ref_vector m_es, m_lhs, m_rhs;
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);
@ -61,9 +73,13 @@ class seq_rewriter {
bool min_length(unsigned n, expr* const* es, unsigned& len);
expr* concat_non_empty(unsigned n, expr* const* es);
void add_next(u_map<expr*>& next, unsigned idx, expr* cond);
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_epsilon(expr* e) const;
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m) {
m_util(m), m_autil(m), m_es(m), m_lhs(m), m_rhs(m) {
}
ast_manager & m() const { return m_util.get_manager(); }
family_id get_fid() const { return m_util.get_family_id(); }
@ -76,6 +92,8 @@ public:
bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs);
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
};
#endif

65
src/ast/seq_decl_plugin.cpp
View file

@ -25,7 +25,6 @@ Revision History:
zstring::zstring(encoding enc): m_encoding(enc) {}
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
// TBD: epply decoding
while (*s) {
m_buffer.push_back(*s);
++s;
@ -42,7 +41,7 @@ zstring::zstring(unsigned num_bits, bool const* ch) {
m_encoding = (num_bits == 8)?ascii:unicode;
unsigned n = 0;
for (unsigned i = 0; i < num_bits; ++i) {
n |= (((unsigned)ch[i]) << num_bits);
n |= (((unsigned)ch[i]) << i);
}
m_buffer.push_back(n);
}
@ -81,12 +80,23 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
return result;
}
static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
"^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
std::string zstring::encode() const {
// TBD apply encodings.
SASSERT(m_encoding == ascii);
std::ostringstream strm;
for (unsigned i = 0; i < m_buffer.size(); ++i) {
strm << (char)(m_buffer[i]);
unsigned char ch = m_buffer[i];
if (0 <= ch && ch < 32) {
strm << esc_table[ch];
}
else if (ch == 127) {
strm << "^?";
}
else {
strm << (char)(ch);
}
}
return strm.str();
}
@ -163,6 +173,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const {
seq_decl_plugin::seq_decl_plugin(): m_init(false),
m_stringc_sym("String"),
m_charc_sym("Char"),
m_string(0),
m_char(0) {}
@ -211,9 +222,9 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
}
/*
\brief match left associative operator.
\brief match right associative operator.
*/
void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
ptr_vector<sort> binding;
ast_manager& m = *m_manager;
TRACE("seq_verbose",
@ -369,7 +380,8 @@ void seq_decl_plugin::init() {
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
decl_plugin::set_manager(m, id);
m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0));
bv_util bv(*m);
m_char = bv.mk_sort(8);
m->inc_ref(m_char);
parameter param(m_char);
m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
@ -391,18 +403,18 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
return m_string;
}
return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters));
case RE_SORT:
case RE_SORT: {
if (num_parameters != 1) {
m.raise_exception("Invalid regex sort, expecting one parameter");
}
if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
m.raise_exception("invalid regex sort, parameter is not a sort");
}
sort * s = to_sort(parameters[0].get_ast());
return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
}
case _STRING_SORT:
return m_string;
case _CHAR_SORT:
return m_char;
default:
UNREACHABLE();
return 0;
@ -430,9 +442,9 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
if (arity == 0) {
m.raise_exception("Invalid function application. At least one argument expected");
}
match_left_assoc(*m_sigs[k], arity, domain, range, rng);
match_right_assoc(*m_sigs[k], arity, domain, range, rng);
func_decl_info info(m_family_id, k_seq);
info.set_left_associative();
info.set_right_associative();
return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
}
@ -470,6 +482,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_STRING_CONST:
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
m.raise_exception("invalid string declaration");
@ -583,7 +597,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
app* seq_decl_plugin::mk_string(symbol const& s) {
parameter param(s);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}
@ -591,12 +605,16 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
symbol sym(s.encode().c_str());
parameter param(sym);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}
bool seq_decl_plugin::is_value(app* e) const {
return is_app_of(e, m_family_id, OP_STRING_CONST);
return
is_app_of(e, m_family_id, OP_SEQ_EMPTY) ||
(is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
m_manager->is_value(e->get_arg(0)));
}
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
@ -609,11 +627,26 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); }
app* seq_util::str::mk_char(zstring const& s, unsigned idx) {
bv_util bvu(m);
return bvu.mk_numeral(s[idx], s.num_bits());
}
app* seq_util::str::mk_char(char ch) {
zstring s(ch, zstring::ascii);
return mk_char(s, 0);
}
bool seq_util::str::is_char(expr* n, zstring& c) const {
if (u.is_char(n)) {
c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
return true;
}
else {
return false;
}
}
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {
@ -626,7 +659,7 @@ bool seq_util::str::is_string(expr const* n, zstring& s) const {
}
void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
expr* e1, *e2;
while (is_concat(e, e1, e2)) {
get_concat(e1, es);

23
src/ast/seq_decl_plugin.h
View file

@ -22,13 +22,13 @@ Revision History:
#define SEQ_DECL_PLUGIN_H_
#include "ast.h"
#include "bv_decl_plugin.h"
enum seq_sort_kind {
SEQ_SORT,
RE_SORT,
_STRING_SORT, // internal only
_CHAR_SORT // internal only
_STRING_SORT // internal only
};
enum seq_op_kind {
@ -131,12 +131,13 @@ class seq_decl_plugin : public decl_plugin {
ptr_vector<psig> m_sigs;
bool m_init;
symbol m_stringc_sym;
symbol m_charc_sym;
sort* m_string;
sort* m_char;
void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
void match_left_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
void match_right_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
bool match(ptr_vector<sort>& binding, sort* s, sort* sP);
@ -187,6 +188,7 @@ public:
ast_manager& get_manager() const { return m; }
bool is_char(sort* s) const { return seq.is_char(s); }
bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
@ -195,6 +197,7 @@ public:
bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@ -212,13 +215,13 @@ 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, &param); }
sort* mk_string_sort() { return m.mk_sort(m_fid, _STRING_SORT, 0, 0); }
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
app* mk_string(zstring const& s);
app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
app* mk_char(char ch);
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
app* mk_concat(expr* a, expr* b, expr* c) {
return mk_concat(mk_concat(a, b), c);
}
app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(a, mk_concat(b, c)); }
expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
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); }
@ -229,8 +232,6 @@ public:
app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
app* mk_char(zstring const& s, unsigned idx);
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
bool is_string(expr const* n, symbol& s) const {
@ -238,6 +239,7 @@ public:
}
bool is_string(expr const* n, zstring& s) const;
bool is_char(expr* n, zstring& s) const;
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
@ -271,8 +273,9 @@ public:
MATCH_BINARY(is_in_re);
MATCH_UNARY(is_unit);
void get_concat(expr* e, ptr_vector<expr>& es) const;
void get_concat(expr* e, expr_ref_vector& es) const;
expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }
expr* get_rightmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e2; return e; }
};
class re {
@ -281,6 +284,8 @@ public:
public:
re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
sort* mk_re(sort* seq) { parameter param(seq); return m.mk_sort(m_fid, RE_SORT, 1, &param); }
app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); }
app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }

4
src/interp/iz3translate.cpp
View file

@ -2023,8 +2023,8 @@ public:
break;
}
default:
pfgoto(proof);
SASSERT(0 && "translate_main: unsupported proof rule");
// pfgoto(proof);
// SASSERT(0 && "translate_main: unsupported proof rule");
throw unsupported();
}
}

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

@ -0,0 +1,23 @@
/*++
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 "automaton.h"
template class automaton<unsigned>;

608
src/math/automata/automaton.h Normal file
View file

@ -0,0 +1,608 @@
/*++
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:
--*/
#ifndef AUTOMATON_H_
#define AUTOMATON_H_
#include "util.h"
#include "vector.h"
#include "uint_set.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 = 0): 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& 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 == 0; }
};
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;
for (unsigned i = 0; i < final.size(); ++i) {
add_to_final_states(final[i]);
}
for (unsigned i = 0; i < mvs.size(); ++i) {
move const& mv = mvs[i];
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 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);
}
// 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;
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));
}
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;
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 i = 0; i < a.m_final_states.size(); ++i) {
mvs.push_back(move(m, init, a.m_final_states[i]));
}
}
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);
}
}
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
//
void compress() {
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 (unsigned k = 0; k < mvs.size(); ++k) {
mvs1.push_back(move(m, src, mvs[k].dst(), mvs[k].t()));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(dst, mvs1[k].dst(), mvs1[k].t());
add(mvs1[k]);
}
}
//
// 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 (unsigned k = 0; k < mvs.size(); ++k) {
SASSERT(mvs[k].is_epsilon());
mvs1.push_back(move(m, mvs[k].src(), dst1, t));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(mvs1[k].src(), dst, 0);
add(mvs1[k]);
}
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 (unsigned k = 0; k < mvs.size(); ++k) {
mvs1.push_back(move(m, mvs[k].src(), dst, mvs[k].t()));
}
for (unsigned k = 0; k < mvs1.size(); ++k) {
remove(mvs1[k].src(), src, mvs1[k].t());
add(mvs1[k]);
}
}
else {
continue;
}
remove(src, dst, 0);
--j;
}
}
}
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;
}
}
}
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 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_epsilon_free() const {
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (unsigned j = 0; j < mvs.size(); ++j) {
if (!mvs[j].t()) return false;
}
}
return true;
}
bool all_epsilon_in(unsigned s) {
moves const& mvs = m_delta_inv[s];
for (unsigned j = 0; j < mvs.size(); ++j) {
if (mvs[j].t()) return false;
}
return true;
}
bool is_empty() const { return m_final_states.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 (unsigned i = 0; i < mvs.size(); ++i) {
if (s == mvs[i].dst()) return true;
}
return false;
}
unsigned move_count() const {
unsigned result = 0;
for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {}
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_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
get_moves(state, m_delta_inv, mvs, epsilon_closure);
}
template<class D = default_display>
std::ostream& display(std::ostream& out, D& displayer = D()) const {
out << "init: " << init() << "\n";
out << "final: ";
for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " ";
out << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (unsigned j = 0; j < mvs.size(); ++j) {
move const& mv = mvs[j];
out << i << " -> " << mv.dst() << " ";
if (mv.t()) {
out << "if ";
displayer.display(out, mv.t());
}
out << "\n";
}
}
return out;
}
private:
void remove_dead_states() {
unsigned_vector remap;
for (unsigned i = 0; i < m_delta.size(); ++i) {
}
}
void add(move const& mv) {
m_delta[mv.src()].push_back(mv);
m_delta_inv[mv.dst()].push_back(mv);
}
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 i = 0; i < a.m_final_states.size(); ++i) {
final.push_back(a.m_final_states[i]+offset);
}
}
};
typedef automaton<unsigned> uautomaton;
#endif

16
src/parsers/smt2/smt2scanner.cpp
View file

@ -169,24 +169,16 @@ namespace smt2 {
char c = curr();
if (c == EOF)
throw scanner_exception("unexpected end of string", m_line, m_spos);
if (c == '\"') {
if (c == '\n') {
new_line();
}
else if (c == '\"') {
next();
if (curr() != '\"') {
m_string.push_back(0);
return STRING_TOKEN;
}
}
else if (c == '\n') {
new_line();
}
else if (c == '\\') {
next();
c = curr();
if (c == EOF)
throw scanner_exception("unexpected end of string", m_line, m_spos);
if (c != '\\' && c != '\"')
throw scanner_exception("invalid escape sequence", m_line, m_spos);
}
m_string.push_back(c);
next();
}

3
src/smt/smt_context.cpp
View file

@ -1382,7 +1382,8 @@ namespace smt {
bool_var v = l.var();
bool_var_data & d = get_bdata(v);
lbool val = get_assignment(v);
TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " " << l << "\n";);
TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode()
<< " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";);
SASSERT(val != l_undef);
if (d.is_enode())
propagate_bool_var_enode(v);

5
src/smt/smt_model_generator.cpp
View file

@ -90,7 +90,9 @@ namespace smt {
sort * s = m_manager.get_sort(r->get_owner());
model_value_proc * proc = 0;
if (m_manager.is_bool(s)) {
SASSERT(m_context->get_assignment(r) == l_true || m_context->get_assignment(r) == l_false);
CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef,
tout << mk_pp(r->get_owner(), m_manager) << "\n";);
SASSERT(m_context->get_assignment(r) != l_undef);
if (m_context->get_assignment(r) == l_true)
proc = alloc(expr_wrapper_proc, m_manager.mk_true());
else
@ -359,6 +361,7 @@ namespace smt {
}
else {
enode * child = d.get_enode();
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
child = child->get_root();
app * val = 0;
m_root2value.find(child, val);

2
src/smt/smt_setup.cpp
View file

@ -815,7 +815,7 @@ namespace smt {
}
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
m_context.register_plugin(alloc(theory_seq, m_manager));
}
void setup::setup_card() {

6
src/smt/theory_arith.h
View file

@ -1056,6 +1056,10 @@ namespace smt {
// -----------------------------------
virtual bool get_value(enode * n, expr_ref & r);
bool get_lower(enode* n, expr_ref& r);
bool get_upper(enode* n, expr_ref& r);
bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);
// -----------------------------------
//
@ -1071,6 +1075,8 @@ namespace smt {
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params, parameter* params);
inf_eps_rational<inf_rational> conflict_minimize();
private:
virtual expr_ref mk_gt(theory_var v);

1
src/smt/theory_arith_aux.h
View file

@ -2157,6 +2157,7 @@ namespace smt {
enode * r = n->get_root();
enode_vector::const_iterator it = r->begin_parents();
enode_vector::const_iterator end = r->end_parents();
TRACE("shared", tout << get_context().get_scope_level() << " " << v << " " << r->get_num_parents() << "\n";);
for (; it != end; ++it) {
enode * parent = *it;
app * o = parent->get_owner();

37
src/smt/theory_arith_core.h
View file

@ -3089,20 +3089,35 @@ namespace smt {
// -----------------------------------
template<typename Ext>
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
if (v == null_theory_var) {
// TODO: generate fresh value different from other get_value(v) for all v.
return false;
bool theory_arith<Ext>::to_expr(inf_numeral const& val, bool is_int, expr_ref & r) {
if (val.get_infinitesimal().is_zero()) {
numeral _val = val.get_rational();
r = m_util.mk_numeral(_val.to_rational(), is_int);
return true;
}
inf_numeral const & val = get_value(v);
if (!val.get_infinitesimal().is_zero()) {
// TODO: add support for infinitesimals
else {
return false;
}
numeral _val = val.get_rational();
r = m_util.mk_numeral(_val.to_rational(), is_int(v));
return true;
}
template<typename Ext>
bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
}
template<typename Ext>
bool theory_arith<Ext>::get_lower(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? 0 : lower(v);
return b && to_expr(b->get_value(), is_int(v), r);
}
template<typename Ext>
bool theory_arith<Ext>::get_upper(enode * n, expr_ref & r) {
theory_var v = n->get_th_var(get_id());
bound* b = (v == null_theory_var) ? 0 : upper(v);
return b && to_expr(b->get_value(), is_int(v), r);
}
// -----------------------------------

45
src/smt/theory_bv.cpp
View file

@ -424,6 +424,39 @@ namespace smt {
};
void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
++m_stats.m_num_eq_dynamic;
if (v1 > v2) {
std::swap(v1, v2);
}
unsigned sz = get_bv_size(v1);
ast_manager& m = get_manager();
context & ctx = get_context();
app* o1 = get_enode(v1)->get_owner();
app* o2 = get_enode(v2)->get_owner();
literal oeq = mk_eq(o1, o2, true);
TRACE("bv",
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
<< ctx.get_scope_level() << "\n";);
literal_vector eqs;
for (unsigned i = 0; i < sz; ++i) {
literal l1 = m_bits[v1][i];
literal l2 = m_bits[v2][i];
expr_ref e1(m), e2(m);
e1 = mk_bit2bool(o1, i);
e2 = mk_bit2bool(o2, i);
literal eq = mk_eq(e1, e2, true);
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
ctx.mk_th_axiom(get_id(), l1, l2, eq);
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
ctx.mk_th_axiom(get_id(), eq, ~oeq);
eqs.push_back(~eq);
}
eqs.push_back(oeq);
ctx.mk_th_axiom(get_id(), eqs.size(), eqs.c_ptr());
}
void theory_bv::fixed_var_eh(theory_var v) {
numeral val;
bool r = get_fixed_value(v, val);
@ -443,7 +476,9 @@ namespace smt {
display_var(tout, v);
display_var(tout, v2););
m_stats.m_num_th2core_eq++;
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
add_fixed_eq(v, v2);
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
m_fixed_var_table.insert(key, v2);
}
}
else {
@ -1177,6 +1212,7 @@ namespace smt {
}
void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
m_stats.m_num_bit2core++;
context & ctx = get_context();
SASSERT(ctx.get_assignment(antecedent) == l_true);
@ -1192,6 +1228,12 @@ namespace smt {
}
else {
ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
literal_vector lits;
lits.push_back(~consequent);
lits.push_back(antecedent);
lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (m_wpos[v2] == idx)
find_wpos(v2);
// REMARK: bit_eq_justification is marked as a theory_bv justification.
@ -1601,6 +1643,7 @@ namespace smt {
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
st.update("bv bit2core", m_stats.m_num_bit2core);
st.update("bv->core eq", m_stats.m_num_th2core_eq);
st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
}
#ifdef Z3DEBUG

5
src/smt/theory_bv.h
View file

@ -34,6 +34,7 @@ namespace smt {
struct theory_bv_stats {
unsigned m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
unsigned m_num_eq_dynamic;
void reset() { memset(this, 0, sizeof(theory_bv_stats)); }
theory_bv_stats() { reset(); }
};
@ -124,8 +125,9 @@ namespace smt {
typedef std::pair<numeral, unsigned> value_sort_pair;
typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
value2var m_fixed_var_table;
value2var m_fixed_var_table;
literal_vector m_tmp_literals;
svector<var_pos> m_prop_queue;
bool m_approximates_large_bvs;
@ -166,6 +168,7 @@ namespace smt {
void find_wpos(theory_var v);
friend class fixed_eq_justification;
void fixed_var_eh(theory_var v);
void add_fixed_eq(theory_var v1, theory_var v2);
bool get_fixed_value(theory_var v, numeral & result) const;
void internalize_num(app * n);
void internalize_add(app * n);

2406
src/smt/theory_seq.cpp
View file

File diff suppressed because it is too large Load diff

405
src/smt/theory_seq.h
View file

@ -25,15 +25,24 @@ Revision History:
#include "th_rewriter.h"
#include "ast_trail.h"
#include "scoped_vector.h"
#include "scoped_ptr_vector.h"
#include "automaton.h"
#include "seq_rewriter.h"
namespace smt {
class theory_seq : public theory {
typedef scoped_dependency_manager<enode_pair> enode_pair_dependency_manager;
typedef enode_pair_dependency_manager::dependency enode_pair_dependency;
struct assumption {
enode* n1, *n2;
literal lit;
assumption(enode* n1, enode* n2): n1(n1), n2(n2), lit(null_literal) {}
assumption(literal lit): n1(0), n2(0), lit(lit) {}
};
typedef scoped_dependency_manager<assumption> dependency_manager;
typedef dependency_manager::dependency dependency;
typedef trail_stack<theory_seq> th_trail_stack;
typedef std::pair<expr*, enode_pair_dependency*> expr_dep;
typedef std::pair<expr*, dependency*> expr_dep;
typedef obj_map<expr, expr_dep> eqdep_map_t;
// cache to track evaluations under equalities
@ -52,27 +61,30 @@ namespace smt {
class solution_map {
enum map_update { INS, DEL };
ast_manager& m;
enode_pair_dependency_manager& m_dm;
dependency_manager& m_dm;
eqdep_map_t m_map;
eval_cache m_cache;
expr_ref_vector m_lhs, m_rhs;
ptr_vector<enode_pair_dependency> m_deps;
ptr_vector<dependency> m_deps;
svector<map_update> m_updates;
unsigned_vector m_limit;
void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
void add_trail(map_update op, expr* l, expr* r, dependency* d);
public:
solution_map(ast_manager& m, enode_pair_dependency_manager& dm):
solution_map(ast_manager& m, dependency_manager& dm):
m(m), m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {}
bool empty() const { return m_map.empty(); }
void update(expr* e, expr* r, enode_pair_dependency* d);
bool empty() const { return m_map.empty(); }
void update(expr* e, expr* r, dependency* d);
void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
expr* find(expr* e, enode_pair_dependency*& d);
void cache(expr* e, expr* r, enode_pair_dependency* d);
void push_scope() { m_limit.push_back(m_updates.size()); }
void pop_scope(unsigned num_scopes);
void display(std::ostream& out) const;
expr* find(expr* e, dependency*& d);
expr* find(expr* e);
bool is_root(expr* e) const;
void cache(expr* e, expr* r, dependency* d);
void reset_cache() { m_cache.reset(); }
void push_scope() { m_limit.push_back(m_updates.size()); }
void pop_scope(unsigned num_scopes);
void display(std::ostream& out) const;
};
// Table of current disequalities
@ -97,52 +109,235 @@ namespace smt {
struct eq {
expr_ref m_lhs;
expr_ref m_rhs;
enode_pair_dependency* m_dep;
eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d):
dependency* m_dep;
eq(expr_ref& l, expr_ref& r, dependency* d):
m_lhs(l), m_rhs(r), m_dep(d) {}
eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; }
};
// asserted or derived disqequality with dependencies
struct ne {
bool m_solved;
expr_ref m_l, m_r;
expr_ref_vector m_lhs;
expr_ref_vector m_rhs;
literal_vector m_lits;
dependency* m_dep;
ne(expr_ref& l, expr_ref& r):
m_solved(false), m_l(l), m_r(r), m_lhs(l.get_manager()), m_rhs(r.get_manager()), m_dep(0) {
m_lhs.push_back(l);
m_rhs.push_back(r);
}
ne(ne const& other):
m_solved(other.m_solved), m_l(other.m_l), m_r(other.m_r), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
ne& operator=(ne const& other) {
m_solved = other.m_solved;
m_l = other.m_l;
m_r = other.m_r;
m_lhs.reset(); m_lhs.append(other.m_lhs);
m_rhs.reset(); m_rhs.append(other.m_rhs);
m_lits.reset(); m_lits.append(other.m_lits);
m_dep = other.m_dep;
return *this;
}
bool is_solved() const { return m_solved; }
};
class pop_lit : public trail<theory_seq> {
unsigned m_idx;
literal m_lit;
public:
pop_lit(theory_seq& th, unsigned idx): m_idx(idx), m_lit(th.m_nqs[idx].m_lits.back()) {
th.m_nqs.ref(m_idx).m_lits.pop_back();
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.push_back(m_lit); }
};
class push_lit : public trail<theory_seq> {
unsigned m_idx;
public:
push_lit(theory_seq& th, unsigned idx, literal lit): m_idx(idx) {
th.m_nqs.ref(m_idx).m_lits.push_back(lit);
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits.pop_back(); }
};
class set_lit : public trail<theory_seq> {
unsigned m_idx;
unsigned m_i;
literal m_lit;
public:
set_lit(theory_seq& th, unsigned idx, unsigned i, literal lit):
m_idx(idx), m_i(i), m_lit(th.m_nqs[idx].m_lits[i]) {
th.m_nqs.ref(m_idx).m_lits[i] = lit;
}
virtual void undo(theory_seq & th) { th.m_nqs.ref(m_idx).m_lits[m_i] = m_lit; }
};
class solved_ne : public trail<theory_seq> {
unsigned m_idx;
public:
solved_ne(theory_seq& th, unsigned idx) : m_idx(idx) { th.m_nqs.ref(idx).m_solved = true; }
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_solved = false; }
};
void mark_solved(unsigned idx);
class push_ne : public trail<theory_seq> {
unsigned m_idx;
public:
push_ne(theory_seq& th, unsigned idx, expr* l, expr* r) : m_idx(idx) {
th.m_nqs.ref(m_idx).m_lhs.push_back(l);
th.m_nqs.ref(m_idx).m_rhs.push_back(r);
}
virtual void undo(theory_seq& th) { th.m_nqs.ref(m_idx).m_lhs.pop_back(); th.m_nqs.ref(m_idx).m_rhs.pop_back(); }
};
class pop_ne : public trail<theory_seq> {
expr_ref m_lhs;
expr_ref m_rhs;
unsigned m_idx;
public:
pop_ne(theory_seq& th, unsigned idx):
m_lhs(th.m_nqs[idx].m_lhs.back(), th.m),
m_rhs(th.m_nqs[idx].m_rhs.back(), th.m),
m_idx(idx) {
th.m_nqs.ref(idx).m_lhs.pop_back();
th.m_nqs.ref(idx).m_rhs.pop_back();
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_lhs.push_back(m_lhs);
th.m_nqs.ref(m_idx).m_rhs.push_back(m_rhs);
m_lhs.reset();
m_rhs.reset();
}
};
class set_ne : public trail<theory_seq> {
expr_ref m_lhs;
expr_ref m_rhs;
unsigned m_idx;
unsigned m_i;
public:
set_ne(theory_seq& th, unsigned idx, unsigned i, expr* l, expr* r):
m_lhs(th.m_nqs[idx].m_lhs[i], th.m),
m_rhs(th.m_nqs[idx].m_rhs[i], th.m),
m_idx(idx),
m_i(i) {
th.m_nqs.ref(idx).m_lhs[i] = l;
th.m_nqs.ref(idx).m_rhs[i] = r;
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_lhs[m_i] = m_lhs;
th.m_nqs.ref(m_idx).m_rhs[m_i] = m_rhs;
m_lhs.reset();
m_rhs.reset();
}
};
class push_dep : public trail<theory_seq> {
dependency* m_dep;
unsigned m_idx;
public:
push_dep(theory_seq& th, unsigned idx, dependency* d): m_dep(th.m_nqs[idx].m_dep), m_idx(idx) {
th.m_nqs.ref(idx).m_dep = d;
}
virtual void undo(theory_seq& th) {
th.m_nqs.ref(m_idx).m_dep = m_dep;
}
};
class apply {
public:
virtual ~apply() {}
virtual void operator()(theory_seq& th) = 0;
};
class replay_length_coherence : public apply {
expr_ref m_e;
public:
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
virtual void operator()(theory_seq& th) {
th.check_length_coherence(m_e);
}
};
class replay_axiom : public apply {
expr_ref m_e;
public:
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
virtual void operator()(theory_seq& th) {
th.enque_axiom(m_e);
}
};
class push_replay : public trail<theory_seq> {
apply* m_apply;
public:
push_replay(apply* app): m_apply(app) {}
virtual void undo(theory_seq& th) {
th.m_replay.push_back(m_apply);
}
};
void erase_index(unsigned idx, unsigned i);
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(stats)); }
unsigned m_num_splits;
unsigned m_num_reductions;
unsigned m_propagate_automata;
unsigned m_check_length_coherence;
unsigned m_branch_variable;
unsigned m_solve_nqs;
unsigned m_solve_eqs;
unsigned m_add_axiom;
};
ast_manager& m;
enode_pair_dependency_manager m_dm;
solution_map m_rep; // unification representative.
scoped_vector<eq> m_eqs; // set of current equations.
ast_manager& m;
dependency_manager m_dm;
solution_map m_rep; // unification representative.
scoped_vector<eq> m_eqs; // set of current equations.
scoped_vector<ne> m_nqs; // set of current disequalities.
seq_factory* m_factory; // value factory
expr_ref_vector m_ineqs; // inequalities to check solution against
exclusion_table m_exclude; // set of asserted disequalities.
expr_ref_vector m_axioms; // list of axioms to add.
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
bool m_has_length; // is length applied
bool m_model_completion; // during model construction, invent values in canonizer
th_rewriter m_rewrite;
seq_util m_util;
arith_util m_autil;
th_trail_stack m_trail_stack;
stats m_stats;
symbol m_prefix_sym;
symbol m_suffix_sym;
symbol m_contains_left_sym;
symbol m_contains_right_sym;
symbol m_left_sym; // split variable left part
symbol m_right_sym; // split variable right part
seq_factory* m_factory; // value factory
exclusion_table m_exclude; // set of asserted disequalities.
expr_ref_vector m_axioms; // list of axioms to add.
obj_hashtable<expr> m_axiom_set;
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
obj_hashtable<expr> m_length; // is length applied
scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg;
th_rewriter m_rewrite;
seq_util m_util;
arith_util m_autil;
th_trail_stack m_trail_stack;
stats m_stats;
symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
symbol m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_extract_prefix, m_at_left, m_at_right;
ptr_vector<expr> m_todo;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
// maintain automata with regular expressions.
scoped_ptr_vector<eautomaton> m_automata;
obj_map<expr, eautomaton*> m_re2aut;
// queue of asserted atoms
ptr_vector<expr> m_atoms;
unsigned_vector m_atoms_lim;
unsigned m_atoms_qhead;
bool m_new_solution; // new solution added
bool m_new_propagation; // new propagation to core
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app*, bool);
virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
virtual bool internalize_term(app*);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void internalize_eq_eh(app * atom, bool_var v) {}
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 void assign_eh(bool_var v, bool is_true);
virtual bool can_propagate();
virtual void propagate();
virtual void push_scope_eh();
@ -159,40 +354,56 @@ namespace smt {
virtual void init_model(model_generator & mg);
// final check
bool check_ineqs(); // check if inequalities are violated.
bool simplify_and_solve_eqs(); // solve unitary equalities
bool branch_variable(); // branch on a variable
bool split_variable(); // split a variable
bool is_solved();
bool check_length_coherence();
bool check_length_coherence_tbd();
bool check_ineq_coherence();
bool check_length_coherence();
bool check_length_coherence(expr* e);
bool propagate_length_coherence(expr* e);
bool pre_process_eqs(bool simplify_or_solve);
bool simplify_eqs();
bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
bool solve_basic_eqs();
bool solve_eqs(unsigned start);
bool solve_eq(expr* l, expr* r, dependency* dep);
bool simplify_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool is_binary_eq(expr* l, expr* r, expr*& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr*& y);
bool solve_binary_eq(expr* l, expr* r, dependency* dep);
bool propagate_max_length(expr* l, expr* r, dependency* dep);
bool solve_nqs(unsigned i);
void solve_ne(unsigned i);
bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; }
bool unchanged(expr* e, expr_ref_vector& es, expr* f, expr_ref_vector& fs) const {
return
(unchanged(e, es) && unchanged(f, fs)) ||
(unchanged(e, fs) && unchanged(e, fs));
}
// asserting consequences
void propagate_lit(enode_pair_dependency* dep, literal lit);
void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
void propagate_eq(bool_var v, expr* e1, expr* e2);
void set_conflict(enode_pair_dependency* dep);
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
void propagate_eq(dependency* dep, enode* n1, enode* n2);
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
bool assume_equality(expr* l, expr* r);
bool find_branch_candidate(dependency* dep, expr* l, expr_ref_vector const& rs);
lbool assume_equality(expr* l, expr* r);
// variable solving utilities
bool occurs(expr* a, expr* b);
bool is_var(expr* b);
void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
bool is_left_select(expr* a, expr*& b);
bool is_right_select(expr* a, expr*& b);
expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
expr_ref expand(expr* e, enode_pair_dependency*& eqs);
void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
bool add_solution(expr* l, expr* r, dependency* dep);
bool is_nth(expr* a) const;
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref canonize(expr* e, dependency*& eqs);
void canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
expr_ref expand(expr* e, dependency*& eqs);
void add_dependency(dependency*& dep, enode* a, enode* b);
void get_concat(expr* e, ptr_vector<expr>& concats);
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
@ -202,28 +413,80 @@ namespace smt {
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
void add_length_axiom(expr* n);
void add_length_unit_axiom(expr* n);
void add_length_empty_axiom(expr* n);
void add_length_concat_axiom(expr* n);
void add_length_string_axiom(expr* n);
bool has_length(expr *e) const { return m_length.contains(e); }
void add_length(expr* e);
void enforce_length(enode* n);
void enforce_length_coherence(enode* n1, enode* n2);
void add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n);
literal mk_equals(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr* mk_sub(expr* a, expr* b);
expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
// arithmetic integration
bool lower_bound(expr* s, rational& lo);
bool upper_bound(expr* s, rational& hi);
bool get_length(expr* s, rational& val);
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
bool is_skolem(symbol const& s, expr* e) const;
void set_incomplete(app* term);
// automata utilities
void propagate_in_re(expr* n, bool is_true);
eautomaton* get_automaton(expr* e);
literal mk_accept(expr* s, expr* idx, expr* re, expr* state);
literal mk_accept(expr* s, expr* idx, expr* re, unsigned i) { return mk_accept(s, idx, re, m_autil.mk_int(i)); }
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }
bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
return is_acc_rej(m_accept, acc, s, idx, re, i, aut);
}
literal mk_reject(expr* s, expr* idx, expr* re, expr* state);
literal mk_reject(expr* s, expr* idx, expr* re, unsigned i) { return mk_reject(s, idx, re, m_autil.mk_int(i)); }
bool is_reject(expr* rej) const { return is_skolem(m_reject, rej); }
bool is_reject(expr* rej, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
}
bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);
bool add_reject2reject(expr* rej);
bool add_accept2step(expr* acc);
bool add_step2accept(expr* step);
bool add_prefix2prefix(expr* e);
bool add_suffix2suffix(expr* e);
bool add_contains2contains(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);
void propagate_non_empty(literal lit, expr* s);
void propagate_is_conc(expr* e, expr* conc);
void propagate_acc_rej_length(literal lit, expr* acc_rej);
bool propagate_automata();
void add_atom(expr* e);
void new_eq_eh(dependency* dep, enode* n1, enode* n2);
// diagnostics
void display_equations(std::ostream& out) const;
void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
void display_disequations(std::ostream& out) const;
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;
public:
theory_seq(ast_manager& m);
virtual ~theory_seq();
// model building
app* mk_value(app* a);
};
};

7
src/smt/theory_seq_empty.h
View file

@ -30,6 +30,7 @@ namespace smt {
seq_util u;
symbol_set m_strings;
unsigned m_next;
char m_char;
std::string m_unique_prefix;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
@ -41,6 +42,7 @@ namespace smt {
m_model(md),
u(m),
m_next(0),
m_char(0),
m_unique_prefix("#B"),
m_trail(m)
{
@ -99,6 +101,11 @@ namespace smt {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
if (u.is_char(s)) {
//char s[2] = { ++m_char, 0 };
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
NOT_IMPLEMENTED_YET();
return 0;
}

47
src/tactic/bv/bit_blaster_tactic.h
View file

@ -1,32 +1,33 @@
/*++
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
Module Name:
bit_blaster_tactic.h
Abstract:
Abstract:
Apply bit-blasting to a given goal.
Author:
Author:
Leonardo (leonardo) 2011-10-25
Notes:
--*/
Notes:
--*/
#ifndef BIT_BLASTER_TACTIC_H_
#define BIT_BLASTER_TACTIC_H_
#include"params.h"
#include"bit_blaster_rewriter.h"
class ast_manager;
class tactic;
#include"params.h"
#include"bit_blaster_rewriter.h"
class ast_manager;
class tactic;
tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p = params_ref());
/*
/*
ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
*/
#endif
*/
#endif

20
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -22,7 +22,7 @@ Revision History:
#include"occurs.h"
#include"cooperate.h"
#include"goal_shared_occs.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
class solve_eqs_tactic : public tactic {
struct imp {
@ -92,21 +92,23 @@ class solve_eqs_tactic : public tactic {
}
// Use: (= x def) and (= def x)
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
bool trivial_solve1(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
var = to_app(lhs);
def = rhs;
pr = 0;
return true;
}
else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) {
var = to_app(rhs);
def = lhs;
if (m_produce_proofs)
pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
return true;
else {
return false;
}
return false;
}
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
return
trivial_solve1(lhs, rhs, var, def, pr) ||
trivial_solve1(rhs, lhs, var, def, pr);
}
// (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))

3
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -102,7 +102,8 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
or_else(try_for(mk_smt_tactic(), 100),
try_for(qe::mk_sat_tactic(m), 1000),
try_for(mk_smt_tactic(), 1000),
and_then(mk_qe_tactic(m), mk_smt_tactic())));
and_then(mk_qe_tactic(m), mk_smt_tactic())
));
st->updt_params(p);
return st;

3
src/util/ref_vector.h
View file

@ -89,9 +89,10 @@ public:
m_nodes.shrink(sz);
}
void push_back(T * n) {
ref_vector_core& push_back(T * n) {
inc_ref(n);
m_nodes.push_back(n);
return *this;
}
void pop_back() {

1
src/util/scoped_ptr_vector.h
View file

@ -30,6 +30,7 @@ public:
~scoped_ptr_vector() { reset(); }
void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); m_vector.reset(); }
void push_back(T * ptr) { m_vector.push_back(ptr); }
void pop_back() { SASSERT(!empty()); set(size()-1, 0); m_vector.pop_back(); }
T * operator[](unsigned idx) const { return m_vector[idx]; }
void set(unsigned idx, T * ptr) {
if (m_vector[idx] == ptr)

15
src/util/scoped_vector.h
View file

@ -46,7 +46,7 @@ public:
m_elems_lim.push_back(m_elems_start);
}
void pop_scopes(unsigned num_scopes) {
void pop_scope(unsigned num_scopes) {
if (num_scopes == 0) return;
unsigned new_size = m_sizes.size() - num_scopes;
unsigned src_lim = m_src_lim[new_size];
@ -72,6 +72,12 @@ public:
return m_elems[m_index[idx]];
}
// breaks abstraction, caller must ensure backtracking.
T& ref(unsigned idx) {
SASSERT(idx < m_size);
return m_elems[m_index[idx]];
}
void set(unsigned idx, T const& t) {
SASSERT(idx < m_size);
unsigned n = m_index[idx];
@ -102,6 +108,13 @@ public:
SASSERT(invariant());
}
void erase_and_swap(unsigned i) {
if (i + 1 < size()) {
set(i, m_elems[m_index[size()-1]]);
}
pop_back();
}
unsigned size() const { return m_size; }
bool empty() const { return m_size == 0; }