Interface: SmtUnsatResult

@kortexya/reasoninglayer

---

@kortexya/reasoninglayer / Smt / SmtUnsatResult

Interface: SmtUnsatResult

Defined in: src/types/smt.ts:167

Result of an SMT check where the formula was proven unsatisfiable.

Remarks

No model is produced: congruence closure refuted every Boolean assignment.

Example

if (response.result === 'unsat') {
  console.log('no EUF model exists');
}

Properties

result

result: "unsat"

Defined in: src/types/smt.ts:169

Discriminant: the formula is unsatisfiable under the EUF theory.