Context.h

 
#pragma once
 
#include <memory>
#include <string>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/Logic.h"
#include "dlinear/solver/LpResult.h"
#include "dlinear/solver/PiecewiseLinearConstraint.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/solver/SmtSolverOutput.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Config.h"
#include "dlinear/util/ScopedVector.hpp"
 
namespace dlinear {
 
class Context {
 public:
  explicit Context(Config &config, SmtSolverOutput * = nullptr);
  Context(const Context &context) = delete;
  Context(Context &&context) noexcept;
  Context &operator=(const Context &) = delete;
  Context &operator=(Context &&) = delete;
  ~Context();
 
  void Assert(const Formula &f);
  void AssertPiecewiseLinearFunction(const Variable &var, const Formula &cond, const Expression &active,
                                     const Expression &inactive);
 
  SatResult CheckSat(mpq_class *actual_precision);
  LpResult CheckOpt(mpq_class *obj_lo, mpq_class *obj_up);
 
  void DeclareVariable(const Variable &v, bool is_model_variable = true);
  void DeclareVariable(const Variable &v, const Expression &lb, const Expression &ub, bool is_model_variable = true);
 
  const PiecewiseLinearConstraint &AddGuidedConstraint(std::unique_ptr<PiecewiseLinearConstraint> &&constraint);
 
  void Exit();
 
  void Minimize(const Expression &f);
 
  void Maximize(const Expression &f);
 
  void Pop(int n);
  void Push(int n);
  void SetInfo(const std::string &key, const std::string &val);
  [[nodiscard]] std::string GetInfo(const std::string &key) const;
  void SetInterval(const Variable &v, const mpq_class &lb, const mpq_class &ub);
  void SetLogic(Logic logic);
  void SetOption(const std::string &key, const std::string &val);
  [[nodiscard]] std::string GetOption(const std::string &key) const;
 
  [[nodiscard]] const Config &config() const;
  [[nodiscard]] const ScopedVector<Formula> &assertions() const;
  [[nodiscard]] const Box &box() const;
  [[nodiscard]] const Box &model() const;
  [[nodiscard]] bool have_objective() const;
  [[nodiscard]] const SmtSolverOutput *solver_output() const;
  SmtSolverOutput *m_solver_output();
  const PredicateAbstractor &predicate_abstractor() const;
 
  [[nodiscard]] bool is_max() const;
 
  [[nodiscard]] bool Verify(const Box &model) const;
 
 private:
  class Impl;
 
  std::unique_ptr<Impl> impl_;  
};
 
}  // namespace dlinear