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

Fix encoding of hypotheses into Z3

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-03-16 11:20:20 +01:00
parent f6ad6bbd2f
commit fb6c18763f
2 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/verification/io.ml
View File

@ -171,7 +171,7 @@ module MakeBackendIO (B : Backend) = struct
match z3_vc with
| Success (encoding, backend_ctx) -> (
Cli.debug_print "The translation to Z3 is the following:@\n%s"
Cli.debug_print "The translation to Z3 is the following:\n%s"
(B.print_encoding encoding);
match B.solve_vc_encoding backend_ctx encoding with
| ProvenTrue -> Cli.result_print "%s" (print_positive_result vc)

11
compiler/verification/z3backend.real.ml
View File

@ -777,11 +777,12 @@ module Backend = struct
let solve_vc_encoding (ctx : backend_context) (encoding : vc_encoding) :
solver_result =
let solver = Z3.Solver.mk_solver ctx.ctx_z3 None in
(* Add all the constraints stored in the context *)
let encoding =
Boolean.mk_and ctx.ctx_z3 (encoding :: ctx.ctx_z3constraints)
in
Z3.Solver.add solver [ Boolean.mk_not ctx.ctx_z3 encoding ];
(* We take the negation of the query to check for possible
counterexamples *)
let query = Boolean.mk_not ctx.ctx_z3 encoding in
(* Add all the hypotheses stored in the context *)
let query_and_hyps = query :: ctx.ctx_z3constraints in
Z3.Solver.add solver query_and_hyps;
match Z3.Solver.check solver [] with
| UNSATISFIABLE -> ProvenTrue
| SATISFIABLE -> ProvenFalse (Z3.Solver.get_model solver)