DeltaQsoptexTheorySolver.h

 
#pragma once
 
#ifndef DLINEAR_ENABLED_QSOPTEX
#error QSopt_ex is not enabled. Please enable it by adding "--//tools:enable_qsoptex" to the bazel command.
#endif
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/QsoptexTheorySolver.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Config.h"
 
namespace dlinear {
 
class DeltaQsoptexTheorySolver : public QsoptexTheorySolver {
 public:
  explicit DeltaQsoptexTheorySolver(PredicateAbstractor& predicate_abstractor,
                                    const std::string& class_name = "DeltaQsoptexTheorySolver");
 
  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 EnableQsxRow(int spx_row, bool truth) override;
};
 
}  // namespace dlinear