CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 00:15:39 +03:00
Code Issues Projects Releases Wiki Activity

Renamed and grouped modules cleanly

Browse Source
This commit is contained in:
Denis Merigoux 2022-01-08 18:37:04 +01:00
parent 8b6595426e
commit 743a1b74c9
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
7 changed files with 69 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/dcalc/dune
View File

@ -1,7 +1,7 @@
(library
(name dcalc)
(public_name catala.dcalc)
(libraries bindlib unionFind utils re camomile runtime z3)
(libraries bindlib unionFind utils re camomile runtime)
(preprocess
(pps visitors.ppx)))

4
compiler/driver.ml
View File

@ -216,7 +216,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
prgm.decl_ctx) typ); *)
match backend with
| Cli.Proof ->
let vcs = Dcalc.Verificator.generate_verification_conditions prgm in
let vcs = Verification.Conditions.generate_verification_conditions prgm in
List.iter
(fun vc ->
Cli.result_print
@ -226,7 +226,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(Dcalc.Print.format_expr prgm.decl_ctx)
vc))
vcs;
Dcalc.Vc_z3encoding.solve_vc vcs;
Verification.Z3encoding.solve_vc vcs;
0
| Cli.Run ->
Cli.debug_print "Starting interpretation...";

11
compiler/dune
View File

@ -1,7 +1,16 @@
(library
(name driver)
(public_name catala.driver)
(libraries utils surface desugared literate dcalc lcalc scalc runtime)
(libraries
utils
surface
desugared
literate
dcalc
lcalc
scalc
runtime
verification)
(modules driver))
(library

1
compiler/dcalc/verificator.ml → compiler/verification/conditions.ml
View File

@ -13,6 +13,7 @@
the License. *)
open Utils
open Dcalc
open Ast
let conjunction (args : expr Pos.marked list) (pos : Pos.t) =

8
compiler/verification/dune Normal file
View File

@ -0,0 +1,8 @@
(library
(name verification)
(public_name catala.verification)
(libraries bindlib utils dcalc runtime z3))
(documentation
(package catala)
(mld_files verification))

3
compiler/verification/verification.mld Normal file
View File

@ -0,0 +1,3 @@
{0 Verification}
TODO

109
compiler/dcalc/vc_z3encoding.ml → compiler/verification/z3encoding.ml
View File

