Interface: SmtSatResult

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

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

Remarks

assignments maps each declared EqualityAtomDto.id to whether that equality holds in the produced model: true → it holds, false → it does not.

if (response.result === 'sat') {
  console.log(response.assignments[0]); // does atom #0 hold in the model?
}

assignments: Record<number, boolean>

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

Boolean assignment for each equality atom, keyed by the equality’s id.

result: "sat"

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

Discriminant: the formula is satisfiable under the EUF theory.