mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

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

Browse source 
This reverts commit d3db21ccde, reversing
changes made to e463d5d899.
This commit is contained in:
Christoph M. Wintersteiger 2015-06-24 16:27:32 +01:00
parent 3a49223076
commit 9a62d989e6
8 changed files with 2 additions and 3456 deletions
Download patch file Download diff file Expand all files Collapse all files

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);