mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-19 16:33:34 -07:00
commit 8241ba784d
11 changed files with 159 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.travis.yml
View file

@ -84,7 +84,7 @@ matrix:
- os: osx
osx_image: xcode8.3
# Note: Apple Clang does not support OpenMP
env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0
script:
# Use `travis_wait` when doing LTO builds because this configuration will
# have long link times during which it will not show any output which

7
cmake/modules/FindDotNetToolchain.cmake
View file

@ -33,13 +33,18 @@ if (DOTNET_CSC_EXECUTABLE)
set(DOTNET_TOOLCHAIN_IS_MONO TRUE)
set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE)
message(STATUS ".NET toolchain is Mono")
elseif ("${CSC_STD_OUT}" MATCHES "^Turbo[ ]+C#")
set(DOTNET_DETERMINED_VENDOR TRUE)
set(DOTNET_TOOLCHAIN_IS_MONO TRUE)
set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE)
message(STATUS ".NET toolchain is Mono")
elseif ("${CSC_STD_OUT}" MATCHES "^Microsoft.+Visual[ ]+C#")
set(DOTNET_DETERMINED_VENDOR TRUE)
set(DOTNET_TOOLCHAIN_IS_MONO FALSE)
set(DOTNET_TOOLCHAIN_IS_WINDOWS TRUE)
message(STATUS ".NET toolchain is Windows native")
else()
message(STATUS ".NET toolchain is unknown")
message(STATUS ".NET toolchain is unknown: ${CSC_STD_OUT}")
endif()
endif()
endif()

129
src/ast/rewriter/arith_rewriter.cpp
View file

@ -800,52 +800,105 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
result = m_util.mk_numeral(div(v1, v2), is_int);
return BR_DONE;
}
expr_ref quot(m());
if (divides(arg1, arg2, quot)) {
result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
return BR_REWRITE2;
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
result = arg1;
return BR_DONE;
}
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
return BR_FAILED;
}
if (arg1 == arg2) {
expr_ref zero(m_util.mk_int(0), m());
result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
return BR_REWRITE3;
}
if (divides(arg1, arg2, result)) {
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
if (d == n) {
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
//
// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
//
bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
expr_fast_mark1 mark;
rational num_r(1), den_r(1);
expr* num_e = nullptr, *den_e = nullptr;
ptr_buffer<expr> args1, args2;
flat_mul(num, args1);
flat_mul(den, args2);
for (expr * arg : args1) {
mark.mark(arg);
if (m_util.is_numeral(arg, num_r)) num_e = arg;
}
for (expr* arg : args2) {
if (mark.is_marked(arg)) {
result = remove_divisor(arg, num, den);
return true;
}
if (m_util.is_numeral(arg, den_r)) den_e = arg;
}
rational g = gcd(num_r, den_r);
if (!g.is_one()) {
SASSERT(g.is_pos());
// replace num_e, den_e by their gcd reduction.
for (unsigned i = 0; i < args1.size(); ++i) {
if (args1[i] == num_e) {
args1[i] = m_util.mk_numeral(num_r / g, true);
break;
}
}
for (unsigned i = 0; i < args2.size(); ++i) {
if (args2[i] == den_e) {
args2[i] = m_util.mk_numeral(den_r / g, true);
break;
}
}
num = m_util.mk_mul(args1.size(), args1.c_ptr());
den = m_util.mk_mul(args2.size(), args2.c_ptr());
result = m_util.mk_idiv(num, den);
return true;
}
if (m_util.is_mul(n)) {
expr_ref_vector muls(m());
muls.push_back(n);
expr* n1, *n2;
rational r1, r2;
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_mul(muls[i].get(), n1, n2)) {
muls[i] = n1;
muls.push_back(n2);
--i;
}
}
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
for (unsigned i = 0; i < muls.size(); ++i) {
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
}
else {
for (unsigned i = 0; i < muls.size(); ++i) {
if (d == muls[i].get()) {
muls[i] = muls.back();
muls.pop_back();
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
return true;
}
}
return false;
}
expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
ptr_buffer<expr> args1, args2;
flat_mul(num, args1);
flat_mul(den, args2);
remove_divisor(arg, args1);
remove_divisor(arg, args2);
expr_ref zero(m_util.mk_int(0), m());
num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr());
den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr());
return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m());
}
void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
args.push_back(e);
for (unsigned i = 0; i < args.size(); ++i) {
e = args[i];
if (m_util.is_mul(e)) {
args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
args[i] = args.back();
args.shrink(args.size()-1);
--i;
}
}
}
void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
for (unsigned i = 0; i < args.size(); ++i) {
if (args[i] == d) {
args[i] = args.back();
args.shrink(args.size()-1);
return;
}
}
return false;
UNREACHABLE();
}
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {

5
src/ast/rewriter/arith_rewriter.h
View file

@ -95,7 +95,10 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
expr_ref neg_monomial(expr * e) const;
expr * mk_sin_value(rational const & k);
app * mk_sqrt(rational const & k);
bool divides(expr* d, expr* n, expr_ref& quot);
bool divides(expr* d, expr* n, expr_ref& result);
expr_ref remove_divisor(expr* arg, expr* num, expr* den);
void flat_mul(expr* e, ptr_buffer<expr>& args);
void remove_divisor(expr* d, ptr_buffer<expr>& args);
public:
arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):

