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
4710f0d5
Commit
4710f0d5
authored
2 years ago
by
Julien Girard-Satabin
Browse files
Options
Downloads
Patches
Plain Diff
[SAVer] Small change in SVM theory name.
parent
d36d26a3
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/language.ml
+2
-2
2 additions, 2 deletions
src/language.ml
tests/simple_ovo.t
+1
-1
1 addition, 1 deletion
tests/simple_ovo.t
with
3 additions
and
3 deletions
src/language.ml
+
2
−
2
View file @
4710f0d5
...
...
@@ -53,7 +53,7 @@ let register_svm_as_array nb_inputs nb_classes filename env =
let
svm_type
=
Ty
.
ty_app
Theory
.(
ns_find_ts
svm
.
mod_theory
.
th_export
[
"svm"
])
[]
in
let
id_as_array
=
Ident
.
id_fresh
"SVM
A
sArray"
in
let
id_as_array
=
Ident
.
id_fresh
"SVM
a
sArray"
in
let
th_uc
=
Pmodule
.
create_module
env
id_as_array
in
let
th_uc
=
Pmodule
.
use_export
th_uc
svm
in
let
ls_svm_apply
=
...
...
@@ -64,7 +64,7 @@ let register_svm_as_array nb_inputs nb_classes filename env =
Pmodule
.
add_pdecl
~
vc
:
false
th_uc
(
Pdecl
.
create_pure_decl
(
Decl
.
create_param_decl
ls_svm_apply
))
in
Wstdlib
.
Mstr
.
singleton
"SVM
A
sArray"
(
Pmodule
.
close_module
th_uc
)
Wstdlib
.
Mstr
.
singleton
"SVM
a
sArray"
(
Pmodule
.
close_module
th_uc
)
let
nnet_parser
env
_
filename
_
=
let
model
=
Nnet
.
parse
filename
in
...
...
This diff is collapsed.
Click to expand it.
tests/simple_ovo.t
+
1
−
1
View file @
4710f0d5
...
...
@@ -27,7 +27,7 @@ Test verify
$
caisar
verify
-
L
.
--
format
whyml
--
prover
=
SAVer
--
dataset
-
csv
=
test_data
.
csv
-
2
>&
1
<<
EOF
|
sed
'
s/\/tmp\/[a-z0-9_./]*/$TMPFILE/
'
>
theory
T
>
use
TestSVM
.
SVM
A
sArray
>
use
TestSVM
.
SVM
a
sArray
>
use
ieee_float
.
Float64
>
use
caisar
.
IOShape
>
use
caisar
.
SVM
...
...
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