Commit 456404e9 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

added more theories

parent 077fb951
......@@ -9,7 +9,7 @@
module Parser = Onnx_parser
module Onnxpiqi = Piqi_interface.Onnx_piqi
module IR = Ir.Nier_cfg
module SMT = Smt.Smtifyer
module SMT = Smtlib.Smtifyer
module P = Printf
module Arg = Arg
module F = Filename
......
(executables
(package ISAIEH)
(public_names converter)
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface ISAIEH.output.smt)
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface ISAIEH.output.smtlib)
)
(env
......
(executables
(names converter_static)
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface ISAIEH.output.smt)
(libraries ISAIEH.onnx_parser ISAIEH.piqi_interface
ISAIEH.output.smtlib)
(flags (-ccopt -static))
)
......
(library
(name smt)
(public_name ISAIEH.output.smt)
(name smtlib)
(public_name ISAIEH.output.smtlib)
(preprocess (pps ppx_inline_test))
(inline_tests)
(libraries ocplib-endian piqirun.pb zarith ocamlgraph ISAIEH.ir))
......
......@@ -24,7 +24,13 @@ module IR = Ir.Nier_cfg
(** {1 Definition of the supported theories
for SMTLIB2 output format} *)
type theory = Real_Theory | Float_Theory | Linear_Real_Theory
type theory =
| Real_Theory
| Float_Theory
| Linear_Real_Theory
| Quantifier_Free_Real_Theory
| Quantifier_Free_Linear_Theory
| Quantifier_Free_Float_Theory
(** {1 Environment utilities} *)
(** Environment stores shapes and raw data for all variables.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment