Module

Baskerville.Conformance.Smt

Package: purescript-baskerville-mycroft
Repository: afcondon/purescript-baskerville-mycroft

The SMT-backed oracle: the ⊨ side of Baskerville's seam when the world space is too large to enumerate. The founding restriction — the claim universe stays finite — survives; only world enumeration is replaced by the solver. So the instruments mirror Baskerville.Conformance one for one, each claim asked with one query inside a push/pop scope, plus one the counting oracle could never offer: whyEntailed, the unsat core over the named observations — the ⊨-side twin of ⊢'s axiomsBehind.

#SmtTheory Source

type SmtTheory claim = { declare :: Array SExpr, encode :: claim -> Term, observations :: Array { name :: String, term :: Term }, universe :: Array claim }

A client's theory: raw declarations and domain axioms (sent verbatim), an encoding of claims as formulas, the observations as named assertions (names are what unsat cores are made of), and the finite claim universe — still finite, still yours.

#Session Source

newtype Session claim

#newSession Source

newSession :: forall claim. Solver -> SmtTheory claim -> Aff (Session claim)

Load a theory into a solver: options, declarations, named observations, and one up-front consistency check — the analogue of asking whether any world survives the observations.

#consistent Source

consistent :: forall claim. Session claim -> Boolean

#entailed Source

entailed :: forall claim. Session claim -> claim -> Aff Boolean

True in every world consistent with the observations. Mirrors the counting oracle's stance on contradiction: an empty world set entails nothing, rather than everything.

#countermodel Source

countermodel :: forall claim. Session claim -> claim -> Aff (Maybe Model)

A world where the claim fails, if one survives — as a solver model.

#unsound Source

unsound :: forall residue claim rule axiom. Ord claim => Session claim -> KB residue claim rule axiom -> Aff (Array claim)

Claims the engine believes that the oracle refutes. Soundness means this is empty, on every stream, at every position.

#gap Source

gap :: forall residue claim rule axiom. Ord claim => Session claim -> KB residue claim rule axiom -> Aff (Array claim)

Claims true in every world that the engine has not derived — the completeness gap, now measurable where enumeration can't reach.

#explainOr Source

explainOr :: forall residue claim rule axiom. Ord claim => Session claim -> KB residue claim rule axiom -> claim -> Aff (Either (Refutation Model) (DerivationDag claim rule axiom))

The seam: ⊢ if the engine can, else what ⊨ has to say about it.

#whyEntailed Source

whyEntailed :: forall claim. Session claim -> claim -> Aff (Maybe (Array String))

Which observations force this claim: the unsat core over the named observations when the negated claim is refuted. Nothing when the claim isn't entailed at all.

Modules: Baskerville.Conformance.Smt