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>>

getSort

• getSort(i: number): Sort<Name>

• Return the uninterpreted sort at the given index.

  Parameters

  • i: number

    Index of the sort (must be less than numSorts())

  Returns Sort<Name>

  The sort at the given index

  Example

  const model = solver.model();
  for (let i = 0; i < model.numSorts(); i++) {
    const sort = model.getSort(i);
    console.log('Sort:', sort.toString());
  }
  Copy

getSorts

• getSorts(): Sort<Name>[]

• Return all uninterpreted sorts that have an interpretation in the model.

  Returns Sort<Name>[]

  An array of all uninterpreted sorts

  Example

  const model = solver.model();
  const sorts = model.getSorts();
  for (const sort of sorts) {
    console.log('Sort:', sort.toString());
    const universe = model.sortUniverse(sort);
    console.log('Universe size:', universe.length());
  }
  Copy

keys

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

• Returns IterableIterator<number, any, any>

length

• length(): number

• Returns number

numSorts

• numSorts(): number

• Return the number of uninterpreted sorts that have an interpretation in the model.

  Returns number

  The number of uninterpreted sorts

  Example

  const { Solver, Sort } = await init();
  const solver = new Solver();
  const A = Sort.declare('A');
  const x = Const('x', A);
  solver.add(x.eq(x));
  await solver.check();
  const model = solver.model();
  console.log('Number of sorts:', model.numSorts());
  Copy

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

sortUniverse

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

• Return the finite set of elements that represent the interpretation for the given sort. This is only applicable to uninterpreted sorts with finite interpretations.

  Parameters

  • sort: Sort<Name>

    The sort to get the universe for

  Returns AstVector<Name, AnyExpr<Name>>

  An AstVector containing all elements in the sort's universe

  Example

  const { Solver, Sort, Const } = await init();
  const solver = new Solver();
  const A = Sort.declare('A');
  const x = Const('x', A);
  const y = Const('y', A);
  solver.add(x.neq(y));
  await solver.check();
  const model = solver.model();
  const universe = model.sortUniverse(A);
  console.log('Universe has', universe.length(), 'elements');
  for (let i = 0; i < universe.length(); i++) {
    console.log('Element:', universe.get(i).toString());
  }
  Copy

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>