Commit d0bd45de authored by MARCHE Claude's avatar MARCHE Claude

support for CVC4 1.6 finalized

need to tell that the printer is for version SMT-LIB 2.6
parent 1e35d2e3
......@@ -13,6 +13,7 @@ prelude "(set-logic AUFBVDTNIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
......
......@@ -8,6 +8,7 @@ prelude "(set-logic AUFNIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......
......@@ -11,6 +11,7 @@ prelude "(set-logic AUFBVDTNIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
......
(** Why3 driver for CVC4 >= 1.5 *)
(** Why3 driver for CVC4 1.5 *)
prelude ";; produced by cvc4_15.drv ;;"
prelude "(set-logic AUFBVDTNIRA)"
......@@ -10,10 +10,8 @@ prelude "(set-logic AUFBVDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "discrimination.gen"
......@@ -26,14 +24,12 @@ 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 *)
(* 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"
......
import "cvc4_15.drv"
(* Counterexamples: set model parser *)
model_parser "smtv2"
theory BuiltIn
meta "get_counterexmp" ""
......
(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
prelude ";; produced by cvc4_16.drv ;;"
prelude "(set-info :smt-lib-version 2.5)"
prelude "(set-info :smt-lib-version 2.6)"
prelude "(set-logic AUFBVFPDTNIRA)"
(*
A : Array
......@@ -11,11 +11,9 @@ prelude "(set-logic AUFBVFPDTNIRA)"
DT : Datatypes
NIRA : NonLinear Integer+Real Arithmetic
*)
prelude "(set-info :source |VC generated by SPARK 2014|)"
prelude "(set-info :category industrial)"
prelude "(set-info :status unknown)"
import "smt-libv2.drv"
printer "smtv2.6"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
......@@ -24,20 +22,22 @@ 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"
(* remove pointless quantifiers from the goal *)
transformation "introduce_premises"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
......@@ -47,3 +47,27 @@ steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* CVC4 division seems to be the Euclidean one, not the Computer one *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
(** 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
*)
import "cvc4_16.drv"
(* 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" ""
meta "meta_incremental" ""
end
......@@ -16,7 +16,6 @@ prelude "(set-logic AUFNIRA)"
*)
printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
......
......@@ -8,6 +8,7 @@ prelude "(set-logic AUFLIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "discrimination.gen"
(* specific message from veriT 201310 *)
......
......@@ -8,6 +8,7 @@ prelude "(set-logic QF_AUFLIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "discrimination.gen"
(* specific messages from Yices-smt2 *)
......
......@@ -7,6 +7,7 @@ prelude "(set-logic AUFNIRA)"
*)
import "smt-libv2.drv"
printer "smtv2"
import "discrimination.gen"
transformation "inline_trivial"
......
......@@ -8,6 +8,7 @@
model_parser "smtv2"
import "smt-libv2.drv"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......
......@@ -8,6 +8,7 @@
model_parser "smtv2"
import "smt-libv2.drv"
printer "smtv2"
import "smt-libv2-bv.gen"
import "z3_bv.gen"
import "smt-libv2-floats.gen"
......
......@@ -49,16 +49,44 @@ command_steps = "%e -steps-bound %S %f"
driver = "alt_ergo"
editor = "altgr-ergo"
# CVC4 version >= 1.5, with counterexamples
# CVC4 version >= 1.6, with counterexamples
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
exec = "cvc4-1.6"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.6"
driver = "cvc4_16_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version >= 1.6
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.6"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.6"
driver = "cvc4_16"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%e --tlimit=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
use_at_auto_level = 1
# CVC4 version = 1.5, with counterexamples
[ATP cvc4-ce]
name = "CVC4"
alternative = "counterexamples"
exec = "cvc4"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.5"
driver = "cvc4_15_counterexample"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
......@@ -66,15 +94,13 @@ driver = "cvc4_15_counterexample"
command = "%e --tlimit-per=%t000 --lang=smt2 %f"
command_steps = "%e --stats --rlimit=%S --lang=smt2 %f"
# CVC4 version >= 1.5
# CVC4 version 1.5
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.6"
exec = "cvc4-1.5"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.6"
version_ok = "1.5"
driver = "cvc4_15"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
......
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