Type Alias: SmtVerdict
@kortexya/reasoninglayer / Smt / SmtVerdict
Type Alias: SmtVerdict
SmtVerdict =
"sat"|"unsat"|"unknown"
Defined in: src/types/smt.ts:88
Satisfiability verdict returned by the native DPLL(T) SMT solver.
Remarks
Serialized on the wire as the bare lowercase string (e.g. "sat"), not as a
tagged object. Note the abbreviations differ from the propositional SAT
solver’s verdict ("sat"/"unsat" here, "satisfiable"/"unsatisfiable"
there).
Example
const verdict: SmtVerdict = 'unsat';