Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Mathias Preiner, Liana Hadarean, Dejan Jovanovic
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * SAT Solver.
      14                 :            :  *
      15                 :            :  * Implementation of the minisat interface for cvc5.
      16                 :            :  */
      17                 :            : 
      18                 :            : #pragma once
      19                 :            : 
      20                 :            : #include "prop/minisat/simp/SimpSolver.h"
      21                 :            : #include "prop/sat_solver.h"
      22                 :            : #include "smt/env_obj.h"
      23                 :            : #include "util/statistics_registry.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : 
      27                 :            : template <class Solver>
      28                 :            : prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
      29                 :            : 
      30                 :            : template <class Solver>
      31                 :            : void toSatClause(const typename Solver::TClause& minisat_cl,
      32                 :            :                  prop::SatClause& sat_cl);
      33                 :            : 
      34                 :            : namespace prop {
      35                 :            : 
      36                 :            : class MinisatSatSolver : public CDCLTSatSolver, protected EnvObj
      37                 :            : {
      38                 :            :  public:
      39                 :            :   MinisatSatSolver(Env& env, StatisticsRegistry& registry);
      40                 :            :   ~MinisatSatSolver() override;
      41                 :            : 
      42                 :            :   static SatVariable     toSatVariable(Minisat::Var var);
      43                 :            :   static Minisat::Lit    toMinisatLit(SatLiteral lit);
      44                 :            :   static SatLiteral      toSatLiteral(Minisat::Lit lit);
      45                 :            :   static SatValue        toSatLiteralValue(Minisat::lbool res);
      46                 :            :   static Minisat::lbool  toMinisatlbool(SatValue val);
      47                 :            :   //(Commented because not in use) static bool            tobool(SatValue val);
      48                 :            : 
      49                 :            :   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
      50                 :            :   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
      51                 :            :   void initialize(context::Context* context,
      52                 :            :                   TheoryProxy* theoryProxy,
      53                 :            :                   context::UserContext* userContext,
      54                 :            :                   PropPfManager* ppm) override;
      55                 :            : 
      56                 :            :   ClauseId addClause(SatClause& clause, bool removable) override;
      57                 :          0 :   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
      58                 :            :   {
      59                 :          0 :     Unreachable() << "Minisat does not support native XOR reasoning";
      60                 :            :   }
      61                 :            : 
      62                 :            :   SatVariable newVar(bool isTheoryAtom, bool canErase) override;
      63                 :      50395 :   SatVariable trueVar() override { return d_minisat->trueVar(); }
      64                 :      50395 :   SatVariable falseVar() override { return d_minisat->falseVar(); }
      65                 :            : 
      66                 :            :   SatValue solve() override;
      67                 :            :   SatValue solve(long unsigned int&) override;
      68                 :            :   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
      69                 :            :   void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override;
      70                 :            : 
      71                 :            :   bool ok() const override;
      72                 :            : 
      73                 :            :   void interrupt() override;
      74                 :            : 
      75                 :            :   SatValue value(SatLiteral l) override;
      76                 :            : 
      77                 :            :   SatValue modelValue(SatLiteral l) override;
      78                 :            : 
      79                 :            :   /** Incremental interface */
      80                 :            : 
      81                 :            :   uint32_t getAssertionLevel() const override;
      82                 :            : 
      83                 :            :   void push() override;
      84                 :            : 
      85                 :            :   void pop() override;
      86                 :            : 
      87                 :            :   void resetTrail() override;
      88                 :            : 
      89                 :            :   void preferPhase(SatLiteral lit) override;
      90                 :            : 
      91                 :            :   bool isDecision(SatVariable decn) const override;
      92                 :            : 
      93                 :            :   bool isFixed(SatVariable var) const override;
      94                 :            : 
      95                 :            :   /** Return the list of current list of decisions that have been made by the
      96                 :            :    * solver at the point when this function is called.
      97                 :            :    */
      98                 :            :   std::vector<SatLiteral> getDecisions() const override;
      99                 :            : 
     100                 :            :   /** Return the order heap.
     101                 :            :    */
     102                 :            :   std::vector<Node> getOrderHeap() const override;
     103                 :            : 
     104                 :            :   /** Retrieve a pointer to the underlying solver. */
     105                 :            :   Minisat::SimpSolver* getSolver() { return d_minisat; }
     106                 :            : 
     107                 :            :   /** Retrieve the refutation proof of this SAT solver. */
     108                 :            :   std::shared_ptr<ProofNode> getProof() override;
     109                 :            : 
     110                 :            :  private:
     111                 :            : 
     112                 :            :   /** The SatSolver used */
     113                 :            :   Minisat::SimpSolver* d_minisat;
     114                 :            : 
     115                 :            :   /** Context we will be using to synchronize the sat solver */
     116                 :            :   context::Context* d_context;
     117                 :            : 
     118                 :            :   /**
     119                 :            :    * Stores assumptions passed via last solve() call.
     120                 :            :    *
     121                 :            :    * It is used in getUnsatAssumptions() to determine which of the literals in
     122                 :            :    * the final conflict clause are assumptions.
     123                 :            :    */
     124                 :            :   std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions;
     125                 :            : 
     126                 :            :   void setupOptions();
     127                 :            : 
     128                 :            :   class Statistics {
     129                 :            :   private:
     130                 :            :    ReferenceStat<int64_t> d_statStarts, d_statDecisions;
     131                 :            :    ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations;
     132                 :            :    ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals;
     133                 :            :    ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals;
     134                 :            :    ReferenceStat<int64_t> d_statTotLiterals;
     135                 :            : 
     136                 :            :   public:
     137                 :            :    Statistics(StatisticsRegistry& registry);
     138                 :            :    void init(Minisat::SimpSolver* d_minisat);
     139                 :            :    void deinit();
     140                 :            :   };/* class MinisatSatSolver::Statistics */
     141                 :            :   Statistics d_statistics;
     142                 :            : 
     143                 :            : }; /* class MinisatSatSolver */
     144                 :            : 
     145                 :            : }  // namespace prop
     146                 :            : }  // namespace cvc5::internal