mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-mpf-rem

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-04 16:24:56 +01:00
commit 40b9d0871a
12 changed files with 2928 additions and 3426 deletions
Download patch file Download diff file Expand all files Collapse all files

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

36
src/api/ml/z3native.ml.pre Normal file
View file

@ -0,0 +1,36 @@
(** The native (raw) interface to the dynamic Z3 library. *)
open Z3enums
(**/**)
type ptr
and symbol = ptr
and config = ptr
and context = ptr
and ast = ptr
and app = ast
and sort = ast
and func_decl = ast
and pattern = ast
and model = ptr
and literals = ptr
and constructor = ptr
and constructor_list = ptr
and solver = ptr
and goal = ptr
and tactic = ptr
and params = ptr
and probe = ptr
and stats = ptr
and ast_vector = ptr
and ast_map = ptr
and apply_result = ptr
and func_interp = ptr
and func_entry = ptr
and fixedpoint = ptr
and optimize = ptr
and param_descrs = ptr
and rcf_num = ptr
external set_internal_error_handler : ptr -> unit
= "n_set_internal_error_handler"

445
src/api/ml/z3native_stubs.c.pre Normal file
View file

@ -0,0 +1,445 @@
#include <stddef.h>
#include <string.h>
#include <assert.h>
#ifdef __cplusplus
extern "C" {
#endif
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/alloc.h>
#include <caml/fail.h>
#include <caml/callback.h>
#ifdef Custom_tag
#include <caml/custom.h>
#include <caml/bigarray.h>
#endif
#ifdef __cplusplus
}
#endif
#include <z3.h>
#include <z3native_stubs.h>
#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal1(X6)
#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal2(X6,X7)
#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal3(X6,X7,X8)
#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam2(X6,X7)
#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam3(X6,X7,X8)
#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9)
#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12)
#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13)
static struct custom_operations default_custom_ops = {
(char*) "default handling",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
int compare_pointers(void* pt1, void* pt2) {
if (pt1 == pt2)
return 0;
else if ((intnat)pt1 < (intnat)pt2)
return -1;
else
return +1;
}
#define MK_CTX_OF(X) \
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_context_plus cp; \
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \
cp = p->cp; \
result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \
*(Z3_context_plus *)Data_custom_val(result) = cp; \
/* We increment the usage counter of the context, as we just \
created a second custom block holding that context */ \
cp->obj_count++; \
CAMLreturn(result); \
} \
\
CAMLprim value DLL_PUBLIC n_is_null_ ## X (value v) { \
CAMLparam1(v); \
Z3_ ## X ## _plus* pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
CAMLreturn(Val_bool(pp->p == NULL)); \
} \
\
CAMLprim value DLL_PUBLIC n_mk_null_ ## X (value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \
Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \
result = caml_alloc_custom(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), 0, 1); \
*(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \
CAMLreturn(result); \
}
/* Context objects */
/* The Z3context_plus_data exists exactly once for each context,
no matter how many custom blocks for that context exist.
Each custom block only stores a pointer to the corresponding
Z3_context_plus_data. This ensures that the reference counting
is performed at exactly one place and not within the custom
blocks that get copied. */
typedef struct {
Z3_context ctx;
unsigned long obj_count;
} Z3_context_plus_data;
/* A context is wrapped to an OCaml value by storing a pointer
to its associated Z3_context_plus_data instance.
This instance gets created in mk_context and is deleted
together with the Z3 context instance in try_to_delete_context
whenever the obj_count field is zero. */
typedef Z3_context_plus_data* Z3_context_plus;
Z3_context_plus Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data));
r->ctx = c;
/* The context created here will be wrapped into a custom block.
We regard custom blocks that point to a Z3_context_plus structure
as a usage of this structure. Hence, we assign it a counter of one. */
r->obj_count = 1;
return r;
}
Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
return (*cp)->ctx;
}
void try_to_delete_context(Z3_context_plus cp) {
if (cp->obj_count == 0) {
/* printf("try_to_delete_context: Deleting context %p(%p) with cnt=0.\n", cp, cp->ctx); */
Z3_del_context(cp->ctx);
free(cp);
}
/*
else if (cp->obj_count > 0)
printf("try_to_delete_context: Not deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count);
else if (cp->obj_count < 0)
printf("try_to_delete_context: ERROR, found context %p(%p) with negative cnt=%lu.\n", cp, cp->ctx, cp->obj_count);
*/
}
void Z3_context_finalize(value v) {
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
cp->obj_count--;
try_to_delete_context(cp);
}
int Z3_context_compare(value v1, value v2) {
/* As each context created within the OCaml bindings has a unique
Z3_context_plus_data allocated to store the handle and the ref counters,
we can just compare pointers here. This suffices to test for (in)equality
and induces an arbitrary (but fixed) ordering. */
Z3_context_plus cp1 = *(Z3_context_plus*)Data_custom_val(v1);
Z3_context_plus cp2 = *(Z3_context_plus*)Data_custom_val(v2);
return compare_pointers(cp1, cp2);
}
int Z3_context_compare_ext(value v1, value v2) {
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v1);
return compare_pointers(cp, (void*)Val_int(v2));
}
/* We use the pointer to the Z3_context_plus_data structure as
a hash value; it is unique, at least. */
intnat Z3_context_hash(value v) {
/* We use the address of the context's Z3_context_plus_data structure
as a hash value */
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
return (intnat)cp;
}
static struct custom_operations Z3_context_plus_custom_ops = {
(char*) "Z3_context ops",
Z3_context_finalize,
Z3_context_compare,
Z3_context_hash,
custom_serialize_default,
custom_deserialize_default,
Z3_context_compare_ext
};
/* AST objects */
typedef struct {
Z3_context_plus cp;
Z3_ast p;
} Z3_ast_plus;
Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus cp, Z3_ast p) {
Z3_ast_plus r;
r.cp = cp;
r.p = p;
/* printf("++\n"); */
cp->obj_count++;
if (p != NULL)
Z3_inc_ref(cp->ctx, p);
return r;
}
Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) {
return ap->p;
}
void Z3_ast_finalize(value v) {
/* printf("--\n"); */
Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v));
if (ap->p != NULL)
Z3_dec_ref(ap->cp->ctx, ap->p);
ap->cp->obj_count--;
try_to_delete_context(ap->cp);
}
int Z3_ast_compare(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
/* if the two ASTs belong to different contexts, we take
their contexts' addresses to order them (arbitrarily, but fixed) */
if (a1->cp->ctx != a2->cp->ctx)
return compare_pointers(a1->cp->ctx, a2->cp->ctx);
/* handling of NULL pointers */
if (a1->p == NULL && a2->p == NULL)
return 0;
if (a1->p == NULL)
return -1;
if (a2->p == NULL)
return +1;
/* Comparison according to AST ids. */
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
if (id1 == id2)
return 0;
else if (id1 < id2)
return -1;
else
return +1;
}
int Z3_ast_compare_ext(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
unsigned id1;
int id2 = Val_int(v2);
if (a1->p == NULL && id2 == 0)
return 0;
if (a1->p == NULL)
return -1;
if (id2 == 0)
return +1;
id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
if (id1 == id2)
return 0;
else if (id1 < id2)
return -1;
else
return +1;
}
intnat Z3_ast_hash(value v) {
Z3_ast_plus * ap = (Z3_ast_plus*)Data_custom_val(v);
if (ap->p == NULL)
return 0;
else
return Z3_get_ast_hash(ap->cp->ctx, ap->p);
}
static struct custom_operations Z3_ast_plus_custom_ops = {
(char*) "Z3_ast ops",
Z3_ast_finalize,
Z3_ast_compare,
Z3_ast_hash,
custom_serialize_default,
custom_deserialize_default,
Z3_ast_compare_ext
};
MK_CTX_OF(ast)
#define MK_PLUS_OBJ_NO_REF(X) \
typedef struct { \
Z3_context_plus cp; \
Z3_ ## X p; \
} Z3_ ## X ## _plus; \
\
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \
r.cp = cp; \
r.p = p; \
r.cp->obj_count++; \
return r; \
} \
\
Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \
return pp->p; \
} \
\
void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
pp->cp->obj_count--; \
try_to_delete_context(pp->cp); \
} \
\
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \
Z3_ ## X ## _compare, \
Z3_ ## X ## _hash, \
custom_serialize_default, \
custom_deserialize_default, \
Z3_ ## X ## _compare_ext \
}; \
\
MK_CTX_OF(X)
#define MK_PLUS_OBJ(X) \
typedef struct { \
Z3_context_plus cp; \
Z3_ ## X p; \
} Z3_ ## X ## _plus; \
\
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \
r.cp = cp; \
r.p = p; \
r.cp->obj_count++; \
if (p != NULL) \
Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \
} \
\
Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \
return pp->p; \
} \
\
void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
if (pp->p != NULL) \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
pp->cp->obj_count--; \
try_to_delete_context(pp->cp); \
} \
\
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \
Z3_ ## X ## _compare, \
Z3_ ## X ## _hash, \
custom_serialize_default, \
custom_deserialize_default, \
Z3_ ## X ## _compare_ext \
}; \
\
MK_CTX_OF(X)
MK_PLUS_OBJ_NO_REF(symbol)
MK_PLUS_OBJ_NO_REF(constructor)
MK_PLUS_OBJ_NO_REF(constructor_list)
MK_PLUS_OBJ_NO_REF(rcf_num)
MK_PLUS_OBJ(params)
MK_PLUS_OBJ(param_descrs)
MK_PLUS_OBJ(model)
MK_PLUS_OBJ(func_interp)
MK_PLUS_OBJ(func_entry)
MK_PLUS_OBJ(goal)
MK_PLUS_OBJ(tactic)
MK_PLUS_OBJ(probe)
MK_PLUS_OBJ(apply_result)
MK_PLUS_OBJ(solver)
MK_PLUS_OBJ(stats)
MK_PLUS_OBJ(ast_map)
MK_PLUS_OBJ(ast_vector)
MK_PLUS_OBJ(fixedpoint)
MK_PLUS_OBJ(optimize)
#ifdef __cplusplus
extern "C" {
#endif
void MLErrorHandler(Z3_context c, Z3_error_code e)
{
/* Internal do-nothing error handler. This is required to avoid that Z3 calls exit()
upon errors, but the actual error handling is done by throwing exceptions in the
n_* wrapper functions. */
}
CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v)
{
CAMLparam1(ctx_v);
Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(ctx_v);
Z3_set_error_handler(ctx_p->ctx, MLErrorHandler);
CAMLreturn(Val_unit);
}

