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

Method test_dependency_chain

tests/test_z3_ported.py:1227–1234  ·  view source on GitHub ↗

If A depends on B and B depends on C, installing A without C is unsat.

(self, kernel)

Source from the content-addressed store, hash-verified

1225 """Guide: Package dependency modeling."""
1226
1227 def test_dependency_chain(self, kernel):
1228 """If A depends on B and B depends on C, installing A without C is unsat."""
1229 a, b, c = Bools("a b c")
1230 deps = And(Implies(a, b), Implies(b, c))
1231 # Install A but not C is contradictory
1232 s = Solver()
1233 s.add(deps, a, Not(c))
1234 assert s.check() == unsat
1235
1236 def test_conflict(self, kernel):
1237 """A conflicts with B: can't install both."""

Callers

nothing calls this directly

Calls 7

addMethod · 0.95
checkMethod · 0.95
BoolsFunction · 0.90
AndFunction · 0.90
ImpliesFunction · 0.90
SolverClass · 0.90
NotFunction · 0.90

Tested by

no test coverage detected