Branch data     Line data    Source code

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