8
src/sat/sat_clause_set.cpp
View file

@ -35,6 +35,8 @@ namespace sat {
unsigned id = c.id();
if (id >= m_id2pos.size())
return;
if (empty())
return;
unsigned pos = m_id2pos[id];
if (pos == UINT_MAX)
return;
@ -52,7 +54,11 @@ namespace sat {
clause & clause_set::erase() {
SASSERT(!empty());
clause & c = *m_set.back();
m_id2pos[c.id()] = UINT_MAX;
SASSERT(c.id() < m_id2pos.size());
SASSERT(m_id2pos[c.id()] == m_set.size()-1);
if (c.id() < m_id2pos.size()) {
m_id2pos[c.id()] = UINT_MAX;
}
m_set.pop_back();
return c;
}

26
src/smt/theory_arith_core.h
View file

@ -1866,7 +1866,7 @@ namespace smt {
template<typename Ext>
template<bool Lazy>
void theory_arith<Ext>::pivot(theory_var x_i, theory_var x_j, numeral const & a_ij, bool apply_gcd_test) {
TRACE("arith_pivot", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";);
TRACE("arith_pivoting", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";);
m_stats.m_pivots++;
SASSERT(is_base(x_i) || is_quasi_base(x_i));
SASSERT(x_i != x_j);
@ -2067,14 +2067,14 @@ namespace smt {
theory_var max = get_num_vars();
theory_var result = max;
row const & r = m_rows[get_var_row(x_i)];
int n;
int best_col_sz = INT_MAX;
int best_so_far = INT_MAX;
typename vector<row_entry>::const_iterator it = r.begin_entries();
int n = 0;
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
for (; it != end; ++it) {
if (!it->is_dead()) {
theory_var x_j = it->m_var;
numeral const & a_ij = it->m_coeff;
@ -2090,14 +2090,14 @@ namespace smt {
best_so_far = num;
best_col_sz = col_sz;
n = 1;
}
}
else if (num == best_so_far && col_sz == best_col_sz) {
n++;
if (m_random()%n == 0) {
result = x_j;
out_a_ij = a_ij;
}
}
}
}
}
}
@ -2174,6 +2174,7 @@ namespace smt {
inf_numeral curr_error;
typename var_heap::iterator it = m_to_patch.begin();
typename var_heap::iterator end = m_to_patch.end();
//unsigned n = 0;
for (; it != end; ++it) {
theory_var v = *it;
if (below_lower(v))
@ -2188,7 +2189,16 @@ namespace smt {
<< ", best_error: " << best_error << ", curr_error: " << curr_error << "\n";);
best = v;
best_error = curr_error;
//n = 2;
}
#if 0
else if (false && n > 0 && curr_error == best_error) {
n++;
if (m_random()%n == 0) {
best = v;
}
}
#endif
}
if (best == null_theory_var)
m_to_patch.clear(); // all variables are satisfied

6
src/smt/theory_seq.cpp
View file

@ -2380,7 +2380,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id());
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
@ -2469,7 +2469,9 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
for (unsigned i = 0; i < concats.size(); ++i) {
expr* c = concats[i], *c1;
if (m_util.str.is_unit(c, c1)) {
sv->add_dependency(ctx.get_enode(c1));
if (ctx.e_internalized(c1)) {
sv->add_dependency(ctx.get_enode(c1));
}
}
else if (m_util.str.is_string(c)) {
sv->add_string(c);

25
src/smt/theory_seq_empty.h
View file

@ -25,6 +25,7 @@ Revision History:
namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
proto_model& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
@ -34,8 +35,9 @@ namespace smt {
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid):
seq_factory(ast_manager & m, family_id fid, proto_model& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
@ -78,6 +80,17 @@ namespace smt {
v2 = u.str.mk_string(symbol("b"));
return true;
}
sort* ch;
if (u.is_seq(s, ch)) {
if (m_model.get_some_values(ch, v1, v2)) {
v1 = u.str.mk_unit(v1);
v2 = u.str.mk_unit(v2);
return true;
}
else {
return false;
}
}
NOT_IMPLEMENTED_YET();
return false;
}
@ -92,7 +105,7 @@ namespace smt {
return u.str.mk_string(sym);
}
}
sort* seq = 0;
sort* seq = 0, *ch = 0;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
@ -102,7 +115,11 @@ namespace smt {
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
NOT_IMPLEMENTED_YET();
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
return u.str.mk_unit(v);
}
UNREACHABLE();
return 0;
}
virtual void register_value(expr* n) {
@ -126,7 +143,7 @@ namespace smt {
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
virtual void init_model(model_generator & mg) {
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id()));
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
}
};