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

Added implementation of pb2bv_model_converter::translate

Browse source 
Fixes #623
This commit is contained in:
Christoph M. Wintersteiger 2016-05-26 18:39:51 +01:00
parent ec270acd32
commit 1fe4a82c76
2 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/tactic/arith/pb2bv_model_converter.cpp
View file

@ -21,6 +21,10 @@ Notes:
#include"model_v2_pp.h"
#include"pb2bv_model_converter.h"
pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m) : m(_m) {
}
pb2bv_model_converter::pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm):
m(_m) {
obj_map<func_decl, expr*>::iterator it = c2bit.begin();
@ -98,5 +102,16 @@ void pb2bv_model_converter::display(std::ostream & out) {
}
model_converter * pb2bv_model_converter::translate(ast_translation & translator) {
NOT_IMPLEMENTED_YET();
ast_manager & to = translator.to();
pb2bv_model_converter * res = alloc(pb2bv_model_converter, to);
svector<func_decl_pair>::iterator it = m_c2bit.begin();
svector<func_decl_pair>::iterator end = m_c2bit.end();
for (; it != end; it++) {
func_decl * f1 = translator(it->first);
func_decl * f2 = translator(it->second);
res->m_c2bit.push_back(func_decl_pair(f1, f2));
m.inc_ref(f1);
m.inc_ref(f2);
}
return res;
}

1
src/tactic/arith/pb2bv_model_converter.h
View file

@ -28,6 +28,7 @@ class pb2bv_model_converter : public model_converter {
ast_manager & m;
svector<func_decl_pair> m_c2bit;
public:
pb2bv_model_converter(ast_manager & _m);
pb2bv_model_converter(ast_manager & _m, obj_map<func_decl, expr*> const & c2bit, bound_manager const & bm);
virtual ~pb2bv_model_converter();
virtual void operator()(model_ref & md);