mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into lackr

Browse source
This commit is contained in:
Mikolas Janota 2016-02-08 12:54:22 +00:00
commit b614e7732b
26 changed files with 785 additions and 615 deletions
Download patch file Download diff file Expand all files Collapse all files

5
scripts/mk_util.py
View file

@ -596,7 +596,7 @@ def display_help(exit_code):
else:
print(" --parallel=num use cl option /MP with 'num' parallel processes")
print(" --pypkgdir=<dir> Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
print(" -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build).")
print(" -b <subdir>, --build=<subdir> subdirectory where Z3 will be built (default: %s)." % BUILD_DIR)
print(" --githash=hash include the given hash in the binaries.")
print(" -d, --debug compile Z3 in debug mode.")
print(" -t, --trace enable tracing in release mode.")
@ -742,7 +742,8 @@ def extract_c_includes(fname):
# Given a path dir1/subdir2/subdir3 returns ../../..
def reverse_path(p):
l = p.split(os.sep)
# Filter out empty components (e.g. will have one if path ends in a slash)
l = list(filter(lambda x: len(x) > 0, p.split(os.sep)))
n = len(l)
r = '..'
for i in range(1, n):

6
src/api/z3_api.h
View file

@ -5642,6 +5642,9 @@ extern "C" {
if the result is \c Z3_L_UNDEF, but the returned model
is not guaranteed to satisfy quantified assertions.
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
*/
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
@ -5662,6 +5665,9 @@ extern "C" {
The solver supports the commands #Z3_solver_push and #Z3_solver_pop, but it
will always solve each #Z3_solver_check from scratch.
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC)))
*/
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);

19
src/ast/arith_decl_plugin.h
View file

@ -211,6 +211,25 @@ public:
virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind())
{
case OP_0_PW_0_INT:
case OP_0_PW_0_REAL:
case OP_NEG_ROOT:
case OP_DIV_0:
case OP_IDIV_0:
case OP_MOD_0:
case OP_U_ASIN:
case OP_U_ACOS:
return true;
default:
return false;
}
return false;
}
};
/**

2
src/ast/ast.h
View file

@ -992,6 +992,8 @@ public:
// Event handlers for deleting/translating PARAM_EXTERNAL
virtual void del(parameter const & p) {}
virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
};
// -----------------------------------

17
src/ast/bv_decl_plugin.h
View file

@ -266,6 +266,22 @@ public:
virtual bool are_distinct(app* a, app* b) const;
virtual expr * get_some_value(sort * s);
virtual bool is_considered_uninterpreted(func_decl * f) {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind()) {
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
return true;
default:
return false;
}
return false;
}
};
class bv_recognizers {
@ -353,7 +369,6 @@ public:
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
bool has_sign_bit(rational const & n, unsigned bv_size) const;
bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
};
class bv_util : public bv_recognizers {

15
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -419,11 +419,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
dbg_decouple("fpa2bv_add_exp_delta", exp_delta);
// cap the delta
expr_ref cap(m), cap_le_delta(m);
cap = m_bv_util.mk_numeral(sbits+2, ebits);
cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
if (log2(sbits + 2) < ebits + 2)
{
// cap the delta
expr_ref cap(m), cap_le_delta(m);
cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2);
cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta));
m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta);
exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta);
dbg_decouple("fpa2bv_add_exp_cap", cap);
}
dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);

50
src/ast/rewriter/bit_blaster/bit_blaster.cpp
View file

@ -21,10 +21,10 @@ Revision History:
#include"ast_pp.h"
#include"bv_decl_plugin.h"
bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s):
bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw):
m_util(u),
m_params(p),
s(_s) {
m_rw(rw) {
}
static void sort_args(expr * & l1, expr * & l2, expr * & l3) {
@ -47,30 +47,30 @@ void bit_blaster_cfg::mk_xor3(expr * l1, expr * l2, expr * l3, expr_ref & r) {
else if (l2 == l3)
r = l1;
else if (m().is_complement(l1, l2))
s.mk_not(l3, r);
m_rw.mk_not(l3, r);
else if (m().is_complement(l1, l3))
s.mk_not(l2, r);
m_rw.mk_not(l2, r);
else if (m().is_complement(l2, l3))
s.mk_not(l1, r);
m_rw.mk_not(l1, r);
else if (m().is_true(l1))
s.mk_iff(l2, l3, r);
m_rw.mk_iff(l2, l3, r);
else if (m().is_false(l1))
s.mk_xor(l2, l3, r);
m_rw.mk_xor(l2, l3, r);
else if (m().is_true(l2))
s.mk_iff(l1, l3, r);
m_rw.mk_iff(l1, l3, r);
else if (m().is_false(l2))
s.mk_xor(l1, l3, r);
m_rw.mk_xor(l1, l3, r);
else if (m().is_true(l3))
s.mk_iff(l1, l2, r);
m_rw.mk_iff(l1, l2, r);
else if (m().is_false(l3))
s.mk_xor(l1, l2, r);
m_rw.mk_xor(l1, l2, r);
else
r = m().mk_app(m_util.get_family_id(), OP_XOR3, l1, l2, l3);
}
else {
expr_ref t(m());
s.mk_xor(l1, l2, t);
s.mk_xor(t, l3, r);
m_rw.mk_xor(l1, l2, t);
m_rw.mk_xor(t, l3, r);
}
}
@ -90,17 +90,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) {
else if (l1 == l2 && l1 == l3)
r = l1;
else if (m().is_false(l1))
s.mk_and(l2, l3, r);
m_rw.mk_and(l2, l3, r);
else if (m().is_false(l2))
s.mk_and(l1, l3, r);
m_rw.mk_and(l1, l3, r);
else if (m().is_false(l3))
s.mk_and(l1, l2, r);
m_rw.mk_and(l1, l2, r);
else if (m().is_true(l1))
s.mk_or(l2, l3, r);
m_rw.mk_or(l2, l3, r);
else if (m().is_true(l2))
s.mk_or(l1, l3, r);
m_rw.mk_or(l1, l3, r);
else if (m().is_true(l3))
s.mk_or(l1, l2, r);
m_rw.mk_or(l1, l2, r);
else if (m().is_complement(l1, l2))
r = l3;
else if (m().is_complement(l1, l3))
@ -112,17 +112,17 @@ void bit_blaster_cfg::mk_carry(expr * l1, expr * l2, expr * l3, expr_ref & r) {
}
else {
expr_ref t1(m()), t2(m()), t3(m());
s.mk_and(l1, l2, t1);
s.mk_and(l1, l3, t2);
s.mk_and(l2, l3, t3);
s.mk_or(t1, t2, t3, r);
m_rw.mk_and(l1, l2, t1);
m_rw.mk_and(l1, l3, t2);
m_rw.mk_and(l2, l3, t3);
m_rw.mk_or(t1, t2, t3, r);
}
}
template class bit_blaster_tpl<bit_blaster_cfg>;
bit_blaster::bit_blaster(ast_manager & m, bit_blaster_params const & params):
bit_blaster_tpl<bit_blaster_cfg>(bit_blaster_cfg(m_util, params, m_simp)),
bit_blaster_tpl<bit_blaster_cfg>(bit_blaster_cfg(m_util, params, m_rw)),
m_util(m),
m_simp(m) {
m_rw(m) {
}

32
src/ast/rewriter/bit_blaster/bit_blaster.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef BIT_BLASTER_H_
#define BIT_BLASTER_H_
#include"basic_simplifier_plugin.h"
#include"bool_rewriter.h"
#include"bit_blaster_params.h"
#include"bit_blaster_tpl.h"
#include"bv_decl_plugin.h"
@ -31,31 +31,31 @@ public:
protected:
bv_util & m_util;
bit_blaster_params const & m_params;
basic_simplifier_plugin & s;
bool_rewriter & m_rw;
public:
bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s);
bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw);
ast_manager & m() const { return m_util.get_manager(); }
numeral power(unsigned n) const { return rational::power_of_two(n); }
void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); }
void mk_xor(expr * a, expr * b, expr_ref & r) { m_rw.mk_xor(a, b, r); }
void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r);
void mk_carry(expr * a, expr * b, expr * c, expr_ref & r);
void mk_iff(expr * a, expr * b, expr_ref & r) { s.mk_iff(a, b, r); }
void mk_and(expr * a, expr * b, expr_ref & r) { s.mk_and(a, b, r); }
void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_and(a, b, c, r); }
void mk_and(unsigned sz, expr * const * args, expr_ref & r) { s.mk_and(sz, args, r); }
void mk_or(expr * a, expr * b, expr_ref & r) { s.mk_or(a, b, r); }
void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { s.mk_or(a, b, c, r); }
void mk_or(unsigned sz, expr * const * args, expr_ref & r) { s.mk_or(sz, args, r); }
void mk_not(expr * a, expr_ref & r) { s.mk_not(a, r); }
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { s.mk_ite(c, t, e, r); }
void mk_nand(expr * a, expr * b, expr_ref & r) { s.mk_nand(a, b, r); }
void mk_nor(expr * a, expr * b, expr_ref & r) { s.mk_nor(a, b, r); }
void mk_iff(expr * a, expr * b, expr_ref & r) { m_rw.mk_iff(a, b, r); }
void mk_and(expr * a, expr * b, expr_ref & r) { m_rw.mk_and(a, b, r); }
void mk_and(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_and(a, b, c, r); }
void mk_and(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_and(sz, args, r); }
void mk_or(expr * a, expr * b, expr_ref & r) { m_rw.mk_or(a, b, r); }
void mk_or(expr * a, expr * b, expr * c, expr_ref & r) { m_rw.mk_or(a, b, c, r); }
void mk_or(unsigned sz, expr * const * args, expr_ref & r) { m_rw.mk_or(sz, args, r); }
void mk_not(expr * a, expr_ref & r) { m_rw.mk_not(a, r); }
void mk_ite(expr * c, expr * t, expr * e, expr_ref & r) { m_rw.mk_ite(c, t, e, r); }
void mk_nand(expr * a, expr * b, expr_ref & r) { m_rw.mk_nand(a, b, r); }
void mk_nor(expr * a, expr * b, expr_ref & r) { m_rw.mk_nor(a, b, r); }
};
class bit_blaster : public bit_blaster_tpl<bit_blaster_cfg> {
bv_util m_util;
basic_simplifier_plugin m_simp;
bool_rewriter m_rw;
public:
bit_blaster(ast_manager & m, bit_blaster_params const & params);
bit_blaster_params const & get_params() const { return this->m_params; }

1
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -362,6 +362,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
if (butil().is_bv(args[1])) {

1
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -23,6 +23,7 @@ Revision History:
#include"common_msgs.h"
#include"rewriter_types.h"
template<typename Cfg>
void bit_blaster_tpl<Cfg>::checkpoint() {
if (memory::get_allocation_size() > m_max_memory)

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

@ -694,7 +694,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) {
if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BSDIV0, arg1);
return BR_DONE;
return BR_REWRITE1;
}
else {
// The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
@ -745,7 +745,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) {
if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BUDIV0, arg1);
return BR_DONE;
return BR_REWRITE1;
}
else {
// The "hardware interpretation" for (bvudiv x 0) is #xffff
@ -808,7 +808,7 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e
if (r2.is_zero()) {
if (!hi_div0) {
result = m().mk_app(get_fid(), OP_BSREM0, arg1);
return BR_DONE;
return BR_REWRITE1;
}
else {
// The "hardware interpretation" for (bvsrem x 0) is x
@ -2010,8 +2010,8 @@ bool bv_rewriter::is_add_mul_const(expr* e) const {
bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
return
(m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs)))) ||
(m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs))));
(m_util.is_concat(lhs) && is_concat_split_target(rhs)) ||
(m_util.is_concat(rhs) && is_concat_split_target(lhs));
}
bool bv_rewriter::has_numeral(app* a) const {

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

@ -174,6 +174,8 @@ public:
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
bool hi_div0() const { return m_hi_div0; }
bv_util & get_util() { return m_util; }
};
#endif

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -875,6 +875,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
if (m().is_false(cond)) {
continue;
}
if (m().is_true(cond)) {
add_next(next, trail, mv.dst(), acc);
continue;
}
expr* args[2] = { cond, acc };
cond = mk_and(m(), 2, args);
add_next(next, trail, mv.dst(), cond);

7
src/ast/seq_decl_plugin.cpp
View file

@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation
Module Name:
dl_decl_plugin.h
seq_decl_plugin.h
Abstract:
<abstract>
decl_plugin for the theory of sequences
Author:
@ -173,6 +173,9 @@ std::string zstring::encode() const {
if (0 <= ch && ch < 32) {
strm << esc_table[ch];
}
else if (ch == '\\') {
strm << "\\\\";
}
else {
strm << (char)(ch);
}

2
src/ast/seq_decl_plugin.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
<abstract>
decl_plugin for the theory of sequences
Author:

4
src/ast/simplifier/fpa_simplifier_plugin.cpp
View file

@ -28,12 +28,12 @@ bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * cons
SASSERT(f->get_family_id() == get_family_id());
return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE;
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
}
bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE;
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
}

39
src/ast/simplifier/seq_simplifier_plugin.cpp Normal file
View file

@ -0,0 +1,39 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
seq_simplifier_plugin.cpp
Abstract:
Simplifier for the theory of sequences
Author:
Nikolaj Bjorner (nbjorner) 2016-02-05
--*/
#include"seq_simplifier_plugin.h"
seq_simplifier_plugin::seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) :
simplifier_plugin(symbol("seq"), m),
m_util(m),
m_rw(m) {}
seq_simplifier_plugin::~seq_simplifier_plugin() {}
bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == get_family_id());
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
}
bool seq_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
}

