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

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-06 14:51:25 +01:00
commit 7534b53bae
16 changed files with 1033 additions and 79 deletions
Download patch file Download diff file Expand all files Collapse all files

2
contrib/cmake/src/ast/rewriter/CMakeLists.txt
View file

@ -20,6 +20,8 @@ z3_add_component(rewriter
seq_rewriter.cpp
th_rewriter.cpp
var_subst.cpp
bv_trailing.cpp
mk_extract_proc.cpp
COMPONENT_DEPENDENCIES
ast
automata

5
src/api/z3_api.h
View file

@ -4538,6 +4538,9 @@ extern "C" {
If \c model_completion is Z3_TRUE, then Z3 will assign an interpretation for any constant or function that does
not have an interpretation in \c m. These constants and functions were essentially don't cares.
If \c model_completion is Z3_FALSE, then Z3 will not assign interpretations to constants for functions that do
not have interpretations in \c m. Evaluation behaves as the identify function in this case.
The evaluation may fail for the following reasons:
- \c t contains a quantifier.
@ -4547,6 +4550,8 @@ extern "C" {
- \c t is type incorrect.
- \c Z3_interrupt was invoked during evaluation.
def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
*/
Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);

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

@ -22,45 +22,13 @@ Notes:
#include"ast_smt2_pp.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),
m_low(UINT_MAX),
m_domain(0),
m_f_cached(0) {
}
mk_extract_proc::~mk_extract_proc() {
if (m_f_cached) {
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
ast_manager & m = m_util.get_manager();
m.dec_ref(m_f_cached);
}
}
app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
ast_manager & m = m_util.get_manager();
sort * s = m.get_sort(arg);
if (m_low == low && m_high == high && m_domain == s)
return m.mk_app(m_f_cached, arg);
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
if (m_f_cached)
m.dec_ref(m_f_cached);
app * r = to_app(m_util.mk_extract(high, low, arg));
m_high = high;
m_low = low;
m_domain = s;
m_f_cached = r->get_decl();
m.inc_ref(m_f_cached);
return r;
}
void bv_rewriter::updt_local_params(params_ref const & _p) {
bv_rewriter_params p(_p);
m_hi_div0 = p.hi_div0();
m_elim_sign_ext = p.elim_sign_ext();
m_mul2concat = p.mul2concat();
m_bit2bool = p.bit2bool();
m_trailing = p.bv_trailing();
m_blast_eq_value = p.blast_eq_value();
m_split_concat_eq = p.split_concat_eq();
m_udiv2mul = p.udiv2mul();
@ -2124,6 +2092,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return st;
}
if (m_trailing) {
st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
m_rm_trailing.reset_cache(1 << 12);
if (st != BR_FAILED) {
TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
return st;
}
}
st = mk_mul_eq(lhs, rhs, result);
if (st != BR_FAILED) {
TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
@ -2187,6 +2164,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
return BR_FAILED;
}
br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
if (m_mkbv2num) {
unsigned i;

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

@ -22,18 +22,8 @@ Notes:
#include"poly_rewriter.h"
#include"bv_decl_plugin.h"
#include"arith_decl_plugin.h"
class mk_extract_proc {
bv_util & m_util;
unsigned m_high;
unsigned m_low;
sort * m_domain;
func_decl * m_f_cached;
public:
mk_extract_proc(bv_util & u);
~mk_extract_proc();
app * operator()(unsigned high, unsigned low, expr * arg);
};
#include"mk_extract_proc.h"
#include"bv_trailing.h"
class bv_rewriter_core {
protected:
@ -58,6 +48,7 @@ public:
class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
mk_extract_proc m_mk_extract;
bv_trailing m_rm_trailing;
arith_util m_autil;
bool m_hi_div0;
bool m_elim_sign_ext;
@ -69,6 +60,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_udiv2mul;
bool m_bvnot2arith;
bool m_bv_sort_ac;
bool m_trailing;
bool is_zero_bit(expr * x, unsigned idx);
@ -148,6 +140,7 @@ public:
bv_rewriter(ast_manager & m, params_ref const & p = params_ref()):
poly_rewriter<bv_rewriter_core>(m, p),
m_mk_extract(m_util),
m_rm_trailing(m_mk_extract),
m_autil(m) {
updt_local_params(p);
}

3
src/ast/rewriter/bv_rewriter_params.pyg
View file

@ -9,5 +9,6 @@ def_module_params(module_name='rewriter',
("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators")
("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
("bv_trailing", BOOL, False, "lean removal of trailing zeros")
))

404
src/ast/rewriter/bv_trailing.cpp Normal file
View file

@ -0,0 +1,404 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
bv_trailing.cpp
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#include"bv_trailing.h"
#include"bv_decl_plugin.h"
#include"ast_smt2_pp.h"
// The analyzer gives up analysis after going TRAILING_DEPTH deep.
// This number shouldn't be too big.
#define TRAILING_DEPTH 5
struct bv_trailing::imp {
typedef rational numeral;
typedef obj_map<expr, std::pair<unsigned,unsigned> > map;
mk_extract_proc& m_mk_extract;
bv_util& m_util;
ast_manager& m_m;
// keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level
map* m_count_cache[TRAILING_DEPTH + 1];
imp(mk_extract_proc& mk_extract)
: m_mk_extract(mk_extract)
, m_util(mk_extract.bvutil())
, m_m(mk_extract.m()) {
for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
m_count_cache[i] = NULL;
}
virtual ~imp() {
reset_cache(0);
}
ast_manager & m() const { return m_util.get_manager(); }
br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m()) << "\n=\n" << mk_ismt2_pp(e2, m()) << "\n";);
SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2));
SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2));
unsigned max1, min1, max2, min2;
count_trailing(e1, min1, max1, TRAILING_DEPTH);
count_trailing(e2, min2, max2, TRAILING_DEPTH);
if (min1 > max2 || min2 > max1) { // bounds have empty intersection
result = m().mk_false();
return BR_DONE;
}
const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds
if (min == 0) { // nothing to remove
result = m().mk_eq(e1, e2);
return BR_FAILED;
}
const unsigned sz = m_util.get_bv_size(e1);
if (min == sz) { // everything removed, unlikely but we check anyhow for safety
result = m().mk_true();
return BR_DONE;
}
expr_ref out1(m());
expr_ref out2(m());
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min);
const bool are_eq = m().are_equal(out1, out2);
result = are_eq ? m().mk_true() : m().mk_eq(out1, out2);
return are_eq ? BR_DONE : BR_REWRITE2;
}
// This routine needs to be implemented carefully so that whenever it
// returns a lower bound on trailing zeros min, the routine remove_trailing
// must be capable of removing at least that many zeros from the expression.
void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
SASSERT(e && m_util.is_bv(e));
if (is_cached(depth, e, min, max)) return;
count_trailing_core(e, min, max, depth);
TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n:" << min << " - " << max << "\n";);
SASSERT(min <= max);
SASSERT(max <= m_util.get_bv_size(e));
cache(depth, e, min, max); // store result into the cache
}
unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
const unsigned retv = remove_trailing_core(e, n, result, depth);
CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m()) << "\n--->\n" << mk_ismt2_pp(result.get(), m()) << "\n";);
CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m()) << "\n---> [EMPTY]\n";);
return retv;
}
// Assumes that count_trailing gives me a lower bound that we can also remove from each summand.
unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv_add(a));
const unsigned num = a->get_num_args();
if (depth <= 1) {
result = a;
return 0;
}
unsigned min, max;
count_trailing(a, min, max, depth); // caching is important here
const unsigned to_rm = std::min(min, n);
if (to_rm == 0) {
result = a;
return 0;
}
const unsigned sz = m_util.get_bv_size(a);
if (to_rm == sz) {
result = NULL;
return sz;
}
expr_ref_vector new_args(m());
expr_ref tmp(m());
for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i);
const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1);
new_args.push_back(tmp);
SASSERT(crm == to_rm);
}
result = m().mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
return to_rm;
}
unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv_mul(a));
const unsigned num = a->get_num_args();
if (depth <= 1 || !num) {
result = a;
return 0;
}
expr_ref tmp(m());
expr * const coefficient = a->get_arg(0);
const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1);
SASSERT(retv <= n);
if (retv == 0) {
result = a;
return 0;
}
expr_ref_vector new_args(m());
numeral c_val;
unsigned c_sz;
if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
new_args.push_back(tmp);
const unsigned sz = m_util.get_bv_size(coefficient);
const unsigned new_sz = sz - retv;
if (!new_sz) {
result = NULL;
return retv;
}
SASSERT(m_util.get_bv_size(tmp) == new_sz);
for (unsigned i = 1; i < num; i++) {
expr * const curr = a->get_arg(i);
new_args.push_back(m_mk_extract(new_sz - 1, 0, curr));
}
switch (new_args.size()) {
case 0: result = m_util.mk_numeral(1, new_sz); break;
case 1: result = new_args.get(0); break;
default: result = m().mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
}
return retv;
}
unsigned remove_trailing_concat(app * a, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_concat(a));
if (depth <= 1) {
result = a;
return 0;
}
const unsigned num = a->get_num_args();
unsigned retv = 0;
unsigned i = num;
expr_ref new_last(NULL, m());
while (i && retv < n) {
i--;
expr * const curr = a->get_arg(i);
const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
const unsigned curr_sz = m_util.get_bv_size(curr);
retv += cur_rm;
if (cur_rm < curr_sz) break;
}
if (retv == 0) {
result = a;
return 0;
}
if (!i) {// all args eaten completely
SASSERT(new_last.get() == NULL);
SASSERT(retv == m_util.get_bv_size(a));
result = NULL;
return retv;
}
expr_ref_vector new_args(m());
for (size_t j=0; j<i;++j)
new_args.push_back(a->get_arg(j));
if (new_last.get()) new_args.push_back(new_last);
result = new_args.size() == 1 ? new_args.get(0)
: m_util.mk_concat(new_args.size(), new_args.c_ptr());
return retv;
}
unsigned remove_trailing(size_t max_rm, numeral& a) {
numeral two(2);
unsigned retv = 0;
while (max_rm && a.is_even()) {
div(a, two, a);
++retv;
--max_rm;
}
return retv;
}
unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) {
SASSERT(m_util.is_bv(e));
if (!depth || !n) return 0;
unsigned sz;
unsigned retv = 0;
numeral e_val;
if (m_util.is_numeral(e, e_val, sz)) {
retv = remove_trailing(n, e_val);
const unsigned new_sz = sz - retv;
result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
return retv;
}
if (m_util.is_bv_mul(e))
return remove_trailing_mul(to_app(e), n, result, depth);
if (m_util.is_bv_add(e))
return remove_trailing_add(to_app(e), n, result, depth);
if (m_util.is_concat(e))
return remove_trailing_concat(to_app(e), n, result, depth);
return 0;
}
void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
max = min = 0; // treat empty concat as the empty string
unsigned num = a->get_num_args();
bool update_min = true;
bool update_max = true;
unsigned tmp_min, tmp_max;
while (num-- && update_max) {
expr * const curr = a->get_arg(num);
const unsigned curr_sz = m_util.get_bv_size(curr);
count_trailing(curr, tmp_min, tmp_max, depth - 1);
SASSERT(curr_sz != tmp_min || curr_sz == tmp_max);
max += tmp_max;
if (update_min) min += tmp_min;
// continue updating only if eaten away completely
update_min &= curr_sz == tmp_min;
update_max &= curr_sz == tmp_max;
}
}
void count_trailing_add(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
const unsigned num = a->get_num_args();
const unsigned sz = m_util.get_bv_size(a);
min = max = sz; // treat empty addition as 0
unsigned tmp_min;
unsigned tmp_max;
bool known_parity = true;
bool is_odd = false;
for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i);
count_trailing(curr, tmp_min, tmp_max, depth - 1);
min = std::min(min, tmp_min);
known_parity = known_parity && (!tmp_max || tmp_min);
if (known_parity && !tmp_max) is_odd = !is_odd;
if (!known_parity && !min) break; // no more information can be gained
}
max = known_parity && is_odd ? 0 : sz; // max is known if parity is 1
}
void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) {
if (depth <= 1) {
min = 0;
max = m_util.get_bv_size(a);
}
const unsigned num = a->get_num_args();
if (!num) {
max = min = 0; // treat empty multiplication as 1
return;
}
// assume that numerals are pushed in the front, count only for the first element
expr * const curr = a->get_arg(0);
unsigned tmp_max;
count_trailing(curr, min, tmp_max, depth - 1);
max = num == 1 ? tmp_max : m_util.get_bv_size(a);
return;
}
void count_trailing_core(expr * e, unsigned& min, unsigned& max, unsigned depth) {
if (!depth) {
min = 0;
max = m_util.get_bv_size(e);
return;
}
unsigned sz;
numeral e_val;
if (m_util.is_numeral(e, e_val, sz)) {
min = max = 0;
numeral two(2);
while (sz-- && e_val.is_even()) {
++max;
++min;
div(e_val, two, e_val);
}
return;
}
if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth);
else if (m_util.is_bv_add(e)) count_trailing_add(to_app(e), min, max, depth);
else if (m_util.is_concat(e)) count_trailing_concat(to_app(e), min, max, depth);
else {
min = 0;
max = m_util.get_bv_size(e);
}
}
void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
SASSERT(depth <= TRAILING_DEPTH);
if (depth == 0) return;
if (m_count_cache[depth] == NULL)
m_count_cache[depth] = alloc(map);
m().inc_ref(e);
m_count_cache[depth]->insert(e, std::make_pair(min, max));
TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
}
bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) {
SASSERT(depth <= TRAILING_DEPTH);
if (depth == 0) {
min = 0;
max = m_util.get_bv_size(e);
return true;
}
if (m_count_cache[depth] == NULL)
return false;
const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e);
if (oe == NULL) return false;
min = oe->get_data().m_value.first;
max = oe->get_data().m_value.second;
TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
return true;
}
void reset_cache(unsigned condition) {
SASSERT(m_count_cache[0] == NULL);
for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
if (m_count_cache[i] == NULL) continue;
if (m_count_cache[i]->size() < condition) continue;
map::iterator it = m_count_cache[i]->begin();
map::iterator end = m_count_cache[i]->end();
for (; it != end; ++it) m().dec_ref(it->m_key);
dealloc(m_count_cache[i]);
m_count_cache[i] = NULL;
}
}
};
bv_trailing::bv_trailing(mk_extract_proc& mk_extract) {
m_imp = alloc(imp, mk_extract);
}
bv_trailing::~bv_trailing() {
if (m_imp) dealloc(m_imp);
}
br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
return m_imp->eq_remove_trailing(e1, e2, result);
}
void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) {
m_imp->count_trailing(e, min, max, TRAILING_DEPTH);
}
unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) {
return m_imp->remove_trailing(e, n, result, TRAILING_DEPTH);
}
void bv_trailing::reset_cache(unsigned condition) {
m_imp->reset_cache(condition);
}

46
src/ast/rewriter/bv_trailing.h Normal file
View file

@ -0,0 +1,46 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
bv_trailing.h
Abstract:
A utility to count trailing zeros of an expression. Treats 2x and x++0 equivalently.
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#ifndef BV_TRAILING_H_
#define BV_TRAILING_H_
#include"ast.h"
#include"rewriter_types.h"
#include"mk_extract_proc.h"
class bv_trailing {
public:
bv_trailing(mk_extract_proc& ep);
virtual ~bv_trailing();
public:
// Remove trailing zeros from both sides of an equality (might give False).
br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result);
// Gives a lower and upper bound on trailing zeros in e.
void count_trailing(expr * e, unsigned& min, unsigned& max);
// Attempts removing n trailing zeros from e. Returns how many were successfully removed.
// We're assuming that it can remove at least as many zeros as min returned by count_training.
// Removing the bit-width of e, sets result to NULL.
unsigned remove_trailing(expr * e, unsigned n, expr_ref& result);
// Reset cache(s) if it exceeded size condition.
void reset_cache(unsigned condition);
protected:
struct imp;
imp * m_imp;
};
#endif /* BV_TRAILING_H_ */

49
src/ast/rewriter/mk_extract_proc.cpp Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
mk_extract_proc.cpp
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#include"mk_extract_proc.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),
m_low(UINT_MAX),
m_domain(0),
m_f_cached(0) {
}
mk_extract_proc::~mk_extract_proc() {
if (m_f_cached) {
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
ast_manager & m = m_util.get_manager();
m.dec_ref(m_f_cached);
}
}
app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
ast_manager & m = m_util.get_manager();
sort * s = m.get_sort(arg);
if (m_low == low && m_high == high && m_domain == s)
return m.mk_app(m_f_cached, arg);
// m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
if (m_f_cached)
m.dec_ref(m_f_cached);
app * r = to_app(m_util.mk_extract(high, low, arg));
m_high = high;
m_low = low;
m_domain = s;
m_f_cached = r->get_decl();
m.inc_ref(m_f_cached);
return r;
}

