mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

disable debug output from check_relation

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-24 16:21:58 +01:00 • committed by Christoph M. Wintersteiger
parent 5cc8c8bde6
commit 30eb461e01
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/muz/rel/check_relation.cpp
View file

@ -720,12 +720,12 @@ namespace datalog {
relation_signature const& sig1 = dst.get_signature(); relation_signature const& sig1 = dst.get_signature();
relation_signature const& sig2 = neg.get_signature(); relation_signature const& sig2 = neg.get_signature();
expr_ref dstf(m), negf(m); expr_ref dstf(m), negf(m);
std::cout << mk_pp(dst0, m) << "\n"; //std::cout << mk_pp(dst0, m) << "\n";
expr_ref_vector eqs(m); expr_ref_vector eqs(m);
dst.to_formula(dstf); dst.to_formula(dstf);
std::cout << mk_pp(dstf, m) << "\n"; //std::cout << mk_pp(dstf, m) << "\n";
neg.to_formula(negf); neg.to_formula(negf);
std::cout << mk_pp(negf, m) << "\n"; //std::cout << mk_pp(negf, m) << "\n";
eqs.push_back(negf); eqs.push_back(negf);
for (unsigned i = 0; i < cols1.size(); ++i) { for (unsigned i = 0; i < cols1.size(); ++i) {
var_ref v1(m), v2(m); var_ref v1(m), v2(m);
@ -747,8 +747,8 @@ namespace datalog {
negf = m.mk_and(dst0, m.mk_not(negf)); negf = m.mk_and(dst0, m.mk_not(negf));
negf = ground(dst, negf); negf = ground(dst, negf);
dstf = ground(dst, dstf); dstf = ground(dst, dstf);
std::cout << negf << "\n"; //std::cout << negf << "\n";
std::cout << dstf << "\n"; //std::cout << dstf << "\n";
check_equiv("filter by negation", dstf, negf); check_equiv("filter by negation", dstf, negf);
} }