mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 17:00:44 +01:00
parent 13eac21b2c 7161d6c150
commit 8f388d83a2
47 changed files with 819 additions and 199 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
examples/tptp/tptp5.cpp
View file

@ -809,8 +809,12 @@ class env {
r = terms[0] / terms[1];
}
else if (!strcmp(ch,"$distinct")) {
check_arity(terms.size(), 2);
r = terms[0] != terms[1];
if (terms.size() == 2) {
r = terms[0] != terms[1];
}
else {
r = distinct(terms);
}
}
else if (!strcmp(ch,"$floor") || !strcmp(ch,"$to_int")) {
check_arity(terms.size(), 1);
@ -1089,12 +1093,11 @@ class env {
}
z3::sort mk_sort(char const* s) {
z3::symbol sym = symbol(s);
return mk_sort(sym);
return m_context.uninterpreted_sort(s);
}
z3::sort mk_sort(z3::symbol& s) {
return z3::sort(m_context, Z3_mk_uninterpreted_sort(m_context, s));
return m_context.uninterpreted_sort(s);
}
public:

2
scripts/mk_project.py
View file

@ -55,7 +55,6 @@ def init_project_def():
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat'], 'qe')
add_lib('duality', ['smt', 'interp', 'qe'])
@ -71,6 +70,7 @@ def init_project_def():
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')

10
scripts/update_api.py
View file

@ -568,10 +568,12 @@ def mk_java():
java_native.write(' public static class ObjArrayPtr { public long[] value; }\n')
java_native.write(' public static class UIntArrayPtr { public int[] value; }\n')
java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n')
if IS_WINDOWS or os.uname()[0]=="CYGWIN":
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name)
else:
java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name
java_native.write(' static {\n')
java_native.write(' try { System.loadLibrary("z3java"); }\n')
java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n')
java_native.write(' }\n')
java_native.write('\n')
for name, result, params in _dotnet_decls:
java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name)))

4
src/api/api_solver.cpp
View file

@ -355,6 +355,10 @@ extern "C" {
init_solver(c, s);
Z3_stats_ref * st = alloc(Z3_stats_ref);
to_solver_ref(s)->collect_statistics(st->m_stats);
unsigned long long max_mem = memory::get_max_used_memory();
unsigned long long mem = memory::get_allocation_size();
st->m_stats.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
st->m_stats.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);
RETURN_Z3(r);

34
src/api/c++/z3++.h
View file