@ -13,66 +13,57 @@
the License. *)
open Utils
open Dcalc
open Ast
open Z3
(** [translate_lit] returns the Z3 expression as a literal corresponding to [lit] **)
let translate_lit (ctx : context) (l : lit) : Expr.expr =
match l with
| LBool b ->
if b then Boolean.mk_true ctx else Boolean.mk_false ctx
| LBool b -> if b then Boolean.mk_true ctx else Boolean.mk_false ctx
| LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| LInt n -> Arithmetic.Integer.mk_numeral_i ctx (Runtime.integer_to_int n)
| LRat _ -> failwith "[Z3 encoding] LRat literals not supported"
| LMoney _ -> failwith "[Z3 encoding] LMoney literals not supported"
| LUnit -> failwith "[Z3 encoding] LUnit literals not supported"
| LDate _ -> failwith "[Z3 encoding] LDate literals not supported"
| LDuration _ -> failwith "[Z3 encoding] LDuration literals not supported"
(** [translate_op] returns the Z3 expression corresponding to the
application of [op] to the arguments [args] **)
(** [translate_op] returns the Z3 expression corresponding to the application of [op] to the
arguments [args] **)
let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked list) : Expr.expr =
match op with
| Ternop _top ->
let _e1, _e2, _e3 = match args with
| [e1; e2; e3] -> e1, e2, e3
let _e1, _e2, _e3 =
match args with
| [ e1; e2; e3 ] -> (e1, e2, e3)
(* TODO: Print term for error message *)
| _ -> failwith "[Z3 encoding] Ill-formed ternary operator application"
in
failwith "[Z3 encoding] ternary operator application not supported"
| Binop bop ->
let e1, e2 = match args with
| [e1 ; e2] -> e1, e2
| Binop bop -> (
let e1, e2 =
match args with
| [ e1; e2 ] -> (e1, e2)
(* TODO: Print term for error message *)
| _ -> failwith "[Z3 encoding] Ill-formed binary operator application"
in
(match bop with
| And -> Boolean.mk_and ctx [translate_expr ctx e1; translate_expr ctx e2]
| Or -> Boolean.mk_or ctx [translate_expr ctx e1; translate_expr ctx e2]
match bop with
| And -> Boolean.mk_and ctx [ translate_expr ctx e1; translate_expr ctx e2 ]
| Or -> Boolean.mk_or ctx [ translate_expr ctx e1; translate_expr ctx e2 ]
| Xor -> failwith "[Z3 encoding] application of binary operator Xor not supported"
| Add _ -> failwith "[Z3 encoding] application of binary operator Add not supported"
| Sub _ -> failwith "[Z3 encoding] application of binary operator Sub not supported"
| Mult _ -> failwith "[Z3 encoding] application of binary operator Mult not supported"
| Div _ -> failwith "[Z3 encoding] application of binary operator Div not supported"
| Lt op_kind ->
(match op_kind with
| KInt -> Arithmetic.mk_lt ctx (translate_expr ctx e1) (translate_expr ctx e2)
| _ -> failwith "[Z3 encoding] application of binary operator Lt for non-integers not supported"
)
| Lt op_kind -> (
match op_kind with
| KInt -> Arithmetic.mk_lt ctx (translate_expr ctx e1) (translate_expr ctx e2)
| _ ->
failwith
"[Z3 encoding] application of binary operator Lt for non-integers not supported")
| Lte _ -> failwith "[Z3 encoding] application of binary operator Lte not supported"
| Gt _ -> failwith "[Z3 encoding] application of binary operator Gt not supported"
| Gte _ -> failwith "[Z3 encoding] application of binary operator Gte not supported"
@ -80,33 +71,28 @@ let rec translate_op (ctx : context) (op : operator) (args : expr Pos.marked lis
| Neq -> failwith "[Z3 encoding] application of binary operator New not supported"
| Map -> failwith "[Z3 encoding] application of binary operator Map not supported"
| Concat -> failwith "[Z3 encoding] application of binary operator Concat not supported"
| Filter -> failwith "[Z3 encoding] application of binary operator Filter not supported"
)
| Unop uop ->
let e1 = match args with
| [e1] -> e1
| Filter -> failwith "[Z3 encoding] application of binary operator Filter not supported")
| Unop uop -> (
let e1 =
match args with
| [ e1 ] -> e1
(* TODO: Print term for error message *)
| _ -> failwith "[Z3 encoding] Ill-formed unary operator application"
in
(match uop with
match uop with
| Not -> failwith "[Z3 encoding] application of unary operator Not not supported"
| Minus _ -> failwith "[Z3 encoding] application of unary operator Minus not supported"
(* Omitting the log from the VC *)
| Log _ -> translate_expr ctx e1
| Length -> failwith "[Z3 encoding] application of unary operator Length not supported"
| IntToRat -> failwith "[Z3 encoding] application of unary operator IntToRat not supported"
| GetDay -> failwith "[Z3 encoding] application of unary operator GetDay not supported"
| GetMonth -> failwith "[Z3 encoding] application of unary operator GetMonth not supported"
| GetYear -> failwith "[Z3 encoding] application of unary operator GetYear not supported"
)
| GetYear -> failwith "[Z3 encoding] application of unary operator GetYear not supported")
(** [translate_expr] translate the expression [vc] to its corresponding Z3 expression **)
and translate_expr (ctx:context) (vc : expr Pos.marked) : Expr.expr =
and translate_expr (ctx : context) (vc : expr Pos.marked) : Expr.expr =
match Pos.unmark vc with
| EVar _ -> failwith "[Z3 encoding] EVar unsupported"
| ETuple _ -> failwith "[Z3 encoding] ETuple unsupported"
@ -114,38 +100,33 @@ and translate_expr (ctx:context) (vc : expr Pos.marked) : Expr.expr =
| EInj _ -> failwith "[Z3 encoding] EInj unsupported"
| EMatch _ -> failwith "[Z3 encoding] EMatch unsupported"
| EArray _ -> failwith "[Z3 encoding] EArray unsupported"
| ELit l -> translate_lit ctx l
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported"
| EApp (head, args) -> (match Pos.unmark head with
| EApp (head, args) -> (
match Pos.unmark head with
| EOp op -> translate_op ctx op args
| _ -> failwith "[Z3 encoding] EApp of a non-operator unsupported"
)
| EAssert _ -> failwith "[Z3 encoding] EAssert unsupported"
| _ -> failwith "[Z3 encoding] EApp of a non-operator unsupported")
| EAssert _ -> failwith "[Z3 encoding] EAssert unsupported"
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EIfThenElse (e_if, e_then, e_else) ->
(* Encode this as (e_if ==> e_then) /\ (not e_if ==> e_else) *)
let z3_if = translate_expr ctx e_if in
Boolean.mk_and ctx [
Boolean.mk_implies ctx z3_if (translate_expr ctx e_then);
Boolean.mk_implies ctx (Boolean.mk_not ctx z3_if) (translate_expr ctx e_else)
]
Boolean.mk_and ctx
[
Boolean.mk_implies ctx z3_if (translate_expr ctx e_then);
Boolean.mk_implies ctx (Boolean.mk_not ctx z3_if) (translate_expr ctx e_else);
]
| ErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
(** [solve_vc] is the main entry point of this module.
It takes a list of expressions [vcs] corresponding to verification conditions
that must be discharged by Z3, and attempts to solve them **)
(** [solve_vc] is the main entry point of this module. It takes a list of expressions [vcs]
corresponding to verification conditions that must be discharged by Z3, and attempts to solve
them **)
let solve_vc (vcs : expr Pos.marked list) : unit =
Printf.printf "Running Z3 version %s\n" Version.to_string ;
Printf.printf "Running Z3 version %s\n" Version.to_string;
let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let cfg = [ ("model", "true"); ("proof", "false") ] in
let ctx = mk_context cfg in
let solver = Solver.mk_solver ctx None in
@ -155,9 +136,7 @@ let solve_vc (vcs : expr Pos.marked list) : unit =
Solver.add solver z3_vcs;
if (Solver.check solver []) = SATISFIABLE then
Printf.printf "Success: Empty unreachable\n"
if Solver.check solver [] = SATISFIABLE then Printf.printf "Success: Empty unreachable\n"
else
(* TODO: Print model as error message for Catala debugging purposes *)
Printf.printf "Failure: Empty reachable\n"