8#include "dlinear/util/exception.h"
25 DLINEAR_RUNTIME_ERROR_FMT(
"{} is not one of [Real, Int, Bool, Binary].", s);
28std::ostream &operator<<(std::ostream &os,
const Sort &sort) {
37 return os <<
"Binary";
39 DLINEAR_UNREACHABLE();
54 DLINEAR_UNREACHABLE();
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.
Variable::Type SortToType(Sort sort)
Convert a sort to a variable type.
Sort ParseSort(const std::string &s)
Parse a string to a sort.