Interface: SmtCheckRequest

@kortexya/reasoninglayer / Smt / SmtCheckRequest

Interface: SmtCheckRequest

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

Request body for checking satisfiability of an EUF (equality with uninterpreted functions) formula.

Remarks

Declare constants and optional functions, state the equalities between them, then constrain their Boolean abstraction with clauses, assertTrue and assertFalse. No tenant context is required — the SMT context is stateless and independent of the OSFKB.

Example

const request: SmtCheckRequest = {
  constants: ['a', 'b', 'c'],
  equalities: [
    { id: 0, lhs: 'a', rhs: 'b' },
    { id: 1, lhs: 'b', rhs: 'c' },
    { id: 2, lhs: 'a', rhs: 'c' },
  ],
  assertTrue: [0, 1],
  assertFalse: [2], // unsat by congruence closure (transitivity)
};

Properties

assertFalse?

optional assertFalse: number[]

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

Equality atom IDs forced to be false (asserted as unit negative clauses).

assertTrue?

optional assertTrue: number[]

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

Equality atom IDs forced to be true (asserted as unit positive clauses).

clauses?

optional clauses: EqLiteralDto[][]

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

Boolean clauses over equality atoms: each clause is a non-empty disjunction of EqLiteralDtos.

constants

constants: string[]

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

Uninterpreted constant names.

equalities?

optional equalities: EqualityAtomDto[]

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

Equality atoms between pairs of terms. Each must have a unique id.

functions?

optional functions: SmtFunctionApplicationDto[]

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

Uninterpreted function applications (optional).