39
src/ast/simplifier/seq_simplifier_plugin.h Normal file
View file

@ -0,0 +1,39 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
seq_simplifier_plugin.h
Abstract:
Simplifier for the sequence theory
Author:
Nikolaj Bjorner (nbjorner) 2016-02-05
--*/
#ifndef SEQ_SIMPLIFIER_PLUGIN_H_
#define SEQ_SIMPLIFIER_PLUGIN_H_
#include"basic_simplifier_plugin.h"
#include"seq_decl_plugin.h"
#include"seq_rewriter.h"
class seq_simplifier_plugin : public simplifier_plugin {
seq_util m_util;
seq_rewriter m_rw;
public:
seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
~seq_simplifier_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
};
#endif /* SEQ_SIMPLIFIER_PLUGIN_H_ */

6
src/model/model_evaluator.cpp
View file

@ -181,6 +181,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f);
if (fi != 0) {
@ -199,7 +200,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
return true;
}
if (f->get_family_id() == null_family_id && m_model_completion) {
if (m_model_completion &&
(f->get_family_id() == null_family_id ||
m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m(), f->get_arity());

7
src/opt/opt_context.cpp
View file

@ -883,11 +883,11 @@ namespace opt {
bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
objective& obj = m_objectives[index];
if (obj.m_type != O_MAXSMT) {
// change from maximize/minimize.
obj.m_id = id;
obj.m_type = O_MAXSMT;
obj.m_weights.append(weights);
SASSERT(!m_maxsmts.contains(id));
add_maxsmt(id);
}
@ -895,10 +895,13 @@ namespace opt {
SASSERT(obj.m_id == id);
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_weights.reset();
obj.m_weights.append(weights);
obj.m_adjust_value.set_offset(offset);
obj.m_adjust_value.set_negate(neg);
m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";
tout << terms << "\n";);
}
else if (is_maximize(fml, tr, orig_term, index)) {
purify(tr);

2
src/smt/asserted_formulas.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include"array_simplifier_plugin.h"
#include"datatype_simplifier_plugin.h"
#include"fpa_simplifier_plugin.h"
#include"seq_simplifier_plugin.h"
#include"bv_simplifier_plugin.h"
#include"for_each_expr.h"
#include"well_sorted.h"
@ -98,6 +99,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp));
}
void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {

2
src/smt/theory_bv.cpp
View file

@ -471,12 +471,12 @@ namespace smt {
if (get_enode(v)->get_root() != get_enode(v2)->get_root()) {
SASSERT(get_bv_size(v) == get_bv_size(v2));
context & ctx = get_context();
justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
TRACE("fixed_var_eh", tout << "detected equality: v" << v << " = v" << v2 << "\n";
display_var(tout, v);
display_var(tout, v2););
m_stats.m_num_th2core_eq++;
add_fixed_eq(v, v2);
justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
m_fixed_var_table.insert(key, v2);
}

3
src/smt/theory_fpa.cpp
View file

@ -30,12 +30,13 @@ namespace smt {
expr * m_e;
public:
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
m(m), m_conversions(c), m_e(e) {}
m(m), m_conversions(c), m_e(e) { m.inc_ref(e); }
virtual ~fpa2bv_conversion_trail_elem() {}
virtual void undo(theory_fpa & th) {
expr * v = m_conversions.find(m_e);
m_conversions.remove(m_e);
m.dec_ref(v);
m.dec_ref(m_e);
}
};

18
src/smt/theory_seq.cpp
View file

@ -823,6 +823,23 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
}
bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) {
rational val1, val2;
if (has_length(l) && has_length(r) &&
get_length(l, val1) && get_length(r, val2) && val1 == val2) {
context& ctx = get_context();
expr_ref len1(m_util.str.mk_length(l), m);
expr_ref len2(m_util.str.mk_length(r), m);
literal lit = mk_eq(len1, len2, false);
if (ctx.get_assignment(lit) == l_true) {
lits.push_back(lit);
return true;
}
else {
TRACE("seq", tout << "Assignment: " << len1 << " = " << len2 << " " << ctx.get_assignment(lit) << "\n";);
return false;
}
}
expr_ref len1(m), len2(m);
lits.reset();
if (get_length(l, len1, lits) &&
@ -2431,6 +2448,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero));
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
}
/*

11
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -106,9 +106,14 @@ class solve_eqs_tactic : public tactic {
}
}
bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
return
trivial_solve1(lhs, rhs, var, def, pr) ||
trivial_solve1(rhs, lhs, var, def, pr);
if (trivial_solve1(lhs, rhs, var, def, pr)) return true;
if (trivial_solve1(rhs, lhs, var, def, pr)) {
if (m_produce_proofs) {
pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
}
return true;
}
return false;
}
// (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))

2
src/util/debug.cpp
View file

@ -76,7 +76,7 @@ void invoke_gdb() {
for (;;) {
std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
char result;
bool ok = (std::cin >> result);
bool ok = bool(std::cin >> result);
if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or unattached.
switch(result) {
case 'C':