mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

More renaming floats -> fpa

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-08 13:47:26 +00:00
parent 5e5758bb25
commit 0cedd32ea2
5 changed files with 21 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/fpa/fpa2bv_converter.h
View file

@ -45,7 +45,7 @@ class fpa2bv_converter {
protected: protected:
ast_manager & m; ast_manager & m;
basic_simplifier_plugin m_simp; basic_simplifier_plugin m_simp;
float_util m_util; fpa_util m_util;
bv_util m_bv_util; bv_util m_bv_util;
arith_util m_arith_util; arith_util m_arith_util;
mpf_manager & m_mpf_manager; mpf_manager & m_mpf_manager;
@ -62,7 +62,7 @@ public:
fpa2bv_converter(ast_manager & m); fpa2bv_converter(ast_manager & m);
~fpa2bv_converter(); ~fpa2bv_converter();
float_util & fu() { return m_util; } fpa_util & fu() { return m_util; }
bv_util & bu() { return m_bv_util; } bv_util & bu() { return m_bv_util; }
arith_util & au() { return m_arith_util; } arith_util & au() { return m_arith_util; }

2
src/smt/theory_fpa.cpp
View file

@ -700,7 +700,7 @@ namespace smt {
void theory_fpa::init_model(model_generator & mg) { void theory_fpa::init_model(model_generator & mg) {
TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout);); TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
m_factory = alloc(fpa_factory, get_manager(), get_family_id()); m_factory = alloc(fpa_value_factory, get_manager(), get_family_id());
mg.register_factory(m_factory); mg.register_factory(m_factory);
} }

20
src/smt/theory_fpa.h
View file

@ -29,7 +29,7 @@ Revision History:
namespace smt { namespace smt {
class fpa_value_actory : public value_factory { class fpa_value_factory : public value_factory {
fpa_util m_util; fpa_util m_util;
virtual app * mk_value_core(mpf const & val, sort * s) { virtual app * mk_value_core(mpf const & val, sort * s) {
@ -39,11 +39,11 @@ namespace smt {
} }
public: public:
fpa_value_actory(ast_manager & m, family_id fid) : fpa_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid), value_factory(m, fid),
m_util(m) {} m_util(m) {}
virtual ~fpa_value_actory() {} virtual ~fpa_value_factory() {}
virtual expr * get_some_value(sort * s) { virtual expr * get_some_value(sort * s) {
mpf_manager & mpfm = m_util.fm(); mpf_manager & mpfm = m_util.fm();
@ -97,7 +97,7 @@ namespace smt {
public: public:
fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
m_th(*th), m_fu(th->m_float_util), m_bu(th->m_bv_util), m(th->get_manager()), m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()),
m_ebits(ebits), m_sbits(sbits) {} m_ebits(ebits), m_sbits(sbits) {}
virtual ~fpa_value_proc() {} virtual ~fpa_value_proc() {}
@ -112,15 +112,15 @@ namespace smt {
}; };
class fpa_rm_value_proc : public model_value_proc { class fpa_rm_value_proc : public model_value_proc {
theory_fpa & m_th; theory_fpa & m_th;
ast_manager & m; ast_manager & m;
float_util & m_fu; fpa_util & m_fu;
bv_util & m_bu; bv_util & m_bu;
buffer<model_value_dependency> m_deps; buffer<model_value_dependency> m_deps;
public: public:
fpa_rm_value_proc(theory_fpa * th) : fpa_rm_value_proc(theory_fpa * th) :
m_th(*th), m_fu(th->m_float_util), m_bu(th->m_bv_util), m(th->get_manager()) {} m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()) {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
@ -137,8 +137,8 @@ namespace smt {
fpa2bv_rewriter m_rw; fpa2bv_rewriter m_rw;
th_rewriter m_th_rw; th_rewriter m_th_rw;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;
fpa_factory * m_factory; fpa_value_factory * m_factory;
float_util & m_float_util; fpa_util & m_fpa_util;
bv_util & m_bv_util; bv_util & m_bv_util;
arith_util & m_arith_util; arith_util & m_arith_util;
obj_map<sort, func_decl*> m_wraps; obj_map<sort, func_decl*> m_wraps;

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

@ -48,6 +48,10 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
return st; return st;
} }
tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p) {
return mk_qffp_tactic(m, p);
}
struct is_non_qffp_predicate { struct is_non_qffp_predicate {
struct found {}; struct found {};
ast_manager & m; ast_manager & m;
@ -90,3 +94,6 @@ probe * mk_is_qffp_probe() {
return alloc(is_qffp_probe); return alloc(is_qffp_probe);
} }
probe * mk_is_qffpbv_probe() {
return alloc(is_qffp_probe);
}

1
src/tactic/fpa/qffp_tactic.h
View file

@ -25,6 +25,7 @@ class ast_manager;
class tactic; class tactic;
tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_qffpbv_tactic(ast_manager & m, params_ref const & p = params_ref());
/* /*
ADD_TACTIC("qffp", "(try to) solve goal using the tactic for QF_FP.", "mk_qffp_tactic(m, p)") ADD_TACTIC("qffp", "(try to) solve goal using the tactic for QF_FP.", "mk_qffp_tactic(m, p)")
ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).", "mk_qffpbv_tactic(m, p)") ADD_TACTIC("qffpbv", "(try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).", "mk_qffpbv_tactic(m, p)")