dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
Sort.cpp
1
6#include "Sort.h"
7
8#include "dlinear/util/exception.h"
9
10namespace dlinear::smt2 {
11
12Sort ParseSort(const std::string &s) {
13 if (s == "Real") {
14 return Sort::Real;
15 }
16 if (s == "Int") {
17 return Sort::Int;
18 }
19 if (s == "Bool") {
20 return Sort::Bool;
21 }
22 if (s == "Binary") {
23 return Sort::Binary;
24 }
25 DLINEAR_RUNTIME_ERROR_FMT("{} is not one of [Real, Int, Bool, Binary].", s);
26}
27
28std::ostream &operator<<(std::ostream &os, const Sort &sort) {
29 switch (sort) {
30 case Sort::Bool:
31 return os << "Bool";
32 case Sort::Int:
33 return os << "Int";
34 case Sort::Real:
35 return os << "Real";
36 case Sort::Binary:
37 return os << "Binary";
38 default:
39 DLINEAR_UNREACHABLE();
40 }
41}
42
44 switch (sort) {
45 case Sort::Binary:
47 case Sort::Bool:
49 case Sort::Int:
51 case Sort::Real:
53 }
54 DLINEAR_UNREACHABLE();
55}
56
57} // namespace dlinear::smt2
Type
Supported types of symbolic variables.
@ INTEGER
An INTEGER variable takes an int value.
@ BINARY
A BINARY variable takes an integer value from {0, 1}.
@ CONTINUOUS
A CONTINUOUS variable takes a mpq_class value.
@ BOOLEAN
A BOOLEAN variable takes a bool value.
Namespace for the SMT2 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.
Variable::Type SortToType(Sort sort)
Convert a sort to a variable type.
Definition Sort.cpp:43
Sort ParseSort(const std::string &s)
Parse a string to a sort.
Definition Sort.cpp:12