Type Alias: SmtCheckResponse

@kortexya/reasoninglayer

---

@kortexya/reasoninglayer / Smt / SmtCheckResponse

Type Alias: SmtCheckResponse

SmtCheckResponse = SmtSatResult | SmtUnsatResult | SmtUnknownResult

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

Response from checking satisfiability of an EUF formula.

Remarks

A discriminated union over SmtVerdict: narrow on result to reach the model (sat) or the explanation (unknown).

Example

const response = await client.smt.check({ constants: ['a'] });
switch (response.result) {
  case 'sat':
    console.log(response.assignments);
    break;
  case 'unsat':
    console.log('UNSAT');
    break;
  case 'unknown':
    console.log(response.unknownReason);
    break;
}