package catala

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Z3backend.IoSource

Sourceval init_backend : unit -> unit
Sourcetype backend_context
Sourcetype vc_encoding
Sourcetype model
Sourcetype vc_encoding_result =
  1. | Success of vc_encoding * backend_context
  2. | Fail of string
Sourceval print_negative_result : Conditions.verification_condition -> backend_context -> model option -> string

encode_and_check_vc spawns a new Z3 solver and tries to solve the expression vc. Returns true if the vs was proven true and false otherwise. *

OCaml

Innovation. Community. Security.