mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

remove copy in generic_model_converter

Browse source
This commit is contained in:
Nuno Lopes 2018-07-03 17:51:40 +01:00
parent f00264663c
commit 72f60f5bfc
2 changed files with 2 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/generic_model_converter.cpp
View file

@ -33,10 +33,9 @@ generic_model_converter::~generic_model_converter() {
void generic_model_converter::add(func_decl * d, expr* e) {
VERIFY(e);
entry et(d, e, m, ADD);
VERIFY(d->get_range() == m.get_sort(e));
m_first_idx.insert_if_not_there(et.m_f, m_entries.size());
m_entries.push_back(et);
m_first_idx.insert_if_not_there(d, m_entries.size());
m_entries.push_back(entry(d, e, m, ADD));
}
void generic_model_converter::operator()(model_ref & md) {
@ -250,7 +249,6 @@ void generic_model_converter::get_units(obj_map<expr, bool>& units) {
*/
expr_ref generic_model_converter::simplify_def(entry const& e) {
expr_ref result(m);
expr_ref c(m.mk_const(e.m_f), m);
if (m.is_bool(c) && occurs(c, e.m_def)) {
expr_safe_replace rep(m);

7
src/tactic/generic_model_converter.h
View file

@ -30,13 +30,6 @@ class generic_model_converter : public model_converter {
instruction m_instruction;
entry(func_decl* f, expr* d, ast_manager& m, instruction i):
m_f(f, m), m_def(d, m), m_instruction(i) {}
entry& operator=(entry const& other) {
m_f = other.m_f;
m_def = other.m_def;
m_instruction = other.m_instruction;
return *this;
}
};
ast_manager& m;
std::string m_orig;