mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
use std::vector per Nuno's analysis to fix #420
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
26f27867bf
commit
8c4d791f01
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "ast.h"
|
||||
#include "map.h"
|
||||
#include "vector.h"
|
||||
#include <vector>
|
||||
|
||||
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<std::string> m_suffixes;
|
||||
std::vector<std::string> m_suffixes;
|
||||
|
||||
|
||||
/**
|
||||
|
|
|
@ -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";
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue