dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
Sort.h
1
8#pragma once
9
10#include <ostream>
11#include <string>
12
13#include "dlinear/symbolic/literal.h"
14
15namespace dlinear::vnnlib {
16
18enum class Sort {
19 Binary,
20 Bool,
21 Int,
22 Real,
23};
24
30Sort ParseSort(const std::string &s);
43
44std::ostream &operator<<(std::ostream &os, const Sort &sort);
45
46} // namespace dlinear::vnnlib
47
48#ifdef DLINEAR_INCLUDE_FMT
49
50#include "dlinear/util/logging.h"
51
52OSTREAM_FORMATTER(dlinear::vnnlib::Sort)
53
54#endif
Type
Supported types of symbolic variables.
Namespace for the VNNLIB parser of the dlinear library.
Definition Driver.cpp:17
Sort
Sort of a term.
Definition Sort.h:18
@ Int
Integer sort.
@ Binary
Binary sort.
@ Bool
Boolean sort.
Sort ParseSort(const std::string &s)
Parse a string to a sort.
Definition Sort.cpp:12
Variable::Type SortToType(Sort sort)
Convert a sort to a variable type.
Definition Sort.cpp:43