mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nils Becker 2019-05-02 20:09:06 +02:00
commit 2c40da23a2
33 changed files with 424 additions and 401 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_datalog.cpp
View file

@ -588,23 +588,6 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d) {
Z3_TRY;
LOG_Z3_fixedpoint_push(c, d);
RESET_ERROR_CODE();
to_fixedpoint_ref(d)->ctx().push();
Z3_CATCH;
}
void Z3_API Z3_fixedpoint_pop(Z3_context c,Z3_fixedpoint d) {
Z3_TRY;
LOG_Z3_fixedpoint_pop(c, d);
RESET_ERROR_CODE();
to_fixedpoint_ref(d)->ctx().pop();
Z3_CATCH;
}
void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d,
void *state,
Z3_fixedpoint_new_lemma_eh new_lemma_eh,

2
src/api/api_datatype.cpp
View file

@ -580,7 +580,7 @@ extern "C" {
expr* args[2] = { _t, _v };
sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) };
parameter param(_f);
func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_DT_UPDATE_FIELD, 1, &param, 2, domain);
func_decl * d = m.mk_func_decl(mk_c(c)->get_dt_fid(), OP_DT_UPDATE_FIELD, 1, &param, 2, domain);
app* r = m.mk_app(d, 2, args);
mk_c(c)->save_ast_trail(r);
check_sorts(c, r);

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

@ -2787,8 +2787,6 @@ namespace z3 {
array<Z3_ast> qs(queries);
return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
}
void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
};
inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }

2
src/api/dotnet/CMakeLists.txt
View file

@ -178,7 +178,7 @@ option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install targ
if(INSTALL_DOTNET_BINDINGS)
install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
# move the local repo to the installation directory (cancel the build-time repo)
install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)")
install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" \"${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget\")")
install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
# TODO GAC?
# set(GAC_PKG_NAME "Microsoft.Z3.Sharp")

20
src/api/dotnet/Fixedpoint.cs
View file

@ -161,26 +161,6 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Creates a backtracking point.
/// </summary>
/// <seealso cref="Pop"/>
public void Push()
{
Native.Z3_fixedpoint_push(Context.nCtx, NativeObject);
}
/// <summary>
/// Backtrack one backtracking point.
/// </summary>
/// <remarks>Note that an exception is thrown if Pop is called without a corresponding <c>Push</c></remarks>
/// <seealso cref="Push"/>
public void Pop()
{
Native.Z3_fixedpoint_pop(Context.nCtx, NativeObject);
}
/// <summary>
/// Update named rule into in the fixedpoint solver.
/// </summary>

19
src/api/java/Fixedpoint.java
View file

