Interface: SmtUnsatResult
@kortexya/reasoninglayer / SmtUnsatResult
Interface: SmtUnsatResult
Section titled “Interface: SmtUnsatResult”Defined in: src/types/smt.ts:167
Result of an SMT check where the formula was proven unsatisfiable.
Remarks
Section titled “Remarks”No model is produced: congruence closure refuted every Boolean assignment.
Example
Section titled “Example”if (response.result === 'unsat') { console.log('no EUF model exists');}Properties
Section titled “Properties”result
Section titled “result”result:
"unsat"
Defined in: src/types/smt.ts:169
Discriminant: the formula is unsatisfiable under the EUF theory.