Interface Model<Name>

Readonlyctx

Readonlyptr

addFuncInterp

• addFuncInterp<
      DomainSort extends Sort<Name>[] = Sort<Name>[],
      RangeSort extends Sort<Name> = Sort<Name>,
  >(
      decl: FuncDecl<Name, DomainSort, RangeSort>,
      defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
  ): FuncInterp<Name>

• Type Parameters

  • DomainSort extends Sort<Name>[] = Sort<Name>[]
  • RangeSort extends Sort<Name> = Sort<Name>

  Parameters

  • decl: FuncDecl<Name, DomainSort, RangeSort>
  • defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>

  Returns FuncInterp<Name>

decls

• decls(): FuncDecl<Name, Sort<Name>[], Sort<Name>>[]

• Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>[]

entries

• entries(): IterableIterator<
      [number, FuncDecl<Name, Sort<Name>[], Sort<Name>>],
      any,
      any,
  >

• Returns IterableIterator<[number, FuncDecl<Name, Sort<Name>[], Sort<Name>>], any, any>

eval

• eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>

• Parameters

  • expr: Bool<Name>
  • OptionalmodelCompletion: boolean

  Returns Bool<Name>

• eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>

• Parameters

  • expr: Arith<Name>
  • OptionalmodelCompletion: boolean

  Returns Arith<Name>

• eval<Bits extends number = number>(
      expr: BitVec<Bits, Name>,
      modelCompletion?: boolean,
  ): BitVecNum<Bits, Name>

• Type Parameters

  • Bits extends number = number

  Parameters

  • expr: BitVec<Bits, Name>
  • OptionalmodelCompletion: boolean

  Returns BitVecNum<Bits, Name>

• eval(
      expr: Expr<Name, AnySort<Name>, unknown>,
      modelCompletion?: boolean,
  ): Expr<Name, AnySort<Name>, unknown>

• Parameters

  • expr: Expr<Name, AnySort<Name>, unknown>
  • OptionalmodelCompletion: boolean

  Returns Expr<Name, AnySort<Name>, unknown>

get

• get(i: number): FuncDecl<Name, Sort<Name>[], Sort<Name>>

• Parameters

  • i: number

  Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>

• get(from: number, to: number): FuncDecl<Name, Sort<Name>[], Sort<Name>>[]

• Parameters

  • from: number
  • to: number

  Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>[]

• get(
      declaration: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
  ): Expr<Name, AnySort<Name>, unknown> | FuncInterp<Name>

• Parameters

  • declaration: FuncDecl<Name, Sort<Name>[], Sort<Name>>

  Returns Expr<Name, AnySort<Name>, unknown> | FuncInterp<Name>

• get(
      constant: Expr<Name, AnySort<Name>, unknown>,
  ): Expr<Name, AnySort<Name>, unknown>

• Parameters

  • constant: Expr<Name, AnySort<Name>, unknown>

  Returns Expr<Name, AnySort<Name>, unknown>

• get(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>

• Parameters

  • sort: Sort<Name>

  Returns AstVector<Name, AnyExpr<Name>>

keys

• keys(): IterableIterator<number, any, any>

• Returns IterableIterator<number, any, any>

length

• length(): number

• Returns number

release

• release(): void

• Manually decrease the reference count of the model This is automatically done when the model is garbage collected, but calling this eagerly can help release memory sooner.

  Returns void

sexpr

• sexpr(): string

• Returns string

updateValue

• updateValue(
      decl:
          | FuncDecl<Name, Sort<Name>[], Sort<Name>>
          | Expr<Name, AnySort<Name>, unknown>,
      a: FuncInterp<Name> | Ast<Name, unknown>,
  ): void

• Parameters

  • decl: FuncDecl<Name, Sort<Name>[], Sort<Name>> | Expr<Name, AnySort<Name>, unknown>
  • a: FuncInterp<Name> | Ast<Name, unknown>

  Returns void

values

• values(): IterableIterator<FuncDecl<Name, Sort<Name>[], Sort<Name>>, any, any>

• Returns IterableIterator<FuncDecl<Name, Sort<Name>[], Sort<Name>>, any, any>