@ -157,25 +157,6 @@ public class Fixedpoint extends Z3Object
}
}
/**
* Creates a backtracking point.
* @see #pop
**/
public void push() {
Native.fixedpointPush(getContext().nCtx(), getNativeObject());
}
/**
* Backtrack one backtracking point.
* Remarks: Note that an exception is thrown if {@code pop}
* is called without a corresponding {@code push}
*
* @see #push
**/
public void pop() {
Native.fixedpointPop(getContext().nCtx(), getNativeObject());
}
/**
* Update named rule into in the fixedpoint solver.
*

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

@ -1883,8 +1883,6 @@ struct
| L_FALSE -> Solver.UNSATISFIABLE
| _ -> Solver.UNKNOWN
let push x = Z3native.fixedpoint_push (gc x) x
let pop x = Z3native.fixedpoint_pop (gc x) x
let update_rule x = Z3native.fixedpoint_update_rule (gc x) x
let get_answer x =

10
src/api/ml/z3.mli
View file

@ -3256,16 +3256,6 @@ sig
The query is unsatisfiable if there are no derivations satisfying any of the relations. *)
val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status
(** Creates a backtracking point.
{!pop} *)
val push : fixedpoint -> unit
(** Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding [Push]</remarks>
{!push} *)
val pop : fixedpoint -> unit
(** Update named rule into in the fixedpoint solver. *)
val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit

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

File diff suppressed because it is too large Load diff

18
src/api/python/z3/z3util.py
View file

@ -75,7 +75,7 @@ def ehash(v):
x_783810685_1 x_783810685_1 x_783810685_2
"""
if __debug__:
if z3_debug():
assert is_expr(v)
return "{}_{}_{}".format(str(v),v.hash(),v.sort_kind())
@ -148,7 +148,7 @@ def get_vars(f,rs=[]):
[x, y, a, b]
"""
if __debug__:
if z3_debug():
assert is_expr(f)
if is_const(f):
@ -228,13 +228,13 @@ def prove(claim,assume=None,verbose=0):
"""
if __debug__:
if z3_debug():
assert not assume or is_expr(assume)
to_prove = claim
if assume:
if __debug__:
if z3_debug():
is_proved,_ = prove(Not(assume))
def _f():
@ -266,7 +266,7 @@ def prove(claim,assume=None,verbose=0):
elif models == False: #unsat
return True,None
else: #sat
if __debug__:
if z3_debug():
assert isinstance(models,list)
if models:
@ -312,7 +312,7 @@ def get_models(f,k):
"""
if __debug__:
if z3_debug():
assert is_expr(f)
assert k>=1
@ -448,13 +448,13 @@ def myBinOp(op,*L):
AssertionError
"""
if __debug__:
if z3_debug():
assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
L = L[0]
if __debug__:
if z3_debug():
assert all(not isinstance(l,bool) for l in L)
L = [l for l in L if is_expr(l)]
@ -493,7 +493,7 @@ def model_str(m,as_str=True):
see doctest exampels from function prove()
"""
if __debug__:
if z3_debug():
assert m is None or m == [] or isinstance(m,ModelRef)
if m :

23
src/api/z3_fixedpoint.h
View file

@ -334,29 +334,6 @@ extern "C" {
Z3_fixedpoint f,
Z3_string s);
/**
\brief Create a backtracking point.
The fixedpoint solver contains a set of rules, added facts and assertions.
The set of rules, facts and assertions are restored upon calling #Z3_fixedpoint_pop.
\sa Z3_fixedpoint_pop
def_API('Z3_fixedpoint_push', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d);
/**
\brief Backtrack one backtracking point.
\sa Z3_fixedpoint_push
\pre The number of calls to pop cannot exceed calls to push.
def_API('Z3_fixedpoint_pop', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
*/
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d);
/** \brief The following utilities allows adding user-defined domains. */
typedef void Z3_fixedpoint_reduce_assign_callback_fptr(

42
src/ast/array_decl_plugin.cpp
View file

@ -30,13 +30,14 @@ array_decl_plugin::array_decl_plugin():
m_default_sym("default"),
m_map_sym("map"),
m_set_union_sym("union"),
m_set_intersect_sym("intersect"),
m_set_difference_sym("difference"),
m_set_intersect_sym("intersection"),
m_set_difference_sym("setminus"),
m_set_complement_sym("complement"),
m_set_subset_sym("subset"),
m_array_ext_sym("array-ext"),
m_as_array_sym("as-array"),
m_set_has_size_sym("set-has-size") {
m_set_has_size_sym("set-has-size"),
m_set_card_sym("card") {
}
#define ARRAY_SORT_STR "Array"
@ -440,6 +441,21 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma
func_decl_info(m_family_id, OP_SET_SUBSET));
}
func_decl * array_decl_plugin::mk_set_card(unsigned arity, sort * const* domain) {
if (arity != 1) {
m_manager->raise_exception("card takes only one argument");
return nullptr;
}
arith_util arith(*m_manager);
if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
m_manager->raise_exception("card expects an array of Booleans");
}
sort * int_sort = arith.mk_int();
return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort,
func_decl_info(m_family_id, OP_SET_CARD));
}
func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) {
if (arity != 2) {
m_manager->raise_exception("set-has-size takes two arguments");
@ -525,6 +541,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_set_subset(arity, domain);
case OP_SET_HAS_SIZE:
return mk_set_has_size(arity, domain);
case OP_SET_CARD:
return mk_set_card(arity, domain);
case OP_AS_ARRAY: {
if (num_parameters != 1 ||
!parameters[0].is_ast() ||
@ -548,8 +566,10 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT));
sort_names.push_back(builtin_name("=>", ARRAY_SORT));
// TBD: this could easily break users even though it is already used in CVC4:
// sort_names.push_back(builtin_name("Set", _SET_SORT));
if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
// this could easily break users even though it is already used in CVC4:
sort_names.push_back(builtin_name("Set", _SET_SORT));
}
}
void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
@ -561,13 +581,14 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("map",OP_ARRAY_MAP));
op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT));
op_names.push_back(builtin_name("union",OP_SET_UNION));
op_names.push_back(builtin_name("intersect",OP_SET_INTERSECT));
op_names.push_back(builtin_name("difference",OP_SET_DIFFERENCE));
op_names.push_back(builtin_name("intersection",OP_SET_INTERSECT));
op_names.push_back(builtin_name("setminus",OP_SET_DIFFERENCE));
op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE));
op_names.push_back(builtin_name("card", OP_SET_CARD));
}
}
@ -595,6 +616,13 @@ func_decl * array_recognizers::get_as_array_func_decl(expr * n) const {
return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast());
}
func_decl * array_recognizers::get_map_func_decl(func_decl* f) const {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_ast());
SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
return to_func_decl(f->get_parameter(0).get_ast());
}
func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const {
SASSERT(is_as_array(f));
return to_func_decl(f->get_parameter(0).get_ast());

30
src/ast/array_decl_plugin.h
View file

@ -52,6 +52,7 @@ enum array_op_kind {
OP_SET_COMPLEMENT,
OP_SET_SUBSET,
OP_SET_HAS_SIZE,
OP_SET_CARD,
OP_AS_ARRAY, // used for model construction
LAST_ARRAY_OP
};
@ -70,6 +71,7 @@ class array_decl_plugin : public decl_plugin {
symbol m_array_ext_sym;
symbol m_as_array_sym;
symbol m_set_has_size_sym;
symbol m_set_card_sym;
bool check_set_arguments(unsigned arity, sort * const * domain);
@ -99,6 +101,8 @@ class array_decl_plugin : public decl_plugin {
func_decl* mk_set_has_size(unsigned arity, sort * const* domain);
func_decl* mk_set_card(unsigned arity, sort * const* domain);
bool is_array_sort(sort* s) const;
public:
array_decl_plugin();
@ -149,15 +153,19 @@ public:
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); }
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
func_decl * get_as_array_func_decl(expr * n) const;
func_decl * get_as_array_func_decl(func_decl* f) const;
func_decl * get_map_func_decl(func_decl* f) const;
func_decl * get_map_func_decl(expr* e) const { return get_map_func_decl(to_app(e)->get_decl()); }
bool is_const(expr* e, expr*& v) const;
@ -184,6 +192,16 @@ public:
parameter p(f);
return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args);
}
expr * mk_map_assoc(func_decl * f, unsigned num_args, expr * const * args) {
expr* r = args[0];
for (unsigned i = 1; i < num_args; ++i) {
expr* es[2] = { r, args[i] };
r = mk_map(f, 2, es);
}
return r;
}
app * mk_const_array(sort * s, expr * v) {
parameter param(s);
return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v);
@ -195,6 +213,18 @@ public:
return mk_const_array(s, m_manager.mk_true());
}
app * mk_setminus(expr* s1, expr* s2) {
return m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, s1, s2);
}
app * mk_intersection(expr* s1, expr* s2) {
return m_manager.mk_app(m_fid, OP_SET_INTERSECT, s1, s2);
}
app * mk_union(expr* s1, expr* s2) {
return m_manager.mk_app(m_fid, OP_SET_UNION, s1, s2);
}
app* mk_has_size(expr* set, expr* n) {
return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n);
}

