Commit 5b98a355 authored by Sylvain Dailler's avatar Sylvain Dailler

R515-014 Adapt new cvc4 to ce

This commit adapts the changes made by Florian to the drivers of cvc4 for
counterexamples (for float with cvc4 version 1.6). It reuses without
changes the drivers he intended to use.
I modified the model parser so that it can recognize float models of cvc4.

* drivers/cvc4_16_counterexample.drv
Added import smt-libv2-floats.gen.

* src/driver/parse_smtv2_model_lexer.mll
Added a token for float_type.

* src/driver/parse_smtv2_model_parser.mly
Float_type can be encountered as names in the model but produce nothing.


Change-Id: I64b49dd1824138a5d3f98ab046da0fdbc9420e66
(cherry picked from commit 226d70801ad449fb86d73d35ac07fcfd56b8ba65)

Conflicts:
	drivers/cvc4_15_counterexample.drv
	drivers/cvc4_16_counterexample.drv
	drivers/cvc4_gnatprove_ce.drv
parent 49a561d1
(** Why3 driver for CVC4 >= 1.5 *)
prelude ";; produced by cvc4_16_counterexample.drv ;;"
prelude "(set-info :smt-lib-version 2.5)"
prelude "(set-logic AUFBVFPDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
BV : BitVectors
FP : FloatingPoint
DT : Datatypes
NIRA : NonLinear Integer+Real Arithmetic
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* 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.
Note: does nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
theory BuiltIn
meta "get_counterexmp" ""
end
......@@ -64,7 +64,7 @@ rule token = parse
| "(_" space+ "BitVec" space+ num")" { BITVECTOR_TYPE }
| "(_" space+ "extract" space+ num space+ num ")" as s { BITVECTOR_EXTRACT s }
| "(_" space+ "int2bv" space+ num ")" as s { INT_TO_BV s}
| "(_" space+ "FloatingPoint" space+ (num as exp) space+ (num as mantissa)")" { FLOAT_TYPE (exp, mantissa) }
| "(_" space+ "+zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_zero }
| "(_" space+ "-zero" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Minus_zero }
| "(_" space+ "+oo" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Plus_infinity }
......
......@@ -39,6 +39,7 @@
%token <string> BITVECTOR_EXTRACT
%token <string> INT_TO_BV
%token BITVECTOR_TYPE
%token <string * string> FLOAT_TYPE
%token <string> INT_STR
%token <string> MINUS_INT_STR
%token <string * string> DEC_STR
......@@ -172,6 +173,7 @@ name:
(* Should not happen in relevant part of the model (ad hoc) *)
| BITVECTOR_TYPE { "" }
| BITVECTOR_EXTRACT { $1 }
| FLOAT_TYPE { "" }
(* Z3 specific boolean expression. This should maybe be used in the future as
it may give some information on the counterexample. *)
......
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