34
src/ast/rewriter/mk_extract_proc.h Normal file
View file

@ -0,0 +1,34 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
mk_extract_proc.h
Abstract:
Author:
Mikolas Janota (MikolasJanota)
Revision History:
--*/
#ifndef MK_EXTRACT_PROC_H_
#define MK_EXTRACT_PROC_H_
#include"ast.h"
#include"bv_decl_plugin.h"
class mk_extract_proc {
bv_util & m_util;
unsigned m_high;
unsigned m_low;
sort * m_domain;
func_decl * m_f_cached;
public:
mk_extract_proc(bv_util & u);
~mk_extract_proc();
app * operator()(unsigned high, unsigned low, expr * arg);
ast_manager & m() { return m_util.get_manager(); }
bv_util & bvutil() { return m_util; }
};
#endif /* MK_EXTRACT_PROC_H_ */

18
src/ast/rewriter/poly_rewriter_def.h
View file

@ -825,15 +825,17 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
if (c_at_rhs) {
c.neg();
normalize(c);
new_rhs_monomials[0] = mk_numeral(c);
lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1);
rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr());
}
else {
new_lhs_monomials[0] = mk_numeral(c);
lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr());
rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1);
}
// When recreating the lhs and rhs also insert coefficient on the appropriate side.
// Ignore coefficient if it's 0 and there are no other summands.
const bool insert_c_lhs = !c_at_rhs && (new_lhs_monomials.size() == 1 || !c.is_zero());
const bool insert_c_rhs = c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero());
const unsigned lhs_offset = insert_c_lhs ? 0 : 1;
const unsigned rhs_offset = insert_c_rhs ? 0 : 1;
new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL;
new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL;
lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
return BR_DONE;
}

