mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-14 03:04:44 +00:00
Code Activity

local changes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-15 09:34:11 -07:00
parent f61f2b1f55
commit f253b20820
4 changed files with 26 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_elim_eqs.cpp
View file

@ -78,7 +78,7 @@ namespace sat {
clause_vector::iterator end = cs.end();
for (; it != end; ++it) {
clause & c = *(*it);
TRACE("elim_eqs", tout << "processing: " << c << "\n";);
TRACE("sats", tout << "processing: " << c << "\n";);
unsigned sz = c.size();
unsigned i;
for (i = 0; i < sz; i++) {
@ -101,7 +101,12 @@ namespace sat {
c[i] = norm(roots, c[i]);
}
std::sort(c.begin(), c.end());
TRACE("elim_eqs", tout << "after normalization/sorting: " << c << "\n";);
TRACE("sats", tout << "after normalization/sorting: " << c << "\n"; tout.flush(););
DEBUG_CODE({
for (unsigned i = 0; i < sz; i++) {
CTRACE("sats", c[i] != norm(roots, c[i]), tout << c[i] << " " << norm(roots, c[i]) << "\n"; tout.flush(););
SASSERT(c[i] == norm(roots, c[i]));
} });
// remove duplicates, and check if it is a tautology
literal l_prev = null_literal;
unsigned j = 0;