Commit 1cdfa8c6 authored by David Hauzar's avatar David Hauzar

Move of the transformations introduce_premises and...

Move of the transformations introduce_premises and intro_projections_counterexmp to the end of the driver.
Note that this requires putting meta "inline : no" for every projection function to the source file.
Otherwise, declarations projection functions are removed and the transformation intro_projections_counterexmp fails.
parent 58560850
......@@ -15,10 +15,6 @@ prelude "(set-logic AUFBVDTLIRA)"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_intro" *)
(* 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"
(* Counterexamples: set model parser *)
model_parser "smtv2"
......@@ -39,6 +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"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
......
......@@ -8,10 +8,6 @@
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* 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"
(* Counterexamples: set model parser *)
model_parser "smtv2"
......@@ -36,6 +32,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"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
......
......@@ -8,6 +8,7 @@ module M
=
l+100
meta "inline : no" function projf
meta "model_projection" function projf
val y "model_projected" "model_trace:y" :ref int
......
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