Interface Fixedpoint<Name>

Readonlyctx

Readonlyptr

add

• add(...constraints: Bool<Name>[]): void

• Assert a constraint (or multiple) into the fixedpoint solver as background axioms.

  Parameters

  • ...constraints: Bool<Name>[]

  Returns void

addCover

• addCover(
      level: number,
      pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
      property: Expr<Name, AnySort<Name>, unknown>,
  ): void

• Add a property about the predicate at the given level.

  Parameters

  • level: number

    The level to add the property at
  • pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>

    The predicate function declaration
  • property: Expr<Name, AnySort<Name>, unknown>

    The property as an expression

  Returns void

addFact

• addFact(pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>, ...args: number[]): void

• Add a table fact to the fixedpoint solver.

  Parameters

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

    The predicate (function declaration)
  • ...args: number[]

    Arguments to the predicate as integers

  Returns void

addRule

• addRule(rule: Bool<Name>, name?: string): void

• Add a rule (Horn clause) to the fixedpoint solver.

  Parameters

  • rule: Bool<Name>

    The rule as a Boolean expression (implication)
  • Optionalname: string

    Optional name for the rule

  Returns void

fromFile

• fromFile(file: string): AstVector<Name, Bool<Name>>

• Parse an SMT-LIB2 file with fixedpoint rules and add them to the context.

  Parameters

  • file: string

    Path to the file to parse

  Returns AstVector<Name, Bool<Name>>

  Vector of queries from the parsed file

fromString

• fromString(s: string): AstVector<Name, Bool<Name>>

• Parse an SMT-LIB2 string with fixedpoint rules and add them to the context.

  Parameters

  • s: string

    SMT-LIB2 string to parse

  Returns AstVector<Name, Bool<Name>>

  Vector of queries from the parsed string

getAnswer

• getAnswer(): null | Expr<Name, AnySort<Name>, unknown>

• Retrieve the answer (satisfying instance or proof of unsatisfiability) from the last query.

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

  Expression containing the answer, or null if not available

getAssertions

• getAssertions(): AstVector<Name, Bool<Name>>

• Retrieve set of assertions added to the fixedpoint context.

  Returns AstVector<Name, Bool<Name>>

  Vector of assertions

getCoverDelta

• getCoverDelta(
      level: number,
      pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
  ): null | Expr<Name, AnySort<Name>, unknown>

• Retrieve the cover of a predicate at a given level.

  Parameters

  • level: number

    The level to query
  • pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>

    The predicate function declaration

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

  Expression representing the cover, or null if not available

getNumLevels

• getNumLevels(pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>): number

• Retrieve the number of levels explored for a given predicate.

  Parameters

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

    The predicate function declaration

  Returns number

  The number of levels

getReasonUnknown

• getReasonUnknown(): string

• Retrieve the reason why the fixedpoint engine returned 'unknown'.

  Returns string

  A string explaining why the result was unknown

getRules

• getRules(): AstVector<Name, Bool<Name>>

• Retrieve set of rules added to the fixedpoint context.

  Returns AstVector<Name, Bool<Name>>

  Vector of rules

help

• help(): string

• Return a string describing all available options.

  Returns string

query

• query(query: Bool<Name>): Promise<CheckSatResult>

• Query the fixedpoint solver to determine if the formula is derivable.

  Parameters

  • query: Bool<Name>

    The query as a Boolean expression

  Returns Promise<CheckSatResult>

  A promise that resolves to 'sat', 'unsat', or 'unknown'

queryRelations

• queryRelations(
      ...relations: FuncDecl<Name, Sort<Name>[], Sort<Name>>[],
  ): Promise<CheckSatResult>

• Query the fixedpoint solver for a set of relations.

  Parameters

  • ...relations: FuncDecl<Name, Sort<Name>[], Sort<Name>>[]

    Array of function declarations representing relations to query

  Returns Promise<CheckSatResult>

  A promise that resolves to 'sat', 'unsat', or 'unknown'

registerRelation

• registerRelation(pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>): void

• Register a predicate as a recursive relation.

  Parameters

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

    Function declaration to register as a recursive relation

  Returns void

release

• release(): void

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

  Returns void

set

• set(key: string, value: any): void

• Set a configuration option for the fixedpoint solver.

  Parameters

  • key: string

    Configuration parameter name
  • value: any

    Configuration parameter value

  Returns void

setPredicateRepresentation

• setPredicateRepresentation(
      pred: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
      kinds: string[],
  ): void

• Set predicate representation for the Datalog engine.

  Parameters

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

    The predicate function declaration
  • kinds: string[]

    Array of representation kinds

  Returns void

statistics

• statistics(): Statistics<Name>

• Retrieve statistics for the fixedpoint solver. Returns performance metrics and diagnostic information.

  Returns Statistics<Name>

  A Statistics object containing solver metrics

toString

• toString(): string

• Convert the fixedpoint context to a string.

  Returns string

  String representation of the fixedpoint context

updateRule

• updateRule(rule: Bool<Name>, name: string): void

• Update a named rule in the fixedpoint solver.

  Parameters

  • rule: Bool<Name>

    The rule as a Boolean expression (implication)
  • name: string

    Name of the rule to update

  Returns void