Driver.h

 
#pragma once
 
#include <iosfwd>
#include <string>
 
#include "dlinear/solver/Context.h"
#include "dlinear/solver/Logic.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Stats.h"
#include "dlinear/util/Timer.h"
 
namespace dlinear {
 
class Driver {
 public:
  explicit Driver(Context &context, const std::string &class_name = "Driver");
  virtual ~Driver() = default;
 
  bool ParseStream(std::istream &in, const std::string &sname = "stream input");
 
  bool ParseString(const std::string &input, const std::string &sname = "string stream");
 
  virtual bool ParseFile(const std::string &filename);
 
  static void Error(const std::string &m);
 
  void Push(int n) { context_.Push(n); }
  void Pop(int n) { context_.Pop(n); }
 
  void Assert(const Formula &f) { context_.Assert(f); }
 
  void CheckSat();
 
  void GetModel();
 
  void GetAssertions() const;
 
  void GetOption(const std::string &key) const;
 
  void GetInfo(const std::string &key) const;
  void SetInfo(const std::string &key, const std::string &value) { context_.SetInfo(key, value); }
  void SetOption(const std::string &key, const std::string &value) { context_.SetOption(key, value); }
  void SetLogic(const Logic logic) { context_.SetLogic(logic); }
 
  void Maximize(const Expression &f);
 
  void Minimize(const Expression &f);
 
  void Exit() { context_.Exit(); }
 
  [[nodiscard]] bool trace_scanning() const { return debug_scanning_; }
  [[nodiscard]] bool trace_parsing() const { return debug_parsing_; }
  [[nodiscard]] const Context &context() const { return context_; }
  [[nodiscard]] const std::string &stream_name() const { return stream_name_; }
  std::string &m_stream_name() { return stream_name_; }
 
  [[nodiscard]] const Stats &stats() const { return stats_; }
 
 protected:
  virtual bool ParseStreamCore(std::istream &in) = 0;
 
  std::string stream_name_;  
 
  Context &context_;  
 
  bool debug_scanning_{false};  
 
  bool debug_parsing_{false};  
 
  Stats stats_;   
  Timer *timer_;  
};
 
}  // namespace dlinear