Interface Goal<Name>

Readonlyctx

Readonlyptr

add

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

• Add constraints to the goal.

  Parameters

  • ...constraints: (boolean | Bool<Name>)[]

  Returns void

asExpr

• asExpr(): Bool<Name>

• Convert the goal to a single Boolean expression (conjunction of all constraints).

  Returns Bool<Name>

convertModel

• convertModel(model: Model<Name>): Model<Name>

• Convert a model for the goal to a model for the original goal.

  Parameters

  • model: Model<Name>

  Returns Model<Name>

depth

• depth(): number

• Return the depth of the goal (number of tactics applied).

  Returns number

dimacs

• dimacs(includeNames?: boolean): string

• Return a DIMACS string representation of the goal.

  Parameters

  • OptionalincludeNames: boolean

  Returns string

get

• get(i: number): Bool<Name>

• Return a constraint from the goal at the given index.

  Parameters

  • i: number

  Returns Bool<Name>

inconsistent

• inconsistent(): boolean

• Return true if the goal contains the False constraint.

  Returns boolean

isDecidedSat

• isDecidedSat(): boolean

• Return true if the goal is decided to be satisfiable.

  Returns boolean

isDecidedUnsat

• isDecidedUnsat(): boolean

• Return true if the goal is decided to be unsatisfiable.

  Returns boolean

numExprs

• numExprs(): number

• Return the number of expressions in the goal.

  Returns number

precision

• precision(): Z3_goal_prec

• Return the precision of the goal (precise, under-approximation, over-approximation).

  Returns Z3_goal_prec

reset

• reset(): void

• Reset the goal to empty.

  Returns void

size

• size(): number

• Return the number of constraints in the goal.

  Returns number

toString

• toString(): string

• Return a string representation of the goal.

  Returns string