88
src/model/model_evaluator.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include"fpa_rewriter.h"
#include"rewriter_def.h"
#include"cooperate.h"
#include"ast_pp.h"
struct evaluator_cfg : public default_rewriter_cfg {
@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
pb_rewriter m_pb_rw;
fpa_rewriter m_f_rw;
seq_rewriter m_seq_rw;
array_util m_ar;
unsigned long long m_max_memory;
unsigned m_max_steps;
bool m_model_completion;
@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_dt_rw(m),
m_pb_rw(m),
m_f_rw(m),
m_seq_rw(m) {
m_seq_rw(m),
m_ar(m) {
bool flat = true;
m_b_rw.set_flat(flat);
m_a_rw.set_flat(flat);
@ -116,6 +119,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (val != 0) {
result = val;
return BR_DONE;
// return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
}
if (m_model_completion) {
@ -146,6 +150,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_f_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
else if (fid == m_ar_rw.get_fid())
st = mk_array_eq(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
@ -182,6 +188,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
return st;
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
@ -230,6 +237,85 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool cache_results() const { return m_cache; }
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
if (a == b) {
result = m().mk_true();
return BR_DONE;
}
vector<expr_ref_vector> stores;
expr_ref else1(m()), else2(m());
if (extract_array_func_interp(a, stores, else1) &&
extract_array_func_interp(b, stores, else2)) {
expr_ref_vector conj(m()), args1(m()), args2(m());
conj.push_back(m().mk_eq(else1, else2));
args1.push_back(a);
args2.push_back(b);
for (unsigned i = 0; i < stores.size(); ++i) {
args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());
expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr());
expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr());
conj.push_back(m().mk_eq(s1, s2));
}
result = m().mk_and(conj.size(), conj.c_ptr());
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
SASSERT(m_ar.is_array(a));
while (m_ar.is_store(a)) {
expr_ref_vector store(m());
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_ar.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
if (m_ar.is_as_array(a)) {
func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
func_interp* g = m_model.get_func_interp(f);
unsigned sz = g->num_entries();
unsigned arity = f->get_arity();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m());
func_entry const* fe = g->get_entry(i);
store.append(arity, fe->get_args());
store.push_back(fe->get_result());
for (unsigned j = 0; j < store.size(); ++j) {
if (!is_ground(store[j].get())) {
TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
return false;
}
}
stores.push_back(store);
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";);
return false;
}
if (!is_ground(else_case)) {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";);
return false;
}
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
return true;
}
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
return false;
}
};
template class rewriter_tpl<evaluator_cfg>;

2
src/sat/sat_simplifier.cpp
View file

@ -401,7 +401,7 @@ namespace sat {
literal_vector::iterator l_it = m_bs_ls.begin();
for (; it != end; ++it, ++l_it) {
clause & c2 = *(*it);
if (*l_it == null_literal) {
if (!c2.was_removed() && *l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();

2
src/smt/smt_farkas_util.cpp
View file

@ -62,7 +62,7 @@ namespace smt {
app* farkas_util::mk_ge(expr* e1, expr* e2) {
mk_coerce(e1, e2);
return a.mk_gt(e1, e2);
return a.mk_ge(e1, e2);
}
app* farkas_util::mk_gt(expr* e1, expr* e2) {

3
src/smt/theory_arith_core.h
View file

@ -3212,7 +3212,8 @@ 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());
return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
inf_numeral val;
return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
}
template<typename Ext>

380
src/smt/theory_seq.cpp
View file

@ -15,7 +15,6 @@ Author:
Revision History:
// Use instead reference counts for dependencies to GC?
--*/
@ -258,7 +257,7 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>fixed_length\n";);
return FC_CONTINUE;
}
if (branch_variable()) {
if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() || branch_variable()) {
++m_stats.m_branch_variable;
TRACE("seq", tout << ">>branch_variable\n";);
return FC_CONTINUE;
@ -291,8 +290,7 @@ final_check_status theory_seq::final_check_eh() {
return FC_GIVEUP;
}
bool theory_seq::branch_variable() {
bool theory_seq::reduce_length_eq() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
int start = ctx.get_random_value();
@ -304,25 +302,344 @@ bool theory_seq::branch_variable() {
return true;
}
}
return false;
}
bool theory_seq::branch_binary_variable() {
unsigned sz = m_eqs.size();
for (unsigned i = 0; i < sz; ++i) {
eq const& e = m_eqs[i];
if (branch_binary_variable(e)) {
return true;
}
}
return false;
}
bool theory_seq::branch_binary_variable(eq const& e) {
if (is_complex(e)) {
return false;
}
ptr_vector<expr> xs, ys;
expr* x, *y;
bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
if (!is_binary) {
is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
}
if (!is_binary) {
return false;
}
if (x == y) {
return false;
}
// Equation is of the form x ++ xs = ys ++ y
// where xs, ys are units.
// x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs
rational lenX, lenY;
context& ctx = get_context();
if (branch_variable(e)) {
return true;
}
if (!get_length(x, lenX)) {
enforce_length(ensure_enode(x));
return true;
}
if (!get_length(y, lenY)) {
enforce_length(ensure_enode(y));
return true;
}
if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
// |x| - |y| = |ys| - |xs|
expr_ref a(mk_sub(m_util.str.mk_length(x), m_util.str.mk_length(y)), m);
expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m);
propagate_lit(e.dep(), 0, 0, mk_eq(a, b, false));
return true;
}
if (lenX <= rational(ys.size())) {
expr_ref_vector Ys(m);
Ys.append(ys.size(), ys.c_ptr());
branch_unit_variable(e.dep(), x, Ys);
return true;
}
expr_ref le(m_autil.mk_le(m_util.str.mk_length(x), m_autil.mk_int(ys.size())), m);
literal lit = mk_literal(le);
if (l_false == ctx.get_assignment(lit)) {
// |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs
expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
ys.push_back(Y1);
expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m);
expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
literal_vector lits;
lits.push_back(~lit);
dependency* dep = e.dep();
propagate_eq(dep, lits, x, ysY1, true);
propagate_eq(dep, lits, y, Y1Y2, true);
propagate_eq(dep, lits, Y2, xsE, true);
}
else {
ctx.mark_as_relevant(lit);
}
return true;
}
bool theory_seq::branch_unit_variable() {
unsigned sz = m_eqs.size();
for (unsigned i = 0; i < sz; ++i) {
eq const& e = m_eqs[i];
if (is_unit_eq(e.ls(), e.rs())) {
branch_unit_variable(e.dep(), e.ls()[0], e.rs());
return true;
}
else if (is_unit_eq(e.rs(), e.ls())) {
branch_unit_variable(e.dep(), e.rs()[0], e.ls());
return true;
}
}
return false;
}
/**
\brief ls := X... == rs := abcdef
*/
bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) {
if (ls.empty() || !is_var(ls[0])) {
return false;
}
for (unsigned i = 0; i < rs.size(); ++i) {
if (!m_util.str.is_unit(rs[i])) {
return false;
}
}
return true;
}
void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
SASSERT(is_var(X));
context& ctx = get_context();
rational lenX;
if (!get_length(X, lenX)) {
enforce_length(ensure_enode(X));
return;
}
if (lenX > rational(units.size())) {
expr_ref le(m_autil.mk_le(m_util.str.mk_length(X), m_autil.mk_int(units.size())), m);
propagate_lit(dep, 0, 0, mk_literal(le));
return;
}
SASSERT(lenX.is_unsigned());
unsigned lX = lenX.get_unsigned();
if (lX == 0) {
set_empty(X);
}
else {
literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false);
if (l_true == ctx.get_assignment(lit)) {
expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
literal_vector lits;
lits.push_back(lit);
propagate_eq(dep, lits, X, R, true);
}
else {
ctx.mark_as_relevant(lit);
ctx.force_phase(lit);
}
}
}
bool theory_seq::branch_variable_mb() {
context& ctx = get_context();
bool change = false;
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
vector<rational> len1, len2;
if (!is_complex(e)) {
continue;
}
if (e.ls().empty() || e.rs().empty() ||
(!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
continue;
}
if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
change = true;
continue;
}
rational l1, l2;
for (unsigned j = 0; j < len1.size(); ++j) l1 += len1[j];
for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j];
if (l1 != l2) {
TRACE("seq", tout << "lengths are not compatible\n";);
expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
literal_vector lits;
propagate_eq(e.dep(), lits, lnl, lnr, false);
change = true;
continue;
}
if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
TRACE("seq", tout << "split lengths\n";);
return true;
}
}
return change;
}
unsigned s = 0;
bool theory_seq::is_complex(eq const& e) {
unsigned num_vars1 = 0, num_vars2 = 0;
for (unsigned i = 0; i < e.ls().size(); ++i) {
if (is_var(e.ls()[i])) ++num_vars1;
}
for (unsigned i = 0; i < e.rs().size(); ++i) {
if (is_var(e.rs()[i])) ++num_vars2;
}
return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
}
/*
\brief Decompose ls = rs into Xa = bYc, such that
1.
- X != Y
- |b| <= |X| <= |bY| in currrent model
- b is non-empty.
2. X != Y
- b is empty
- |X| <= |Y|
3. |X| = 0
- propagate X = empty
*/
bool theory_seq::split_lengths(dependency* dep,
expr_ref_vector const& ls, expr_ref_vector const& rs,
vector<rational> const& ll, vector<rational> const& rl) {
context& ctx = get_context();
expr_ref X(m), Y(m), b(m);
if (ls.empty() || rs.empty()) {
return false;
}
if (is_var(ls[0]) && ll[0].is_zero()) {
return set_empty(ls[0]);
}
if (is_var(rs[0]) && rl[0].is_zero()) {
return set_empty(rs[0]);
}
if (is_var(rs[0]) && !is_var(ls[0])) {
return split_lengths(dep, rs, ls, rl, ll);
}
if (!is_var(ls[0])) {
return false;
}
X = ls[0];
rational lenX = ll[0];
expr_ref_vector bs(m);
SASSERT(lenX.is_pos());
rational lenB(0), lenY(0);
for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
bs.push_back(rs[i]);
lenY = rl[i];
lenB += lenY;
}
SASSERT(lenX <= lenB);
SASSERT(!bs.empty());
Y = bs.back();
bs.pop_back();
if (!is_var(Y) && !m_util.str.is_unit(Y)) {
TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
return false;
}
if (X == Y) {
TRACE("seq", tout << "Cycle: " << X << "\n";);
return false;
}
if (lenY.is_zero()) {
return set_empty(Y);
}
b = mk_concat(bs, m.get_sort(X));
SASSERT(X != Y);
// |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2
expr_ref lenXE(m_util.str.mk_length(X), m);
expr_ref lenYE(m_util.str.mk_length(Y), m);
expr_ref lenb(m_util.str.mk_length(b), m);
expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m);
expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE),
m_autil.mk_int(0)), m);
literal lit1(~mk_literal(le1));
literal lit2(mk_literal(le2));
literal_vector lits;
lits.push_back(lit1);
lits.push_back(lit2);
if (ctx.get_assignment(lit1) != l_true ||
ctx.get_assignment(lit2) != l_true) {
ctx.mark_as_relevant(lit1);
ctx.mark_as_relevant(lit2);
}
else if (m_util.str.is_unit(Y)) {
SASSERT(lenB == lenX);
bs.push_back(Y);
expr_ref bY(m_util.str.mk_concat(bs), m);
propagate_eq(dep, lits, X, bY, true);
}
else {
SASSERT(is_var(Y));
expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m);
expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m);
expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
propagate_eq(dep, lits, X, bY1, true);
propagate_eq(dep, lits, Y, Y1Y2, true);
}
return true;
}
bool theory_seq::set_empty(expr* x) {
add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x));
return true;
}
bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & len) {
bool all_have_length = true;
rational val;
zstring s;
for (unsigned i = 0; i < es.size(); ++i) {
expr* e = es[i];
if (m_util.str.is_unit(e)) {
len.push_back(rational(1));
}
else if (m_util.str.is_empty(e)) {
len.push_back(rational(0));
}
else if (m_util.str.is_string(e, s)) {
len.push_back(rational(s.length()));
}
else if (get_length(e, val)) {
len.push_back(val);
}
else {
enforce_length(ensure_enode(e));
all_have_length = false;
}
}
return all_have_length;
}
bool theory_seq::branch_variable() {
context& ctx = get_context();
unsigned sz = m_eqs.size();
int start = ctx.get_random_value();
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + start) % sz;
eq const& e = m_eqs[k];
unsigned id = e.id();
s = find_branch_start(2*id);
TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
insert_branch_start(2*id, s);
if (found) {
return true;
}
s = find_branch_start(2*id + 1);
found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
insert_branch_start(2*id + 1, s);
if (found) {
if (branch_variable(e)) {
return true;
}
@ -338,6 +655,22 @@ bool theory_seq::branch_variable() {
return ctx.inconsistent();
}
bool theory_seq::branch_variable(eq const& e) {
unsigned id = e.id();
unsigned s = find_branch_start(2*id);
TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
insert_branch_start(2*id, s);
if (found) {
return true;
}
s = find_branch_start(2*id + 1);
found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
insert_branch_start(2*id + 1, s);
return found;
}
void theory_seq::insert_branch_start(unsigned k, unsigned s) {
m_branch_start.insert(k, s);
m_trail_stack.push(pop_branch(k));
@ -483,7 +816,6 @@ lbool theory_seq::assume_equality(expr* l, expr* r) {
return l_false;
}
return ctx.get_assignment(mk_eq(l, r, false));
//return l_undef;
}
@ -1901,12 +2233,15 @@ void theory_seq::display(std::ostream & out) const {
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
eq const& e = m_eqs[i];
out << e.ls() << " = " << e.rs() << " <- \n";
display_deps(out, e.dep());
display_equation(out, m_eqs[i]);
}
}
void theory_seq::display_equation(std::ostream& out, eq const& e) const {
out << e.ls() << " = " << e.rs() << " <- \n";
display_deps(out, e.dep());
}
void theory_seq::display_disequations(std::ostream& out) const {
bool first = true;
for (unsigned i = 0; i < m_nqs.size(); ++i) {
@ -3050,6 +3385,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_in_re(e)) {
propagate_in_re(e, is_true);
}
else if (is_skolem(symbol("seq.split"), e)) {
// propagate equalities
}
else {
UNREACHABLE();
}

15
src/smt/theory_seq.h
View file

@ -358,6 +358,10 @@ namespace smt {
void init_model(expr_ref_vector const& es);
// final check
bool simplify_and_solve_eqs(); // solve unitary equalities
bool reduce_length_eq();
bool branch_unit_variable(); // branch on XYZ = abcdef
bool branch_binary_variable(); // branch on abcX = Ydefg
bool branch_variable_mb(); // branch on a variable, model based on length
bool branch_variable(); // branch on a variable
bool split_variable(); // split a variable
bool is_solved();
@ -366,7 +370,16 @@ namespace smt {
bool check_length_coherence(expr* e);
bool fixed_length();
bool fixed_length(expr* e);
void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
bool branch_variable(eq const& e);
bool branch_binary_variable(eq const& e);
bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
bool propagate_length_coherence(expr* e);
bool split_lengths(dependency* dep,
expr_ref_vector const& ls, expr_ref_vector const& rs,
vector<rational> const& ll, vector<rational> const& rl);
bool set_empty(expr* x);
bool is_complex(eq const& e);
bool check_extensionality();
bool check_contains();
@ -465,6 +478,7 @@ namespace smt {
bool has_length(expr *e) const { return m_length.contains(e); }
void add_length(expr* e);
void enforce_length(enode* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
void enforce_length_coherence(enode* n1, enode* n2);
void add_elim_string_axiom(expr* n);
@ -532,6 +546,7 @@ namespace smt {
// diagnostics
void display_equations(std::ostream& out) const;
void display_equation(std::ostream& out, eq const& e) 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;