Interface: EqualityAtomDto
@kortexya/reasoninglayer / EqualityAtomDto
Interface: EqualityAtomDto
Section titled “Interface: EqualityAtomDto”Defined in: src/types/smt.ts:45
An equality atom between two terms, referenced by name.
Remarks
Section titled “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
Section titled “Example”// atom #0: a = bconst atom: EqualityAtomDto = { id: 0, lhs: 'a', rhs: 'b' };Properties
Section titled “Properties”id:
number
Defined in: src/types/smt.ts:47
Client-chosen integer ID for this equality (becomes a SAT variable).
lhs:
string
Defined in: src/types/smt.ts:49
Left-hand term name (constant or function application result).
rhs:
string
Defined in: src/types/smt.ts:51
Right-hand term name (constant or function application result).