mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-15 11:37:32 +01:00
parent 2688fd55cf
commit d82afcc48c
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -38,7 +38,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
m_bv2fp->convert_rm_consts(mc, float_mdl, seen); m_bv2fp->convert_rm_consts(mc, float_mdl, seen);
m_bv2fp->convert_min_max_specials(mc, float_mdl, seen); m_bv2fp->convert_min_max_specials(mc, float_mdl, seen);
m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen); m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen);
// Keep all the non-float constants. // Keep all the non-float constants.
unsigned sz = mc->get_num_constants(); unsigned sz = mc->get_num_constants();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
@ -46,7 +46,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
if (!seen.contains(c)) if (!seen.contains(c))
float_mdl->register_decl(c, mc->get_const_interp(c)); float_mdl->register_decl(c, mc->get_const_interp(c));
} }
// And keep everything else // And keep everything else
sz = mc->get_num_functions(); sz = mc->get_num_functions();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
@ -57,7 +57,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
float_mdl->register_decl(f, val); float_mdl->register_decl(f, val);
} }
} }
sz = mc->get_num_uninterpreted_sorts(); sz = mc->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
sort * s = mc->get_uninterpreted_sort(i); sort * s = mc->get_uninterpreted_sort(i);

6
src/tactic/fpa/fpa2bv_model_converter.h
View file

@ -26,7 +26,7 @@ Notes:
class fpa2bv_model_converter : public model_converter { class fpa2bv_model_converter : public model_converter {
ast_manager & m; ast_manager & m;
bv2fpa_converter * m_bv2fp; bv2fpa_converter * m_bv2fp;
public: public:
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv): fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv):
m(m), m(m),
@ -53,10 +53,10 @@ public:
virtual model_converter * translate(ast_translation & translator); virtual model_converter * translate(ast_translation & translator);
protected: protected:
fpa2bv_model_converter(ast_manager & m) : fpa2bv_model_converter(ast_manager & m) :
m(m), m(m),
m_bv2fp(0) {} m_bv2fp(0) {}
void convert(model_core * mc, model * float_mdl); void convert(model_core * mc, model * float_mdl);
}; };