Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A Diophantine equation solver for the theory of arithmetic.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
      16                 :            : #define CVC5__THEORY__ARITH__DIO_SOLVER_H
      17                 :            : 
      18                 :            : #include <unordered_map>
      19                 :            : #include <utility>
      20                 :            : #include <vector>
      21                 :            : 
      22                 :            : #include "context/cdlist.h"
      23                 :            : #include "context/cdmaybe.h"
      24                 :            : #include "context/cdo.h"
      25                 :            : #include "context/cdqueue.h"
      26                 :            : #include "smt/env_obj.h"
      27                 :            : #include "theory/arith/linear/normal_form.h"
      28                 :            : #include "util/rational.h"
      29                 :            : #include "util/statistics_stats.h"
      30                 :            : 
      31                 :            : namespace cvc5::context {
      32                 :            : class Context;
      33                 :            : }
      34                 :            : namespace cvc5::internal {
      35                 :            : namespace theory {
      36                 :            : namespace arith::linear {
      37                 :            : 
      38                 :            : class DioSolver : protected EnvObj
      39                 :            : {
      40                 :            :  private:
      41                 :            :   typedef size_t TrailIndex;
      42                 :            :   typedef size_t InputConstraintIndex;
      43                 :            :   typedef size_t SubIndex;
      44                 :            : 
      45                 :            :   std::vector<Variable> d_proofVariablePool;
      46                 :            :   /** Sat context dependent. */
      47                 :            :   context::CDO<size_t> d_lastUsedProofVariable;
      48                 :            : 
      49                 :            :   /**
      50                 :            :    * The set of input constraints is stored in a CDList.
      51                 :            :    * Each constraint point to an element of the trail.
      52                 :            :    */
      53                 :            :   struct InputConstraint
      54                 :            :   {
      55                 :            :     Node d_reason;
      56                 :            :     TrailIndex d_trailPos;
      57                 :      43709 :     InputConstraint(Node reason, TrailIndex pos)
      58                 :      43709 :         : d_reason(reason), d_trailPos(pos)
      59                 :            :     {
      60                 :      43709 :     }
      61                 :            :   };
      62                 :            :   context::CDList<InputConstraint> d_inputConstraints;
      63                 :            : 
      64                 :            :   /**
      65                 :            :    * This is the next input constraint to handle.
      66                 :            :    */
      67                 :            :   context::CDO<size_t> d_nextInputConstraintToEnqueue;
      68                 :            : 
      69                 :            :   /**
      70                 :            :    * We maintain a map from the variables associated with proofs to an input
      71                 :            :    * constraint. These variables can then be used in polynomial manipulations.
      72                 :            :    */
      73                 :            :   typedef std::unordered_map<Node, InputConstraintIndex>
      74                 :            :       NodeToInputConstraintIndexMap;
      75                 :            :   NodeToInputConstraintIndexMap d_varToInputConstraintMap;
      76                 :            : 
      77                 :        791 :   Node proofVariableToReason(const Variable& v) const
      78                 :            :   {
      79 [ -  + ][ -  + ]:        791 :     Assert(d_varToInputConstraintMap.find(v.getNode())
                 [ -  - ]
      80                 :            :            != d_varToInputConstraintMap.end());
      81                 :            :     InputConstraintIndex pos =
      82                 :        791 :         (*(d_varToInputConstraintMap.find(v.getNode()))).second;
      83 [ -  + ][ -  + ]:        791 :     Assert(pos < d_inputConstraints.size());
                 [ -  - ]
      84                 :        791 :     return d_inputConstraints[pos].d_reason;
      85                 :            :   }
      86                 :            : 
      87                 :            :   /**
      88                 :            :    * The main work horse of the algorithm, the trail of constraints.
      89                 :            :    * Each constraint is a SumPair that implicitly represents an equality against
      90                 :            :    * 0. d_trail[i].d_eq = (+ c (+ [(* coeff var)])) representing (+ [(* coeff
      91                 :            :    * var)]) = -c Each constraint has a proof in terms of a linear combination of
      92                 :            :    * the input constraints. d_trail[i].d_proof
      93                 :            :    *
      94                 :            :    * Each Constraint also a monomial in d_eq.getPolynomial()
      95                 :            :    * of minimal absolute value by the coefficients.
      96                 :            :    * d_trail[i].d_minimalMonomial
      97                 :            :    *
      98                 :            :    * See Alberto's paper for how linear proofs are maintained for the abstract
      99                 :            :    * state machine in rules (7), (8) and (9).
     100                 :            :    */
     101                 :            :   struct Constraint
     102                 :            :   {
     103                 :            :     SumPair d_eq;
     104                 :            :     Polynomial d_proof;
     105                 :            :     Monomial d_minimalMonomial;
     106                 :     119499 :     Constraint(const SumPair& eq, const Polynomial& p)
     107                 :     119499 :         : d_eq(eq),
     108                 :     119499 :           d_proof(p),
     109                 :     119499 :           d_minimalMonomial(d_eq.getPolynomial().selectAbsMinimum())
     110                 :            :     {
     111                 :     119499 :     }
     112                 :            :   };
     113                 :            :   context::CDList<Constraint> d_trail;
     114                 :            : 
     115                 :            :   // /** Compare by d_minimal. */
     116                 :            :   // struct TrailMinimalCoefficientOrder {
     117                 :            :   //   const context::CDList<Constraint>& d_trail;
     118                 :            :   //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>&
     119                 :            :   //   trail):
     120                 :            :   //     d_trail(trail)
     121                 :            :   //   {}
     122                 :            : 
     123                 :            :   //   bool operator()(TrailIndex i, TrailIndex j){
     124                 :            :   //     return
     125                 :            :   //     d_trail[i].d_minimalMonomial.absLessThan(d_trail[j].d_minimalMonomial);
     126                 :            :   //   }
     127                 :            :   // };
     128                 :            : 
     129                 :            :   /**
     130                 :            :    * A substitution is stored as a constraint in the trail together with
     131                 :            :    * the variable to be eliminated, and a fresh variable if one was introduced.
     132                 :            :    * The variable d_subs[i].d_eliminated is substituted using the implicit
     133                 :            :    * equality in d_trail[d_subs[i].d_constraint]
     134                 :            :    *  - d_subs[i].d_eliminated is normalized to have coefficient -1 in
     135                 :            :    *    d_trail[d_subs[i].d_constraint].
     136                 :            :    *  - d_subs[i].d_fresh is either Node::null() or it is variable it is
     137                 :            :    * normalized to have coefficient 1 in d_trail[d_subs[i].d_constraint].
     138                 :            :    */
     139                 :            :   struct Substitution
     140                 :            :   {
     141                 :            :     Node d_fresh;
     142                 :            :     Variable d_eliminated;
     143                 :            :     TrailIndex d_constraint;
     144                 :      29203 :     Substitution(Node f, const Variable& e, TrailIndex c)
     145                 :      29203 :         : d_fresh(f), d_eliminated(e), d_constraint(c)
     146                 :            :     {
     147                 :      29203 :     }
     148                 :            :   };
     149                 :            :   context::CDList<Substitution> d_subs;
     150                 :            : 
     151                 :            :   /**
     152                 :            :    * This is the queue of constraints to be processed in the current context
     153                 :            :    * level. This is to be empty upon entering solver and cleared upon leaving
     154                 :            :    * the solver.
     155                 :            :    *
     156                 :            :    * All elements in currentF:
     157                 :            :    * - are fully substituted according to d_subs.
     158                 :            :    * - !isConstant().
     159                 :            :    * - If the element is (+ constant (+ [(* coeff var)] )), then the gcd(coeff)
     160                 :            :    * = 1
     161                 :            :    */
     162                 :            :   std::deque<TrailIndex> d_currentF;
     163                 :            :   context::CDList<TrailIndex> d_savedQueue;
     164                 :            :   context::CDO<size_t> d_savedQueueIndex;
     165                 :            :   context::CDMaybe<TrailIndex> d_conflictIndex;
     166                 :            : 
     167                 :            :   /**
     168                 :            :    * Drop derived constraints with a coefficient length larger than
     169                 :            :    * the maximum input constraints length than 2**MAX_GROWTH_RATE.
     170                 :            :    */
     171                 :            :   context::CDO<uint32_t> d_maxInputCoefficientLength;
     172                 :            :   static constexpr uint32_t MAX_GROWTH_RATE = 3;
     173                 :            : 
     174                 :            :   /** Returns true if the element on the trail should be dropped.*/
     175                 :            :   bool anyCoefficientExceedsMaximum(TrailIndex j) const;
     176                 :            : 
     177                 :            :   /**
     178                 :            :    * Is true if decomposeIndex has been used in this context.
     179                 :            :    */
     180                 :            :   context::CDO<bool> d_usedDecomposeIndex;
     181                 :            : 
     182                 :            :   context::CDO<SubIndex> d_lastPureSubstitution;
     183                 :            :   context::CDO<SubIndex> d_pureSubstitionIter;
     184                 :            : 
     185                 :            :   /**
     186                 :            :    * Decomposition lemma queue.
     187                 :            :    */
     188                 :            :   context::CDQueue<TrailIndex> d_decompositionLemmaQueue;
     189                 :            : 
     190                 :            :  public:
     191                 :            :   /** Construct a Diophantine equation solver with the given context. */
     192                 :            :   DioSolver(Env& env);
     193                 :            : 
     194                 :            :   /** Returns true if the substitutions use no new variables. */
     195                 :          0 :   bool hasMorePureSubstitutions() const
     196                 :            :   {
     197                 :          0 :     return d_pureSubstitionIter < d_lastPureSubstitution;
     198                 :            :   }
     199                 :            : 
     200                 :            :   Node nextPureSubstitution();
     201                 :            : 
     202                 :            :   /**
     203                 :            :    * Adds an equality to the queue of the DioSolver.
     204                 :            :    * orig is blamed in a conflict.
     205                 :            :    * orig can either be of the form (= p c) or (and ub lb).
     206                 :            :    * where ub is either (leq p c) or (not (> p [- c 1])), and
     207                 :            :    * where lb is either (geq p c) or (not (< p [+ c 1]))
     208                 :            :    *
     209                 :            :    * If eq cannot be used, this constraint is dropped.
     210                 :            :    */
     211                 :            :   void pushInputConstraint(const Comparison& eq, Node reason);
     212                 :            : 
     213                 :            :   /**
     214                 :            :    * Processes the queue looking for any conflict.
     215                 :            :    * If a conflict is found, this returns conflict.
     216                 :            :    * Otherwise, it returns null.
     217                 :            :    * The conflict is guarenteed to be over literals given in addEquality.
     218                 :            :    */
     219                 :            :   Node processEquationsForConflict();
     220                 :            : 
     221                 :            :   /**
     222                 :            :    * Processes the queue looking for an integer unsatisfiable cutting plane.
     223                 :            :    * If such a plane is found this returns an entailed plane using no
     224                 :            :    * fresh variables.
     225                 :            :    */
     226                 :            :   SumPair processEquationsForCut();
     227                 :            : 
     228                 :            :  private:
     229                 :            :   /** Returns true if the TrailIndex refers to a element in the trail. */
     230                 :      29456 :   bool inRange(TrailIndex i) const { return i < d_trail.size(); }
     231                 :            : 
     232                 :            :   Node columnGcdIsOne() const;
     233                 :            : 
     234                 :            :   /**
     235                 :            :    * Returns true if the context dependent flag for conflicts
     236                 :            :    * has been raised.
     237                 :            :    */
     238                 :     796555 :   bool inConflict() const { return d_conflictIndex.isSet(); }
     239                 :            : 
     240                 :            :   /** Raises a conflict at the index ti. */
     241                 :       2195 :   void raiseConflict(TrailIndex ti)
     242                 :            :   {
     243 [ -  + ][ -  + ]:       2195 :     Assert(!inConflict());
                 [ -  - ]
     244                 :       2195 :     d_conflictIndex.set(ti);
     245                 :       2195 :   }
     246                 :            : 
     247                 :            :   /** Returns the conflict index. */
     248                 :       2195 :   TrailIndex getConflictIndex() const
     249                 :            :   {
     250 [ -  + ][ -  + ]:       2195 :     Assert(inConflict());
                 [ -  - ]
     251                 :       2195 :     return d_conflictIndex.get();
     252                 :            :   }
     253                 :            : 
     254                 :            :   /**
     255                 :            :    * Allocates a "unique" proof variable.
     256                 :            :    * This variable is fresh with respect to the context.
     257                 :            :    * Returns index of the variable in d_variablePool;
     258                 :            :    */
     259                 :            :   size_t allocateProofVariable();
     260                 :            : 
     261                 :            :   /** Empties the unprocessed input constraints into the queue. */
     262                 :            :   void enqueueInputConstraints();
     263                 :            : 
     264                 :            :   /**
     265                 :            :    * Returns true if an input equality is in the map.
     266                 :            :    * This is expensive and is only for debug assertions.
     267                 :            :    */
     268                 :            :   bool debugEqualityInInputEquations(Node eq);
     269                 :            : 
     270                 :            :   /** Applies the substitution at subIndex to currentF. */
     271                 :            :   void subAndReduceCurrentFByIndex(SubIndex d_subIndex);
     272                 :            : 
     273                 :            :   /**
     274                 :            :    * Takes as input a TrailIndex i and an integer that divides d_trail[i].d_eq,
     275                 :            :    * and returns a TrailIndex j s.t. d_trail[j].d_eq = (1/g) d_trail[i].d_eq and
     276                 :            :    *   d_trail[j].d_proof = (1/g) d_trail[i].d_proof.
     277                 :            :    *
     278                 :            :    * g must be non-zero.
     279                 :            :    *
     280                 :            :    * This corresponds to an application of Alberto's rule (7).
     281                 :            :    */
     282                 :            :   TrailIndex scaleEqAtIndex(TrailIndex i, const Integer& g);
     283                 :            : 
     284                 :            :   /**
     285                 :            :    * Takes as input TrailIndex's i and j and Integer's q and r and a TrailIndex
     286                 :            :    * k s.t. d_trail[k].d_eq == d_trail[i].d_eq * q + d_trail[j].d_eq * r and
     287                 :            :    *   d_trail[k].d_proof == d_trail[i].d_proof * q + d_trail[j].d_proof * r
     288                 :            :    *
     289                 :            :    * This corresponds to an application of Alberto's rule (8).
     290                 :            :    */
     291                 :            :   TrailIndex combineEqAtIndexes(TrailIndex i,
     292                 :            :                                 const Integer& q,
     293                 :            :                                 TrailIndex j,
     294                 :            :                                 const Integer& r);
     295                 :            : 
     296                 :            :   /**
     297                 :            :    * Decomposes the equation at index ti of trail by the variable
     298                 :            :    * with the lowest coefficient.
     299                 :            :    * This corresponds to an application of Alberto's rule (9).
     300                 :            :    *
     301                 :            :    * Returns a pair of a SubIndex and a TrailIndex.
     302                 :            :    * The SubIndex is the index of a newly introduced substition.
     303                 :            :    */
     304                 :            :   std::pair<SubIndex, TrailIndex> decomposeIndex(TrailIndex ti);
     305                 :            : 
     306                 :            :   /** Solves the index at ti for the value in minimumMonomial. */
     307                 :            :   std::pair<SubIndex, TrailIndex> solveIndex(TrailIndex ti);
     308                 :            : 
     309                 :            :   /** Prints the queue for debugging purposes to Trace("arith::dio"). */
     310                 :            :   void printQueue();
     311                 :            : 
     312                 :            :   /**
     313                 :            :    * Exhaustively applies all substitutions discovered to an element of the
     314                 :            :    * trail. Returns a TrailIndex corresponding to the substitutions being
     315                 :            :    * applied.
     316                 :            :    */
     317                 :            :   TrailIndex applyAllSubstitutionsToIndex(TrailIndex i);
     318                 :            : 
     319                 :            :   /**
     320                 :            :    * Applies a substitution to an element in the trail.
     321                 :            :    */
     322                 :            :   TrailIndex applySubstitution(SubIndex s, TrailIndex i);
     323                 :            : 
     324                 :            :   /**
     325                 :            :    * Reduces the trail node at i by the gcd of the variables.
     326                 :            :    * Returns the new trail element.
     327                 :            :    *
     328                 :            :    * This raises the conflict flag if unsat is detected.
     329                 :            :    */
     330                 :            :   TrailIndex reduceByGCD(TrailIndex i);
     331                 :            : 
     332                 :            :   /**
     333                 :            :    * Returns true if i'th element in the trail is trivially true.
     334                 :            :    * (0 = 0)
     335                 :            :    */
     336                 :            :   bool triviallySat(TrailIndex t);
     337                 :            : 
     338                 :            :   /**
     339                 :            :    * Returns true if i'th element in the trail is trivially unsatisfiable.
     340                 :            :    * (1 = 0)
     341                 :            :    */
     342                 :            :   bool triviallyUnsat(TrailIndex t);
     343                 :            : 
     344                 :            :   /** Returns true if the gcd of the i'th element of the trail is 1.*/
     345                 :            :   bool gcdIsOne(TrailIndex t);
     346                 :            : 
     347                 :            :   bool debugAnySubstitionApplies(TrailIndex t);
     348                 :            :   bool debugSubstitutionApplies(SubIndex si, TrailIndex ti);
     349                 :            : 
     350                 :            :   /** Returns true if the queue of nodes to process is empty. */
     351                 :            :   bool queueEmpty() const;
     352                 :            : 
     353                 :            :   bool queueConditions(TrailIndex t);
     354                 :            : 
     355                 :      41859 :   void pushToQueueBack(TrailIndex t)
     356                 :            :   {
     357 [ -  + ][ -  + ]:      41859 :     Assert(queueConditions(t));
                 [ -  - ]
     358                 :      41859 :     d_currentF.push_back(t);
     359                 :      41859 :   }
     360                 :            : 
     361                 :            :   void pushToQueueFront(TrailIndex t)
     362                 :            :   {
     363                 :            :     Assert(queueConditions(t));
     364                 :            :     d_currentF.push_front(t);
     365                 :            :   }
     366                 :            : 
     367                 :            :   /**
     368                 :            :    * Moves the minimum Constraint by absolute value of the minimum coefficient
     369                 :            :    * to the front of the queue.
     370                 :            :    */
     371                 :            :   void moveMinimumByAbsToQueueFront();
     372                 :            : 
     373                 :            :   void saveQueue();
     374                 :            : 
     375                 :            :   TrailIndex impliedGcdOfOne();
     376                 :            : 
     377                 :            :   /**
     378                 :            :    * Processing the current set of equations.
     379                 :            :    *
     380                 :            :    * decomposeIndex() rule is only applied if allowDecomposition is true.
     381                 :            :    */
     382                 :            :   bool processEquations(bool allowDecomposition);
     383                 :            : 
     384                 :            :   /**
     385                 :            :    * Constructs a proof from any d_trail[i] in terms of input literals.
     386                 :            :    */
     387                 :            :   Node proveIndex(TrailIndex i);
     388                 :            : 
     389                 :            :   /**
     390                 :            :    * Returns the SumPair in d_trail[i].d_eq with all of the fresh variables
     391                 :            :    * purified out.
     392                 :            :    */
     393                 :            :   SumPair purifyIndex(TrailIndex i);
     394                 :            : 
     395                 :            :  public:
     396                 :          0 :   bool hasMoreDecompositionLemmas() const
     397                 :            :   {
     398                 :          0 :     return !d_decompositionLemmaQueue.empty();
     399                 :            :   }
     400                 :          0 :   Node nextDecompositionLemma()
     401                 :            :   {
     402                 :          0 :     Assert(hasMoreDecompositionLemmas());
     403                 :          0 :     TrailIndex front = d_decompositionLemmaQueue.front();
     404                 :          0 :     d_decompositionLemmaQueue.pop();
     405                 :          0 :     return trailIndexToEquality(front);
     406                 :            :   }
     407                 :            : 
     408                 :            :  private:
     409                 :            :   Node trailIndexToEquality(TrailIndex i) const;
     410                 :            :   void addTrailElementAsLemma(TrailIndex i);
     411                 :            : 
     412                 :            :  public:
     413                 :            :   /** These fields are designed to be accessible to TheoryArith methods. */
     414                 :            :   class Statistics
     415                 :            :   {
     416                 :            :    public:
     417                 :            :     IntStat d_conflictCalls;
     418                 :            :     IntStat d_cutCalls;
     419                 :            : 
     420                 :            :     IntStat d_cuts;
     421                 :            :     IntStat d_conflicts;
     422                 :            : 
     423                 :            :     TimerStat d_conflictTimer;
     424                 :            :     TimerStat d_cutTimer;
     425                 :            : 
     426                 :            :     Statistics(StatisticsRegistry& sr);
     427                 :            :   };
     428                 :            : 
     429                 :            :   Statistics d_statistics;
     430                 :            : }; /* class DioSolver */
     431                 :            : 
     432                 :            : }  // namespace arith::linear
     433                 :            : }  // namespace theory
     434                 :            : }  // namespace cvc5::internal
     435                 :            : 
     436                 :            : #endif /* CVC5__THEORY__ARITH__DIO_SOLVER_H */