mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 07:15:47 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-06-26 08:24:58 +02:00
commit 47da717947
11 changed files with 16 additions and 3475 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz/rel/check_relation.cpp
View file

@ -429,7 +429,7 @@ namespace datalog {
if (res == l_false) {
IF_VERBOSE(3, verbose_stream() << objective << " verified\n";);
}
else {
else if (res == l_true) {
IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
verbose_stream() << mk_pp(fml1, m) << "\n";
verbose_stream() << mk_pp(fml2, m) << "\n";
@ -720,12 +720,12 @@ namespace datalog {
relation_signature const& sig1 = dst.get_signature();
relation_signature const& sig2 = neg.get_signature();
expr_ref dstf(m), negf(m);
std::cout << mk_pp(dst0, m) << "\n";
//std::cout << mk_pp(dst0, m) << "\n";
expr_ref_vector eqs(m);
dst.to_formula(dstf);
std::cout << mk_pp(dstf, m) << "\n";
//std::cout << mk_pp(dstf, m) << "\n";
neg.to_formula(negf);
std::cout << mk_pp(negf, m) << "\n";
//std::cout << mk_pp(negf, m) << "\n";
eqs.push_back(negf);
for (unsigned i = 0; i < cols1.size(); ++i) {
var_ref v1(m), v2(m);
@ -747,8 +747,8 @@ namespace datalog {
negf = m.mk_and(dst0, m.mk_not(negf));
negf = ground(dst, negf);
dstf = ground(dst, dstf);
std::cout << negf << "\n";
std::cout << dstf << "\n";
//std::cout << negf << "\n";
//std::cout << dstf << "\n";
check_equiv("filter by negation", dstf, negf);
}

20
src/muz/rel/udoc_relation.cpp
View file

@ -723,12 +723,9 @@ namespace datalog {
conds.push_back(m.mk_eq(e1, e2));
}
void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const {
d.reset(dm);
d.push_back(dm.allocateX());
apply_guard(g, d, discard_cols);
}
void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
void udoc_relation::compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
result.push_back(dm.allocateX());
// datastructure to store equalities with columns that will be projected out
union_find_default_ctx union_ctx;
subset_ints equalities(union_ctx);
@ -737,6 +734,7 @@ namespace datalog {
}
apply_guard(g, result, equalities, discard_cols);
}
bool udoc_relation::apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const {
udoc_plugin& p = get_plugin();
unsigned num_bits;
@ -753,9 +751,6 @@ namespace datalog {
return false;
}
bool udoc_relation::apply_bv_eq(
expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const {
udoc_plugin& p = get_plugin();
@ -926,9 +921,10 @@ namespace datalog {
expr_ref guard(m);
for (unsigned i = 0; i < num_bits; ++i) {
m_equalities.mk_var();
}
t.extract_guard(condition, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_empty_bv);
}
t.extract_guard(condition, guard, m_reduced_condition);
m_udoc.push_back(dm.allocateX());
t.apply_guard(guard, m_udoc, m_equalities, m_empty_bv);
TRACE("doc",
tout << "original condition: " << mk_pp(condition, m) << "\n";

1
src/muz/rel/udoc_relation.h
View file

@ -72,7 +72,6 @@ namespace datalog {
void extract_equalities(
expr* e1, expr* e2, expr_ref_vector& conds,
subset_ints& equalities, unsigned_vector& roots) const;
void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
bool apply_ground_eq(doc_ref& d, unsigned v, unsigned hi, unsigned lo, expr* c) const;
bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const;

2
src/sat/sat_solver.h
View file

@ -210,7 +210,6 @@ namespace sat {
public:
bool inconsistent() const { return m_inconsistent; }
unsigned num_vars() const { return m_level.size(); }
unsigned num_clauses() const;
bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
@ -448,6 +447,7 @@ namespace sat {
protected:
void display_binary(std::ostream & out) const;
void display_units(std::ostream & out) const;
unsigned num_clauses() const;
bool is_unit(clause const & c) const;
bool is_empty(clause const & c) const;
bool check_missed_propagation(clause_vector const & cs) const;

150
src/tactic/fpa/const_intro_rewriter.h
View file

@ -1,150 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
const_intro_rewriter.h
Abstract:
Rewriter for converting FPA to BV
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#ifndef _CONST_INTRO_REWRITER_H_
#define _CONST_INTRO_REWRITER_H_
#include"cooperate.h"
#include"bv_decl_plugin.h"
#include"tactic_exception.h"
#include"fpa2bv_converter_prec.h"
struct const_intro_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr * m_exp;
func_decl_ref_vector m_introduced_consts;
obj_map<func_decl, app*> m_const2term_map;
unsigned long long m_max_memory;
unsigned m_max_steps;
fpa_util m_float_util;
ast_manager & m() const { return m_manager; }
const_intro_rewriter_cfg(ast_manager & m, params_ref const & p):
m_manager(m),
m_introduced_consts(m),
m_float_util(m) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
~const_intro_rewriter_cfg() {
for (obj_map<func_decl, app*>::iterator it = m_const2term_map.begin();
it != m_const2term_map.end();
it++)
{
m().dec_ref(it->m_key);
m().dec_ref(it->m_value);
}
}
void cleanup_buffers() {
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_float_util.is_float(f->get_range())) {
app * f_cnst = m_manager.mk_const(f);
if (!m_introduced_consts.contains(f))
m_introduced_consts.push_back(f);
result = f_cnst;
return BR_DONE;
}
if (f->get_family_id() == m_float_util.get_family_id()) {
switch (f->get_decl_kind()) {
case OP_FPA_ADD:
case OP_FPA_SUB:
case OP_FPA_NEG:
case OP_FPA_MUL:
case OP_FPA_DIV:
case OP_FPA_REM:
case OP_FPA_ABS:
case OP_FPA_MIN:
case OP_FPA_MAX:
case OP_FPA_FMA:
case OP_FPA_SQRT:
case OP_FPA_TO_FP:
case OP_FPA_ROUND_TO_INTEGRAL:
{
app * f_app = m_manager.mk_app(f, num, args);
result = m_manager.mk_fresh_const(NULL, f->get_range());
func_decl * fd = to_app(result)->get_decl();
m_introduced_consts.push_back(fd);
m_const2term_map.insert_if_not_there(fd, f_app);
m().inc_ref(fd);
m().inc_ref(f_app);
return BR_DONE;
}
default:
return BR_FAILED;
}
}
return BR_FAILED;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
return false;
}
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
return false;
}
bool pre_visit(expr * t){
return true;
}
};
template class rewriter_tpl<const_intro_rewriter_cfg>;
struct const_intro_rewriter : public rewriter_tpl<const_intro_rewriter_cfg> {
const_intro_rewriter_cfg m_cfg;
const_intro_rewriter(ast_manager & m, params_ref const & p):
rewriter_tpl<const_intro_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, p) {
}
};
#endif

1313
src/tactic/fpa/fpa2bv_approx_tactic.cpp
View file

File diff suppressed because it is too large Load diff

33
src/tactic/fpa/fpa2bv_approx_tactic.h
View file

@ -1,33 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_lazy_tactic.h
Abstract:
Tactic that converts floating points to bit-vectors lazily
Author:
Aleksander Zeljic 2012-11-15
Notes:
--*/
#ifndef _FPA2BV_APPROX_TACTIC_
#define _FPA2BV_APPROX_TACTIC_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_fpa2bv_approx_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("fpa2bv_approx", "An iterative approximation based bit-blasting decision procedure for FPA.", "mk_fpa2bv_approx_tactic(m, p)")
*/
#endif

1594
src/tactic/fpa/fpa2bv_converter_prec.cpp
View file

File diff suppressed because it is too large Load diff

103
src/tactic/fpa/fpa2bv_converter_prec.h
View file

@ -1,103 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_converter_prec.h
Abstract:
Conversion routines for Floating Point -> Bit-Vector
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#ifndef _FPA2BV_CONVERTER_PREC
#define _FPA2BV_CONVERTER_PREC
#include"ast.h"
#include"obj_hashtable.h"
#include"ref_util.h"
#include"fpa_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"model_converter.h"
#include"basic_simplifier_plugin.h"
#include"fpa2bv_converter.h"
#define MAX_PRECISION 100
#define MIN_PRECISION 0
class fpa2bv_prec_model_converter;
enum fpa_approximation_mode {
FPAA_PRECISE, // Always use precise encoding
FPAA_FIXBITS, // Approximate by fixing some bits of the encoding
FPAA_SMALL_FLOATS // Approximate by using smaller floats
};
#define FPAA_DEFAULT_MODE FPAA_SMALL_FLOATS
class fpa2bv_converter_prec : public fpa2bv_converter {
fpa_approximation_mode m_mode;
void fix_bits(unsigned prec, expr_ref rounded, unsigned sbits, unsigned ebits);//expr_ref& fixed,
void mk_small_op(func_decl * f, unsigned prec, unsigned num, expr * const * args, func_decl_ref & small_op, expr_ref_vector & cast_args);
void mk_small_op(func_decl * f, unsigned new_ebits, unsigned new_sbits, unsigned num, expr * const * args, func_decl_ref & small_op, expr_ref_vector & cast_args);
void mk_cast_small_to_big(func_decl * big_fd, expr * arg, expr_ref & result);
void mk_cast_small_to_big(unsigned sbits, unsigned ebits, expr * arg, expr_ref & result);
void match_sorts(expr * a, expr * b, expr_ref & n_a, expr_ref & n_b);
void establish_sort(unsigned num, expr * const * args, unsigned & ebits, unsigned & sbits);
public:
fpa2bv_converter_prec(ast_manager & m, fpa_approximation_mode mode);
void mk_const(func_decl * f, unsigned prec, expr_ref & result);
void mk_eq(expr * a, expr * b, expr_ref & result);
void mk_ite(expr * c, expr * t, expr * f, expr_ref & result);
void mk_add(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_sub(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_uminus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_mul(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_div(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_remainder(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_abs(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_min(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_max(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_fusedma(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_sqrt(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_round_to_integral(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_float_eq(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_float_lt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_float_gt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_float_le(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_float_ge(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
/*
void mk_is_zero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_pzero(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_sign_minus(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nan(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_inf(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_normal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
void mk_is_subnormal(func_decl * f, unsigned prec, unsigned num, expr * const * args, expr_ref & result);
*/
void reset() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
}
};
#endif

261
src/tactic/fpa/fpa2bv_rewriter_prec.h
View file

@ -1,261 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_rewriter.h
Abstract:
Rewriter for converting FPA to BV
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#ifndef _FPA2BV_REWRITER_H_
#define _FPA2BV_REWRITER_H_
#include"cooperate.h"
#include"rewriter_def.h"
#include"bv_decl_plugin.h"
#include"fpa2bv_converter_prec.h"
#include"tactic_exception.h"
#include <vector>
struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr_ref_vector m_out;
fpa2bv_converter_prec & m_conv;
obj_map<func_decl,unsigned> * cnst2prec_map;
unsigned precision;
unsigned long long m_max_memory;
unsigned m_max_steps;
ast_manager & m() const { return m_manager; }
fpa2bv_rewriter_prec_cfg(ast_manager & m, fpa2bv_converter_prec & c, params_ref const & p):
m_manager(m),
m_out(m),
m_conv(c) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
~fpa2bv_rewriter_prec_cfg() {
}
void cleanup_buffers() {
m_out.finalize();
}
unsigned get_precision(func_decl * f){
if(cnst2prec_map->contains(f))
return cnst2prec_map->find(f);
else return precision;
}
void set_precision(unsigned p) { precision=p; }
void set_mappings(obj_map<func_decl,unsigned> * o2p)
{
this->cnst2prec_map=o2p;
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
return num_steps > m_max_steps;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, get_precision(f), result);
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
//SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
else if (m_conv.is_rm(ds)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
return BR_FAILED;
}
expr_ref newAssertion(m_manager);
if (m_conv.is_float_family(f))
{
switch (f->get_decl_kind())
{
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_POSITIVE:
case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FPA_ADD:
m_conv.mk_add(f,get_precision(f), num, args, result);return BR_DONE;
case OP_FPA_SUB:
m_conv.mk_sub(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_NEG:
m_conv.mk_uminus(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MUL:
m_conv.mk_mul(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_DIV:
m_conv.mk_div(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_REM:
m_conv.mk_remainder(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_FMA:
m_conv.mk_fusedma(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_SQRT:
m_conv.mk_sqrt(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
NOT_IMPLEMENTED_YET();
}
}
if (f->get_family_id() == null_family_id)
{
bool is_float_uf = m_conv.is_float(f->get_range());
unsigned i = 0;
while (!is_float_uf && i < num)
{
is_float_uf = m_conv.is_float(f->get_domain()[i]);
i++;
}
if (is_float_uf)
{
m_conv.mk_uninterpreted_function(f, num, args, result);
return BR_DONE;
}
}
return BR_FAILED;
}
bool pre_visit(expr * t)
{
TRACE("pre_visit_prec", tout << mk_ismt2_pp(t, m()) << std::endl;);
if(t->get_kind() == AST_APP && is_app_of(t, to_app(t)->get_family_id(), OP_EQ)) {
//Equation over non-boolean expressions, it should be of form constantI = subexprI
app * a = to_app(t);
if (a->get_num_args() == 2) {
expr * a0 = a->get_arg(0);
expr * a1 = a->get_arg(1);
func_decl * cnst = 0;
if (a0->get_kind() == AST_APP && cnst2prec_map->contains(to_app(a0)->get_decl()))
cnst = to_app(a0)->get_decl();
else if (a1->get_kind() == AST_APP && cnst2prec_map->contains(to_app(a1)->get_decl()))
cnst = to_app(a1)->get_decl();
if (cnst == 0) {
// For all equalities that were in the original problem, we don't
// have any precision tracking, so those simply get 100% precision.
set_precision(100);
}
else
set_precision(cnst2prec_map->find(cnst));
TRACE("pre_visit_prec", tout << "Precision = " << get_precision(NULL) << std::endl;);
}
}
return true;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
return false;
}
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
return false;
}
};
template class rewriter_tpl<fpa2bv_rewriter_prec_cfg>;
struct fpa2bv_rewriter_prec : public rewriter_tpl<fpa2bv_rewriter_prec_cfg> {
fpa2bv_rewriter_prec_cfg m_cfg;
fpa2bv_rewriter_prec(ast_manager & m, fpa2bv_converter_prec & c, params_ref const & p):
rewriter_tpl<fpa2bv_rewriter_prec_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};
#endif

2
src/util/mpf.h
View file

@ -169,7 +169,7 @@ public:
bool is_ninf(mpf const & x);
bool is_normal(mpf const & x);
bool is_denormal(mpf const & x);
bool is_regular(mpf const & x) { return x.sbits == 0 || is_zero(x) || is_normal(x) || is_denormal(x); }
bool is_regular(mpf const & x) { return x.sbits == 0 || is_normal(x) || is_denormal(x); }
bool is_int(mpf const & x);