Interface: SmtSatResult
@kortexya/reasoninglayer / SmtSatResult
Interface: SmtSatResult
Section titled “Interface: SmtSatResult”Defined in: src/types/smt.ts:147
Result of an SMT check where the formula was proven satisfiable.
Remarks
Section titled “Remarks”assignments maps each declared EqualityAtomDto.id to whether
that equality holds in the produced model: true → it holds, false → it
does not.
Example
Section titled “Example”if (response.result === 'sat') { console.log(response.assignments[0]); // does atom #0 hold in the model?}Properties
Section titled “Properties”assignments
Section titled “assignments”assignments:
Record<number,boolean>
Defined in: src/types/smt.ts:151
Boolean assignment for each equality atom, keyed by the equality’s id.
result
Section titled “result”result:
"sat"
Defined in: src/types/smt.ts:149
Discriminant: the formula is satisfiable under the EUF theory.