Z3_goal_prec class abstract

\brief A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.

  • Z3_GOAL_PRECISE: Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
  • Z3_GOAL_UNDER: Goal is the product of a under-approximation (sat answers are preserved).
  • Z3_GOAL_OVER: Goal is the product of an over-approximation (unsat answers are preserved).
  • Z3_GOAL_UNDER_OVER: Goal is garbage (it is the product of over- and under-approximations, sat and unsat answers are not preserved).

Constructors

Z3_goal_prec()

Properties

hashCode int
The hash code for this object.
no setterinherited
runtimeType Type
A representation of the runtime type of the object.
no setterinherited

Methods

noSuchMethod(Invocation invocation) → dynamic
Invoked when a nonexistent method or property is accessed.
inherited
toString() String
A string representation of this object.
inherited

Operators

operator ==(Object other) bool
The equality operator.
inherited

Constants

GOAL_OVER → const int
GOAL_PRECISE → const int
GOAL_UNDER → const int
GOAL_UNDER_OVER → const int