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

spacing, unit test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-17 08:07:23 -04:00
parent fe14a22baa
commit 4cae91b096
5 changed files with 98 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -56,7 +56,7 @@ protected:
special_t m_min_max_specials;
friend class fpa2bv_model_converter;
friend class bv2fpa_converter;
friend class bv2fpa_converter;
public:
fpa2bv_converter(ast_manager & m);
@ -138,11 +138,11 @@ public:
void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; }
@ -227,9 +227,9 @@ private:
void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result);
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width);
expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits);
};
#endif

68
src/smt/theory_fpa.cpp
View file

@ -84,15 +84,15 @@ namespace smt {
}
}
theory_fpa::theory_fpa(ast_manager & m) :
theory(m.mk_family_id("fpa")),
m_converter(m, this),
m_rw(m, m_converter, params_ref()),
m_th_rw(m),
m_trail_stack(*this),
m_fpa_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
m_arith_util(m_converter.au()),
theory_fpa::theory_fpa(ast_manager & m) :
theory(m.mk_family_id("fpa")),
m_converter(m, this),
m_rw(m, m_converter, params_ref()),
m_th_rw(m),
m_trail_stack(*this),
m_fpa_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
m_arith_util(m_converter.au()),
m_is_initialized(false)
{
params_ref p;
@ -799,33 +799,35 @@ namespace smt {
}
void theory_fpa::finalize_model(model_generator & mg) {
#if 0
ast_manager & m = get_manager();
proto_model & mdl = mg.get_model();
proto_model new_model(m);
bv2fpa_converter bv2fp(m, m_converter);
obj_hashtable<func_decl> seen;
bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
for (obj_hashtable<func_decl>::iterator it = seen.begin();
it != seen.end();
it++)
mdl.unregister_decl(*it);
for (unsigned i = 0; i < new_model.get_num_constants(); i++) {
func_decl * f = new_model.get_constant(i);
mdl.register_decl(f, new_model.get_const_interp(f));
}
for (unsigned i = 0; i < new_model.get_num_functions(); i++) {
func_decl * f = new_model.get_function(i);
func_interp * fi = new_model.get_func_interp(f)->copy();
mdl.register_decl(f, fi);
}
proto_model new_model(m);
bv2fpa_converter bv2fp(m, m_converter);
obj_hashtable<func_decl> seen;
bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
for (obj_hashtable<func_decl>::iterator it = seen.begin();
it != seen.end();
it++)
mdl.unregister_decl(*it);
for (unsigned i = 0; i < new_model.get_num_constants(); i++) {
func_decl * f = new_model.get_constant(i);
mdl.register_decl(f, new_model.get_const_interp(f));
}
for (unsigned i = 0; i < new_model.get_num_functions(); i++) {
func_decl * f = new_model.get_function(i);
func_interp * fi = new_model.get_func_interp(f)->copy();
mdl.register_decl(f, fi);
}
#endif
}
void theory_fpa::display(std::ostream & out) const
{
ast_manager & m = get_manager();

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

@ -22,52 +22,48 @@ Notes:
void fpa2bv_model_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter";
m_bv2fp->display(out);
m_bv2fp->display(out);
out << ")";
}
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
res->m_bv2fp = m_bv2fp->translate(translator);
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
res->m_bv2fp = m_bv2fp->translate(translator);
return res;
}
void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
obj_hashtable<func_decl> seen;
m_bv2fp->convert_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_uf2bvuf(mc, float_mdl, seen);
// Keep all the non-float constants.
unsigned sz = mc->get_num_constants();
for (unsigned i = 0; i < sz; i++)
{
func_decl * c = mc->get_constant(i);
if (!seen.contains(c))
float_mdl->register_decl(c, mc->get_const_interp(c));
}
// And keep everything else
sz = mc->get_num_functions();
for (unsigned i = 0; i < sz; i++)
{
func_decl * f = mc->get_function(i);
if (!seen.contains(f))
{
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
func_interp * val = mc->get_func_interp(f)->copy();
float_mdl->register_decl(f, val);
}
}
sz = mc->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++)
{
sort * s = mc->get_uninterpreted_sort(i);
ptr_vector<expr> u = mc->get_universe(s);
float_mdl->register_usort(s, u.size(), u.c_ptr());
}
obj_hashtable<func_decl> seen;
m_bv2fp->convert_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_uf2bvuf(mc, float_mdl, seen);
// Keep all the non-float constants.
unsigned sz = mc->get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * c = mc->get_constant(i);
if (!seen.contains(c))
float_mdl->register_decl(c, mc->get_const_interp(c));
}
// And keep everything else
sz = mc->get_num_functions();
for (unsigned i = 0; i < sz; i++) {
func_decl * f = mc->get_function(i);
if (!seen.contains(f)) {
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
func_interp * val = mc->get_func_interp(f)->copy();
float_mdl->register_decl(f, val);
}
}
sz = mc->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++) {
sort * s = mc->get_uninterpreted_sort(i);
ptr_vector<expr> u = mc->get_universe(s);
float_mdl->register_usort(s, u.size(), u.c_ptr());
}
}
model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) {

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

@ -25,23 +25,22 @@ Notes:
class fpa2bv_model_converter : public model_converter {
ast_manager & m;
bv2fpa_converter * m_bv2fp;
bv2fpa_converter * m_bv2fp;
public:
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) :
m(m) {
m_bv2fp = alloc(bv2fpa_converter, m, conv);
fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv):
m(m),
m_bv2fp(alloc(bv2fpa_converter, m, conv)) {
}
virtual ~fpa2bv_model_converter() {
if (m_bv2fp) dealloc(m_bv2fp);
m_bv2fp = 0;
dealloc(m_bv2fp);
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
model * new_model = alloc(model, m);
convert(md.get(), new_model);
convert(md.get(), new_model);
md = new_model;
}
@ -56,9 +55,9 @@ public:
protected:
fpa2bv_model_converter(ast_manager & m) :
m(m),
m_bv2fp(0) {}
void convert(model_core * mc, model * float_mdl);
m_bv2fp(0) {}
void convert(model_core * mc, model * float_mdl);
};

13
src/test/get_consequences.cpp
View file

@ -8,6 +8,7 @@ Copyright (c) 2016 Microsoft Corporation
#include "datatype_decl_plugin.h"
#include "reg_decl_plugins.h"
#include "ast_pp.h"
#include "dt2bv.h"
//include
static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
@ -72,6 +73,18 @@ static void test2() {
g->assert_expr(m.mk_not(m.mk_eq(x, r)));
g->assert_expr(m.mk_not(m.mk_eq(x, b)));
g->display(std::cout);
tactic_ref dt2bv = mk_dt2bv_tactic(m);
goal_ref_buffer result;
model_converter_ref mc;
proof_converter_ref pc;
expr_dependency_ref core;
(*dt2bv)(g, result, mc, pc, core);
model_ref mdl1 = alloc(model, m);
model_ref mdl2 = (*mc)(*mdl1);
expr_ref val(m);
mdl2->eval(x, val);
std::cout << val << "\n";
}
void tst_get_consequences() {