mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix translation to pdd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
030da1f8ac
commit
c473cd78d8
|
@ -80,7 +80,6 @@ namespace sat {
|
|||
clause_vector clauses(s.clauses());
|
||||
af(clauses);
|
||||
|
||||
literal_vector _xors;
|
||||
std::function<void (literal_vector const&)> on_xor =
|
||||
[&,this](literal_vector const& xors) {
|
||||
SASSERT(xors.size() > 1);
|
||||
|
|
|
@ -374,7 +374,7 @@ namespace sat {
|
|||
auto& m = ps.get_manager();
|
||||
auto v = lit2pdd(b.first);
|
||||
auto w = lit2pdd(b.second);
|
||||
dd::pdd p = v | w;
|
||||
dd::pdd p = (v | w) + 1;
|
||||
ps.add(p);
|
||||
TRACE("anf_simplifier", tout << "bin: " << b.first << " " << b.second << " : " << p << "\n";);
|
||||
}
|
||||
|
@ -384,13 +384,14 @@ namespace sat {
|
|||
auto& m = ps.get_manager();
|
||||
dd::pdd p = m.zero();
|
||||
for (literal l : c) p |= lit2pdd(l);
|
||||
p = p + 1;
|
||||
ps.add(p);
|
||||
TRACE("anf_simplifier", tout << "clause: " << c << " : " << p << "\n";);
|
||||
}
|
||||
|
||||
void anf_simplifier::add_xor(literal_vector const& x, pdd_solver& ps) {
|
||||
auto& m = ps.get_manager();
|
||||
dd::pdd p = m.zero();
|
||||
dd::pdd p = m.one();
|
||||
for (literal l : x) p ^= lit2pdd(l);
|
||||
ps.add(p);
|
||||
TRACE("anf_simplifier", tout << "xor: " << x << " : " << p << "\n";);
|
||||
|
|
Loading…
Reference in a new issue