mirror of
https://github.com/Z3Prover/z3
synced 2025-07-22 04:12:05 +00:00
Merge branch 'opt' of https://git01.codeplex.com/z3 into opt
This commit is contained in:
commit
28fb266d8c
3 changed files with 49 additions and 103 deletions
|
@ -65,22 +65,29 @@ namespace Microsoft.Z3
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Checks whether the assertions in the context are consistent or not.
|
/// Checks whether the assertions in the context are consistent or not.
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public static Status Check(Context ctx, List<BoolExpr> core, params Expr[] assumptions)
|
public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
|
||||||
{
|
{
|
||||||
Z3_lbool r;
|
Z3_lbool r;
|
||||||
core = null;
|
model = null;
|
||||||
|
proof = null;
|
||||||
if (assumptions == null || assumptions.Length == 0)
|
if (assumptions == null || assumptions.Length == 0)
|
||||||
r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
|
r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
|
||||||
else {
|
else {
|
||||||
IntPtr model = IntPtr.Zero, proof = IntPtr.Zero;
|
IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
|
||||||
uint core_size = 0;
|
uint core_size = 0;
|
||||||
IntPtr[] native_core = new IntPtr[assumptions.Length];
|
IntPtr[] native_core = new IntPtr[assumptions.Length];
|
||||||
r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
|
r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
|
||||||
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
|
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
|
||||||
ref model, ref proof, ref core_size, native_core);
|
ref mdl, ref prf, ref core_size, native_core);
|
||||||
|
|
||||||
for (uint i = 0; i < core_size; i++)
|
for (uint i = 0; i < core_size; i++)
|
||||||
core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
|
core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
|
||||||
|
if (mdl != IntPtr.Zero) {
|
||||||
|
model = new Model(ctx, mdl);
|
||||||
|
}
|
||||||
|
if (prf != IntPtr.Zero) {
|
||||||
|
proof = Expr.Create(ctx, prf);
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
switch (r)
|
switch (r)
|
||||||
|
|
|
@ -904,12 +904,17 @@ namespace datalog {
|
||||||
else if (m.is_not(g, e1)) {
|
else if (m.is_not(g, e1)) {
|
||||||
udoc sub;
|
udoc sub;
|
||||||
sub.push_back(dm.allocateX());
|
sub.push_back(dm.allocateX());
|
||||||
apply_guard(e1, sub, equalities, discard_cols);
|
// TODO: right now we state that no columns are discarded to avoid
|
||||||
|
// silent column merging. This can be optimized if the set of merged
|
||||||
|
// columns is returned so that here we remove different columns.
|
||||||
|
bit_vector empty;
|
||||||
|
empty.resize(discard_cols.size(), false);
|
||||||
|
apply_guard(e1, sub, equalities, empty);
|
||||||
|
result.subtract(dm, sub);
|
||||||
|
result.simplify(dm);
|
||||||
TRACE("doc",
|
TRACE("doc",
|
||||||
result.display(dm, tout << "result0:") << "\n";
|
result.display(dm, tout << "result0:") << "\n";
|
||||||
sub.display(dm, tout << "sub:") << "\n";);
|
sub.display(dm, tout << "sub:") << "\n";);
|
||||||
result.subtract(dm, sub);
|
|
||||||
result.simplify(dm);
|
|
||||||
sub.reset(dm);
|
sub.reset(dm);
|
||||||
TRACE("doc", result.display(dm, tout << "result:") << "\n";);
|
TRACE("doc", result.display(dm, tout << "result:") << "\n";);
|
||||||
}
|
}
|
||||||
|
@ -1022,7 +1027,7 @@ namespace datalog {
|
||||||
return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0;
|
return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0;
|
||||||
}
|
}
|
||||||
|
|
||||||
class udoc_plugin::join_project_fn : convenient_relation_join_project_fn {
|
class udoc_plugin::join_project_fn : public convenient_relation_join_project_fn {
|
||||||
udoc_plugin::join_fn m_joiner;
|
udoc_plugin::join_fn m_joiner;
|
||||||
union_find_default_ctx union_ctx;
|
union_find_default_ctx union_ctx;
|
||||||
bit_vector m_to_delete;
|
bit_vector m_to_delete;
|
||||||
|
@ -1114,18 +1119,21 @@ namespace datalog {
|
||||||
utbv& neg = d->neg();
|
utbv& neg = d->neg();
|
||||||
unsigned mid = dm1.num_tbits();
|
unsigned mid = dm1.num_tbits();
|
||||||
unsigned hi = dm.num_tbits();
|
unsigned hi = dm.num_tbits();
|
||||||
tbm.set(pos,d1.pos(), mid-1, 0);
|
tbm.set(pos, d1.pos(), mid-1, 0);
|
||||||
tbm.set(pos,d2.pos(), hi-1, mid);
|
tbm.set(pos, d2.pos(), hi-1, mid);
|
||||||
for (unsigned i = 0; i < d1.neg().size(); ++i) {
|
for (unsigned i = 0; i < d1.neg().size(); ++i) {
|
||||||
t = tbm.allocateX();
|
t = tbm.allocateX();
|
||||||
tbm.set(*t, d1.neg()[i], mid-1, 0);
|
tbm.set(*t, d1.neg()[i], mid-1, 0);
|
||||||
|
VERIFY(tbm.set_and(*t, pos));
|
||||||
neg.push_back(t.detach());
|
neg.push_back(t.detach());
|
||||||
}
|
}
|
||||||
for (unsigned i = 0; i < d2.neg().size(); ++i) {
|
for (unsigned i = 0; i < d2.neg().size(); ++i) {
|
||||||
t = tbm.allocateX();
|
t = tbm.allocateX();
|
||||||
tbm.set(*t, d2.neg()[i], hi-1, mid);
|
tbm.set(*t, d2.neg()[i], hi-1, mid);
|
||||||
|
VERIFY(tbm.set_and(*t, pos));
|
||||||
neg.push_back(t.detach());
|
neg.push_back(t.detach());
|
||||||
}
|
}
|
||||||
|
SASSERT(dm.well_formed(*d));
|
||||||
return d.detach();
|
return d.detach();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1135,15 +1143,11 @@ namespace datalog {
|
||||||
relation_base const& t1, relation_base const& t2,
|
relation_base const& t1, relation_base const& t2,
|
||||||
unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2,
|
unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2,
|
||||||
unsigned removed_col_cnt, const unsigned * removed_cols) {
|
unsigned removed_col_cnt, const unsigned * removed_cols) {
|
||||||
if (check_kind(t1) && check_kind(t2))
|
if (!check_kind(t1) || !check_kind(t2))
|
||||||
return 0;
|
return 0;
|
||||||
#if 0
|
return alloc(join_project_fn, get(t1), get(t2),
|
||||||
return alloc(join_project_fn, get(t1), ge(t2),
|
|
||||||
joined_col_cnt, cols1, cols2,
|
joined_col_cnt, cols1, cols2,
|
||||||
removed_col_cnt, removed_cols);
|
removed_col_cnt, removed_cols);
|
||||||
#endif
|
|
||||||
else
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -376,15 +376,31 @@ public:
|
||||||
unsigned_vector remove;
|
unsigned_vector remove;
|
||||||
remove.push_back(0);
|
remove.push_back(0);
|
||||||
remove.push_back(2);
|
remove.push_back(2);
|
||||||
|
|
||||||
t1 = mk_full(sig2);
|
t1 = mk_full(sig2);
|
||||||
|
apply_filter(*t1, conds[2].get());
|
||||||
|
apply_filter_project(*t1, remove, conds[2].get());
|
||||||
|
apply_filter_project(*t1, remove, conds[3].get());
|
||||||
|
t1->deallocate();
|
||||||
|
|
||||||
|
t1 = mk_full(sig2);
|
||||||
|
apply_filter(*t1, conds[3].get());
|
||||||
|
apply_filter_project(*t1, remove, conds[2].get());
|
||||||
|
apply_filter_project(*t1, remove, conds[3].get());
|
||||||
|
t1->deallocate();
|
||||||
|
|
||||||
for (unsigned i = 0; i < conds.size(); ++i) {
|
for (unsigned i = 0; i < conds.size(); ++i) {
|
||||||
|
t1 = mk_full(sig2);
|
||||||
apply_filter_project(*t1, remove, conds[i].get());
|
apply_filter_project(*t1, remove, conds[i].get());
|
||||||
|
t1->deallocate();
|
||||||
}
|
}
|
||||||
|
|
||||||
remove[1] = 1;
|
remove[1] = 1;
|
||||||
for (unsigned i = 0; i < conds.size(); ++i) {
|
for (unsigned i = 0; i < conds.size(); ++i) {
|
||||||
|
t1 = mk_full(sig2);
|
||||||
apply_filter_project(*t1, remove, conds[i].get());
|
apply_filter_project(*t1, remove, conds[i].get());
|
||||||
|
t1->deallocate();
|
||||||
}
|
}
|
||||||
t1->deallocate();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@ -476,52 +492,13 @@ public:
|
||||||
scoped_ptr<datalog::relation_transformer_fn> rename;
|
scoped_ptr<datalog::relation_transformer_fn> rename;
|
||||||
rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr());
|
rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr());
|
||||||
relation_base* t = (*rename)(*t1);
|
relation_base* t = (*rename)(*t1);
|
||||||
verify_permutation(*t1,*t, cycle);
|
cr.verify_permutation(*t1,*t, cycle);
|
||||||
t1->display(std::cout); std::cout << "\n";
|
t1->display(std::cout); std::cout << "\n";
|
||||||
t->display(std::cout); std::cout << "\n";
|
t->display(std::cout); std::cout << "\n";
|
||||||
t->deallocate();
|
t->deallocate();
|
||||||
t1->deallocate();
|
t1->deallocate();
|
||||||
}
|
}
|
||||||
|
|
||||||
void verify_permutation(relation_base const& src, relation_base const& dst,
|
|
||||||
unsigned_vector const& cycle) {
|
|
||||||
unsigned_vector perm;
|
|
||||||
relation_signature const& sig1 = src.get_signature();
|
|
||||||
relation_signature const& sig2 = dst.get_signature();
|
|
||||||
for (unsigned i = 0; i < sig1.size(); ++i) {
|
|
||||||
perm.push_back(i);
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < cycle.size(); ++i) {
|
|
||||||
unsigned j = (i + 1)%cycle.size();
|
|
||||||
unsigned col1 = cycle[i];
|
|
||||||
unsigned col2 = cycle[j];
|
|
||||||
perm[col2] = col1;
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < perm.size(); ++i) {
|
|
||||||
SASSERT(sig2[perm[i]] == sig1[i]);
|
|
||||||
}
|
|
||||||
expr_ref_vector sub(m);
|
|
||||||
for (unsigned i = 0; i < perm.size(); ++i) {
|
|
||||||
sub.push_back(m.mk_var(perm[i], sig1[i]));
|
|
||||||
}
|
|
||||||
var_subst subst(m, false);
|
|
||||||
expr_ref fml1(m), fml2(m);
|
|
||||||
src.to_formula(fml1);
|
|
||||||
dst.to_formula(fml2);
|
|
||||||
subst(fml1, sub.size(), sub.c_ptr(), fml1);
|
|
||||||
expr_ref_vector vars(m);
|
|
||||||
for (unsigned i = 0; i < sig2.size(); ++i) {
|
|
||||||
std::stringstream strm;
|
|
||||||
strm << "x" << i;
|
|
||||||
vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig2[i]));
|
|
||||||
}
|
|
||||||
|
|
||||||
subst(fml1, vars.size(), vars.c_ptr(), fml1);
|
|
||||||
subst(fml2, vars.size(), vars.c_ptr(), fml2);
|
|
||||||
|
|
||||||
check_equiv(fml1, fml2);
|
|
||||||
}
|
|
||||||
|
|
||||||
/*
|
/*
|
||||||
The filter_by_negation postcondition:
|
The filter_by_negation postcondition:
|
||||||
filter_by_negation(tgt, neg, columns in tgt: c1,...,cN,
|
filter_by_negation(tgt, neg, columns in tgt: c1,...,cN,
|
||||||
|
@ -733,51 +710,9 @@ public:
|
||||||
void apply_filter_project(udoc_relation& t, unsigned_vector const& rm, app* cond) {
|
void apply_filter_project(udoc_relation& t, unsigned_vector const& rm, app* cond) {
|
||||||
scoped_ptr<datalog::relation_transformer_fn> rt;
|
scoped_ptr<datalog::relation_transformer_fn> rt;
|
||||||
rt = p.mk_filter_interpreted_and_project_fn(t, cond, rm.size(), rm.c_ptr());
|
rt = p.mk_filter_interpreted_and_project_fn(t, cond, rm.size(), rm.c_ptr());
|
||||||
udoc_relation* full = mk_full(t.get_signature());
|
|
||||||
rel_union union_fn = p.mk_union_fn(t, *full, 0);
|
|
||||||
(*union_fn)(t, *full, 0);
|
|
||||||
datalog::relation_base* result = (*rt)(t);
|
datalog::relation_base* result = (*rt)(t);
|
||||||
|
cr.verify_filter_project(t, *result, cond, rm);
|
||||||
for (unsigned i = 0; i < rm.size(); ++i) {
|
|
||||||
std::cout << rm[i] << " ";
|
|
||||||
}
|
|
||||||
std::cout << mk_pp(cond, m) << "\n";
|
|
||||||
t.display(std::cout);
|
|
||||||
result->display(std::cout);
|
|
||||||
result->deallocate();
|
result->deallocate();
|
||||||
full->deallocate();
|
|
||||||
}
|
|
||||||
|
|
||||||
void verify_filter_project(udoc_relation const& r, unsigned_vector const& rm, app* cond) {
|
|
||||||
expr_ref fml(m), cfml(m);
|
|
||||||
r.to_formula(fml);
|
|
||||||
cfml = cond;
|
|
||||||
relation_signature const& sig = r.get_signature();
|
|
||||||
expr_ref_vector vars(m);
|
|
||||||
for (unsigned i = 0, j = 0, k = 0; i < sig.size(); ++i) {
|
|
||||||
if (j < rm.size() && rm[j] == i) {
|
|
||||||
project_var(i, sig[i], cfml);
|
|
||||||
++j;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
vars.push_back(m.mk_var(k, sig[i]));
|
|
||||||
++k;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
check_equiv(fml, cfml);
|
|
||||||
}
|
|
||||||
|
|
||||||
void check_equiv(expr* fml1, expr* fml2) {
|
|
||||||
TRACE("doc", tout << mk_pp(fml1, m) << "\n";
|
|
||||||
tout << mk_pp(fml2, m) << "\n";);
|
|
||||||
smt_params fp;
|
|
||||||
smt::kernel solver(m, fp);
|
|
||||||
expr_ref tmp(m);
|
|
||||||
tmp = m.mk_not(m.mk_eq(fml1, fml2));
|
|
||||||
solver.assert_expr(tmp);
|
|
||||||
lbool res = solver.check();
|
|
||||||
SASSERT(res == l_false);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void project_var(unsigned i, sort* s, expr_ref& fml) {
|
void project_var(unsigned i, sort* s, expr_ref& fml) {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue