diff --git a/src/saver.ml b/src/saver.ml index 2c563a4653f18a4dc528ac88026511a7ca5f12a2..243f1561ef1b4669c8e4f1c5c2ed1103ba1ea1cf 100644 --- a/src/saver.ml +++ b/src/saver.ml @@ -32,7 +32,9 @@ type interpreted_task = { } let find_predicate_ls env p = - let dataset_th = Pmodule.read_module env [ "caisar" ] "DataSet" in + let dataset_th = + Pmodule.read_module env [ "caisar" ] "DataSetClassification" + in Theory.ns_find_ls dataset_th.mod_theory.th_export [ p ] let interpret_predicate env ls = diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw index 7d02870e52d7544f039668c12a11831cee08f8aa..302a893232ee5a50a230a7aeb536cd0055636c0a 100644 --- a/stdlib/caisar.mlw +++ b/stdlib/caisar.mlw @@ -38,7 +38,7 @@ theory Model function predict: model -> array t -> int end -theory DataSet +theory DataSetClassification use ieee_float.Float64 use int.Int use array.Array diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t index cd85182748a04e25c65b59def61e8e309345c49c..df79cd4207e880575e59b8298bfdcba05c6c6825 100644 --- a/tests/simple_ovo.t +++ b/tests/simple_ovo.t @@ -30,8 +30,7 @@ Test verify > use TestSVM.SVMasArray > use ieee_float.Float64 > use int.Int - > use array.Array - > use caisar.DataSet + > use caisar.DataSetClassification > > goal G: robust svm_apply dataset (8.0:t) > goal H: correct svm_apply dataset (8.0:t)