Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
caisar
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
caisar
Commits
e6323e2e
Commit
e6323e2e
authored
2 weeks ago
by
Michele Alberti
Browse files
Options
Downloads
Patches
Plain Diff
Rework answer API.
parent
df6536db
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
src/verification.ml
+1
-1
1 addition, 1 deletion
src/verification.ml
src/verification_types.ml
+7
-9
7 additions, 9 deletions
src/verification_types.ml
src/verification_types.mli
+2
-2
2 additions, 2 deletions
src/verification_types.mli
with
10 additions
and
12 deletions
src/verification.ml
+
1
−
1
View file @
e6323e2e
...
...
@@ -515,7 +515,7 @@ let verify ?format query =
call_prover
~
cwd
~
limit
main
env
query
.
prover
config_prover
driver
?
dataset
definitions
task
in
Verification_types
.
Answer
.
make
~
parent_query
:
(
Some
query
)
answer
)
Verification_types
.
Answer
.
make
~
query
answer
)
tasks
)
mstr_theory
in
...
...
This diff is collapsed.
Click to expand it.
src/verification_types.ml
+
7
−
9
View file @
e6323e2e
...
...
@@ -108,7 +108,7 @@ module Query = struct
let
make
~
loadpath
?
memlimit
?
timelimit
?
onnx_out_dir
?
dataset
prover
?
prover_altern
problem
=
let
id
=
"
caisar_verification_
query"
in
let
id
=
"query"
in
let
id
=
Int
.
incr
id_int
;
id
^
Int
.
to_string
!
id_int
...
...
@@ -164,7 +164,6 @@ module Query = struct
JSON file@]"
))
|
Some
_
as
output_file
->
{
query
with
output_file
}
let
get_id
t
=
t
.
id
let
pretty
fmt
=
Fmt
.
fmt
"%a"
fmt
pp
end
...
...
@@ -175,6 +174,7 @@ module Answer = struct
type
t
=
{
id
:
string
;
query_id
:
string
;
problem_answer
:
problem_answer
;
}
[
@@
deriving
to_yojson
,
show
]
...
...
@@ -207,16 +207,14 @@ module Answer = struct
}
[
@@
deriving
to_yojson
,
show
]
let
make
~
(
parent_query
:
Query
.
t
option
)
p
=
let
parent_query_id
=
Option
.
value
~
default
:
""
@@
Option
.
map
~
f
:
Query
.
get_id
parent_query
in
let
id
=
"caisar_verification_answer"
in
let
make
~
(
query
:
Query
.
t
)
problem_answer
=
let
id
=
"answer"
in
let
id
=
Int
.
incr
id_int
;
id
^
Int
.
to_string
!
id_int
^
parent_query_id
id
^
Int
.
to_string
!
id_int
in
{
id
;
problem_answer
=
p
}
let
query_id
=
query
.
id
in
{
id
;
query_id
;
problem_answer
}
let
pretty
fmt
=
Fmt
.
fmt
"%a"
fmt
pp
end
This diff is collapsed.
Click to expand it.
src/verification_types.mli
+
2
−
2
View file @
e6323e2e
...
...
@@ -112,7 +112,6 @@ module Query : sig
@param timelimit is the timeout granted to the verification.
@param outfile is the output file to store the result of the query. *)
val
get_id
:
t
->
string
val
memlimit_of_string
:
string
->
int
(* TO BE REMOVED *)
val
timelimit_of_string
:
string
->
int
(* TO BE REMOVED *)
end
...
...
@@ -121,6 +120,7 @@ end
module
Answer
:
sig
type
t
=
private
{
id
:
string
;
query_id
:
string
;
problem_answer
:
problem_answer
;
}
[
@@
deriving
to_yojson
,
show
]
...
...
@@ -152,6 +152,6 @@ module Answer : sig
}
[
@@
deriving
to_yojson
,
show
]
val
make
:
parent_
query
:
Query
.
t
option
->
problem_answer
->
t
val
make
:
query
:
Query
.
t
->
problem_answer
->
t
val
pretty
:
Format
.
formatter
->
t
->
unit
end
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment