Commit a0c76576 authored by MARCHE Claude's avatar MARCHE Claude

Removed remaining 'bare' drivers

parent 638a46fe
import "cvc3_bare.drv"
import "discrimination.gen"
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
(* Why3 driver for CVC3 *)
prelude "%%% this is a prelude for CVC3 "
printer "cvc3"
filename "%f-%t-%g.cvc"
(* 'fail' must be before 'valid'; otherwise it is ignored *)
fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid\\."
unknown "Unknown\\." ""
outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
timeout "self-timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "INT"
syntax type real "REAL"
syntax predicate (=) "(%1 = %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude "%%% this is a prelude for CVC3 integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude "%%% this is a prelude for CVC3 real arithmetic"
prelude "div_by_zero: (REAL) -> REAL;"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(IF (%2 = 0) THEN (div_by_zero(%1)) ELSE (%1 / %2) ENDIF)"
syntax function (-_) "(- %1)"
syntax function inv "(IF (%1 = 0) THEN (div_by_zero(1)) ELSE (1 / %1) ENDIF)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
theory real.FromInt
syntax function from_int "%1"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory Bool
syntax type bool "BITVECTOR(1)"
syntax function True "0bin1"
syntax function False "0bin0"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(%1 & %2)"
syntax function orb "(%1 | %2)"
syntax function xorb "(BVXOR(%1,%2))"
syntax function notb "(~ %1)"
end
theory map.Map
syntax type map "(ARRAY %1 OF %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
syntax function get "(%1[%2])"
syntax function set "(%1 WITH [%2] := %3)"
end
import "discrimination.gen"
(* Why driver for SMT syntax *)
prelude "%%% this is a prelude for CVC3 "
printer "cvc3"
filename "%f-%t-%g.cvc"
(* 'fail' must be before 'valid'; otherwise it is ignored *)
fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid\\."
unknown "Unknown\\." ""
outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
timeout "self-timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type int "INT"
syntax type real "REAL"
syntax predicate (=) "(%1 = %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude "%%% this is a prelude for CVC3 integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
end
theory real.Real
prelude "%%% this is a prelude for CVC3 real arithmetic"
prelude "div_by_zero: (REAL) -> REAL;"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(IF (%2 = 0) THEN (div_by_zero(%1)) ELSE (%1 / %2) ENDIF)"
syntax function (-_) "(- %1)"
syntax function inv "(IF (%1 = 0) THEN (div_by_zero(1)) ELSE (1 / %1) ENDIF)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
theory real.FromInt
syntax function from_int "%1"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory Bool
syntax type bool "BITVECTOR(1)"
syntax function True "0bin1"
syntax function False "0bin0"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(%1 & %2)"
syntax function orb "(%1 | %2)"
syntax function xorb "(BVXOR(%1,%2))"
syntax function notb "(~ %1)"
end
theory map.Map
syntax type map "(ARRAY %1 OF %2)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
syntax function get "(%1[%2])"
syntax function set "(%1 WITH [%2] := %3)"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
prelude "(set-logic AUFNIRA)"
(* cvc4 does not support generating counterexamples with non-linear arithmetic *)
(* prelude "(set-logic AUFLIRA)" *)
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)" *)
(* Counterexamples: enable model construction *)
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* 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"
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
(* regexp for steps *)
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(* CVC4 division seems to be neither the Euclidean one, nor 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
*)
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