11
src/ast/ast_smt_pp.cpp
View file

@ -924,11 +924,11 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
decl_collector decls(m);
smt_renaming rn;
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
decls.visit(m_assumptions[i].get());
for (expr* a : m_assumptions) {
decls.visit(a);
}
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
decls.visit(m_assumptions_star[i].get());
for (expr* a : m_assumptions_star) {
decls.visit(a);
}
decls.visit(n);
@ -959,8 +959,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
#else
decls.order_deps();
ast_mark sort_mark;
for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
sort* s = decls.get_sorts()[i];
for (sort* s : decls.get_sorts()) {
if (!(*m_is_declared)(s)) {
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
p.pp_sort_decl(sort_mark, s);

4
src/ast/decl_collector.h
View file

@ -57,8 +57,8 @@ public:
unsigned get_num_sorts() const { return m_sorts.size(); }
unsigned get_num_decls() const { return m_decls.size(); }
sort * const * get_sorts() const { return m_sorts.c_ptr(); }
func_decl * const * get_func_decls() const { return m_decls.c_ptr(); }
ptr_vector<sort> const& get_sorts() const { return m_sorts; }
ptr_vector<func_decl> const& get_func_decls() const { return m_decls; }
};
#endif

103
src/ast/rewriter/array_rewriter.cpp
View file

@ -45,10 +45,7 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
st = mk_store_core(num_args, args, result);
break;
case OP_ARRAY_MAP:
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_ast());
SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
st = mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
st = mk_map_core(m_util.get_map_func_decl(f), num_args, args, result);
break;
case OP_SET_UNION:
st = mk_set_union(num_args, args, result);
@ -69,14 +66,15 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
st = mk_set_difference(args[0], args[1], result);
break;
default:
return BR_FAILED;
st = BR_FAILED;
break;
}
TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m()) << "\n";
}
tout << "\n --> " << result << "\n";
);
CTRACE("array_rewriter", st != BR_FAILED,
tout << mk_pp(f, m()) << "\n";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m()) << "\n";
}
tout << "\n --> " << result << "\n";);
return st;
}
@ -241,6 +239,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
return BR_FAILED;
}
sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) {
sort* s0 = m().get_sort(args[0]);
unsigned sz = get_array_arity(s0);
ptr_vector<sort> domain;
for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
return sort_ref(m_util.mk_array_sort(sz, domain.c_ptr(), f->get_range()), m());
}
br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
app* store_expr = nullptr;
@ -291,11 +297,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
}
else {
expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m());
sort* s0 = m().get_sort(args[0]);
unsigned sz = get_array_arity(s0);
ptr_vector<sort> domain;
for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m());
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, value);
}
return BR_REWRITE2;
@ -336,6 +338,75 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
return BR_REWRITE3;
}
if (m().is_and(f)) {
ast_mark mark;
ptr_buffer<expr> es;
bool change = false;
unsigned j = 0;
es.append(num_args, args);
for (unsigned i = 0; i < es.size(); ++i) {
expr* e = es[i];
if (mark.is_marked(e)) {
change = true;
}
else if (m_util.is_map(e) && m().is_and(m_util.get_map_func_decl(e))) {
mark.mark(e, true);
es.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else {
mark.mark(e, true);
es[j++] = es[i];
}
}
es.shrink(j);
for (expr* e : es) {
if (m().is_not(e, e) && mark.is_marked(e)) {
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, m().mk_false());
return BR_DONE;
}
}
if (change) {
result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
return BR_DONE;
}
}
if (m().is_or(f)) {
ast_mark mark;
ptr_buffer<expr> es;
es.append(num_args, args);
unsigned j = 0;
bool change = false;
for (unsigned i = 0; i < es.size(); ++i) {
expr* e = es[i];
if (mark.is_marked(e)) {
change = true;
}
else if (m_util.is_map(e) && m().is_or(m_util.get_map_func_decl(e))) {
mark.mark(e, true);
es.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else {
mark.mark(e, true);
es[j++] = es[i];
}
}
es.shrink(j);
for (expr* e : es) {
if (m().is_not(e, e) && mark.is_marked(e)) {
sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, m().mk_true());
return BR_DONE;
}
}
if (change) {
result = m_util.mk_map_assoc(f, es.size(), es.c_ptr());
return BR_DONE;
}
}
return BR_FAILED;
}

3
src/ast/rewriter/array_rewriter.h
View file

@ -37,6 +37,9 @@ class array_rewriter {
lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls);
sort_ref get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args);
public:
array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {

6
src/cmd_context/cmd_context.cpp
View file

@ -2033,10 +2033,8 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr
// TODO: display uninterpreted sort decls, and datatype decls.
unsigned num_decls = decls.get_num_decls();
func_decl * const * fs = decls.get_func_decls();
for (unsigned i = 0; i < num_decls; i++) {
display(out, fs[i]);
for (func_decl* f : decls.get_func_decls()) {
display(out, f);
out << std::endl;
}

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

@ -348,6 +348,7 @@ public:
//
void compress() {
SASSERT(!m_delta.empty());
TRACE("seq", display(tout););
for (unsigned i = 0; i < m_delta.size(); ++i) {
for (unsigned j = 0; j < m_delta[i].size(); ++j) {
move const& mv = m_delta[i][j];
@ -460,6 +461,7 @@ public:
}
}
sinkify_dead_states();
TRACE("seq", display(tout););
}
bool is_sequence(unsigned& length) const {
@ -559,9 +561,8 @@ public:
template<class D>
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";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
@ -577,6 +578,22 @@ public:
}
private:
std::ostream& display(std::ostream& out) const {
out << "init: " << init() << "\n";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
out << i << " -> " << mv.dst() << " ";
if (mv.t()) {
out << "if *** ";
}
out << "\n";
}
}
return out;
}
void sinkify_dead_states() {
uint_set dead_states;
for (unsigned i = 0; i < m_delta.size(); ++i) {
@ -604,7 +621,9 @@ private:
}
to_remove.reset();
}
TRACE("seq", tout << "remove: " << dead_states << "\n";);
TRACE("seq", tout << "remove: " << dead_states << "\n";
tout << "final: " << m_final_states << "\n";
);
for (unsigned s : dead_states) {
CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";);
m_delta[s].reset();

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

@ -379,9 +379,21 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
pair2id.insert(init_pair, 0);
moves_t mvs;
unsigned_vector final;
if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
final.push_back(0);
unsigned_vector a_init, b_init;
a.get_epsilon_closure(a.init(), a_init);
for (unsigned ia : a_init) {
if (a.is_final_state(ia)) {
b.get_epsilon_closure(b.init(), b_init);
for (unsigned ib : b_init) {
if (b.is_final_state(ib)) {
final.push_back(0);
break;
}
}
break;
}
}
unsigned n = 1;
moves_t mvsA, mvsB;
while (!todo.empty()) {

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

@ -479,44 +479,6 @@ public:
}
};
/**
\brief fixedpoint-push command.
*/
class dl_push_cmd : public cmd {
ref<dl_context> m_dl_ctx;
public:
dl_push_cmd(dl_context * dl_ctx):
cmd("fixedpoint-push"),
m_dl_ctx(dl_ctx)
{}
char const * get_usage() const override { return ""; }
char const * get_descr(cmd_context & ctx) const override { return "push the fixedpoint context"; }
unsigned get_arity() const override { return 0; }
void execute(cmd_context & ctx) override {
m_dl_ctx->push();
}
};
/**
\brief fixedpoint-pop command.
*/
class dl_pop_cmd : public cmd {
ref<dl_context> m_dl_ctx;
public:
dl_pop_cmd(dl_context * dl_ctx):
cmd("fixedpoint-pop"),
m_dl_ctx(dl_ctx)
{}
char const * get_usage() const override { return ""; }
char const * get_descr(cmd_context & ctx) const override { return "pop the fixedpoint context"; }
unsigned get_arity() const override { return 0; }
void execute(cmd_context & ctx) override {
m_dl_ctx->pop();
}
};
static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
@ -524,8 +486,6 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c
ctx.insert(alloc(dl_query_cmd, dl_ctx));
ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
ctx.insert(alloc(dl_push_cmd, dl_ctx));
ctx.insert(alloc(dl_pop_cmd, dl_ctx));
}
void install_dl_cmds(cmd_context & ctx) {

11
src/nlsat/nlsat_solver.cpp
View file

@ -1347,6 +1347,7 @@ namespace nlsat {
restore_order();
CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout););
CTRACE("nlsat", r == l_false, display(tout););
SASSERT(r != l_true || check_satisfied(m_clauses));
return r;
}
@ -1867,11 +1868,17 @@ namespace nlsat {
if (m_bk != null_bool_var)
num = m_bk;
for (bool_var b = 0; b < num; b++) {
SASSERT(check_satisfied(m_bwatches[b]));
if (!check_satisfied(m_bwatches[b])) {
UNREACHABLE();
return false;
}
}
if (m_xk != null_var) {
for (var x = 0; x < m_xk; x++) {
SASSERT(check_satisfied(m_watches[x]));
if (!check_satisfied(m_watches[x])) {
UNREACHABLE();
return false;
}
}
}
return true;

7
src/nlsat/tactic/nlsat_tactic.cpp
View file

@ -85,6 +85,9 @@ class nlsat_tactic : public tactic {
for (unsigned i = 0; i < sz; i++) {
if (!model.is_true(g.form(i))) {
TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(0, verbose_stream() << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";);
IF_VERBOSE(1, verbose_stream() << model << "\n");
IF_VERBOSE(1, m_solver.display(verbose_stream()));
return false;
}
}
@ -123,6 +126,7 @@ class nlsat_tactic : public tactic {
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
}
DEBUG_CODE(eval_model(*md.get(), g););
// VERIFY(eval_model(*md.get(), g));
mc = model2model_converter(md.get());
return ok;
}
@ -149,6 +153,9 @@ class nlsat_tactic : public tactic {
t2x.mk_inv(m_display_var.m_var2expr);
m_solver.set_display_var(m_display_var);
IF_VERBOSE(10000, m_solver.display(verbose_stream()));
IF_VERBOSE(10000, g->display(verbose_stream()));
lbool st = m_solver.check();
if (st == l_undef) {

7
src/opt/opt_context.cpp
View file

@ -361,7 +361,8 @@ namespace opt {
void context::fix_model(model_ref& mdl) {
if (mdl && !m_model_fixed.contains(mdl.get())) {
TRACE("opt", tout << "fix-model\n";);
TRACE("opt", m_fm->display(tout << "fix-model\n");
m_model_converter->display(tout););
(*m_fm)(mdl);
apply(m_model_converter, mdl);
m_model_fixed.push_back(mdl.get());
@ -1116,7 +1117,9 @@ namespace opt {
val = (*mdl)(term);
unsigned bvsz;
if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
TRACE("opt", tout << "model does not evaluate objective to a value\n";);
TRACE("opt", tout << "model does not evaluate objective to a value but instead " << val << "\n";
tout << *mdl << "\n";
);
return false;
}
if (r != v) {

45
src/smt/theory_array_bapa.cpp
View file

@ -102,7 +102,7 @@ namespace smt {
theory_array_full& th;
arith_util m_arith;
array_util m_autil;
array_rewriter m_rw;
th_rewriter m_rw;
arith_value m_arith_value;
ast_ref_vector m_pinned;
obj_map<app, sz_info*> m_sizeof;
@ -204,26 +204,29 @@ namespace smt {
return l_true;
}
lbool ensure_disjoint(app* sz1, app* sz2) {
bool ensure_disjoint(app* sz1, app* sz2) {
sz_info& i1 = *m_sizeof[sz1];
sz_info& i2 = *m_sizeof[sz2];
SASSERT(i1.m_is_leaf);
SASSERT(i2.m_is_leaf);
expr* s = sz1->get_arg(0);
expr* t = sz2->get_arg(0);
if (m.get_sort(s) != m.get_sort(t)) {
return true;
}
enode* r1 = get_root(s);
enode* r2 = get_root(t);
if (r1 == r2) {
return l_true;
return true;
}
if (!ctx().is_diseq(r1, r2) && ctx().assume_eq(r1, r2)) {
return l_false;
return false;
}
if (do_intersect(i1.m_selects, i2.m_selects)) {
add_disjoint(sz1, sz2);
return l_false;
return false;
}
return l_true;
return true;
}
bool do_intersect(obj_map<enode, expr*> const& s, obj_map<enode, expr*> const& t) const {
@ -265,11 +268,15 @@ namespace smt {
}
expr_ref mk_subtract(expr* t, expr* s) {
return m_rw.mk_set_difference(t, s);
expr_ref d(m_autil.mk_setminus(t, s), m);
m_rw(d);
return d;
}
expr_ref mk_intersect(expr* t, expr* s) {
return m_rw.mk_set_intersect(t, s);
expr_ref i(m_autil.mk_intersection(t, s), m);
m_rw(i);
return i;
}
void propagate(expr* assumption, expr* conseq) {
@ -436,6 +443,15 @@ namespace smt {
reset();
}
void internalize_term(app* term) {
if (th.is_set_has_size(term)) {
internalize_size(term);
}
else if (th.is_set_card(term)) {
internalize_card(term);
}
}
/**
* Size(S, n) => n >= 0, default(S) = false
*/
@ -458,6 +474,17 @@ namespace smt {
ctx().push_trail(remove_sz(m_sizeof, term));
}
/**
\brief whenever there is a cardinality function, it includes an axiom
that entails the set is finite.
*/
void internalize_card(app* term) {
SASSERT(ctx().e_internalized(term));
app_ref has_size(m_autil.mk_has_size(term->get_arg(0), term), m);
literal lit = mk_literal(has_size);
ctx().assign(lit, nullptr);
}
final_check_status final_check() {
lbool r = ensure_functional();
if (r == l_true) update_indices();
@ -494,7 +521,7 @@ namespace smt {
theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); }
void theory_array_bapa::internalize_size(app* term) { m_imp->internalize_size(term); }
void theory_array_bapa::internalize_term(app* term) { m_imp->internalize_term(term); }
final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); }

2
src/smt/theory_array_bapa.h
View file

@ -32,7 +32,7 @@ namespace smt {
public:
theory_array_bapa(theory_array_full& th);
~theory_array_bapa();
void internalize_size(app* term);
void internalize_term(app* term);
final_check_status final_check();
void init_model();
};

2
src/smt/theory_array_base.h
View file

@ -43,6 +43,7 @@ namespace smt {
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); }
bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); }
bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); }
bool is_store(enode const * n) const { return is_store(n->get_owner()); }
bool is_map(enode const* n) const { return is_map(n->get_owner()); }
@ -52,6 +53,7 @@ namespace smt {
bool is_default(enode const* n) const { return is_default(n->get_owner()); }
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); }
bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); }
bool is_set_carde(enode const* n) const { return is_set_card(n->get_owner()); }
app * mk_select(unsigned num_args, expr * const * args);

6
src/smt/theory_array_full.cpp
View file

@ -250,7 +250,7 @@ namespace smt {
return theory_array::internalize_term(n);
}
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n)) {
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n) && !is_set_card(n)) {
if (!is_array_ext(n))
found_unsupported_op(n);
return false;
@ -274,11 +274,11 @@ namespace smt {
mk_var(arg0);
}
}
else if (is_set_has_size(n)) {
else if (is_set_has_size(n) || is_set_card(n)) {
if (!m_bapa) {
m_bapa = alloc(theory_array_bapa, *this);
}
m_bapa->internalize_size(n);
m_bapa->internalize_term(n);
}
enode* node = ctx.get_enode(n);

8
src/smt/theory_seq.cpp
View file

@ -3576,7 +3576,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
// n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
// n < 0 & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
// 10^k <= n < 10^{k+1}-1 => len(e) = k
// 10^k <= n < 10^{k+1}-1 => len(e) => k
void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
context& ctx = get_context();
@ -3618,15 +3618,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
rational ub = power(rational(10), k) - 1;
arith_util& a = m_autil;
literal lbl = mk_literal(a.mk_ge(n, a.mk_int(lb)));
literal ubl = mk_literal(a.mk_le(n, a.mk_int(ub)));
literal ge_k = mk_literal(a.mk_ge(len, a.mk_int(k)));
literal le_k = mk_literal(a.mk_le(len, a.mk_int(k)));
// n >= lb => len(s) >= k
// n >= 0 & len(s) >= k => n >= lb
// 0 <= n <= ub => len(s) <= k
add_axiom(~lbl, ge_k);
add_axiom(~ge0, lbl, ~ge_k);
add_axiom(~ge0, ~ubl, le_k);
}

1
src/smt/theory_seq_empty.h
View file

@ -117,6 +117,7 @@ namespace smt {
}
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
if (!v) return nullptr;
return u.str.mk_unit(v);
}
UNREACHABLE();

4
src/tactic/arith/lia2card_tactic.cpp
View file

@ -143,7 +143,9 @@ public:
expr_ref last_v(m);
if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card");
if (hi == 0) {
return expr_ref(a.mk_int(0), m);
expr* r = a.mk_int(0);
m_mc->add(x->get_decl(), r);
return expr_ref(r, m);
}
if (lo > 0) {
xs.push_back(a.mk_int(lo));

2
src/tactic/tactical.cpp
View file

@ -917,7 +917,7 @@ public:
{
// Warning: scoped_timer is not thread safe in Linux.
scoped_timer timer(m_timeout, &eh);
m_t->operator()(in, result);
m_t->operator()(in, result);
}
}

45
src/util/critical_flet.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
critical flet.cpp
Abstract:
Version of flet using "omp critical" directive.
Warning: it uses omp critical section "critical_flet"
Author:
Leonardo de Moura (leonardo) 2011-05-12
Revision History:
--*/
#ifndef CRITICAL_FLET_H_
#define CRITICAL_FLET_H_
template<typename T>
class critical_flet {
T & m_ref;
T m_old_value;
public:
critical_flet(T & ref, const T & new_value):
m_ref(ref),
m_old_value(ref) {
#pragma omp critical (critical_flet)
{
m_ref = new_value;
}
}
~critical_flet() {
#pragma omp critical (critical_flet)
{
m_ref = m_old_value;
}
}
};
#endif