getPrecision method

GoalPrecision getPrecision()

Return the "precision" of the given goal.

Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Implementation

GoalPrecision getPrecision() {
  final result = _c._z3.goal_precision(_goal);
  switch (result) {
    case Z3_goal_prec.GOAL_PRECISE:
      return GoalPrecision.precise;
    case Z3_goal_prec.GOAL_UNDER:
      return GoalPrecision.under;
    case Z3_goal_prec.GOAL_OVER:
      return GoalPrecision.over;
    case Z3_goal_prec.GOAL_UNDER_OVER:
      return GoalPrecision.underOver;
    default:
      throw AssertionError('Unknown goal precision: $result');
  }
}