mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

update substitution routines

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-01-21 21:59:20 -08:00
parent b9cc7080e7
commit af4c09c8d3
2 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/test/substitution.cpp
View file

@ -20,9 +20,11 @@ void tst_substitution()
var_ref v1(m.mk_var(0, m.mk_bool_sort()), m);
var_ref v2(m.mk_var(1, m.mk_bool_sort()), m);
var_ref v3(m.mk_var(2, m.mk_bool_sort()), m);
var_ref v4(m.mk_var(3, m.mk_bool_sort()), m);
substitution subst(m);
subst.reserve(1,2);
subst.reserve(1,4);
unifier unif(m);
bool ok1 = unif(v1.get(), v2.get(), subst, false);
@ -34,4 +36,16 @@ void tst_substitution()
TRACE("substitution", tout << ok1 << " " << ok2 << "\n";);
subst.display(std::cout);
subst.apply(v1.get(), res);
TRACE("substitution", tout << mk_pp(res, m) << "\n";);
expr_ref q(m), body(m);
sort_ref_vector sorts(m);
svector<symbol> names;
sorts.push_back(m.mk_bool_sort());
names.push_back(symbol("dude"));
body = m.mk_and(m.mk_eq(v1,v2), m.mk_eq(v3,v4));
q = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), body);
subst.apply(q, res);
TRACE("substitution", tout << mk_pp(q, m) << "\n->\n" << mk_pp(res, m) << "\n";);
}