Commit 2bd39ed9 authored by David Hauzar's avatar David Hauzar

A single transformation for preparing a task for getting a counter-example model.

parent 1cdfa8c6
......@@ -165,6 +165,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
encoding_sort simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \
prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
reduction_engine compute induction_pr prop_curry
......
......@@ -35,9 +35,10 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
transformation "introduce_premises"
transformation "intro_projections_counterexmp"
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
......
......@@ -4,10 +4,6 @@
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: enable model construction *)
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* Counterexamples: set model parser *)
model_parser "smtv2"
......@@ -32,9 +28,10 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
transformation "introduce_premises"
transformation "intro_projections_counterexmp"
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
......
let prepare_for_counterexmp =
Trans.compose
Intro_projections_counterexmp.intro_projections_counterexmp
(Trans.goal Introduction.intros)
let () = Trans.register_transform "prepare_for_counterexmp" prepare_for_counterexmp
~desc:"Transformation@ that@ prepares@ the@ task@ for@ quering@ for@ \
the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \
when@ the@ solver@ will@ be@ asked@ for@ the@ counter-example."
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val prepare_for_counterexmp : Task.task Trans.trans
(**
Transformation that prepares the task for quering for
the counter-example model.
This transformation does so only when the solver will be asked
for the counter-example.
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment