Up  

Module Rac.Why

module Why: sig .. end

RAC implementation using a Why3 transformation and prover

The RAC implementation is based on a Why3 transformation (usually compute_in_goal) and a Why3 prover. The procedure to decide (check) a term uses three steps, and terminates with the first step that gives a definitive answer (i.e. the term is valid or invalid) and progresses with the next if a step doesn't yield a definitive answer (the step is incomplete for the term).

  1. Apply the transformation. The term is valid (resp. invalid) if it is reduced to true (resp. false), and otherwise the step is incomplete.
  2. Apply the prover. The term is valid (resp. invalid) if the prover shows that it is valid (resp. invalid), and otherwise the step is incomplete.
  3. Apply the prover to the negation of the term. The term is valid (resp. invalid) if the prover shows that it is invalid (resp. valid), and otherwise the step, and hence the whole procedure, is incomplete.
type why_prover = {
   command : string;
   driver : Driver.driver;
   limit : Call_provers.resource_limit;
}

The configuration of the prover used for reducing terms in RAC

val mk_why_prover : command:string ->
       Driver.driver -> Call_provers.resource_limit -> why_prover
val mk_check_term : ?metas:(Theory.meta * Theory.meta_arg list) list ->
       ?trans:Task.task Trans.tlist ->
       ?why_prover:why_prover ->
       ?oracle_quant_var:Rac.oracle_quant_var ->
       config:Whyconf.config ->
       elim_eps:Task.task Trans.trans -> unit -> Pinterp_core.check_term

Metas are applied to all tasks, the tasks are first reduce using trans, and if this is insufficient for deciding the term, checked using why_prover. The oracle oracle_quant_var is used to instantiate variables in top-level universal quantifications during reduction with trans. By default, all arguments are empty or dummy.

val mk_check_term_lit : Whyconf.config ->
       Env.env ->
       ?metas:(string * string option) list ->
       ?trans:string ->
       ?why_prover:string ->
       ?oracle_quant_var:Rac.oracle_quant_var -> unit -> Pinterp_core.check_term

mk_rac_lit cnf env ?metas ?trans ?prover ?try_negate () configures the term reduction of RAC. trans is the name of a transformation ("compute_in_goal" by default). why_prover is a prover string with optional, space-sparated time limit and memory limit.

If the environment variable WHY3RACTASKDIR is set, it is used as a directory to print all SMT tasks sent to the RAC prover, if --debug=rac-check-term-sat is set.

val mk_compute_term : ?metas:(Theory.meta * Theory.meta_arg list) list ->
       ?trans:Task.task list Trans.trans ->
       ?oracle_quant_var:Rac.oracle_quant_var -> unit -> Pinterp_core.compute_term
val mk_compute_term_lit : Env.env ->
       ?metas:(string * string option) list ->
       ?trans:string ->
       ?oracle_quant_var:Rac.oracle_quant_var -> unit -> Pinterp_core.compute_term

Create a compute_term function. The transformation trans is "compute_in_goal" by default.