Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
122
Issues
122
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
0d0a403d
Commit
0d0a403d
authored
Apr 26, 2010
by
Francois Bobot
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Un peu de documentation
parent
50f410a8
Changes
11
Hide whitespace changes
Inline
Side-by-side
Showing
11 changed files
with
86 additions
and
16 deletions
+86
-16
src/driver/call_provers.mli
src/driver/call_provers.mli
+25
-6
src/driver/driver.mli
src/driver/driver.mli
+1
-1
src/driver/prover.mli
src/driver/prover.mli
+2
-0
src/driver/register.mli
src/driver/register.mli
+8
-7
src/driver/whyconf.mli
src/driver/whyconf.mli
+2
-0
src/transform/encoding_decorate.mli
src/transform/encoding_decorate.mli
+4
-0
src/transform/split_conjunction.mli
src/transform/split_conjunction.mli
+35
-0
src/util/hashcons.mli
src/util/hashcons.mli
+2
-0
src/util/hashweak.mli
src/util/hashweak.mli
+2
-0
src/util/rc.mli
src/util/rc.mli
+3
-2
src/util/util.mli
src/util/util.mli
+2
-0
No files found.
src/driver/call_provers.mli
View file @
0d0a403d
...
...
@@ -17,22 +17,39 @@
(* *)
(**************************************************************************)
(** Call provers and parse there outputs *)
type
prover_answer
=
|
Valid
|
Invalid
|
Timeout
|
Unknown
of
string
|
Valid
(** The task is valid according to the prover *)
|
Invalid
(** The task is invalid *)
|
Timeout
(** the task timeout, ie it takes more time than specified*)
|
Unknown
of
string
(** The prover can't determined the validity or not of the task *)
|
Failure
of
string
|
HighFailure
(** The prover report a failure *)
|
HighFailure
(** An error occured during the call to the prover or none of
the given regexp match the output of the prover *)
type
prover_result
=
{
pr_answer
:
prover_answer
;
(* The answer of the prover on the given task*)
pr_output
:
string
;
(* The output of the prover currently stderr and stdout *)
pr_time
:
float
;
(* The time taken by the prover *)
}
val
print_prover_answer
:
Format
.
formatter
->
prover_answer
->
unit
(** Pretty-print a {! prover_answer} *)
val
print_prover_result
:
Format
.
formatter
->
prover_result
->
unit
(** Pretty-print a prover_result. The answer and the time are output.
The output of the prover is printed if and only if the answer is an
[HighFailure] *)
val
call_on_buffer
:
?
debug
:
bool
->
...
...
@@ -44,4 +61,6 @@ val call_on_buffer :
filename
:
string
->
Buffer
.
t
->
unit
->
prover_result
(** Call a prover on the task printed in the {!type: Buffer.t} given.
@param debug : set the debug flag.
Print on stderr the commandline called and the output of the prover. *)
src/driver/driver.mli
View file @
0d0a403d
...
...
@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
(**
Drivers for calling external pro
vers *)
(**
Manage Why dri
vers *)
open
Format
open
Util
...
...
src/driver/prover.mli
View file @
0d0a403d
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Apply printers and registered transformations mentionned in drivers *)
val
print_task
:
Driver
.
driver
->
Format
.
formatter
->
Task
.
task
->
unit
val
prove_task
:
...
...
src/driver/register.mli
View file @
0d0a403d
...
...
@@ -119,16 +119,17 @@ val catch_unsupportedtype : (Ty.ty -> 'a) -> (Ty.ty -> 'a)
(** [catch_unsupportedtype f] return a function which applied on [arg] :
- return [f arg] if [f arg] doesn't raise the {!
Unsupported} exception.
- raise [unsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)
- raise [Error (unsupportedType (arg,s))] if [f arg]
raises [Unsupported s]*)
val
catch_unsupportedterm
:
(
Term
.
term
->
'
a
)
->
(
Term
.
term
->
'
a
)
(** same as {! catch_unsupportedtype} but raise {!
UnsupportedExpression} instead of {! UnsupportedType}
*)
(** same as {! catch_unsupportedtype} but use [UnsupportedExpression]
instead of [UnsupportedType]
*)
val
catch_unsupportedfmla
:
(
Term
.
fmla
->
'
a
)
->
(
Term
.
fmla
->
'
a
)
(** same as {! catch_unsupportedtype} but raise {!
UnsupportedExpression} instead of {! UnsupportedType}
*)
(** same as {! catch_unsupportedtype} but use [UnsupportedExpression]
instead of [UnsupportedType]
*)
val
catch_unsupportedDeclaration
:
(
Decl
.
decl
->
'
a
)
->
(
Decl
.
decl
->
'
a
)
(** same as {! catch_unsupportedtype} but
raise {!
UnsupportedDeclaration} instead of {! UnsupportedType}
*)
(** same as {! catch_unsupportedtype} but
use
[UnsupportedDeclaration] instead of [UnsupportedType]
*)
src/driver/whyconf.mli
View file @
0d0a403d
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Manage the config file of Why *)
open
Util
type
config_prover
=
{
...
...
src/transform/encoding_decorate.mli
View file @
0d0a403d
...
...
@@ -17,3 +17,7 @@
(* *)
(**************************************************************************)
(** A transformation between polymorphic logic and multi-sorted logic*)
(** {{:http://www.lri.fr/~lescuyer/pdf/CADE-CL07.ps}
Handling Polymorphism in Automated Deduction}.
Jean-Francois Couchot et Stephane Lescuyer *)
src/transform/split_conjunction.mli
0 → 100644
View file @
0d0a403d
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** Move the conjunctions to top level and split the axiom or goal *)
val
split_pos_goal
:
Task
.
task
Register
.
tlist_reg
val
split_pos_neg_goal
:
Task
.
task
Register
.
tlist_reg
val
split_pos_axiom
:
Task
.
task
Register
.
tlist_reg
val
split_pos_neg_axiom
:
Task
.
task
Register
.
tlist_reg
val
split_pos_all
:
Task
.
task
Register
.
tlist_reg
val
split_pos_neg_all
:
Task
.
task
Register
.
tlist_reg
(** naming convention :
- pos : move the conjuctions in positive sub-formula to top level
- pos : move the conjuctions in negative sub-formula to top level
- goal : apply the transformation only to goal
- axiom : apply the transformation only to axioms
- all : apply the transformation to goal and axioms *)
src/util/hashcons.mli
View file @
0d0a403d
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Hash tables for hash consing *)
(*s Hash tables for hash consing.
Hash consed values are of the
...
...
src/util/hashweak.mli
View file @
0d0a403d
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Hashtable with weak key used for memoization *)
module
type
S
=
sig
type
key
...
...
src/util/rc.mli
View file @
0d0a403d
...
...
@@ -25,6 +25,7 @@
(* *)
(**************************************************************************)
(** Parse rc files *)
type
rc_value
=
|
RCint
of
int
...
...
@@ -44,8 +45,8 @@ val string : rc_value -> string
val
from_file
:
string
->
(
string
list
*
(
string
*
rc_value
)
list
)
list
(** returns the records of the file [f]
@raise
s
Not_found is f does not exists
@raise
s
Failure "lexing" in case of incorrect syntax *)
@raise Not_found is f does not exists
@raise Failure "lexing" in case of incorrect syntax *)
val
get_home_dir
:
unit
->
string
(** returns the home dir of the user *)
...
...
src/util/util.mli
View file @
0d0a403d
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Useful functions *)
(* useful option combinators *)
val
of_option
:
'
a
option
->
'
a
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment