DeltaSoplexTheorySolver.h

 
#pragma once
 
#include <string>
 
#ifndef DLINEAR_ENABLED_SOPLEX
#error SoPlex is not enabled. Please enable it by adding "--//tools:enable_soplex" to the bazel command.
#endif
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/solver/SoplexTheorySolver.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/util/Box.h"
 
namespace dlinear {
 
class DeltaSoplexTheorySolver : public SoplexTheorySolver {
 public:
  explicit DeltaSoplexTheorySolver(PredicateAbstractor& predicate_abstractor,
                                   const std::string& class_name = "DeltaSoplexTheorySolver");
 
  Explanations EnableLiteral(const Literal& lit) override;
 
  void AddLiteral(const Variable& formula_var, const Formula& formula) override;
 
  SatResult CheckSatCore(mpq_class* actual_precision, Explanations& explanations) override;
 
 private:
  void EnableSpxRow(int spx_row, bool truth) override;
};
 
}  // namespace dlinear