ContextImpl.h

 
#pragma once
 
#include <memory>
#include <optional>
#include <string>
#include <unordered_map>
#include <unordered_set>
#ifndef NDEBUG
#include <set>
#endif
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/Context.h"
#include "dlinear/solver/Logic.h"
#include "dlinear/solver/LpResult.h"
#include "dlinear/solver/PiecewiseLinearConstraint.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/solver/SatSolver.h"
#include "dlinear/solver/SmtSolverOutput.h"
#include "dlinear/solver/TheorySolver.h"
#include "dlinear/symbolic/IfThenElseEliminator.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::Impl {
 public:
  explicit Impl(Config &config, SmtSolverOutput *output = nullptr);
  Impl(const Impl &) = delete;
  Impl(Impl &&) = delete;
  Impl &operator=(const Impl &) = delete;
  Impl &operator=(Impl &&) = delete;
 
  void Assert(const Formula &f);
 
  void AssertPiecewiseLinearFunction(const Variable &var, const Formula &cond, const Expression &active,
                                     const Expression &inactive);
 
  const PiecewiseLinearConstraint &AddGuidedConstraint(std::unique_ptr<PiecewiseLinearConstraint> &&constraint);
 
  void Pop();
  void Push();
  SatResult CheckSat(mpq_class *precision);
  LpResult CheckOpt(mpq_class *obj_lo, mpq_class *obj_up);
  void DeclareVariable(const Variable &v, bool is_model_variable);
  void SetDomain(const Variable &v, const Expression &lb, const Expression &ub);
  void Minimize(const Expression &obj_function);
  void Maximize(const Expression &obj_function);
  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;
  const Config &config() const { return config_; }
  const ScopedVector<Formula> &assertions() const;
  Box &box() { return boxes_.last(); }
  const Box &box() const { return boxes_.last(); }
  const Box &get_model() { return model_; }
 
  const PredicateAbstractor &predicate_abstractor() const { return predicate_abstractor_; }
  [[nodiscard]] const SmtSolverOutput *solver_output() const { return output_; }
  SmtSolverOutput *m_solver_output() { return output_; }
  bool have_objective() const;
  bool is_max() const;
  [[nodiscard]] bool Verify(const Box &model) const;
 
 private:
  std::unique_ptr<TheorySolver> GetTheorySolver();
  std::unique_ptr<SatSolver> GetSatSolver();
 
  void AddToBox(const Variable &v);
 
  void LearnExplanation(const LiteralSet &explanation);
  void LearnExplanations(const TheorySolver::Explanations &explanations);
 
  SatResult CheckSatCore(mpq_class *actual_precision);
  LpResult CheckOptCore(mpq_class *obj_lo, mpq_class *obj_up);
 
  void MinimizeCore(const Expression &obj_expr);
 
  void MarkModelVariable(const Variable &v);
 
  bool IsModelVariable(const Variable &v) const;
 
  Box ExtractModel(const Box &box) const;
 
  void UpdateAndPrintOutput(SmtResult smt_result) const;
 
  Config &config_;                 
  SmtSolverOutput *const output_;  
 
  std::optional<Logic> logic_;  
  std::unordered_map<std::string, std::string> info_;    
  std::unordered_map<std::string, std::string> option_;  
 
  ScopedVector<Box> boxes_;                           
  ScopedVector<Formula> stack_;                       
  std::unordered_set<Variable::Id> model_variables_;  
 
  Box model_;  
 
  bool have_objective_;  
  bool is_max_;          
 
  std::vector<std::unique_ptr<PiecewiseLinearConstraint>>
      pl_constraints_;  
 
  PredicateAbstractor predicate_abstractor_;  
  IfThenElseEliminator ite_eliminator_;       
  // TODO: these could become templated classes for added efficiency
  const std::unique_ptr<SatSolver> sat_solver_;        
  const std::unique_ptr<TheorySolver> theory_solver_;  
 
#ifndef NDEBUG
  std::set<LiteralSet> explanations_so_far;  
#endif
};
 
}  // namespace dlinear