From e4eca577f6746af778fa66200127704bad80e1ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Mar 2019 07:03:04 -0700 Subject: [PATCH] fix po model Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/theory_special_relations.cpp | 10 ++++------ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0012f1433..a40efe228 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4453,7 +4453,6 @@ namespace smt { } recfun::util u(m); func_decl_ref_vector recfuns = u.get_rec_funs(); - std::cout << recfuns << "\n"; for (func_decl* f : recfuns) { auto& def = u.get_def(f); expr* rhs = def.get_rhs(); @@ -4475,6 +4474,7 @@ namespace smt { fi->set_else(bodyr); m_model->register_decl(f, fi); } + TRACE("model", tout << *m_model << "\n";); } }; diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 8339c658e..6e8c04a97 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -727,16 +727,14 @@ namespace smt { var* vars3[3] = { xV, yV, SV }; p.set_definition(rep, c2, 3, vars3, connected_rec_body); -#if 0 - // TBD: doesn't terminate with model_evaluator/rewriter - // r.m_decl(x,y) -> snd(connected2(x,y,nil)) + xV = m.mk_var(0, s); + yV = m.mk_var(1, s); + x = xV, y = yV; func_interp* fi = alloc(func_interp, m, 2); - fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_const(nil)))); + fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, x, m.mk_const(nil))))); mg.get_model().register_decl(r.decl(), fi); -#endif - }