Interface: SmtFunctionApplicationDto

@kortexya/reasoninglayer / SmtFunctionApplicationDto

Interface: SmtFunctionApplicationDto

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

An uninterpreted function application declared in an SMT context.

Remarks

Plain JSON object — no tagged value serialization is involved. args must reference previously declared constants or the resultName of an earlier application; resultName names this application so it can be used as a term in equality atoms.

Example

// f(a, b) named "fab"
const application: SmtFunctionApplicationDto = {
  symbol: 'f',
  args: ['a', 'b'],
  resultName: 'fab',
};

Properties

args

args: string[]

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

Argument names (must be previously declared constants or resultNames).

resultName

resultName: string

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

Name assigned to this application — used to reference the result in equalities.

symbol

symbol: string

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

Function symbol name.