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                 :            :  * [[ Add one-line brief description here ]]
      11                 :            :  *
      12                 :            :  * [[ Add lengthier description here ]]
      13                 :            :  * \todo document this file
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #pragma once
      19                 :            : 
      20                 :            : #include <vector>
      21                 :            : 
      22                 :            : #include "theory/arith/linear/arithvar.h"
      23                 :            : #include "theory/arith/linear/matrix.h"
      24                 :            : #include "util/dense_map.h"
      25                 :            : #include "util/rational.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : namespace theory {
      29                 :            : namespace arith::linear {
      30                 :            : 
      31                 :            : /**
      32                 :            :  * A Tableau is a Rational matrix that keeps its rows in solved form.
      33                 :            :  * Each row has a basic variable with coefficient -1 that is solved.
      34                 :            :  * Tableau is optimized for pivoting.
      35                 :            :  * The tableau should only be updated via pivot calls.
      36                 :            :  */
      37                 :            : class Tableau : public Matrix<Rational>
      38                 :            : {
      39                 :            :  public:
      40                 :            :  private:
      41                 :            :   typedef DenseMap<RowIndex> BasicToRowMap;
      42                 :            :   // Set of all of the basic variables in the tableau.
      43                 :            :   // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
      44                 :            :   BasicToRowMap d_basic2RowIndex;
      45                 :            : 
      46                 :            :   // RowIndex |-> Basic Variable
      47                 :            :   typedef DenseMap<ArithVar> RowIndexToBasicMap;
      48                 :            :   RowIndexToBasicMap d_rowIndex2basic;
      49                 :            : 
      50                 :            :  public:
      51                 :     102032 :   Tableau() : Matrix<Rational>(Rational(0)) {}
      52                 :            : 
      53                 :            :   typedef Matrix<Rational>::ColIterator ColIterator;
      54                 :            :   typedef Matrix<Rational>::RowIterator RowIterator;
      55                 :            :   typedef BasicToRowMap::const_iterator BasicIterator;
      56                 :            : 
      57                 :            :   typedef MatrixEntry<Rational> Entry;
      58                 :            : 
      59                 :   34558881 :   bool isBasic(ArithVar v) const { return d_basic2RowIndex.isKey(v); }
      60                 :            : 
      61                 :          0 :   void debugPrintIsBasic(ArithVar v) const
      62                 :            :   {
      63         [ -  - ]:          0 :     if (isBasic(v))
      64                 :            :     {
      65         [ -  - ]:          0 :       Trace("model") << v << " is basic." << std::endl;
      66                 :            :     }
      67                 :            :     else
      68                 :            :     {
      69         [ -  - ]:          0 :       Trace("model") << v << " is non-basic." << std::endl;
      70                 :            :     }
      71                 :          0 :   }
      72                 :            : 
      73                 :          0 :   BasicIterator beginBasic() const { return d_basic2RowIndex.begin(); }
      74                 :          0 :   BasicIterator endBasic() const { return d_basic2RowIndex.end(); }
      75                 :            : 
      76                 :   21193097 :   RowIndex basicToRowIndex(ArithVar x) const { return d_basic2RowIndex[x]; }
      77                 :            : 
      78                 :   18128774 :   ArithVar rowIndexToBasic(RowIndex rid) const
      79                 :            :   {
      80 [ -  + ][ -  + ]:   18128774 :     Assert(d_rowIndex2basic.isKey(rid));
                 [ -  - ]
      81                 :   18128774 :     return d_rowIndex2basic[rid];
      82                 :            :   }
      83                 :            : 
      84                 :   12293621 :   ColIterator colIterator(ArithVar x) const { return getColumn(x).begin(); }
      85                 :            : 
      86                 :   13119470 :   RowIterator ridRowIterator(RowIndex rid) const { return getRow(rid).begin(); }
      87                 :            : 
      88                 :    1185258 :   RowIterator basicRowIterator(ArithVar basic) const
      89                 :            :   {
      90                 :    1185258 :     return ridRowIterator(basicToRowIndex(basic));
      91                 :            :   }
      92                 :            : 
      93                 :          0 :   const Entry& basicFindEntry(ArithVar basic, ArithVar col) const
      94                 :            :   {
      95                 :          0 :     return findEntry(basicToRowIndex(basic), col);
      96                 :            :   }
      97                 :            : 
      98                 :            :   /**
      99                 :            :    * Adds a row to the tableau.
     100                 :            :    * The new row is equivalent to:
     101                 :            :    *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
     102                 :            :    * preconditions:
     103                 :            :    *   basicVar is already declared to be basic
     104                 :            :    *   basicVar does not have a row associated with it in the tableau.
     105                 :            :    *
     106                 :            :    * Note: each variables[i] does not have to be non-basic.
     107                 :            :    * Pivoting will be mimicked if it is basic.
     108                 :            :    */
     109                 :            :   void addRow(ArithVar basicVar,
     110                 :            :               const std::vector<Rational>& coeffs,
     111                 :            :               const std::vector<ArithVar>& variables);
     112                 :            : 
     113                 :            :   /**
     114                 :            :    * preconditions:
     115                 :            :    *   x_r is basic,
     116                 :            :    *   x_s is non-basic, and
     117                 :            :    *   a_rs != 0.
     118                 :            :    */
     119                 :            :   void pivot(ArithVar basicOld,
     120                 :            :              ArithVar basicNew,
     121                 :            :              CoefficientChangeCallback& cb);
     122                 :            : 
     123                 :            :   void removeBasicRow(ArithVar basic);
     124                 :            : 
     125                 :    1652652 :   uint32_t basicRowLength(ArithVar basic) const
     126                 :            :   {
     127                 :    1652652 :     RowIndex ridx = basicToRowIndex(basic);
     128                 :    1652652 :     return getRowLength(ridx);
     129                 :            :   }
     130                 :            : 
     131                 :            :   /**
     132                 :            :    *  to += mult * from
     133                 :            :    * replacing from with its row.
     134                 :            :    */
     135                 :            :   void substitutePlusTimesConstant(ArithVar to,
     136                 :            :                                    ArithVar from,
     137                 :            :                                    const Rational& mult,
     138                 :            :                                    CoefficientChangeCallback& cb);
     139                 :            : 
     140                 :       4541 :   void directlyAddToCoefficient(ArithVar rowVar,
     141                 :            :                                 ArithVar col,
     142                 :            :                                 const Rational& mult,
     143                 :            :                                 CoefficientChangeCallback& cb)
     144                 :            :   {
     145                 :       4541 :     RowIndex ridx = basicToRowIndex(rowVar);
     146                 :       4541 :     manipulateRowEntry(ridx, col, mult, cb);
     147                 :       4541 :   }
     148                 :            : 
     149                 :            :   /* Returns the complexity of a row in the tableau. */
     150                 :            :   uint32_t rowComplexity(ArithVar basic) const;
     151                 :            : 
     152                 :            :   /* Returns the average complexity of the rows in the tableau. */
     153                 :            :   double avgRowComplexity() const;
     154                 :            : 
     155                 :            :   void printBasicRow(ArithVar basic, std::ostream& out);
     156                 :            : 
     157                 :            :  private:
     158                 :            :   /* Changes the basic variable on the row for basicOld to basicNew. */
     159                 :            :   void rowPivot(ArithVar basicOld,
     160                 :            :                 ArithVar basicNew,
     161                 :            :                 CoefficientChangeCallback& cb);
     162                 :            : 
     163                 :            : }; /* class Tableau */
     164                 :            : 
     165                 :            : }  // namespace arith::linear
     166                 :            : }  // namespace theory
     167                 :            : }  // namespace cvc5::internal