Interface: EqualityAtomDto

@kortexya/reasoninglayer / Smt / EqualityAtomDto

Interface: EqualityAtomDto

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

An equality atom between two terms, referenced by name.

Remarks

Each equality is assigned a client-chosen integer id that becomes a SAT variable in the Boolean abstraction handed to DPLL(T). The id must be unique within a single SmtCheckRequest.

Example

// atom #0: a = b
const atom: EqualityAtomDto = { id: 0, lhs: 'a', rhs: 'b' };

Properties

id

id: number

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

Client-chosen integer ID for this equality (becomes a SAT variable).

lhs

lhs: string

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

Left-hand term name (constant or function application result).

rhs

rhs: string

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

Right-hand term name (constant or function application result).