SmtSolver.h

 
#pragma once
 
#include <string>
 
#include "dlinear/solver/Context.h"
#include "dlinear/solver/SmtSolverOutput.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Config.h"
 
namespace dlinear {
 
class SmtSolver {
 public:
  explicit SmtSolver(Config config = Config{});
  explicit SmtSolver(const std::string &filename);
  SmtSolver(const SmtSolver &) = delete;
  SmtSolver(SmtSolver &&) noexcept = default;
  SmtSolver &operator=(const SmtSolver &) = delete;
  SmtSolver &operator=(SmtSolver &&) = delete;
 
  [[nodiscard]] std::string GetInfo(const std::string &key) const;
  [[nodiscard]] std::string GetOption(const std::string &key) const;
  [[nodiscard]] SmtResult GetExpected() const;
 
  void Assert(const Formula &f);
 
  const SmtSolverOutput &Parse();
 
  const SmtSolverOutput &Parse(const std::string &filename);
 
  const SmtSolverOutput &CheckSat();
 
  [[nodiscard]] bool Verify(const Box &model) const;
 
 private:
  bool ParseInput();
 
  Config config_;           
  SmtSolverOutput output_;  
  Context context_;         
};
 
}  // namespace dlinear