SatSolver.h

 
#pragma once
 
#include <cstddef>
#include <map>
#include <optional>
#include <set>
#include <string>
#include <vector>
 
#include "dlinear/symbolic/PlaistedGreenbaumCnfizer.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
#include "dlinear/util/Config.h"
#include "dlinear/util/ScopedUnorderedMap.hpp"
#include "dlinear/util/ScopedUnorderedSet.hpp"
#include "dlinear/util/Stats.h"
 
namespace dlinear {
 
class SatSolver {
 public:
  explicit SatSolver(PredicateAbstractor &predicate_abstractor, const std::string &class_name = "SatSolver");
  virtual ~SatSolver() = default;
 
  virtual void Push() = 0;
  virtual void Pop() = 0;
  void AddFormula(const Formula &f);
  void AddFormulas(const std::vector<Formula> &formulas);
  void AddClause(const Formula &f);
  void AddClauses(const std::vector<Formula> &formulas);
  virtual void AddLearnedClause(const LiteralSet &literals) = 0;
  virtual void AddLearnedClause(const Literal &literals) = 0;
  LiteralSet FixedTheoryLiterals();
  virtual void FixedTheoryLiterals(LiteralSet &fixed_literals) = 0;
 
  void Assume(const LiteralSet &literals);
  virtual void Assume(const Literal &lit) = 0;
 
  void MarkAsCnfVariable(const Variable &var);
 
  virtual std::optional<Model> CheckSat() = 0;
  [[nodiscard]] const IterationStats &stats() const { return stats_; }
  [[nodiscard]] const IterationStats &cnfizer_stats() const;
  [[nodiscard]] const PredicateAbstractor &predicate_abstractor() const { return predicate_abstractor_; }
 
  [[nodiscard]] std::vector<std::vector<Literal>> clauses() const;
 
 protected:
  virtual void AddClauseToSat(const Formula &f) = 0;
  virtual void MakeSatVar(const Variable &var) = 0;
  void AddLiteral(const Formula &f);
  virtual void AddLiteral(const Literal &l, bool learned) = 0;
  virtual std::set<int> GetMainActiveLiterals() = 0;
  void GetMainActiveLiterals(std::set<int> &lits) const;
  Model OnSatResult();
  void UpdateLookup(int lit);
 
  const Config &config_;  
 
  // Data to help with removing literals that are only required by learned clauses.
  std::vector<int> main_clauses_copy_;  
  std::map<int, std::set<std::size_t>> main_clause_lookup_;  
  std::size_t cur_clause_start_;                             
 
  ScopedUnorderedMap<Variable::Id, int> var_to_sat_;  
  ScopedUnorderedMap<int, Variable> sat_to_var_;      
  ScopedUnorderedSet<Variable::Id>
      cnf_variables_;  
 
  PlaistedGreenbaumCnfizer cnfizer_;           
  PredicateAbstractor &predicate_abstractor_;  
 
  IterationStats stats_;  
};
 
}  // namespace dlinear