Sort.h

 
#pragma once
 
#include <ostream>
#include <string>
 
#include "dlinear/symbolic/literal.h"
 
namespace dlinear::smt2 {
 
enum class Sort {
  Binary,  
  Bool,    
  Int,     
  Real,    
};
 
Sort ParseSort(const std::string &s);
Variable::Type SortToType(Sort sort);
 
std::ostream &operator<<(std::ostream &os, const Sort &sort);
 
}  // namespace dlinear::smt2
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::smt2::Sort)
 
#endif