summaryrefslogtreecommitdiff
path: root/src/theory/arith/row_vector.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/row_vector.h')
-rw-r--r--src/theory/arith/row_vector.h233
1 files changed, 0 insertions, 233 deletions
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
deleted file mode 100644
index 5fd471700..000000000
--- a/src/theory/arith/row_vector.h
+++ /dev/null
@@ -1,233 +0,0 @@
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ROW_VECTOR_H
-#define __CVC4__THEORY__ARITH__ROW_VECTOR_H
-
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/arithvar_set.h"
-#include "util/rational.h"
-#include <vector>
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-class VarCoeffPair {
-private:
- ArithVar d_variable;
- Rational d_coeff;
-
-public:
- VarCoeffPair(ArithVar v, const Rational& q): d_variable(v), d_coeff(q) {}
-
- ArithVar getArithVar() const { return d_variable; }
- Rational& getCoefficient() { return d_coeff; }
- const Rational& getCoefficient() const { return d_coeff; }
-
- bool operator<(const VarCoeffPair& other) const{
- return getArithVar() < other.getArithVar();
- }
-
- static bool variableLess(const VarCoeffPair& a, const VarCoeffPair& b){
- return a < b;
- }
-};
-
-/**
- * ReducedRowVector is a sparse vector representation that represents the
- * row as a strictly sorted array of "VarCoeffPair"s.
- * The row has a notion of a basic variable.
- * This is a variable that must have a coefficient of -1 in the array.
- */
-class ReducedRowVector {
-public:
- typedef std::vector<VarCoeffPair> VarCoeffArray;
- typedef VarCoeffArray::const_iterator const_iterator;
-
-private:
- typedef std::vector<bool> ArithVarContainsSet;
- typedef VarCoeffArray::iterator iterator;
-
- /**
- * Invariants:
- * - isSorted(d_entries, true)
- * - noZeroCoefficients(d_entries)
- */
- VarCoeffArray d_entries;
-
- /**
- * Buffer for d_entries to reduce allocations by addRowTimesConstant.
- */
- VarCoeffArray d_buffer;
-
- /**
- * The basic variable associated with the row.
- * Must have a coefficient of -1.
- */
- ArithVar d_basic;
-
-
- /**
- * Invariants:
- * - This set is the same as the set maintained in d_entries.
- */
- ArithVarContainsSet d_contains;
-
- std::vector<uint32_t>& d_rowCount;
- std::vector<PermissiveBackArithVarSet>& d_columnMatrix;
-
-
-public:
-
- ReducedRowVector(ArithVar basic,
- const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- std::vector<uint32_t>& count,
- std::vector< PermissiveBackArithVarSet >& columnMatrix);
- ~ReducedRowVector();
-
- void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,
- std::vector< Rational >& coefficients) const;
-
- /** Returns the basic variable.*/
- ArithVar basic() const{
- Assert(basicIsSet());
- return d_basic;
- }
-
- /** Returns the number of nonzero variables in the vector. */
- uint32_t size() const {
- return d_entries.size();
- }
-
- /** Iterates over the nonzero entries in the vector. */
- const_iterator begin() const { return d_entries.begin(); }
- const_iterator end() const { return d_entries.end(); }
-
- /** Returns true if the variable is in the row. */
- bool has(ArithVar x_j) const{
- if(x_j >= d_contains.size()){
- return false;
- }else{
- return d_contains[x_j];
- }
- }
-
- /**
- * Returns the coefficient of a variable in the row.
- */
- const Rational& lookup(ArithVar x_j) const{
- Assert(has(x_j));
- Assert(hasInEntries(x_j));
- const_iterator lb = lower_bound(x_j);
- return (*lb).getCoefficient();
- }
-
-
- /** Prints the row to the buffer Debug("row::print"). */
- void printRow();
-
- /**
- * Changes the basic variable to x_j.
- * Precondition: has(x_j)
- */
- void pivot(ArithVar x_j);
-
- /**
- * Replaces other.basic() in the current row using the other row.
- * This assumes the other row represents an equality equal to zero.
- *
- * \sum(this->entries) -= this->lookup(other.basic()) * (\sum(other.d_entries))
- * Precondition:
- * has(other.basic())
- * basic != other.basic()
- */
- void substitute(const ReducedRowVector& other);
-
- /**
- * Returns the reduced row as an equality with
- * the basic variable on the lhs equal to the sum of the non-basics variables.
- * The mapped from ArithVars to Nodes is specificied by map.
- */
- Node asEquality(const ArithVarToNodeMap& map) const;
-
-private:
-
- /**
- * \sum(this->entries) += c * (\sum(other.d_entries) )
- *
- * Updates the current row to be the sum of itself and
- * another vector times c (c != 0).
- */
- void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
-
-
- /** Multiplies the coefficients of the RowVector by c (where c != 0). */
- void multiply(const Rational& c);
-
- /**
- * Adds v to d_contains.
- * This may resize d_contains.
- */
- static void addArithVar(ArithVarContainsSet& contains, ArithVar v);
-
- /** Removes v from d_contains. */
- static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
-
-
- /**
- * Let c be -1 if strictlySorted is true and c be 0 otherwise.
- * isSorted(arr, strictlySorted) is then equivalent to
- * If i<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
- */
- static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
-
- /**
- * Zips together an array of variables and coefficients and appends
- * it to the end of an output vector.
- */
- static void zip(const std::vector< ArithVar >& variables,
- const std::vector< Rational >& coefficients,
- VarCoeffArray& output);
-
- /**
- * Debugging code.
- * noZeroCoefficients(arr) is equivalent to
- * 0 != getCoefficient(arr[i]) for all i.
- */
- static bool noZeroCoefficients(const VarCoeffArray& arr);
-
- /** Debugging code.*/
- bool matchingCounts() const;
-
- const_iterator lower_bound(ArithVar x_j) const{
- return std::lower_bound(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j, 0));
- }
-
- /** Debugging code */
- bool wellFormed() const{
- return
- isSorted(d_entries, true) &&
- noZeroCoefficients(d_entries) &&
- basicIsSet() &&
- has(basic()) &&
- lookup(basic()) == Rational(-1);
- }
-
- bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
-
- /** Debugging code. */
- bool hasInEntries(ArithVar x_j) const {
- return std::binary_search(d_entries.begin(), d_entries.end(), VarCoeffPair(x_j,0));
- }
-
-}; /* class ReducedRowVector */
-
-
-}/* namespace CVC4::theory::arith */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
-
-#endif /* __CVC4__THEORY__ARITH_ARITH_CONSTANTS_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback