diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-28 15:25:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-28 15:25:12 -0500 |
| commit | 2978e5fa3434b80d3ca440ec482d5fe07bf5d368 (patch) | |
| tree | 4d23b1ad09a1448b980b2db1708c115b585437cf /src/theory/booleans/circuit_propagator.cpp | |
| parent | f9173b366ff32814ce74402765310efed48d4610 (diff) | |
Solve equalities between Boolean variables in presolve. (#2390)
Diffstat (limited to 'src/theory/booleans/circuit_propagator.cpp')
| -rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index d04b71ee1..2548cf5c3 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -368,7 +368,9 @@ bool CircuitPropagator::propagate() { Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl; // Is this an atom - bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar(); + bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar() + || (current.getKind() == kind::EQUAL + && (current[0].isVar() && current[1].isVar())); // If an atom, add to the list for simplification if (atom) { |