@ -203,7 +203,12 @@ namespace z3 {
and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
*/
sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
/**
\brief create an uninterpreted sort with the name given by the string or symbol.
*/
sort uninterpreted_sort(char const* name);
sort uninterpreted_sort(symbol const& name);
func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
func_decl function(symbol const& name, sort_vector const& domain, sort const& range);
@ -678,7 +683,7 @@ namespace z3 {
friend expr operator+(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b };
r = Z3_mk_add(a.ctx(), 2, args);
@ -698,7 +703,7 @@ namespace z3 {
friend expr operator*(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b };
r = Z3_mk_mul(a.ctx(), 2, args);
@ -725,7 +730,7 @@ namespace z3 {
friend expr operator/(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_div(a.ctx(), a, b);
}
@ -743,7 +748,7 @@ namespace z3 {
friend expr operator/(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) / b; }
friend expr operator-(expr const & a) {
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith()) {
r = Z3_mk_unary_minus(a.ctx(), a);
}
@ -760,7 +765,7 @@ namespace z3 {
friend expr operator-(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
Z3_ast args[2] = { a, b };
r = Z3_mk_sub(a.ctx(), 2, args);
@ -780,7 +785,7 @@ namespace z3 {
friend expr operator<=(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_le(a.ctx(), a, b);
}
@ -799,7 +804,7 @@ namespace z3 {
friend expr operator>=(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_ge(a.ctx(), a, b);
}
@ -818,7 +823,7 @@ namespace z3 {
friend expr operator<(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_lt(a.ctx(), a, b);
}
@ -837,7 +842,7 @@ namespace z3 {
friend expr operator>(expr const & a, expr const & b) {
check_context(a, b);
Z3_ast r;
Z3_ast r = 0;
if (a.is_arith() && b.is_arith()) {
r = Z3_mk_gt(a.ctx(), a, b);
}
@ -1184,7 +1189,7 @@ namespace z3 {
expr eval(expr const & n, bool model_completion=false) const {
check_context(*this, n);
Z3_ast r;
Z3_ast r = 0;
Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
check_error();
if (status == Z3_FALSE)
@ -1637,6 +1642,13 @@ namespace z3 {
for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
return s;
}
inline sort context::uninterpreted_sort(char const* name) {
Z3_symbol _name = Z3_mk_string_symbol(*this, name);
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
}
inline sort context::uninterpreted_sort(symbol const& name) {
return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
}
inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
array<Z3_sort> args(arity);

3
src/api/java/InterpolationContext.java
View file

@ -108,7 +108,8 @@ public class InterpolationContext extends Context
res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE)
res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
if (res.status == Z3_lbool.Z3_L_TRUE)
res.model = new Model(this, n_m.value);
return res;
}

31
src/api/python/z3.py
View file

@ -5617,7 +5617,7 @@ class Statistics:
sat
>>> st = s.statistics()
>>> len(st)
2
4
"""
return int(Z3_stats_size(self.ctx.ref(), self.stats))
@ -5631,7 +5631,7 @@ class Statistics:
sat
>>> st = s.statistics()
>>> len(st)
2
4
>>> st[0]
('nlsat propagations', 2)
>>> st[1]
@ -5655,7 +5655,7 @@ class Statistics:
sat
>>> st = s.statistics()
>>> st.keys()
['nlsat propagations', 'nlsat stages']
['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
"""
return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
@ -5692,7 +5692,7 @@ class Statistics:
sat
>>> st = s.statistics()
>>> st.keys()
['nlsat propagations', 'nlsat stages']
['nlsat propagations', 'nlsat stages', 'max memory', 'memory']
>>> st.nlsat_propagations
2
>>> st.nlsat_stages
@ -8194,23 +8194,24 @@ def FP(name, fpsort, ctx=None):
>>> eq(x, x2)
True
"""
ctx = fpsort.ctx
if isinstance(fpsort, FPSortRef):
ctx = fpsort.ctx
else:
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
def FPs(names, fpsort, ctx=None):
"""Return an array of floating-point constants.
>>> x, y, z = BitVecs('x y z', 16)
>>> x.size()
16
>>> x, y, z = FPs('x y z', FPSort(8, 24))
>>> x.sort()
BitVec(16)
>>> Sum(x, y, z)
0 + x + y + z
>>> Product(x, y, z)
1*x*y*z
>>> simplify(Product(x, y, z))
x*y*z
FPSort(8, 24)
>>> x.sbits()
24
>>> x.ebits()
8
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
fpMul(RNE(), fpAdd(RNE(), x, y), z)
"""
ctx = z3._get_ctx(ctx)
if isinstance(names, str):

8
src/ast/ast_smt2_pp.cpp
View file

@ -341,22 +341,22 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
}
else {
SASSERT(u.is_irrational_algebraic_numeral(t));
anum const & val = u.to_irrational_algebraic_numeral(t);
anum const & val2 = u.to_irrational_algebraic_numeral(t);
algebraic_numbers::manager & am = u.am();
format * vf;
std::ostringstream buffer;
bool is_neg = false;
if (decimal) {
scoped_anum abs_val(am);
am.set(abs_val, val);
if (am.is_neg(val)) {
am.set(abs_val, val2);
if (am.is_neg(val2)) {
is_neg = true;
am.neg(abs_val);
}
am.display_decimal(buffer, abs_val, decimal_prec);
}
else {
am.display_root_smt2(buffer, val);
am.display_root_smt2(buffer, val2);
}
vf = mk_string(get_manager(), buffer.str().c_str());
return is_neg ? mk_neg(vf) : vf;

6
src/ast/ast_util.cpp
View file

@ -44,12 +44,12 @@ app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned nu
return mk_list_assoc_app(m, decl, num_args, args);
}
bool is_well_formed_vars(ptr_vector<sort>& bound, expr* e) {
bool is_well_formed_vars(ptr_vector<sort>& bound, expr * top) {
ptr_vector<expr> todo;
ast_mark mark;
todo.push_back(e);
todo.push_back(top);
while (!todo.empty()) {
expr* e = todo.back();
expr * e = todo.back();
todo.pop_back();
if (mark.is_marked(e)) {
continue;

37
src/ast/bv_decl_plugin.cpp
View file

@ -501,13 +501,17 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) {
if (arity != r->get_arity()) {
m_manager->raise_exception("declared arity mismatches supplied arity");
return 0;
if (r->get_info()->is_associative())
arity = r->get_arity();
else {
m_manager->raise_exception("declared arity mismatches supplied arity");
return 0;
}
}
for (unsigned i = 0; i < arity; ++i) {
if (domain[i] != r->get_domain(i)) {
m_manager->raise_exception("declared sorts do not match supplied sorts");
return 0;
return 0;
}
}
return r;
@ -566,6 +570,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
ast_manager& m = *m_manager;
int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in.
@ -589,11 +594,35 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
}
else if (num_args == 0 || !get_bv_size(args[0], bv_size)) {
m_manager->raise_exception("operator is applied to arguments of the wrong sort");
m.raise_exception("operator is applied to arguments of the wrong sort");
return 0;
}
func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) {
if (num_args != r->get_arity()) {
if (r->get_info()->is_associative()) {
sort * fs = r->get_domain(0);
for (unsigned i = 0; i < num_args; ++i) {
if (m.get_sort(args[i]) != fs) {
m_manager->raise_exception("declared sorts do not match supplied sorts");
return 0;
}
}
return r;
}
else {
m.raise_exception("declared arity mismatches supplied arity");
return 0;
}
}
for (unsigned i = 0; i < num_args; ++i) {
if (m.get_sort(args[i]) != r->get_domain(i)) {
std::ostringstream buffer;
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
m.raise_exception(buffer.str().c_str());
return 0;
}
}
return r;
}
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);

14
src/ast/datatype_decl_plugin.cpp
View file

@ -149,10 +149,10 @@ enum status {
*/
static bool is_recursive_datatype(parameter const * parameters) {
unsigned num_types = parameters[0].get_int();
unsigned tid = parameters[1].get_int();
unsigned top_tid = parameters[1].get_int();
buffer<status> already_found(num_types, WHITE);
buffer<unsigned> todo;
todo.push_back(tid);
todo.push_back(top_tid);
while (!todo.empty()) {
unsigned tid = todo.back();
if (already_found[tid] == BLACK) {
@ -198,11 +198,11 @@ static bool is_recursive_datatype(parameter const * parameters) {
*/
static sort_size get_datatype_size(parameter const * parameters) {
unsigned num_types = parameters[0].get_int();
unsigned tid = parameters[1].get_int();
unsigned top_tid = parameters[1].get_int();
buffer<sort_size> szs(num_types, sort_size());
buffer<status> already_found(num_types, WHITE);
buffer<unsigned> todo;
todo.push_back(tid);
todo.push_back(top_tid);
while (!todo.empty()) {
unsigned tid = todo.back();
if (already_found[tid] == BLACK) {
@ -280,7 +280,7 @@ static sort_size get_datatype_size(parameter const * parameters) {
}
}
}
return szs[tid];
return szs[top_tid];
}
/**
@ -657,8 +657,8 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const {
for (unsigned tid = 0; tid < num_types; tid++) {
unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset
unsigned num_constructors = parameters[o].get_int();
for (unsigned s = 1; s <= num_constructors; s++) {
unsigned k_i = parameters[o + s].get_int();
for (unsigned si = 1; si <= num_constructors; si++) {
unsigned k_i = parameters[o + si].get_int();
unsigned num_accessors = parameters[k_i + 2].get_int();
unsigned r = 0;
for (; r < num_accessors; r++) {

10
src/ast/expr2polynomial.cpp
View file

@ -367,16 +367,16 @@ struct expr2polynomial::imp {
begin_loop:
checkpoint();
frame & fr = m_frame_stack.back();
app * t = fr.m_curr;
TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(t, m()) << "\n";);
unsigned num_args = t->get_num_args();
app * a = fr.m_curr;
TRACE("expr2polynomial", tout << "processing: " << fr.m_idx << "\n" << mk_ismt2_pp(a, m()) << "\n";);
unsigned num_args = a->get_num_args();
while (fr.m_idx < num_args) {
expr * arg = t->get_arg(fr.m_idx);
expr * arg = a->get_arg(fr.m_idx);
fr.m_idx++;
if (!visit(arg))
goto begin_loop;
}
process_app(t);
process_app(a);
m_frame_stack.pop_back();
}
}

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

@ -1071,7 +1071,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
split_fp(x, x_sgn, x_exp, x_sig);
split_fp(y, y_sgn, y_exp, y_sig);
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
mk_is_zero(x, x_is_zero);
mk_is_zero(y, y_is_zero);
m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
@ -1079,12 +1079,16 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
mk_is_nan(y, y_is_nan);
mk_pzero(f, pzero);
expr_ref sgn_diff(m);
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
expr_ref lt(m);
mk_float_lt(f, num, args, lt);
result = y;
mk_ite(lt, x, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);
@ -1109,12 +1113,16 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
mk_is_nan(y, y_is_nan);
mk_pzero(f, pzero);
expr_ref sgn_diff(m);
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
expr_ref gt(m);
mk_float_gt(f, num, args, gt);
result = y;
mk_ite(gt, x, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(both_zero, y, result, result);
mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);
@ -2211,13 +2219,13 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
SASSERT(sz == 3);
BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
mpf_rounding_mode rm;
mpf_rounding_mode mrm;
switch (bv_rm) {
case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break;
case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break;
case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break;
case BV_RM_TIES_TO_AWAY: mrm = MPF_ROUND_NEAREST_TAWAY; break;
case BV_RM_TIES_TO_EVEN: mrm = MPF_ROUND_NEAREST_TEVEN; break;
case BV_RM_TO_NEGATIVE: mrm = MPF_ROUND_TOWARD_NEGATIVE; break;
case BV_RM_TO_POSITIVE: mrm = MPF_ROUND_TOWARD_POSITIVE; break;
case BV_RM_TO_ZERO: mrm = MPF_ROUND_TOWARD_ZERO; break;
default: UNREACHABLE();
}
@ -2229,17 +2237,15 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
return mk_pzero(f, result);
else {
scoped_mpf v(m_mpf_manager);
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
m_util.fm().set(v, ebits, sbits, mrm, q.to_mpq());
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
mk_bias(unbiased_exp, e);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, e, s, result);
mk_fp(sgn, exp, sig, result);
}
}
else if (m_util.au().is_numeral(x)) {
@ -2267,44 +2273,45 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
expr_ref v1(m), v2(m), v3(m), v4(m);
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
expr_ref sgn(m), sig(m), exp(m), unbiased_exp(m);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v1);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v1);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v2);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v2);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v3);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v3);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v4);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, exp, sig, v4);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_bias(unbiased_exp, exp);
mk_fp(sgn, e, s, result);
mk_fp(sgn, exp, sig, result);
mk_ite(rm_tn, v4, result, result);
mk_ite(rm_tp, v3, result, result);
mk_ite(rm_nte, v2, result, result);
mk_ite(rm_nta, v1, result, result);
}
}
else {
else {
SASSERT(!m_arith_util.is_numeral(x));
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2322,12 +2329,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
expr_ref rme(rm, m);
round(s, rme, sgn, sig, exp, result);
expr_ref c0(m);
mk_is_zero(x, c0);
mk_ite(c0, x, result, result);
expr * e = m.mk_eq(m_util.mk_to_real(result), x);
m_extra_assertions.push_back(e);
m_extra_assertions.push_back(e);
}
SASSERT(is_well_sorted(m, result));
@ -2950,9 +2953,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
dbg_decouple("fpa2bv_to_sbv_shift", shift);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
dbg_decouple("fpa2bv_to_sbv_shift", shift);
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...]
@ -2961,34 +2963,48 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
expr_ref c_in_limits(m);
c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2));
dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits);
expr_ref shifted_sig(m);
shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
dbg_decouple("fpa2bv_to_sbv_shifted_sig", shifted_sig);
expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m);
huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz));
huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs);
huge_shifted_sig = m_bv_util.mk_bv_lshr(huge_sig, huge_shift);
dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig);
SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz);
expr_ref upper_hss(m), lower_hss(m);
upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig);
lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig);
SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1);
SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1);
dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss);
dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss);
expr_ref last(m), round(m), sticky(m);
last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig);
round = m_bv_util.mk_extract(sig_sz - bv_sz - 1, sig_sz - bv_sz - 1, shifted_sig);
sticky = m.mk_ite(m.mk_eq(m_bv_util.mk_extract(sig_sz - bv_sz - 2, 0, shifted_sig),
m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)),
bv0,
bv1);
last = m_bv_util.mk_extract(1, 1, upper_hss);
round = m_bv_util.mk_extract(0, 0, upper_hss);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get());
dbg_decouple("fpa2bv_to_sbv_last", last);
dbg_decouple("fpa2bv_to_sbv_round", round);
dbg_decouple("fpa2bv_to_sbv_sticky", sticky);
expr_ref upper_hss_w_sticky(m);
upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky);
dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky);
SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz);
expr_ref rounding_decision(m);
rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision);
expr_ref unrounded_sig(m), pre_rounded(m), inc(m);
unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig));
inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision));
unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky);
inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision);
pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc);
dbg_decouple("fpa2bv_to_sbv_inc", inc);
dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig);
@ -3345,7 +3361,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
// the maximum shift is `sbits', because after that the mantissa
// would be zero anyways. So we can safely cut the shift variable down,
// as long as we check the higher bits.
expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m);
expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
zero_s = m_bv_util.mk_numeral(0, sbits-1);
sbits_s = m_bv_util.mk_numeral(sbits, sbits);
sh = m_bv_util.mk_extract(ebits-1, sbits, shift);
@ -3406,6 +3422,17 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
}
expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
expr_ref rmr(rm, m);
expr_ref sgnr(sgn, m);
expr_ref lastr(last, m);
expr_ref roundr(round, m);
expr_ref stickyr(sticky, m);
dbg_decouple("fpa2bv_rnd_dec_rm", rmr);
dbg_decouple("fpa2bv_rnd_dec_sgn", sgnr);
dbg_decouple("fpa2bv_rnd_dec_last", lastr);
dbg_decouple("fpa2bv_rnd_dec_round", roundr);
dbg_decouple("fpa2bv_rnd_dec_sticky", stickyr);
expr_ref last_or_sticky(m), round_or_sticky(m), not_last(m), not_round(m), not_sticky(m), not_lors(m), not_rors(m), not_sgn(m);
expr * last_sticky[2] = { last, sticky };
expr * round_sticky[2] = { round, sticky };
@ -3443,6 +3470,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * la
m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, res);
dbg_decouple("fpa2bv_rnd_dec_res", res);
return res;
}

18
src/ast/func_decl_dependencies.cpp
View file

@ -145,24 +145,24 @@ class func_decl_dependencies::top_sort {
return false;
m_todo.push_back(f);
while (!m_todo.empty()) {
func_decl * f = m_todo.back();
func_decl * cf = m_todo.back();
switch (get_color(f)) {
switch (get_color(cf)) {
case CLOSED:
m_todo.pop_back();
break;
case OPEN:
set_color(f, IN_PROGRESS);
if (visit_children(f)) {
SASSERT(m_todo.back() == f);
set_color(cf, IN_PROGRESS);
if (visit_children(cf)) {
SASSERT(m_todo.back() == cf);
m_todo.pop_back();
set_color(f, CLOSED);
set_color(cf, CLOSED);
}
break;
case IN_PROGRESS:
if (all_children_closed(f)) {
SASSERT(m_todo.back() == f);
set_color(f, CLOSED);
if (all_children_closed(cf)) {
SASSERT(m_todo.back() == cf);
set_color(cf, CLOSED);
} else {
m_todo.reset();
return true;

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

@ -464,18 +464,18 @@ void bit_blaster_tpl<Cfg>::mk_udiv_urem(unsigned sz, expr * const * a_bits, expr
// update p
if (i < sz - 1) {
for (unsigned j = sz - 1; j > 0; j--) {
expr_ref i(m());
mk_ite(q, t.get(j-1), p.get(j-1), i);
p.set(j, i);
expr_ref ie(m());
mk_ite(q, t.get(j-1), p.get(j-1), ie);
p.set(j, ie);
}
p.set(0, a_bits[sz - i - 2]);
}
else {
// last step: p contains the remainder
for (unsigned j = 0; j < sz; j++) {
expr_ref i(m());
mk_ite(q, t.get(j), p.get(j), i);
p.set(j, i);
expr_ref ie(m());
mk_ite(q, t.get(j), p.get(j), ie);
p.set(j, ie);
}
}
}

23
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -143,9 +143,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result)
br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) {
if (m_hi_fp_unspecified)
result = m_util.au().mk_numeral(0, false);
else
// The "hardware interpretation" is 0.
result = m_util.au().mk_numeral(rational(0), false);
else
result = m_util.mk_internal_to_real_unspecified();
return BR_DONE;
@ -243,7 +243,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
!m_util.au().is_numeral(args[2], r2))
return BR_FAILED;
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
TRACE("fp_rewriter", tout << "r1: " << r1 << ", r2: " << r2 << "\n";);
m_fm.set(v, ebits, sbits, rmv, r1.to_mpq(), r2.to_mpq().numerator());
result = m_util.mk_value(v);
return BR_DONE;
@ -420,11 +420,15 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
// min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2,
m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1,
arg2))));
arg2)))));
return BR_REWRITE_FULL;
}
@ -445,12 +449,16 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_ite(mk_eq_nan(arg1),
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
arg1,
// max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2),
m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
arg2,
m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1,
arg2))));
arg2)))));
return BR_REWRITE_FULL;
}
@ -583,6 +591,7 @@ br_status fpa_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_zero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -593,6 +602,7 @@ br_status fpa_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_nzero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
@ -603,6 +613,7 @@ br_status fpa_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
br_status fpa_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
scoped_mpf v(m_fm);
if (m_util.is_numeral(arg1, v)) {
result = (m_fm.is_pzero(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;

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

@ -324,7 +324,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
}
result_stack().push_back(def);
TRACE("get_macro", tout << "bindings:\n";
for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";);
begin_scope();
m_num_qvars = 0;
m_root = def;

2
src/ast/shared_occs.h
View file

@ -75,7 +75,7 @@ public:
iterator end_shared() const { return m_shared.end(); }
void reset();
void cleanup();
void display(std::ostream & out, ast_manager & m) const;
void display(std::ostream & out, ast_manager & mgr) const;
};
#endif

12
src/cmd_context/cmd_context.cpp
View file

@ -40,6 +40,7 @@ Notes:
#include"for_each_expr.h"
#include"scoped_timer.h"
#include"interpolant_cmds.h"
#include"model_smt2_pp.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
@ -528,6 +529,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "LRA" ||
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "HORN";
}
@ -547,6 +549,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
s == "QF_AUFBV" ||
s == "QF_BVRE" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "HORN";
}
@ -1402,6 +1405,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
was_pareto = true;
get_opt()->display_assignment(regular_stream());
regular_stream() << "\n";
if (get_opt()->print_model()) {
model_ref mdl;
get_opt()->get_model(mdl);
if (mdl) {
regular_stream() << "(model " << std::endl;
model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2);
regular_stream() << ")" << std::endl;
}
}
r = get_opt()->optimize();
}
}

1
src/cmd_context/cmd_context.h
View file

@ -124,6 +124,7 @@ public:
virtual void display_assignment(std::ostream& out) = 0;
virtual bool is_pareto() = 0;
virtual void set_logic(symbol const& s) = 0;
virtual bool print_model() const = 0;
};
class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {

24
src/interp/iz3mgr.cpp
View file

@ -616,6 +616,30 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
extract_lcd(rats);
}
void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_gomory_cut_coeffs(proof,rats);
coeffs.resize(rats.size());
for(unsigned i = 0; i < rats.size(); i++){
coeffs[i] = make_int(rats[i]);
}
}
void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats){
symb s = sym(proof);
int numps = s->get_num_parameters();
rats.resize(numps-2);
for(int i = 2; i < numps; i++){
rational r;
bool ok = s->get_parameter(i).is_rational(r);
if(!ok)
throw "Bad Farkas coefficient";
rats[i-2] = r;
}
abs_rat(rats);
extract_lcd(rats);
}
void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& coeffs){
std::vector<rational> rats;
get_assign_bounds_rule_coeffs(proof,rats);

8
src/interp/iz3mgr.h
View file

@ -396,7 +396,7 @@ class iz3mgr {
return UnknownTheory;
}
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,GomoryCutKind,ArithMysteryKind,UnknownKind};
lemma_kind get_theory_lemma_kind(const ast &proof){
symb s = sym(proof);
@ -417,6 +417,8 @@ class iz3mgr {
return AssignBoundsKind;
if(foo == "eq-propagate")
return EqPropagateKind;
if(foo == "gomory-cut")
return GomoryCutKind;
return UnknownKind;
}
@ -434,6 +436,10 @@ class iz3mgr {
void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& rats);
void get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats);
void get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& rats);
bool is_farkas_coefficient_negative(const ast &proof, int n);
bool is_true(ast t){

32
src/interp/iz3translate.cpp
View file

@ -1182,6 +1182,31 @@ public:
return res;
}
ast GomoryCutRule2Farkas(const ast &proof, const ast &con, std::vector<Iproof::node> prems){
std::vector<Iproof::node> my_prems = prems;
std::vector<ast> my_coeffs;
std::vector<Iproof::node> my_prem_cons;
get_gomory_cut_coeffs(proof,my_coeffs);
int nargs = num_prems(proof);
if(nargs != (int)(my_coeffs.size()))
throw "bad gomory-cut theory lemma";
for(int i = 0; i < nargs; i++)
my_prem_cons.push_back(conc(prem(proof,i)));
ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons));
Iproof::node hyp = iproof->make_hypothesis(mk_not(my_con));
my_prems.push_back(hyp);
my_coeffs.push_back(make_int("1"));
my_prem_cons.push_back(mk_not(my_con));
Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_prem_cons,my_coeffs);
ast t = arg(my_con,0);
ast c = arg(my_con,1);
ast d = gcd_of_coefficients(t);
t = z3_simplify(mk_idiv(t,d));
c = z3_simplify(mk_idiv(c,d));
ast cut_con = make(op(my_con),t,c);
return iproof->make_cut_rule(my_con,d,cut_con,res);
}
Iproof::node RewriteClause(Iproof::node clause, const ast &rew){
if(pr(rew) == PR_MONOTONICITY){
int nequivs = num_prems(rew);
@ -1912,6 +1937,13 @@ public:
res = AssignBounds2Farkas(proof,conc(proof));
break;
}
case GomoryCutKind: {
if(args.size() > 0)
res = GomoryCutRule2Farkas(proof, conc(proof), args);
else
throw unsupported();
break;
}
case EqPropagateKind: {
std::vector<ast> prems(nprems);
for(unsigned i = 0; i < nprems; i++)

1
src/math/euclid/euclidean_solver.cpp
View file

@ -609,6 +609,7 @@ struct euclidean_solver::imp {
// neg coeffs... to make sure that m_next_x is -1
neg_coeffs(eq.m_as);
neg_coeffs(eq.m_bs);
m().neg(eq.m_c);
}
unsigned sz = eq.size();
for (unsigned i = 0; i < sz; i++) {

4
src/muz/base/dl_context.cpp
View file

@ -945,6 +945,10 @@ namespace datalog {
if (m_engine) {
m_engine->collect_statistics(st);
}
unsigned long long max_mem = memory::get_max_used_memory();
unsigned long long mem = memory::get_allocation_size();
st.update("max memory", static_cast<double>(max_mem)/(1024.0*1024.0));
st.update("memory", static_cast<double>(mem)/(1024.0*1024.0));
}

1
src/muz/base/rule_properties.cpp
View file

@ -194,7 +194,6 @@ void rule_properties::operator()(app* n) {
}
}
else {
std::cout << mk_pp(n, m) << "\n";
}
}

14
src/muz/rel/dl_compiler.cpp
View file

@ -85,7 +85,7 @@ namespace datalog {
removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
reg_idx & result, bool reuse, instruction_block & acc) {
relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
@ -139,7 +139,7 @@ namespace datalog {
return r;
}
compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
compiler::reg_idx compiler::get_single_column_register(const relation_sort s) {
relation_signature singl_sig;
singl_sig.push_back(s);
return get_fresh_register(singl_sig);
@ -165,7 +165,7 @@ namespace datalog {
}
}
void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val,
void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val,
reg_idx & result, bool & dealloc, instruction_block & acc) {
reg_idx singleton_table;
if(!m_constant_registers.find(s, val, singleton_table)) {
@ -185,7 +185,7 @@ namespace datalog {
}
}
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result,
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
bool & dealloc, instruction_block & acc) {
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
@ -862,9 +862,11 @@ namespace datalog {
ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size();
if (pt_len == ut_len) {
// no negated predicates
if (pt_len == ut_len)
return;
}
// populate negative variables:
for (unsigned i = pt_len; i < ut_len; ++i) {
app * neg_tail = r->get_tail(i);

8
src/muz/rel/dl_compiler.h
View file

@ -135,7 +135,7 @@ namespace datalog {
reg_idx get_fresh_register(const relation_signature & sig);
reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r);
reg_idx get_single_column_register(const relation_sort & s);
reg_idx get_single_column_register(const relation_sort s);
/**
\brief Allocate registers for predicates in \c pred and add them into the \c regs map.
@ -150,7 +150,7 @@ namespace datalog {
const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc);
void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
reg_idx & result, bool reuse, instruction_block & acc);
/**
\brief Create add an union or widen operation and put it into \c acc.
@ -174,10 +174,10 @@ namespace datalog {
void make_dealloc_non_void(reg_idx r, instruction_block & acc);
void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val,
void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val,
reg_idx & result, bool & dealloc, instruction_block & acc);
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result,
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
bool & dealloc, instruction_block & acc);
void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc);

6
src/opt/opt_cmds.cpp
View file

@ -323,12 +323,8 @@ private:
void display_statistics(cmd_context& ctx) {
statistics stats;
unsigned long long max_mem = memory::get_max_used_memory();
unsigned long long mem = memory::get_allocation_size();
stats.update("time", ctx.get_seconds());
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
get_opt(ctx).collect_statistics(stats);
stats.update("time", ctx.get_seconds());
stats.display_smt2(ctx.regular_stream());
}
};

10
src/opt/opt_context.cpp
View file

@ -254,6 +254,12 @@ namespace opt {
}
}
bool context::print_model() const {
opt_params optp(m_params);
return optp.print_model();
}
void context::get_base_model(model_ref& mdl) {
mdl = m_model;
}
@ -1179,6 +1185,10 @@ namespace opt {
for (; it != end; ++it) {
it->m_value->collect_statistics(stats);
}
unsigned long long max_mem = memory::get_max_used_memory();
unsigned long long mem = memory::get_allocation_size();
stats.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
stats.update("max memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
}
void context::collect_param_descrs(param_descrs & r) {

1
src/opt/opt_context.h
View file

@ -180,6 +180,7 @@ namespace opt {
virtual void cancel() { set_cancel(true); }
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;
virtual void get_model(model_ref& _m);
virtual void set_model(model_ref& _m);
virtual void fix_model(model_ref& _m);

48
src/qe/qe_mbp.h Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qe_mbp.h
Abstract:
Model-based projection utilities
Author:
Nikolaj Bjorner (nbjorner) 2015-5-28
Revision History:
--*/
#ifndef __QE_MBP_H__
#define __QE_MBP_H__
#include "ast.h"
#include "params.h"
namespace qe {
class mbp {
class impl;
impl * m_impl;
public:
mbp(ast_manager& m);
~mbp();
/**
\brief
Apply model-based qe on constants provided as vector of variables.
Return the updated formula and updated set of variables that were not eliminated.
*/
void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
void set_cancel(bool f);
};
}
#endif

281
src/qe/qsat.cpp Normal file
View file

@ -0,0 +1,281 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qsat.cpp
Abstract:
Quantifier Satisfiability Solver.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-28
Revision History:
--*/
#include "qsat.h"
#include "smt_kernel.h"
#include "qe_mbp.h"
#include "smt_params.h"
#include "ast_util.h"
using namespace qe;
struct qdef_t {
expr_ref m_pred;
expr_ref m_expr;
expr_ref_vector m_vars;
bool m_is_forall;
qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall):
m_pred(p),
m_expr(e),
m_vars(vars),
m_is_forall(is_forall) {}
};
typedef vector<qdef_t> qdefs_t;
struct pdef_t {
expr_ref m_pred;
expr_ref m_atom;
pdef_t(expr_ref& p, expr* a):
m_pred(p),
m_atom(a, p.get_manager())
{}
};
class qsat::impl {
ast_manager& m;
qe::mbp mbp;
smt_params m_smtp;
smt::kernel m_kernel;
expr_ref m_fml_pred; // predicate that encodes top-level formula
expr_ref_vector m_atoms; // predicates that encode atomic subformulas
lbool check_sat() {
// TBD main procedure goes here.
return l_undef;
}
/**
\brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
*/
void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) {
}
/**
\brief create propositional abstration of formula by replacing atomic sub-formulas by fresh
propositional variables, and adding definitions for each propositional formula on the side.
Assumption is that the formula is quantifier-free.
*/
void mk_abstract(expr_ref& fml, vector<pdef_t>& pdefs) {
expr_ref_vector todo(m), trail(m);
obj_map<expr,expr*> cache;
ptr_vector<expr> args;
expr_ref r(m);
todo.push_back(fml);
while (!todo.empty()) {
expr* e = todo.back();
if (cache.contains(e)) {
todo.pop_back();
continue;
}
SASSERT(is_app(e));
app* a = to_app(e);
if (a->get_family_id() == m.get_basic_family_id()) {
unsigned sz = a->get_num_args();
args.reset();
for (unsigned i = 0; i < sz; ++i) {
expr* f = a->get_arg(i);
if (cache.find(f, f)) {
args.push_back(f);
}
else {
todo.push_back(f);
}
}
if (args.size() == sz) {
r = m.mk_app(a->get_decl(), sz, args.c_ptr());
cache.insert(e, r);
trail.push_back(r);
todo.pop_back();
}
}
else if (is_uninterp_const(a)) {
cache.insert(e, e);
}
else {
// TBD: nested Booleans.
r = m.mk_fresh_const("p",m.mk_bool_sort());
trail.push_back(r);
cache.insert(e, r);
pdefs.push_back(pdef_t(r, e));
}
}
fml = cache.find(fml);
}
/**
\brief use dual propagation to minimize model.
*/
bool minimize_assignment(expr_ref_vector& assignment, expr* not_fml) {
bool result = false;
assignment.push_back(not_fml);
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
switch (res) {
case l_true:
UNREACHABLE();
break;
case l_undef:
break;
case l_false:
result = true;
get_core(assignment, not_fml);
break;
}
return result;
}
lbool check_sat(expr_ref_vector& assignment, expr* fml) {
assignment.push_back(fml);
lbool res = m_kernel.check(assignment.size(), assignment.c_ptr());
switch (res) {
case l_true: {
model_ref mdl;
expr_ref tmp(m);
assignment.reset();
m_kernel.get_model(mdl);
for (unsigned i = 0; i < m_atoms.size(); ++i) {
expr* p = m_atoms[i].get();
if (mdl->eval(p, tmp)) {
if (m.is_true(tmp)) {
assignment.push_back(p);
}
else if (m.is_false(tmp)) {
assignment.push_back(m.mk_not(p));
}
}
}
expr_ref not_fml = mk_not(fml);
if (!minimize_assignment(assignment, not_fml)) {
res = l_undef;
}
break;
}
case l_undef:
break;
case l_false:
get_core(assignment, fml);
break;
}
return res;
}
void get_core(expr_ref_vector& core, expr* exclude) {
unsigned sz = m_kernel.get_unsat_core_size();
core.reset();
for (unsigned i = 0; i < sz; ++i) {
expr* e = m_kernel.get_unsat_core_expr(i);
if (e != exclude) {
core.push_back(e);
}
}
}
expr_ref mk_not(expr* e) {
return expr_ref(::mk_not(m, e), m);
}
public:
impl(ast_manager& m):
m(m),
mbp(m),
m_kernel(m, m_smtp),
m_fml_pred(m),
m_atoms(m) {}
void updt_params(params_ref const & p) {
}
void collect_param_descrs(param_descrs & r) {
}
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
}
void collect_statistics(statistics & st) const {
}
void reset_statistics() {
}
void cleanup() {
}
void set_logic(symbol const & l) {
}
void set_progress_callback(progress_callback * callback) {
}
tactic * translate(ast_manager & m) {
return 0;
}
};
qsat::qsat(ast_manager& m) {
m_impl = alloc(impl, m);
}
qsat::~qsat() {
dealloc(m_impl);
}
void qsat::updt_params(params_ref const & p) {
m_impl->updt_params(p);
}
void qsat::collect_param_descrs(param_descrs & r) {
m_impl->collect_param_descrs(r);
}
void qsat::operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
(*m_impl)(in, result, mc, pc, core);
}
void qsat::collect_statistics(statistics & st) const {
m_impl->collect_statistics(st);
}
void qsat::reset_statistics() {
m_impl->reset_statistics();
}
void qsat::cleanup() {
m_impl->cleanup();
}
void qsat::set_logic(symbol const & l) {
m_impl->set_logic(l);
}
void qsat::set_progress_callback(progress_callback * callback) {
m_impl->set_progress_callback(callback);
}
tactic * qsat::translate(ast_manager & m) {
return m_impl->translate(m);
}

52
src/qe/qsat.h Normal file
View file

@ -0,0 +1,52 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qsat.h
Abstract:
Quantifier Satisfiability Solver.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-28
Revision History:
--*/
#ifndef __QE_QSAT_H__
#define __QE_QSAT_H__
#include "tactic.h"
namespace qe {
class qsat : public tactic {
class impl;
impl * m_impl;
public:
qsat(ast_manager& m);
~qsat();
virtual void updt_params(params_ref const & p);
virtual void collect_param_descrs(param_descrs & r);
virtual void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core);
virtual void collect_statistics(statistics & st) const;
virtual void reset_statistics();
virtual void cleanup() = 0;
virtual void set_logic(symbol const & l);
virtual void set_progress_callback(progress_callback * callback);
virtual tactic * translate(ast_manager & m);
};
};
#endif

6
src/smt/smt_internalizer.cpp
View file

@ -1411,6 +1411,10 @@ namespace smt {
void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
justification * js = 0;
TRACE("mk_th_axiom",
display_literals_verbose(tout, num_lits, lits);
tout << "\n";);
if (m_manager.proofs_enabled()) {
js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
}
@ -1425,13 +1429,11 @@ namespace smt {
void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {
literal ls[2] = { l1, l2 };
TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << "\n";);
mk_th_axiom(tid, 2, ls, num_params, params);
}
void context::mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
literal ls[3] = { l1, l2, l3 };
TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << " "; display_literal(tout, l3); tout << "\n";);
mk_th_axiom(tid, 3, ls, num_params, params);
}

2
src/smt/smt_setup.cpp
View file

@ -116,7 +116,7 @@ namespace smt {
setup_LRA();
else if (m_logic == "QF_FP")
setup_QF_FP();
else if (m_logic == "QF_FPBV")
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
setup_QF_FPBV();
else
setup_unknown();

2
src/smt/theory_arith.h
View file

@ -245,6 +245,8 @@ namespace smt {
parameter* params(char const* name);
};
class gomory_cut_justification;
class bound {
protected:
theory_var m_var;

1
src/smt/theory_arith_core.h
View file

@ -439,6 +439,7 @@ namespace smt {
j += rational(1);
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.begin());
#else
// performs slightly worse.
literal_buffer lits;

25
src/smt/theory_arith_int.h
View file

@ -460,13 +460,16 @@ namespace smt {
SASSERT(is_well_sorted(get_manager(), result));
}
class gomory_cut_justification : public ext_theory_propagation_justification {
template<typename Ext>
class theory_arith<Ext>::gomory_cut_justification : public ext_theory_propagation_justification {
public:
gomory_cut_justification(family_id fid, region & r,
gomory_cut_justification(family_id fid, region & r,
unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,
antecedents& bounds,
literal consequent):
ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent) {
ext_theory_propagation_justification(fid, r, num_lits, lits, num_eqs, eqs, consequent,
bounds.num_params(), bounds.params("gomory-cut")) {
}
// Remark: the assignment must be propagated back to arith
virtual theory_id get_from_theory() const { return null_theory_id; }
@ -530,7 +533,7 @@ namespace smt {
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
else {
SASSERT(at_upper(x_j));
@ -546,7 +549,7 @@ namespace smt {
}
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
pol.push_back(row_entry(new_a_ij, x_j));
}
@ -571,7 +574,7 @@ namespace smt {
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
else {
SASSERT(at_upper(x_j));
@ -584,7 +587,7 @@ namespace smt {
new_a_ij.neg(); // the upper terms are inverted
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero(), coeffs_enabled());
upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
pol.push_back(row_entry(new_a_ij, x_j));
@ -600,7 +603,7 @@ namespace smt {
if (pol.empty()) {
SASSERT(k.is_pos());
// conflict 0 >= k where k is positive
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory_cut");
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory-cut");
return true;
}
else if (pol.size() == 1) {
@ -652,7 +655,7 @@ namespace smt {
gomory_cut_justification(
get_id(), ctx.get_region(),
ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l)));
ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
return true;
}
@ -1061,6 +1064,7 @@ namespace smt {
}
if (!failed) {
m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j);
TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";);
}
else {
TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";);
@ -1191,7 +1195,8 @@ namespace smt {
if (l != 0) {
rational l_old = l->get_value().get_rational().to_rational();
rational l_new = g*ceil((l_old - c2)/g) + c2;
TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";);
TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";
tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";);
if (l_new > l_old) {
propagated = true;
mk_lower(v, l_new, l, m_js);

44
src/smt/theory_array_full.cpp
View file

@ -208,6 +208,8 @@ namespace smt {
theory_array::reset_eh();
std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
m_var_data_full.reset();
m_eqs.reset();
m_eqsv.reset();
}
void theory_array_full::display_var(std::ostream & out, theory_var v) const {
@ -223,7 +225,6 @@ namespace smt {
}
theory_var theory_array_full::mk_var(enode * n) {
theory_var r = theory_array::mk_var(n);
SASSERT(r == static_cast<int>(m_var_data_full.size()));
m_var_data_full.push_back(alloc(var_data_full));
@ -512,7 +513,7 @@ namespace smt {
TRACE("array_map_bug",
tout << "select-map axiom\n" << mk_ismt2_pp(sel1, m) << "\n=\n" << mk_ismt2_pp(sel2,m) << "\n";);
return try_assign_eq(sel1, sel2);
}
@ -760,37 +761,36 @@ namespace smt {
r = FC_CONTINUE;
}
}
while (!m_eqsv.empty()) {
literal eq = m_eqsv.back();
m_eqsv.pop_back();
get_context().mark_as_relevant(eq);
assert_axiom(eq);
r = FC_CONTINUE;
}
if (r == FC_DONE && m_found_unsupported_op)
r = FC_GIVEUP;
return r;
}
bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
context& ctx = get_context();
enode* n1 = ctx.get_enode(v1);
enode* n2 = ctx.get_enode(v2);
if (n1->get_root() == n2->get_root()) {
return false;
}
TRACE("array",
tout << mk_bounded_pp(v1, get_manager()) << "\n==\n"
<< mk_bounded_pp(v2, get_manager()) << "\n";);
#if 0
if (m.proofs_enabled()) {
#endif
literal eq(mk_eq(v1,v2,true));
ctx.mark_as_relevant(eq);
assert_axiom(eq);
#if 0
context& ctx = get_context();
if (m_eqs.contains(v1, v2)) {
return false;
}
else {
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
ctx.assign_eq(n1, n2, eq_justification::mk_axiom());
m_eqs.insert(v1, v2, true);
literal eq(mk_eq(v1, v2, true));
get_context().mark_as_relevant(eq);
assert_axiom(eq);
// m_eqsv.push_back(eq);
return true;
}
#endif
return true;
}
void theory_array_full::pop_scope_eh(unsigned num_scopes) {
@ -798,6 +798,8 @@ namespace smt {
theory_array::pop_scope_eh(num_scopes);
std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc<var_data_full>());
m_var_data_full.shrink(num_old_vars);
m_eqs.reset();
m_eqsv.reset();
}
void theory_array_full::collect_statistics(::statistics & st) const {

7
src/smt/theory_array_full.h
View file

@ -38,12 +38,12 @@ namespace smt {
ast2ast_trailmap<sort,app> m_sort2epsilon;
simplifier* m_simp;
obj_pair_map<expr,expr,bool> m_eqs;
svector<literal> m_eqsv;
protected:
#if 0
virtual final_check_status final_check_eh();
#endif
//virtual final_check_status final_check_eh();
virtual void reset_eh();
virtual void set_prop_upward(theory_var v);
@ -84,6 +84,7 @@ namespace smt {
bool try_assign_eq(expr* n1, expr* n2);
void assign_eqs();
public:

4
src/tactic/arith/arith_bounds_tactic.cpp
View file

@ -34,8 +34,8 @@ struct arith_bounds_tactic : public tactic {
bounds_arith_subsumption(in, result);
}
virtual tactic* translate(ast_manager& m) {
return alloc(arith_bounds_tactic, m);
virtual tactic* translate(ast_manager & mgr) {
return alloc(arith_bounds_tactic, mgr);
}
void checkpoint() {

2
src/tactic/arith/card2bv_tactic.cpp
View file

@ -488,7 +488,7 @@ public:
unsigned size = g->size();
expr_ref new_f1(m), new_f2(m);
proof_ref new_pr1(m), new_pr2(m);
for (unsigned idx = 0; idx < size; idx++) {
for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
m_rw1(g->form(idx), new_f1, new_pr1);
TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
m_rw2.rewrite(new_f1, new_f2);

45
src/tactic/fpa/qffp_tactic.cpp
View file

@ -23,9 +23,47 @@ Notes:
#include"fpa2bv_tactic.h"
#include"smt_tactic.h"
#include"propagate_values_tactic.h"
#include"probe_arith.h"
#include"qfnra_tactic.h"
#include"qffp_tactic.h"
struct has_fp_to_real_predicate {
struct found {};
ast_manager & m;
bv_util bu;
fpa_util fu;
arith_util au;
has_fp_to_real_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {}
void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); }
void operator()(app * n) {
sort * s = get_sort(n);
if (au.is_real(s) && n->get_family_id() == fu.get_family_id() &&
is_app(n) && to_app(n)->get_decl_kind() == OP_FPA_TO_REAL)
throw found();
}
};
class has_fp_to_real_probe : public probe {
public:
virtual result operator()(goal const & g) {
return !test<has_fp_to_real_predicate>(g);
}
virtual ~has_fp_to_real_probe() {}
};
probe * mk_has_fp_to_real_probe() {
return alloc(has_fp_to_real_probe);
}
tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool("arith_lhs", true);
@ -40,10 +78,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
mk_propagate_values_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p),
mk_bit_blaster_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p),
using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(),
mk_sat_tactic(m, p),
mk_smt_tactic(p)),
cond(mk_has_fp_to_real_probe(),
mk_qfnra_tactic(m, p),
mk_smt_tactic(p))
),
mk_fail_if_undecided_tactic())));
st->updt_params(p);

2
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
return mk_ufbv_tactic(m, p);
else if (logic=="QF_FP")
return mk_qffp_tactic(m, p);
else if (logic == "QF_FPBV")
else if (logic == "QF_FPBV" || logic == "QF_BVFP")
return mk_qffpbv_tactic(m, p);
else if (logic=="HORN")
return mk_horn_tactic(m, p);

2
src/tactic/tactical.cpp
View file

@ -709,8 +709,6 @@ public:
tactic_ref_vector ts2;
goal_ref_vector g_copies;
ast_manager & m = in->m();
for (unsigned i = 0; i < r1_size; i++) {
ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode());
managers.push_back(new_m);

12
src/util/mpf.cpp
View file

@ -1229,7 +1229,11 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
}
void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x) || (is_zero(x) && is_zero(y)))
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);
@ -1240,7 +1244,11 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
}
void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x) || (is_zero(x) && is_zero(y)))
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);