Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Dejan Jovanovic, Mathias Preiner, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__PROP__SAT_SOLVER_H
      19                 :            : #define CVC5__PROP__SAT_SOLVER_H
      20                 :            : 
      21                 :            : #include <string>
      22                 :            : 
      23                 :            : #include "context/cdlist.h"
      24                 :            : #include "context/context.h"
      25                 :            : #include "expr/node.h"
      26                 :            : #include "proof/clause_id.h"
      27                 :            : #include "prop/prop_proof_manager.h"
      28                 :            : #include "prop/sat_solver_types.h"
      29                 :            : #include "util/statistics_stats.h"
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : 
      33                 :            : namespace prop {
      34                 :            : 
      35                 :            : class SatProofManager;
      36                 :            : class TheoryProxy;
      37                 :            : 
      38                 :            : class SatSolver {
      39                 :            : 
      40                 :            : public:
      41                 :            : 
      42                 :            :   /** Virtual destructor */
      43                 :      91574 :   virtual ~SatSolver() { }
      44                 :            : 
      45                 :            :   /**
      46                 :            :    * Add clause to SAT solver.
      47                 :            :    * @param clause    The clause to add.
      48                 :            :    * @param removable True to indicate that this clause is not irredundant.
      49                 :            :    */
      50                 :            :   virtual ClauseId addClause(SatClause& clause,
      51                 :            :                              bool removable) = 0;
      52                 :            : 
      53                 :            :   /** Return true if the solver supports native xor resoning */
      54                 :          0 :   virtual bool nativeXor() { return false; }
      55                 :            : 
      56                 :            :   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
      57                 :            :   virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
      58                 :            : 
      59                 :            :   /**
      60                 :            :    * Create a new boolean variable in the solver.
      61                 :            :    * @param isTheoryAtom is this a theory atom that needs to be asserted to
      62                 :            :    * theory
      63                 :            :    * @param canErase whether the sat solver can safely eliminate this variable
      64                 :            :    *
      65                 :            :    */
      66                 :            :   virtual SatVariable newVar(bool isTheoryAtom, bool canErase) = 0;
      67                 :            : 
      68                 :            :   /**
      69                 :            :    * Create a new (or return an existing) boolean variable representing the
      70                 :            :    * constant true.
      71                 :            :    * @return The variable representing true.
      72                 :            :    */
      73                 :            :   virtual SatVariable trueVar() = 0;
      74                 :            : 
      75                 :            :   /**
      76                 :            :    * Create a new (or return an existing) boolean variable representing the
      77                 :            :    * constant false.
      78                 :            :    * @return The variable representing false.
      79                 :            :    */
      80                 :            :   virtual SatVariable falseVar() = 0;
      81                 :            : 
      82                 :            :   /** Check the satisfiability of the added clauses */
      83                 :            :   virtual SatValue solve() = 0;
      84                 :            : 
      85                 :            :   /** Check the satisfiability of the added clauses */
      86                 :            :   virtual SatValue solve(long unsigned int&) = 0;
      87                 :            : 
      88                 :            :   /** Check satisfiability under assumptions */
      89                 :          0 :   virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
      90                 :            :   {
      91                 :          0 :     Unimplemented() << "Solving under assumptions not implemented";
      92                 :            :     return SAT_VALUE_UNKNOWN;
      93                 :            :   };
      94                 :            : 
      95                 :            :   /**
      96                 :            :    * Tell SAT solver to only do propagation on next solve().
      97                 :            :    *
      98                 :            :    * @return true if feature is supported, otherwise false.
      99                 :            :    */
     100                 :          0 :   virtual bool setPropagateOnly() { return false; }
     101                 :            : 
     102                 :            :   /** Interrupt the solver */
     103                 :            :   virtual void interrupt() = 0;
     104                 :            : 
     105                 :            :   /** Call value() during the search.*/
     106                 :            :   virtual SatValue value(SatLiteral l) = 0;
     107                 :            : 
     108                 :            :   /** Call modelValue() when the search is done.*/
     109                 :            :   virtual SatValue modelValue(SatLiteral l) = 0;
     110                 :            : 
     111                 :            :   /** Get the current assertion level */
     112                 :            :   virtual uint32_t getAssertionLevel() const = 0;
     113                 :            : 
     114                 :            :   /** Check if the solver is in an inconsistent state */
     115                 :            :   virtual bool ok() const = 0;
     116                 :            : 
     117                 :            :   /**
     118                 :            :    * Get list of unsatisfiable assumptions.
     119                 :            :    *
     120                 :            :    * The returned assumptions are a subset of the assumptions provided to
     121                 :            :    * the solve method.
     122                 :            :    * Can only be called if satisfiability check under assumptions was used and
     123                 :            :    * if it returned SAT_VALUE_FALSE.
     124                 :            :    */
     125                 :          0 :   virtual void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions)
     126                 :            :   {
     127                 :          0 :     Unimplemented() << "getUnsatAssumptions not implemented";
     128                 :            :   }
     129                 :            : 
     130                 :            : };/* class SatSolver */
     131                 :            : 
     132                 :            : class CDCLTSatSolver : public SatSolver
     133                 :            : {
     134                 :            :  public:
     135                 :      91553 :   virtual ~CDCLTSatSolver(){};
     136                 :            : 
     137                 :            :   virtual void initialize(prop::TheoryProxy* theoryProxy,
     138                 :            :                           PropPfManager* ppm) = 0;
     139                 :            : 
     140                 :            :   virtual void push() = 0;
     141                 :            : 
     142                 :            :   virtual void pop() = 0;
     143                 :            : 
     144                 :            :   /**
     145                 :            :    * Reset the decisions in the DPLL(T) SAT solver at the current assertion
     146                 :            :    * level.
     147                 :            :    */
     148                 :            :   virtual void resetTrail() = 0;
     149                 :            : 
     150                 :            :   /**
     151                 :            :    * Configure the preferred phase for a decision literal.
     152                 :            :    *
     153                 :            :    * @note This phase is always enforced when the SAT solver decides to make a
     154                 :            :    *       decision on this variable on its own. If a decision is injected into
     155                 :            :    *       the SAT solver via TheoryProxy::getNextDecisionRequest(), the
     156                 :            :    *       preferred phase will only be considered if the decision was derived
     157                 :            :    *       by the decision engine. It will be ignored if the decision was
     158                 :            :    *       derived from a theory (the phase enforced by the theory overrides
     159                 :            :    *       the preferred phase).
     160                 :            :    *
     161                 :            :    * @param lit The literal.
     162                 :            :    */
     163                 :            :   virtual void preferPhase(SatLiteral lit) = 0;
     164                 :            : 
     165                 :            :   virtual bool isDecision(SatVariable decn) const = 0;
     166                 :            : 
     167                 :            :   /**
     168                 :            :    * Return whether variable has a fixed assignment.
     169                 :            :    */
     170                 :            :   virtual bool isFixed(SatVariable var) const = 0;
     171                 :            : 
     172                 :            :   /**
     173                 :            :    * Return the current list of decisions made by the SAT solver.
     174                 :            :    */
     175                 :            :   virtual std::vector<SatLiteral> getDecisions() const = 0;
     176                 :            : 
     177                 :            :   /**
     178                 :            :    * Return the order heap of the SAT solver, which is a priority queueue
     179                 :            :    * of literals ordered with respect to variable activity.
     180                 :            :    */
     181                 :            :   virtual std::vector<Node> getOrderHeap() const = 0;
     182                 :            : 
     183                 :            :   /**
     184                 :            :    * Get proof, which is used if option prop-proof-mode is PROOF.
     185                 :            :    * @return a complete proof computed by this SAT solver.
     186                 :            :    */
     187                 :            :   virtual std::shared_ptr<ProofNode> getProof() = 0;
     188                 :            : 
     189                 :            : }; /* class CDCLTSatSolver */
     190                 :            : 
     191                 :          0 : inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
     192                 :          0 :   out << lit.toString();
     193                 :          0 :   return out;
     194                 :            : }
     195                 :            : 
     196                 :          0 : inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
     197                 :          0 :   out << "clause:";
     198         [ -  - ]:          0 :   for(unsigned i = 0; i < clause.size(); ++i) {
     199                 :          0 :     out << " " << clause[i];
     200                 :            :   }
     201                 :          0 :   out << ";";
     202                 :          0 :   return out;
     203                 :            : }
     204                 :            : 
     205                 :          0 : inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
     206                 :          0 :   std::string str;
     207 [ -  - ][ -  - ]:          0 :   switch(val) {
     208                 :          0 :   case prop::SAT_VALUE_UNKNOWN:
     209                 :          0 :     str = "_";
     210                 :          0 :     break;
     211                 :          0 :   case prop::SAT_VALUE_TRUE:
     212                 :          0 :     str = "1";
     213                 :          0 :     break;
     214                 :          0 :   case prop::SAT_VALUE_FALSE:
     215                 :          0 :     str = "0";
     216                 :          0 :     break;
     217                 :          0 :   default:
     218                 :          0 :     str = "Error";
     219                 :          0 :     break;
     220                 :            :   }
     221                 :            : 
     222                 :          0 :   out << str;
     223                 :          0 :   return out;
     224                 :            : }
     225                 :            : 
     226                 :            : }  // namespace prop
     227                 :            : }  // namespace cvc5::internal
     228                 :            : 
     229                 :            : #endif /* CVC5__PROP__SAT_MODULE_H */