Commit a303ae72 authored by Sylvain Dailler's avatar Sylvain Dailler

Q217-025 Printer to smt2: convert bool term inside type to bv

This commit solves a CVC4 limitation on boolean inside datatypes for CE.
It converts them to bv by adding a new printer. This commit is a hack and
it will be reverted when the bug is solved in CVC4.

* Makefile.in
(Makefile): Added new printer.
* drivers/smtv-libv2_cvc_ce.drv:
(printer): new printer used is smtv2_cvc_ce
* src/driver/parse_smtv2_model_lexer.mll
(parse): Changed the way constructor of datatype are detected.
* src/printer/smtv2_cvc_ce.ml
(print_constructors): Projections to bool are changed to projections
to bitvectors. Duplicate projections are generated which returns bool and
are used in the rest of smtv2 generated.

Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881
parent 1f6da25d
......@@ -196,7 +196,8 @@ 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 coq pvs isabelle \
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 smtv2_cvc_ce coq\
pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
......
......@@ -15,7 +15,7 @@ prelude "(set-logic AUFBVDTLIRA)"
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-cvc-ce.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
......@@ -49,19 +49,19 @@ rule token = parse
| "false" { FALSE }
| "LAMBDA" { LAMBDA }
| "ARRAY_LAMBDA" { ARRAY_LAMBDA }
| "mk___split_fields"(opt_num as n) opt_num {
| "mk___split_fields"(opt_num as n) opt_num "___" {
match n with
| "" -> MK_SPLIT_FIELD ("mk___split_fields",0)
| n -> MK_SPLIT_FIELD ("mk____split_fields"^n, int_of_string n) }
| "mk___rep"(opt_num as n) opt_num {
| "mk___rep"(opt_num as n) opt_num "___" {
match n with
| "" -> MK_REP ("mk___rep", 0)
| n -> MK_REP ("mk___rep"^n, int_of_string n) }
| "mk___t"(opt_num as n) opt_num {
| "mk___t"(opt_num as n) opt_num "___" {
match n with
| "" -> MK_T ("mk___t", 0)
| n -> MK_T ("mk___t"^n, int_of_string n) }
| "mk___split_discrs"(opt_num as n) opt_num {
| "mk___split_discrs"(opt_num as n) opt_num "___" {
match n with
| "" -> MK_SPLIT_DISCRS ("mk___split_discrs",0)
| n -> MK_SPLIT_DISCRS ("mk____split_discrs"^n, int_of_string n) }
......
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