Commit 33f66330 authored by Sylvain Dailler's avatar Sylvain Dailler

Update cvc4_15 driver

Change prelude to AUFBVDTNIRA and removed smt-libv2-cvc-ce.drv
parent f7def304
......@@ -196,7 +196,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry eliminate_literal
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 smtv2_cvc_ce coq\
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
pvs isabelle \
simplify gappa cvc3 yices mathematica
......
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Invalid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
(error "A non-linear fact was asserted to arithmetic in a linear logic.
The fact in question: (>= (+ x (* (- 1) (* x linearIntDiv_1))) 0)
")
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 14:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test_overflow : Invalid
ce/int_overflow.mlw ModelInt test_overflow : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 18:
x = {"type" : "Integer" , "val" : "65535" }
y = {"type" : "Integer" ,
"val" : "1" }
ce/int_overflow.mlw ModelInt test_overflow2 : Invalid
ce/int_overflow.mlw ModelInt test_overflow2 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 23:
x = {"type" : "Integer" , "val" : "-2" }
y = {"type" : "Integer" ,
"val" : "-1" }
ce/int_overflow.mlw ModelInt test_overflow_int16 : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int16 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 30:
x = {"type" : "Integer" , "val" : "-65536" }
y = {"type" : "Integer" ,
"val" : "-1" }
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 35:
x = {"type" : "Integer" , "val" : "-65536" }
y = {"type" : "Integer" ,
"val" : "-1" }
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 40:
x = {"type" : "Integer" , "val" : "32768" }
y = {"type" : "Integer" ,
"val" : "32768" }
ce/int_overflow.mlw ModelInt test_overflow_int32 : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int32 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 48:
x = {"type" : "Integer" , "val" : "-2147483648" }
y = {"type" : "Integer" ,
"val" : "-1" }
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 53:
x = {"type" : "Integer" , "val" : "1073741824" }
y = {"type" : "Integer" ,
"val" : "1073741824" }
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Invalid
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 58:
x = {"type" : "Integer" , "val" : "1073741824" }
......
ce/logic.mlw T g0 : Invalid
ce/logic.mlw T g0 : Unknown (other)
Counter-example model:File logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
ce/logic.mlw T g1 : Invalid
ce/logic.mlw T g1 : Unknown (other)
Counter-example model:File logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "0" }
ce/logic.mlw T g2 : Invalid
ce/logic.mlw T g2 : Unknown (other)
Counter-example model:File logic.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
......
ce/map.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File map.mlw:
Line 10:
y = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" , "val" : "-2" }
Line 12:
x23 = {"type" : "Integer" , "val" : "0" }
Line 13:
......@@ -9,9 +9,9 @@ x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
"val" : "-1" }
Line 16:
y = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" , "val" : "-1" }
Line 17:
x23 = {"type" : "Integer" , "val" : "1" }
Line 18:
......@@ -27,13 +27,13 @@ x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 23:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" ,
"val" : "0" }
"val" : "-3" }
Line 24:
x = {"type" : "Integer" , "val" : "0" }
Line 25:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "0" }
"val" : "-1" }
ce/real.mlw ModelReal test1 : Invalid
ce/real.mlw ModelReal test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
(error "A non-linear fact was asserted to arithmetic in a linear logic.
The fact in question: (= x (* x nonlinearDiv_1))
")
ce/real.mlw ModelReal test1 : Unknown (other)
ce/real.mlw ModelReal test2 : Unknown (other)
Counter-example model:File real.mlw:
Line 7:
x = {"type" : "Decimal" ,
"val" : "0.0" }
......@@ -3,10 +3,10 @@ Counter-example model:File records.mlw:
Line 27:
x.field_f = {"type" : "Integer" , "val" : "0" }
x.g = {"type" : "Boolean" ,
"val" : false }
"val" : true }
Line 28:
old x.g = {"type" : "Boolean" ,
"val" : false }
"val" : true }
old x.field_f = {"type" : "Integer" ,
"val" : "0" }
......
......@@ -2,11 +2,11 @@ ce/ref.mlw M G : Unknown (other)
ce/ref.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File ref.mlw:
Line 10:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" , "val" : "1" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 11:
old x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" , "val" : "1" }
old y = {"type" : "Integer" ,
"val" : "0" }
Line 13:
......@@ -16,7 +16,7 @@ y = {"type" : "Integer" ,
ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ref.mlw:
Line 18:
y = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" , "val" : "-2" }
Line 20:
x23 = {"type" : "Integer" , "val" : "0" }
Line 21:
......@@ -24,9 +24,9 @@ x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "0" }
"val" : "-1" }
Line 24:
y = {"type" : "Integer" , "val" : "0" }
y = {"type" : "Integer" , "val" : "-1" }
Line 25:
x23 = {"type" : "Integer" , "val" : "1" }
Line 26:
......@@ -42,13 +42,13 @@ x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 31:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" ,
"val" : "0" }
"val" : "-3" }
Line 32:
x = {"type" : "Integer" , "val" : "0" }
Line 33:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "0" }
"val" : "-1" }
ce/simple_array.mlw ModelArray t1 : Invalid
ce/simple_array.mlw ModelArray t1 : Unknown (other)
Counter-example model:File simple_array.mlw:
Line 5:
i = {"type" : "Integer" , "val" : "0" }
......
(** Why3 driver for CVC4 >= 1.5 *)
prelude "(set-logic AUFBVDTLIRA)"
prelude "(set-logic AUFBVDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
......@@ -15,7 +15,7 @@ prelude "(set-logic AUFBVDTLIRA)"
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2-cvc-ce.drv"
import "smt-libv2.drv"
import "smt-libv2-bv.gen"
import "discrimination.gen"
......
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
prelude ";;; generated by SMT-LIB2 driver"
(*
Note: we do not insert any command "set-logic" because its
interpretation is specific to provers
prelude "(set-logic AUFNIRA)"
A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
printer "smtv2_cvc_ce"
filename "%f-%t-%g.smt2"
invalid "^sat$"
unknown "^\\(unknown\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
end
theory algebra.OrderedUnitaryCommutativeRing
remove allprops
end
theory algebra.Field
remove allprops
end
theory algebra.OrderedField
remove allprops
end
theory int.Int
prelude ";;; SMT-LIB2: 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 allprops
end
theory int.Abs
syntax function abs "(abs %1)"
remove allprops
end
theory int.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove allprops
end
theory int.Div2
remove allprops
end
theory int.ComputerDivision
(* really, you should use bitvectors here, but... *)
end
theory real.Real
prelude ";;; SMT-LIB2: real arithmetic"
meta "encoding : kept" type real
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function ( * ) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove allprops
end
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove allprops
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
theory Bool
meta "encoding : kept" type bool
meta "eliminate_algebraic" "no_inversion"
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
remove allprops
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
remove allprops
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
remove allprops
end
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding:ignore_polymorphism_ts" type map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
meta "encoding:ignore_polymorphism_ls" function ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove allprops
end
theory map.Const
meta "encoding : lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
This diff is collapsed.
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