From 8c4d791f011263d1867f5b5c14f11ed11a0d00b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Mar 2016 08:08:17 -0800 Subject: [PATCH] use std::vector per Nuno's analysis to fix #420 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_sym_mux.h | 3 ++- src/test/model_evaluator.cpp | 26 ++++++++++++++++---------- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h index bc1819539..78025f26b 100644 --- a/src/muz/pdr/pdr_sym_mux.h +++ b/src/muz/pdr/pdr_sym_mux.h @@ -23,6 +23,7 @@ Revision History: #include "ast.h" #include "map.h" #include "vector.h" +#include class model_core; @@ -46,7 +47,7 @@ private: mutable unsigned m_next_sym_suffix_idx; mutable symbols m_used_suffixes; /** Here we have default suffixes for each of the variants */ - vector m_suffixes; + std::vector m_suffixes; /** diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index 6e3a1f441..0b509fba6 100644 --- a/src/test/model_evaluator.cpp +++ b/src/test/model_evaluator.cpp @@ -26,13 +26,19 @@ void tst_model_evaluator() { expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m); expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m); expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m); - expr_ref f01(m.mk_app(f, vI0, vB1), m); - expr_ref g01(m.mk_app(g, vI0, vB1), m); - expr_ref h01(m.mk_app(h, vI0, vB1), m); + expr* vI0p = vI0.get(); + expr* vI1p = vI1.get(); + expr* vB0p = vB0.get(); + expr* vB1p = vB1.get(); + expr* vB2p = vB2.get(); + + expr_ref f01(m.mk_app(f, vI0p, vB1p), m); + expr_ref g01(m.mk_app(g, vI0p, vB1p), m); + expr_ref h01(m.mk_app(h, vI0p, vB1p), m); func_interp* fi = alloc(func_interp, m, 2); func_interp* gi = alloc(func_interp, m, 2); func_interp* hi = alloc(func_interp, m, 2); - hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1))); + hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p))); mdl.register_decl(h, hi); @@ -42,23 +48,23 @@ void tst_model_evaluator() { { symbol nI("N"); - fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1))); - gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0)); + fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1))); + gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p)); mdl.register_decl(g, gi); mdl.register_decl(f, fi); model_pp(std::cout, mdl); - e = m.mk_app(h, vI0, vB1); + e = m.mk_app(h, vI0p, vB1p); eval(e, v); std::cout << e << " " << v << "\n"; } { - fi->set_else(m.mk_app(F, vI0, vB1)); - gi->set_else(m.mk_app(G, vI0, vB1)); + fi->set_else(m.mk_app(F, vI0p, vB1p)); + gi->set_else(m.mk_app(G, vI0p, vB1p)); mdl.register_decl(g, gi); mdl.register_decl(h, hi); model_pp(std::cout, mdl); - e = m.mk_app(h, vI0, vB1); + e = m.mk_app(h, vI0p, vB1p); eval(e, v); std::cout << e << " " << v << "\n"; }