mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

add sample bdd vector operations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-16 10:22:48 -07:00
parent af2376e9e4
commit c7868579c0
4 changed files with 73 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/bit_constraint.cpp
View file

@ -39,7 +39,7 @@ namespace polysat {
}
bool bit_constraint::is_currently_false(solver& s) {
return m_viable[m_var].is_false();
return s.m_viable[m_var].is_false();
}
void bit_constraint::narrow(solver& s) {

6
src/math/polysat/justification.cpp
View file

@ -21,10 +21,12 @@ namespace polysat {
case justification_k::unassigned:
return out << "unassigned";
case justification_k::decision:
return out << "decision (level " << level() << ")";
return out << "decision @ " << level();
case justification_k::propagation:
return out << "propagation (level " << level() << ")";
return out << "propagation @ " << level();
}
UNREACHABLE();
return out;
}
}