mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

improve comments

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-20 21:50:35 -04:00
parent ac6ca4d334
commit 9f73359a86
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/qe/qe_lite.cpp
View file

@ -788,12 +788,13 @@ namespace ar {
}
/**
Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x
Ex A. A[x] = t & Phi[A] where x \not\in A, t. A \not\in t, x
=>
Ex A. Phi[store(A,x,t)]
(Not implemented)
Perhaps also:
Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t
Ex A. store(A,y,z)[x] = t & Phi[A] where x \not\in A, t, y, z, A \not\in y z, t
=>
Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)]
@ -822,7 +823,8 @@ namespace ar {
expr_safe_replace rep(m);
rep.insert(A, B);
expr_ref tmp(m);
std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";
TRACE("qe_lite",
tout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
for (unsigned j = 0; j < conjs.size(); ++j) {
if (i == j) {
conjs[j] = m.mk_true();