MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / test_conflict

Method test_conflict

tests/test_z3_ported.py:1236–1242  ·  view source on GitHub ↗

A conflicts with B: can't install both.

(self, kernel)

Source from the content-addressed store, hash-verified

1234 assert s.check() == unsat
1235
1236 def test_conflict(self, kernel):
1237 """A conflicts with B: can't install both."""
1238 a, b = Bools("a b")
1239 conflict = Or(Not(a), Not(b))
1240 s = Solver()
1241 s.add(conflict, a, b)
1242 assert s.check() == unsat
1243
1244
1245# ===================================================================

Callers

nothing calls this directly

Calls 6

addMethod · 0.95
checkMethod · 0.95
BoolsFunction · 0.90
OrFunction · 0.90
NotFunction · 0.90
SolverClass · 0.90

Tested by

no test coverage detected