32
src/smt/mam.cpp
View file

@ -865,9 +865,7 @@ namespace smt {
That is, during execution time, the variables will be already bound
*/
bool all_args_are_bound_vars(app * n) {
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr* arg : *n) {
if (!is_var(arg))
return false;
if (m_vars[to_var(arg)->get_idx()] == -1)
@ -884,9 +882,7 @@ namespace smt {
if (n->is_ground()) {
return;
}
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr* arg : *n) {
if (is_var(arg)) {
sz++;
unsigned var_id = to_var(arg)->get_idx();
@ -928,10 +924,7 @@ namespace smt {
unsigned first_app_sz;
unsigned first_app_num_unbound_vars;
// generate first the non-BIND operations
unsigned_vector::iterator it = m_todo.begin();
unsigned_vector::iterator end = m_todo.end();
for (; it != end; ++it) {
unsigned reg = *it;
for (unsigned reg : m_todo) {
expr * p = m_registers[reg];
SASSERT(!is_quantifier(p));
if (is_var(p)) {
@ -1249,10 +1242,7 @@ namespace smt {
SASSERT(head->m_next == 0);
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
ptr_vector<instruction>::iterator it = m_seq.begin();
ptr_vector<instruction>::iterator end = m_seq.end();
for (; it != end; ++it) {
instruction * curr = *it;
for (instruction * curr : m_seq) {
head->m_next = curr;
head = curr;
}
@ -1495,10 +1485,8 @@ namespace smt {
}
if (num_instr > SIMPLE_SEQ_THRESHOLD || (curr != nullptr && curr->m_opcode == CHOOSE))
simple = false;
unsigned_vector::iterator it = m_to_reset.begin();
unsigned_vector::iterator end = m_to_reset.end();
for (; it != end; ++it)
m_registers[*it] = 0;
for (unsigned reg : m_to_reset)
m_registers[reg] = 0;
return weight;
}
@ -1716,11 +1704,9 @@ namespace smt {
m_num_choices++;
// set: head -> c1 -> c2 -> c3 -> new_child_head1
curr = head;
ptr_vector<instruction>::iterator it1 = m_compatible.begin();
ptr_vector<instruction>::iterator end1 = m_compatible.end();
for (; it1 != end1; ++it1) {
set_next(curr, *it1);
curr = *it1;
for (instruction* instr : m_compatible) {
set_next(curr, instr);
curr = instr;
}
set_next(curr, new_child_head1);
// set: new_child_head1:CHOOSE(new_child_head2) -> i1 -> i2 -> first_child_head

16
src/smt/proto_model/proto_model.cpp
View file

@ -342,10 +342,16 @@ void proto_model::compress() {
\brief Complete the interpretation fi of f if it is partial.
If f does not have an interpretation in the given model, then this is a noop.
*/
void proto_model::complete_partial_func(func_decl * f) {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = fi->get_max_occ_result();
expr * else_value;
if (use_fresh) {
else_value = get_fresh_value(f->get_range());
}
else {
else_value = fi->get_max_occ_result();
}
if (else_value == nullptr)
else_value = get_some_value(f->get_range());
fi->set_else(else_value);
@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) {
/**
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
void proto_model::complete_partial_funcs(bool use_fresh) {
if (m_model_partial)
return;
// m_func_decls may be "expanded" when we invoke get_some_value.
// So, we must not use iterators to traverse it.
for (unsigned i = 0; i < m_func_decls.size(); i++) {
complete_partial_func(m_func_decls[i]);
for (unsigned i = 0; i < m_func_decls.size(); ++i) {
complete_partial_func(m_func_decls.get(i), use_fresh);
}
}

4
src/smt/proto_model/proto_model.h
View file

@ -100,8 +100,8 @@ public:
//
// Complete partial function interps
//
void complete_partial_func(func_decl * f);
void complete_partial_funcs();
void complete_partial_func(func_decl * f, bool use_fresh);
void complete_partial_funcs(bool use_fresh);
//
// Create final model object.

2
src/smt/smt_context.cpp
View file

@ -4364,7 +4364,7 @@ namespace smt {
m_proto_model = m_model_generator->mk_model();
m_qmanager->adjust_model(m_proto_model.get());
TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
m_proto_model->complete_partial_funcs();
m_proto_model->complete_partial_funcs(false);
TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
m_proto_model->cleanup();
if (m_fparams.m_model_compact)

2
src/smt/smt_model_finder.cpp
View file

@ -1028,7 +1028,7 @@ namespace smt {
void complete_partial_funcs(func_decl_set const & partial_funcs) {
for (func_decl * f : partial_funcs) {
// Complete the current interpretation
m_model->complete_partial_func(f);
m_model->complete_partial_func(f, true);
unsigned arity = f->get_arity();
func_interp * fi = m_model->get_func_interp(f);

33
src/smt/theory_arith_core.h
View file

@ -508,13 +508,14 @@ namespace smt {
mk_axiom(eqz, lower, !is_numeral);
mk_axiom(eqz, upper, !is_numeral);
rational k;
context& ctx = get_context();
(void)ctx;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) {
rational j(0);
#if 1
literal_buffer lits;
expr_ref mod_j(m);
context& ctx = get_context();
while(j < k) {
mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true));
ctx.internalize(mod_j, false);
@ -542,6 +543,36 @@ namespace smt {
}
#endif
}
#if 0
// e-matching is too restrictive for multiplication.
// also suffers from use-after free so formulas have to be pinned in solver.
//
if (!m_util.is_numeral(divisor)) {
//
// forall x . (or (= y 0) (= (div (* x y) y) x))
// forall x . (=> (= y 0) (= (div (* x y) y) (div 0 0)))
//
sort* intS = m_util.mk_int();
var_ref v(m.mk_var(0, intS), m);
app_ref mul(m_util.mk_mul(divisor, v), m);
app_ref div(m_util.mk_idiv(mul, divisor), m);
expr_ref divp1(m.mk_pattern(div), m);
app_ref mul2(m_util.mk_mul(v, divisor), m);
app_ref div2(m_util.mk_idiv(mul2, divisor), m);
expr_ref divp2(m.mk_pattern(div2), m);
expr_ref fml1(m.mk_or(m.mk_not(eqz), m.mk_eq(div, m_util.mk_idiv(zero, zero))), m);
expr_ref fml2(m.mk_or(eqz, m.mk_eq(div, v)), m);
symbol name("?x");
expr* pats[2] = { divp1, divp2 };
expr_ref fml(m);
fml = m.mk_forall(1, &intS, &name, fml1, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
proof_ref pr(m.mk_asserted(fml), m);
ctx.internalize_assertion(fml, pr, 0);
fml = m.mk_forall(1, &intS, &name, fml2, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
pr = m.mk_asserted(fml);
ctx.internalize_assertion(fml, pr, 0);
}
#endif
}
}

2
src/smt/theory_fpa.h
View file

@ -62,7 +62,7 @@ namespace smt {
return true;
}
expr * get_fresh_value(sort * s) override { NOT_IMPLEMENTED_YET(); }
expr * get_fresh_value(sort * s) override { return get_some_value(s); }
void register_value(expr * n) override { /* Ignore */ }
app * mk_value(mpf const & x) {