- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
cdvector.h \
cdmaybe.h \
stacking_map.h \
- stacking_vector.h
+ stacking_vector.h \
+ cddense_set.h
\ No newline at end of file
--- /dev/null
+/********************* */
+/*! \file cddense_set.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is an abstraction of a set of unsigned integers.
+ **
+ ** This is an abstraction of a set of unsigned integers.
+ ** This class is designed to provide constant time insertion, element_of,
+ ** and fast iteration. This is done by storing backing vectors of size greater than
+ ** the maximum key.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+
+#include "context/context.h"
+#include "context/cdlist_forward.h"
+#include "context/cdlist.h"
+
+#include "util/index.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class CleanUp = DefaultCleanUp<Index> >
+class CDDenseSet {
+public:
+ typedef Index Element;
+
+private:
+
+ class RemoveIntCleanup {
+ private:
+ std::vector<bool>& d_set;
+
+ /**
+ * The CleanUp functor.
+ */
+ CleanUp d_cleanUp;
+ public:
+ RemoveIntCleanup(std::vector<bool>& set, const CleanUp& cleanup)
+ : d_set(set), d_cleanUp(cleanup)
+ {}
+
+ void operator()(Element* p){
+ d_cleanup(p);
+
+ ArithVar x = *p;
+ Assert(d_set[x]);
+ d_set[x] = false;
+ }
+ };
+
+ typedef CDList<Element, RemoveIntCleanup> ElementList;
+ ElementList d_list;
+
+ std::vector<bool> d_set;
+
+public:
+ typedef ElementList::const_iterator const_iterator;
+
+ CDDenseSet(context::Context* c, const CleanUp& cleanup = CleanUp())
+ : d_set(), d_list(c, true, RemoveIntCleanup(d_set, cleanup))
+ { }
+
+ /** This cannot be const as garbage collection is done lazily. */
+ bool contains(Element x) const{
+ if(x < d_set.size()){
+ return d_set[x];
+ }else{
+ return false;
+ }
+ }
+
+ void insert(Element x){
+ Assert(!contains(x));
+ if(x >= d_set.size()){
+ d_set.resize(x+1, false);
+ }
+ d_list.push_back(x);
+ d_set[x] = true;
+ }
+
+ const_iterator begin() const { return d_list.begin(); }
+ const_iterator end() const { return d_list.end(); }
+
+};/* class CDDenseSet<> */
+
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
partial_model.cpp \
linear_equality.h \
linear_equality.cpp \
- arithvar_set.h \
- tableau.h \
- tableau.cpp \
+ matrix.h \
+ matrix.cpp \
arith_priority_queue.h \
arith_priority_queue.cpp \
simplex.h \
#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/partial_model.h"
#include "util/stats.h"
*/
ArithVarArray d_varOrderQueue;
- PermissiveBackArithVarSet d_varSet;
+ DenseSet d_varSet;
/**
* Reference to the arithmetic partial model for checking if a variable
** \brief Defines ArithVar which is the internal representation of variables in arithmetic
**
** This defines ArithVar which is the internal representation of variables in
- ** arithmetic. This is a typedef from uint32_t to ArithVar.
+ ** arithmetic. This is a typedef from Index to ArithVar.
** This file also provides utilities for ArithVars.
**/
#define __CVC4__THEORY__ARITH__ARITHVAR_H
#include <limits>
-#include <stdint.h>
#include <ext/hash_map>
#include "expr/node.h"
#include "context/cdhashset.h"
+#include "context/cdhashset.h"
+
+#include "util/index.h"
namespace CVC4 {
namespace theory {
namespace arith {
-typedef uint32_t ArithVar;
+typedef Index ArithVar;
const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
//Maps from Nodes -> ArithVars, and vice versa
+++ /dev/null
-/********************* */
-/*! \file arithvar_set.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
-
-#include <vector>
-#include "theory/arith/arithvar.h"
-#include "context/context.h"
-#include "context/cdlist.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-/**
- * This is an abstraction of a set of ArithVars.
- * This class is designed to provide constant time insertion, deletion, and element_of
- * and fast iteration.
- *
- * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet.
- * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars
- * that are greater than allocated(). Asking isMember() of such an ArithVar
- * is an assertion failure. The cost of doing this is that it takes O(M)
- * where M is the total number of ArithVars in memory.
- *
- * PermissiveBackArithVarSet means that all ArithVars are implicitly not in the set,
- * and any ArithVar past the end of d_posVector is not in the set.
- * A permissiveBack allows for less memory to be consumed on average.
- *
- */
-template <bool permissiveBack>
-class ArithVarSetImpl {
-public:
- typedef std::vector<ArithVar> VarList;
-private:
- //List of the ArithVars in the set.
- VarList d_list;
-
- //Each ArithVar in the set is mapped to its position in d_list.
- //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
- std::vector<unsigned> d_posVector;
-
-public:
- typedef VarList::const_iterator const_iterator;
-
- ArithVarSetImpl() : d_list(), d_posVector() {}
-
- size_t size() const {
- return d_list.size();
- }
- bool empty() const {
- return d_list.empty();
- }
-
- size_t allocated() const {
- return d_posVector.size();
- }
-
- void purge() {
- for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end();i!= endIter; ++i){
- d_posVector[*i] = ARITHVAR_SENTINEL;
- }
- d_list.clear();
- Assert(empty());
- }
-
- void increaseSize(ArithVar max){
- Assert(max >= allocated());
- d_posVector.resize(max+1, ARITHVAR_SENTINEL);
- }
-
- void increaseSize(){
- increaseSize(allocated());
- }
-
- bool isMember(ArithVar x) const{
- if(permissiveBack && x >= allocated()){
- return false;
- }else{
- Assert(x < allocated());
- return d_posVector[x] != ARITHVAR_SENTINEL;
- }
- }
-
- /** Invalidates iterators */
- void init(ArithVar x, bool val) {
- Assert(x >= allocated());
- increaseSize(x);
- if(val){
- add(x);
- }
- }
-
- /** Invalidates iterators */
- void add(ArithVar x){
- Assert(!isMember(x));
- if(permissiveBack && x >= allocated()){
- increaseSize(x);
- }
- d_posVector[x] = size();
- d_list.push_back(x);
- }
-
- const_iterator begin() const{ return d_list.begin(); }
- const_iterator end() const{ return d_list.end(); }
-
- /**
- * Invalidates iterators.
- * Adds x to the set if it is not already in the set.
- */
- void softAdd(ArithVar x){
- if(!isMember(x)){
- add(x);
- }
- }
-
- const VarList& getList() const{
- return d_list;
- }
-
- /** Invalidates iterators */
- void remove(ArithVar x){
- Assert(isMember(x));
- swapToBack(x);
- Assert(d_list.back() == x);
- pop_back();
- }
-
- ArithVar pop_back() {
- Assert(!empty());
- ArithVar atBack = d_list.back();
- d_posVector[atBack] = ARITHVAR_SENTINEL;
- d_list.pop_back();
- return atBack;
- }
-
- private:
-
- /** This should be true of all x < allocated() after every operation. */
- bool wellFormed(ArithVar x){
- if(d_posVector[x] == ARITHVAR_SENTINEL){
- return true;
- }else{
- return d_list[d_posVector[x]] == x;
- }
- }
-
- /** Swaps a member x to the back of d_list. */
- void swapToBack(ArithVar x){
- Assert(isMember(x));
-
- unsigned currentPos = d_posVector[x];
- ArithVar atBack = d_list.back();
-
- d_list[currentPos] = atBack;
- d_posVector[atBack] = currentPos;
-
- d_list[size() - 1] = x;
- d_posVector[x] = size() - 1;
- }
-};
-
-typedef ArithVarSetImpl<false> ArithVarSet;
-typedef ArithVarSetImpl<true> PermissiveBackArithVarSet;
-
-
-/**
- * ArithVarMultiset
- */
-class ArithVarMultiset {
-public:
- typedef std::vector<ArithVar> VarList;
-private:
- //List of the ArithVars in the multi set.
- VarList d_list;
-
- //Each ArithVar in the set is mapped to its position in d_list.
- //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
- std::vector<unsigned> d_posVector;
-
- //Count of the number of elements in the array
- std::vector<unsigned> d_counts;
-
-public:
- typedef VarList::const_iterator const_iterator;
-
- ArithVarMultiset() : d_list(), d_posVector() {}
-
- size_t size() const {
- return d_list.size();
- }
-
- bool empty() const {
- return d_list.empty();
- }
-
- size_t allocated() const {
- Assert(d_posVector.size() == d_counts.size());
- return d_posVector.size();
- }
-
- void purge() {
- for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end(); i!= endIter; ++i){
- d_posVector[*i] = ARITHVAR_SENTINEL;
- d_counts[*i] = 0;
- }
- d_list.clear();
- Assert(empty());
- }
-
- void increaseSize(ArithVar max){
- Assert(max >= allocated());
- d_posVector.resize(max+1, ARITHVAR_SENTINEL);
- d_counts.resize(max+1, 0);
- }
-
- void increaseSize(){
- increaseSize(allocated());
- }
-
- bool isMember(ArithVar x) const{
- if( x >= allocated()){
- return false;
- }else{
- Assert(x < allocated());
- return d_posVector[x] != ARITHVAR_SENTINEL;
- }
- }
-
- /**
- * Invalidates iterators.
- */
- void addMultiset(ArithVar x){
- if( x >= allocated()){
- increaseSize(x);
- }
- if(d_counts[x] == 0){
- d_posVector[x] = size();
- d_list.push_back(x);
- }
- d_counts[x]++;
- }
-
- unsigned count(ArithVar x){
- if( x >= allocated()){
- return 0;
- }else{
- return d_counts[x];
- }
- }
-
- const_iterator begin() const{ return d_list.begin(); }
- const_iterator end() const{ return d_list.end(); }
-
- const VarList& getList() const{
- return d_list;
- }
-
- /** Invalidates iterators */
- void remove(ArithVar x){
- Assert(isMember(x));
- swapToBack(x);
- Assert(d_list.back() == x);
- pop_back();
- }
-
- ArithVar pop_back() {
- Assert(!empty());
- ArithVar atBack = d_list.back();
- d_posVector[atBack] = ARITHVAR_SENTINEL;
- d_counts[atBack] = 0;
- d_list.pop_back();
- return atBack;
- }
-
- private:
-
- /** This should be true of all x < allocated() after every operation. */
- bool wellFormed(ArithVar x){
- if(d_posVector[x] == ARITHVAR_SENTINEL){
- return true;
- }else{
- return d_list[d_posVector[x]] == x;
- }
- }
-
- /** Swaps a member x to the back of d_list. */
- void swapToBack(ArithVar x){
- Assert(isMember(x));
-
- unsigned currentPos = d_posVector[x];
- ArithVar atBack = d_list.back();
-
- d_list[currentPos] = atBack;
- d_posVector[atBack] = currentPos;
-
- d_list[size() - 1] = x;
- d_posVector[x] = size() - 1;
- }
-};
-
-class CDArithVarSet {
-private:
-
- class RemoveIntCleanup {
- private:
- std::vector<bool>& d_set;
- public:
- RemoveIntCleanup(std::vector<bool>& set)
- : d_set(set)
- {}
-
- void operator()(ArithVar* p){
- ArithVar x = *p;
- Assert(d_set[x]);
- d_set[x] = false;
- }
- };
-
- std::vector<bool> d_set;
- context::CDList<ArithVar, RemoveIntCleanup> d_list;
-
-public:
- CDArithVarSet(context::Context* c)
- : d_set(), d_list(c, true, RemoveIntCleanup(d_set))
- { }
-
- /** This cannot be const as garbage collection is done lazily. */
- bool contains(ArithVar x) const{
- if(x < d_set.size()){
- return d_set[x];
- }else{
- return false;
- }
- }
-
- void insert(ArithVar x){
- Assert(!contains(x));
- if(x >= d_set.size()){
- d_set.resize(x+1, false);
- }
- d_list.push_back(x);
- d_set[x] = true;
- }
-};
-
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
#pragma once
#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
#include "theory/arith/arithvar_node_map.h"
#include "theory/arith/constraint_forward.h"
#include "context/cdmaybe.h"
#include "util/stats.h"
+#include "util/dense_map.h"
namespace CVC4 {
namespace theory {
* If this is 0 or cannot be 0, this can be signalled.
* The pair of terms for the congruence is stored in watched equalities.
*/
- PermissiveBackArithVarSet d_watchedVariables;
+ DenseSet d_watchedVariables;
/** d_watchedVariables |-> (= x y) */
ArithVarToNodeMap d_watchedEqualities;
#include "context/context.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/partial_model.h"
#include "util/rational.h"
//Assert(matchingSets(d_tableau, x_i));
Tableau::ColIterator basicIter = d_tableau.colIterator(x_i);
for(; !basicIter.atEnd(); ++basicIter){
- const TableauEntry& entry = *basicIter;
+ const Tableau::Entry& entry = *basicIter;
Assert(entry.getColVar() == x_i);
- ArithVar x_j = entry.getRowVar();
+ ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
//ReducedRowVector& row_j = d_tableau.lookup(x_j);
//const Rational& a_ji = row_j.lookup(x_i);
d_partialModel.setAssignment(x_i, v);
- Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i));
//double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i));
//(d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
if(Debug.isOn("arith::simplex:row")){ debugPivot(x_i, x_j); }
- const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j);
+ RowIndex ridx = d_tableau.basicToRowIndex(x_i);
+ const Tableau::Entry& entry_ij = d_tableau.findEntry(ridx, x_j);
Assert(!entry_ij.blank());
//Assert(matchingSets(d_tableau, x_j));
for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){
- const TableauEntry& entry = *iter;
+ const Tableau::Entry& entry = *iter;
Assert(entry.getColVar() == x_j);
- ArithVar x_k = entry.getRowVar();
- if(x_k != x_i ){
+ RowIndex currRow = entry.getRowIndex();
+ if(ridx != currRow ){
+ ArithVar x_k = d_tableau.rowIndexToBasic(currRow);
const Rational& a_kj = entry.getCoefficient();
DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
d_partialModel.setAssignment(x_k, nextAssignment);
// Pivots
++(d_statistics.d_statPivots);
- Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j));
- //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j));
- //(d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
d_tableau.pivot(x_i, x_j);
d_basicVariableUpdates(x_j);
- if(Debug.isOn("tableau")){
- d_tableau.printTableau();
+ if(Debug.isOn("matrix")){
+ d_tableau.printMatrix();
}
}
void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){
Debug("arith::pivot") << "debugPivot("<< x_i <<"|->"<< x_j << ")" << endl;
- for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
- const TableauEntry& entry = *iter;
+ for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
+ const Tableau::Entry& entry = *iter;
ArithVar var = entry.getColVar();
const Rational& coeff = entry.getCoefficient();
* }
*/
void LinearEqualityModule::debugCheckTableau(){
- ArithVarSet::const_iterator basicIter = d_tableau.beginBasic();
- ArithVarSet::const_iterator endIter = d_tableau.endBasic();
+ Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
+ endIter = d_tableau.endBasic();
for(; basicIter != endIter; ++basicIter){
ArithVar basic = *basicIter;
DeltaRational sum;
Debug("paranoid:check_tableau") << "starting row" << basic << endl;
- Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic);
+ Tableau::RowIterator nonbasicIter = d_tableau.basicRowIterator(basic);
for(; !nonbasicIter.atEnd(); ++nonbasicIter){
- const TableauEntry& entry = *nonbasicIter;
+ const Tableau::Entry& entry = *nonbasicIter;
ArithVar nonbasic = entry.getColVar();
if(basic == nonbasic) continue;
DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
DeltaRational sum(0,0);
- for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
- const TableauEntry& entry = (*i);
+ for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+ const Tableau::Entry& entry = (*i);
ArithVar nonbasic = entry.getColVar();
if(nonbasic == basic) continue;
const Rational& coeff = entry.getCoefficient();
Assert(d_tableau.isBasic(x));
DeltaRational sum(0);
- for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){
- const TableauEntry& entry = (*i);
+ for(Tableau::RowIterator i = d_tableau.basicRowIterator(x); !i.atEnd(); ++i){
+ const Tableau::Entry& entry = (*i);
ArithVar nonbasic = entry.getColVar();
if(nonbasic == x) continue;
const Rational& coeff = entry.getCoefficient();
}
bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
- for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
- const TableauEntry& entry = *iter;
+ for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+ const Tableau::Entry& entry = *iter;
ArithVar var = entry.getColVar();
if(var == basic) continue;
vector<Constraint> bounds;
- Tableau::RowIterator iter = d_tableau.rowIterator(basic);
+ Tableau::RowIterator iter = d_tableau.basicRowIterator(basic);
for(; !iter.atEnd(); ++iter){
- const TableauEntry& entry = *iter;
+ const Tableau::Entry& entry = *iter;
ArithVar nonbasic = entry.getColVar();
if(nonbasic == basic) continue;
#include "theory/arith/delta_rational.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/constraint.h"
#include "util/stats.h"
--- /dev/null
+/********************* */
+/*! \file tableau.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+
+#include "theory/arith/matrix.h"
+
+using namespace std;
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+/*
+void Tableau::addRow(ArithVar basicVar,
+ const std::vector<Rational>& coeffs,
+ const std::vector<ArithVar>& variables){
+
+ Assert(coeffs.size() == variables.size());
+
+ //The new basic variable cannot already be a basic variable
+ Assert(!d_basicVariables.isMember(basicVar));
+ d_basicVariables.add(basicVar);
+ ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
+ d_rowsTable[basicVar] = row_current;
+
+ //A variable in the row may have been made non-basic already.
+ //If this is the case we fake pivoting this variable
+ vector<ArithVar>::const_iterator varsIter = variables.begin();
+ vector<ArithVar>::const_iterator varsEnd = variables.end();
+
+ for( ; varsIter != varsEnd; ++varsIter){
+ ArithVar var = *varsIter;
+
+ if(d_basicVariables.isMember(var)){
+ EntryID varID = find(basicVar, var);
+ TableauEntry& entry = d_entryManager.get(varID);
+ const Rational& coeff = entry.getCoefficient();
+
+ loadRowIntoMergeBuffer(var);
+ rowPlusRowTimesConstant(coeff, basicVar, var);
+ emptyRowFromMergeBuffer(var);
+ }
+ }
+}
+*/
+
+/*
+ReducedRowVector* Tableau::removeRow(ArithVar basic){
+ Assert(isBasic(basic));
+
+ ReducedRowVector* row = d_rowsTable[basic];
+
+ d_basicVariables.remove(basic);
+ d_rowsTable[basic] = NULL;
+
+ return row;
+}
+*/
+
+void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
+ Assert(isBasic(oldBasic));
+ Assert(!isBasic(newBasic));
+ Assert(d_mergeBuffer.empty());
+
+ Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
+
+ RowIndex ridx = basicToRowIndex(oldBasic);
+
+ rowPivot(oldBasic, newBasic);
+ Assert(ridx == basicToRowIndex(newBasic));
+
+ loadRowIntoBuffer(ridx);
+
+ ColIterator colIter = colIterator(newBasic);
+ while(!colIter.atEnd()){
+ EntryID id = colIter.getID();
+ Entry& entry = d_entries.get(id);
+
+ ++colIter; //needs to be incremented before the variable is removed
+ if(entry.getRowIndex() == ridx){ continue; }
+
+ RowIndex to = entry.getRowIndex();
+ Rational coeff = entry.getCoefficient();
+
+ rowPlusBufferTimesConstant(to, coeff);
+ }
+ clearBuffer();
+
+ //Clear the column for used for this variable
+
+ Assert(d_mergeBuffer.empty());
+ Assert(!isBasic(oldBasic));
+ Assert(isBasic(newBasic));
+ Assert(getColLength(newBasic) == 1);
+}
+
+// void Tableau::printTableau() const {
+// Debug("tableau") << "Tableau::d_activeRows" << endl;
+
+// ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
+// for(; basicIter != endIter; ++basicIter){
+// ArithVar basic = *basicIter;
+// printRow(basic);
+// }
+// }
+
+// void Tableau::printRow(ArithVar basic) const {
+// Debug("tableau") << "{" << basic << ":";
+// for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
+// const TableauEntry& entry = *entryIter;
+// printEntry(entry);
+// Debug("tableau") << ",";
+// }
+// Debug("tableau") << "}" << endl;
+// }
+
+// void Tableau::printEntry(const TableauEntry& entry) const {
+// Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
+// }
+
+// uint32_t Tableau::numNonZeroEntriesByRow() const {
+// uint32_t rowSum = 0;
+// ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
+// for(; i != end; ++i){
+// ArithVar basic = *i;
+// rowSum += getRowLength(basic);
+// }
+// return rowSum;
+// }
+
+// uint32_t Tableau::numNonZeroEntriesByCol() const {
+// uint32_t colSum = 0;
+// VectorSizeTable::const_iterator i = d_colLengths.begin();
+// VectorSizeTable::const_iterator end = d_colLengths.end();
+// for(; i != end; ++i){
+// colSum += *i;
+// }
+// return colSum;
+// }
+
+
+// EntryID Tableau::findOnRow(ArithVar row, ArithVar col){
+// for(RowIterator i = rowIterator(row); !i.atEnd(); ++i){
+// EntryID id = i.getID();
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+
+// if(colVar == col){
+// return id;
+// }
+// }
+// return ENTRYID_SENTINEL;
+// }
+
+// EntryID Tableau::findOnCol(ArithVar row, ArithVar col){
+// for(ColIterator i = colIterator(col); !i.atEnd(); ++i){
+// EntryID id = i.getID();
+// const TableauEntry& entry = *i;
+// ArithVar rowVar = entry.getRowVar();
+
+// if(rowVar == row){
+// return id;
+// }
+// }
+// return ENTRYID_SENTINEL;
+// }
+
+// const TableauEntry& Tableau::findEntry(ArithVar row, ArithVar col){
+// bool colIsShorter = getColLength(col) < getRowLength(row);
+// EntryID id = colIsShorter ? findOnCol(row,col) : findOnRow(row,col);
+// if(id == ENTRYID_SENTINEL){
+// return d_failedFind;
+// }else{
+// return d_entryManager.get(id);
+// }
+// }
+
+// void Tableau::removeRow(ArithVar basic){
+// RowIterator i = rowIterator(basic);
+// while(!i.atEnd()){
+// EntryID id = i.getID();
+// ++i;
+// removeEntry(id);
+// }
+// d_basicVariables.remove(basic);
+// }
+
+// void Tableau::loadRowIntoMergeBuffer(ArithVar basic){
+// Assert(mergeBufferIsEmpty());
+// for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+// EntryID id = i.getID();
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+// d_mergeBuffer[colVar] = make_pair(id, false);
+// }
+// }
+
+// void Tableau::emptyRowFromMergeBuffer(ArithVar basic){
+// Assert(isBasic(basic));
+// for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+// Assert(d_mergeBuffer[colVar].first == i.getID());
+// d_mergeBuffer[colVar] = make_pair(ENTRYID_SENTINEL, false);
+// }
+
+// Assert(mergeBufferIsEmpty());
+// }
+
+
+/**
+ * Changes basic to newbasic (a variable on the row).
+ */
+void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){
+ Assert(isBasic(basicOld));
+ Assert(!isBasic(basicNew));
+
+ RowIndex rid = basicToRowIndex(basicOld);
+
+ EntryID newBasicID = findOnRow(rid, basicNew);
+
+ Assert(newBasicID != ENTRYID_SENTINEL);
+
+ Tableau::Entry& newBasicEntry = d_entries.get(newBasicID);
+ Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
+
+ for(RowIterator i = basicRowIterator(basicOld); !i.atEnd(); ++i){
+ EntryID id = i.getID();
+ Tableau::Entry& entry = d_entries.get(id);
+
+ entry.getCoefficient() *= negInverseA_rs;
+ }
+
+ d_basic2RowIndex.remove(basicOld);
+ d_basic2RowIndex.set(basicNew, rid);
+ d_rowIndex2basic[rid] = basicNew;
+}
+
+// void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){
+// Assert(coeff != 0);
+
+// EntryID newId = d_entryManager.newEntry();
+// TableauEntry& newEntry = d_entryManager.get(newId);
+// newEntry = TableauEntry( row, col,
+// d_rowHeads[row], d_colHeads[col],
+// ENTRYID_SENTINEL, ENTRYID_SENTINEL,
+// coeff);
+// Assert(newEntry.getCoefficient() != 0);
+
+// Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << endl;
+
+// ++d_entriesInUse;
+
+// if(d_rowHeads[row] != ENTRYID_SENTINEL)
+// d_entryManager.get(d_rowHeads[row]).setPrevRowID(newId);
+
+// if(d_colHeads[col] != ENTRYID_SENTINEL)
+// d_entryManager.get(d_colHeads[col]).setPrevColID(newId);
+
+// d_rowHeads[row] = newId;
+// d_colHeads[col] = newId;
+// ++d_rowLengths[row];
+// ++d_colLengths[col];
+// }
+
+// void Tableau::removeEntry(EntryID id){
+// Assert(d_entriesInUse > 0);
+// --d_entriesInUse;
+
+// TableauEntry& entry = d_entryManager.get(id);
+
+// ArithVar row = entry.getRowVar();
+// ArithVar col = entry.getColVar();
+
+// Assert(d_rowLengths[row] > 0);
+// Assert(d_colLengths[col] > 0);
+
+
+// --d_rowLengths[row];
+// --d_colLengths[col];
+
+// EntryID prevRow = entry.getPrevRowID();
+// EntryID prevCol = entry.getPrevColID();
+
+// EntryID nextRow = entry.getNextRowID();
+// EntryID nextCol = entry.getNextColID();
+
+// if(d_rowHeads[row] == id){
+// d_rowHeads[row] = nextRow;
+// }
+// if(d_colHeads[col] == id){
+// d_colHeads[col] = nextCol;
+// }
+
+// entry.markBlank();
+
+// if(prevRow != ENTRYID_SENTINEL){
+// d_entryManager.get(prevRow).setNextRowID(nextRow);
+// }
+// if(nextRow != ENTRYID_SENTINEL){
+// d_entryManager.get(nextRow).setPrevRowID(prevRow);
+// }
+
+// if(prevCol != ENTRYID_SENTINEL){
+// d_entryManager.get(prevCol).setNextColID(nextCol);
+// }
+// if(nextCol != ENTRYID_SENTINEL){
+// d_entryManager.get(nextCol).setPrevColID(prevCol);
+// }
+
+// d_entryManager.freeEntry(id);
+// }
+
+// void Tableau::rowPlusRowTimesConstant(ArithVar basicTo, const Rational& c, ArithVar basicFrom){
+
+// Debug("tableau") << "rowPlusRowTimesConstant("
+// << basicTo << "," << c << "," << basicFrom << ")"
+// << endl;
+
+// Assert(debugNoZeroCoefficients(basicTo));
+// Assert(debugNoZeroCoefficients(basicFrom));
+
+// Assert(c != 0);
+// Assert(isBasic(basicTo));
+// Assert(isBasic(basicFrom));
+// Assert( d_usedList.empty() );
+
+
+// RowIterator i = rowIterator(basicTo);
+// while(!i.atEnd()){
+// EntryID id = i.getID();
+// TableauEntry& entry = d_entryManager.get(id);
+// ArithVar colVar = entry.getColVar();
+
+// ++i;
+// if(bufferPairIsNotEmpty(d_mergeBuffer[colVar])){
+// d_mergeBuffer[colVar].second = true;
+// d_usedList.push_back(colVar);
+
+// EntryID inOtherRow = d_mergeBuffer[colVar].first;
+// const TableauEntry& other = d_entryManager.get(inOtherRow);
+// entry.getCoefficient() += c * other.getCoefficient();
+
+// if(entry.getCoefficient().sgn() == 0){
+// removeEntry(id);
+// }
+// }
+// }
+
+// for(RowIterator i = rowIterator(basicFrom); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+
+// if(!(d_mergeBuffer[colVar]).second){
+// Rational newCoeff = c * entry.getCoefficient();
+// addEntry(basicTo, colVar, newCoeff);
+// }
+// }
+
+// clearUsedList();
+
+// if(Debug.isOn("tableau")) { printTableau(); }
+// }
+
+// void Tableau::clearUsedList(){
+// ArithVarArray::iterator i, end;
+// for(i = d_usedList.begin(), end = d_usedList.end(); i != end; ++i){
+// ArithVar pos = *i;
+// d_mergeBuffer[pos].second = false;
+// }
+// d_usedList.clear();
+// }
+
+void Tableau::addRow(ArithVar basic,
+ const std::vector<Rational>& coefficients,
+ const std::vector<ArithVar>& variables)
+{
+ Assert(coefficients.size() == variables.size() );
+ Assert(!isBasic(basic));
+
+ RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables);
+ addEntry(newRow, basic, Rational(-1));
+
+ Assert(d_rowIndex2basic.size() == newRow);
+
+ d_basic2RowIndex.set(basic, newRow);
+ d_rowIndex2basic.push_back(basic);
+
+
+ if(Debug.isOn("matrix")){ printMatrix(); }
+
+ vector<Rational>::const_iterator coeffIter = coefficients.begin();
+ vector<ArithVar>::const_iterator varsIter = variables.begin();
+ vector<ArithVar>::const_iterator varsEnd = variables.end();
+ for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+ ArithVar var = *varsIter;
+
+ if(isBasic(var)){
+ Rational coeff = *coeffIter;
+
+ RowIndex ri = basicToRowIndex(var);
+
+ loadRowIntoBuffer(ri);
+ rowPlusBufferTimesConstant(newRow, coeff);
+ clearBuffer();
+ }
+ }
+
+ if(Debug.isOn("matrix")) { printMatrix(); }
+
+ Assert(debugNoZeroCoefficients(newRow));
+ Assert(debugMatchingCountsForRow(newRow));
+ Assert(getColLength(basic) == 1);
+}
+
+// bool Tableau::debugNoZeroCoefficients(ArithVar basic){
+// for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// if(entry.getCoefficient() == 0){
+// return false;
+// }
+// }
+// return true;
+// }
+// bool Tableau::debugMatchingCountsForRow(ArithVar basic){
+// for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+// uint32_t count = debugCountColLength(colVar);
+// Debug("tableau") << "debugMatchingCountsForRow "
+// << basic << ":" << colVar << " " << count
+// <<" "<< d_colLengths[colVar] << endl;
+// if( count != d_colLengths[colVar] ){
+// return false;
+// }
+// }
+// return true;
+// }
+
+
+// uint32_t Tableau::debugCountColLength(ArithVar var){
+// Debug("tableau") << var << " ";
+// uint32_t count = 0;
+// for(ColIterator i=colIterator(var); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// Debug("tableau") << "(" << entry.getRowVar() << ", " << i.getID() << ") ";
+// ++count;
+// }
+// Debug("tableau") << endl;
+// return count;
+// }
+
+// uint32_t Tableau::debugCountRowLength(ArithVar var){
+// uint32_t count = 0;
+// for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){
+// ++count;
+// }
+// return count;
+// }
+
+/*
+void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{
+ for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
+ ArithVar var = (*i).getArithVar();
+ const Rational& q = (*i).getCoefficient();
+ if(var != basic()){
+ variables.push_back(var);
+ coefficients.push_back(q);
+ }
+ }
+ }*/
+
+// Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){
+// using namespace CVC4::kind;
+
+// Assert(getRowLength(basic) >= 2);
+
+// vector<Node> nonBasicPairs;
+// for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
+// const TableauEntry& entry = *i;
+// ArithVar colVar = entry.getColVar();
+// if(colVar == basic) continue;
+// Node var = (map.find(colVar))->second;
+// Node coeff = mkRationalNode(entry.getCoefficient());
+
+// Node mult = NodeBuilder<2>(MULT) << coeff << var;
+// nonBasicPairs.push_back(mult);
+// }
+
+// Node sum = Node::null();
+// if(nonBasicPairs.size() == 1 ){
+// sum = nonBasicPairs.front();
+// }else{
+// Assert(nonBasicPairs.size() >= 2);
+// NodeBuilder<> sumBuilder(PLUS);
+// sumBuilder.append(nonBasicPairs);
+// sum = sumBuilder;
+// }
+// Node basicVar = (map.find(basic))->second;
+// return NodeBuilder<2>(EQUAL) << basicVar << sum;
+// }
+
+// double Tableau::densityMeasure() const{
+// Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
+// Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
+
+// uint32_t n = getNumRows();
+// if(n == 0){
+// return 1.0;
+// }else {
+// uint32_t s = numNonZeroEntries();
+// uint32_t m = d_colHeads.size();
+// uint32_t divisor = (n *(m - n + 1));
+
+// Assert(n >= 1);
+// Assert(m >= n);
+// Assert(divisor > 0);
+// Assert(divisor >= s);
+
+// return (double(s)) / divisor;
+// }
+// }
+
+// void TableauEntryManager::freeEntry(EntryID id){
+// Assert(get(id).blank());
+// Assert(d_size > 0);
+
+// d_freedEntries.push(id);
+// --d_size;
+// }
+
+// EntryID TableauEntryManager::newEntry(){
+// EntryID newId;
+// if(d_freedEntries.empty()){
+// newId = d_entries.size();
+// d_entries.push_back(TableauEntry());
+// }else{
+// newId = d_freedEntries.front();
+// d_freedEntries.pop();
+// }
+// ++d_size;
+// return newId;
+// }
+
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file matrix.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sparse matrix implementations for different types.
+ **
+ ** Sparse matrix implementations for different types.
+ ** This defines Matrix<T>, IntegerEqualityTables and Tableau.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "util/index.h"
+#include "util/dense_map.h"
+
+#include "theory/arith/arithvar.h"
+#include "theory/arith/normal_form.h"
+
+#include <queue>
+#include <vector>
+#include <utility>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef Index EntryID;
+const EntryID ENTRYID_SENTINEL = std::numeric_limits<EntryID>::max();
+
+typedef Index RowIndex;
+const RowIndex ROW_INDEX_SENTINEL = std::numeric_limits<RowIndex>::max();
+
+template<class T>
+class MatrixEntry {
+private:
+ RowIndex d_rowIndex;
+ ArithVar d_colVar;
+
+ EntryID d_nextRow;
+ EntryID d_nextCol;
+
+ EntryID d_prevRow;
+ EntryID d_prevCol;
+
+ T d_coefficient;
+
+public:
+ MatrixEntry():
+ d_rowIndex(ROW_INDEX_SENTINEL),
+ d_colVar(ARITHVAR_SENTINEL),
+ d_nextRow(ENTRYID_SENTINEL),
+ d_nextCol(ENTRYID_SENTINEL),
+ d_prevRow(ENTRYID_SENTINEL),
+ d_prevCol(ENTRYID_SENTINEL),
+ d_coefficient()
+ {}
+
+ MatrixEntry(RowIndex row, ArithVar col, const T& coeff):
+ d_rowIndex(row),
+ d_colVar(col),
+ d_nextRow(ENTRYID_SENTINEL),
+ d_nextCol(ENTRYID_SENTINEL),
+ d_prevRow(ENTRYID_SENTINEL),
+ d_prevCol(ENTRYID_SENTINEL),
+ d_coefficient(coeff)
+ {}
+
+private:
+ bool unusedConsistent() const {
+ return
+ (d_rowIndex == ROW_INDEX_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
+ (d_rowIndex != ROW_INDEX_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
+ }
+
+public:
+
+ EntryID getNextRowEntryID() const {
+ return d_nextRow;
+ }
+
+ EntryID getNextColEntryID() const {
+ return d_nextCol;
+ }
+ EntryID getPrevRowEntryID() const {
+ return d_prevRow;
+ }
+
+ EntryID getPrevColEntryID() const {
+ return d_prevCol;
+ }
+
+ void setNextRowEntryID(EntryID id) {
+ d_nextRow = id;
+ }
+ void setNextColEntryID(EntryID id) {
+ d_nextCol = id;
+ }
+ void setPrevRowEntryID(EntryID id) {
+ d_prevRow = id;
+ }
+ void setPrevColEntryID(EntryID id) {
+ d_prevCol = id;
+ }
+
+ RowIndex getRowIndex() const{
+ return d_rowIndex;
+ }
+
+ ArithVar getColVar() const{
+ return d_colVar;
+ }
+
+ const T& getCoefficient() const {
+ return d_coefficient;
+ }
+
+ T& getCoefficient(){
+ return d_coefficient;
+ }
+
+ void setCoefficient(const T& t){
+ d_coefficient = t;
+ }
+
+ void markBlank() {
+ d_rowIndex = ROW_INDEX_SENTINEL;
+ d_colVar = ARITHVAR_SENTINEL;
+ }
+
+ bool blank() const{
+ Assert(unusedConsistent());
+
+ return d_rowIndex == ROW_INDEX_SENTINEL;
+ }
+}; /* class MatrixEntry<T> */
+
+template<class T>
+class MatrixEntryVector {
+private:
+ typedef MatrixEntry<T> EntryType;
+ typedef std::vector<EntryType> EntryArray;
+
+ EntryArray d_entries;
+ std::queue<EntryID> d_freedEntries;
+
+ uint32_t d_size;
+
+public:
+ MatrixEntryVector():
+ d_entries(), d_freedEntries(), d_size(0)
+ {}
+
+ const EntryType& operator[](EntryID id) const{
+ Assert(inBounds(id));
+ return d_entries[id];
+ }
+
+ EntryType& get(EntryID id){
+ Assert(inBounds(id));
+ return d_entries[id];
+ }
+
+ void freeEntry(EntryID id){
+ Assert(get(id).blank());
+ Assert(d_size > 0);
+
+ d_freedEntries.push(id);
+ --d_size;
+ }
+
+ EntryID newEntry(){
+ EntryID newId;
+ if(d_freedEntries.empty()){
+ newId = d_entries.size();
+ d_entries.push_back(MatrixEntry<T>());
+ }else{
+ newId = d_freedEntries.front();
+ d_freedEntries.pop();
+ }
+ ++d_size;
+ return newId;
+ }
+
+ uint32_t size() const{ return d_size; }
+ uint32_t capacity() const{ return d_entries.capacity(); }
+
+
+private:
+ bool inBounds(EntryID id) const{
+ return id < d_entries.size();
+ }
+}; /* class MatrixEntryVector<T> */
+
+template <class T, bool isRow>
+class MatrixVector {
+private:
+ EntryID d_head;
+ uint32_t d_size;
+
+ MatrixEntryVector<T>* d_entries;
+
+ class Iterator {
+ private:
+ EntryID d_curr;
+ const MatrixEntryVector<T>* d_entries;
+
+ public:
+ Iterator(EntryID start, const MatrixEntryVector<T>* entries) :
+ d_curr(start), d_entries(entries)
+ {}
+
+ public:
+
+ EntryID getID() const {
+ return d_curr;
+ }
+
+ const MatrixEntry<T>& operator*() const{
+ Assert(!atEnd());
+ return (*d_entries)[d_curr];
+ }
+
+ Iterator& operator++(){
+ Assert(!atEnd());
+ const MatrixEntry<T>& entry = (*d_entries)[d_curr];
+ d_curr = isRow ? entry.getNextRowEntryID() : entry.getNextColEntryID();
+ return *this;
+ }
+
+ bool atEnd() const {
+ return d_curr == ENTRYID_SENTINEL;
+ }
+
+ bool operator==(const Iterator& i) const{
+ return d_curr == i.d_curr && d_entries == i.d_entries;
+ }
+
+ bool operator!=(const Iterator& i) const{
+ return !(d_curr == i.d_curr && d_entries == i.d_entries);
+ }
+ }; /* class MatrixVector<T, isRow>::Iterator */
+
+public:
+ MatrixVector(MatrixEntryVector<T>* mev)
+ : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev)
+ {}
+
+ MatrixVector(EntryID head, uint32_t size, MatrixEntryVector<T>* mev)
+ : d_head(head), d_size(size), d_entries(mev)
+ {}
+
+ typedef Iterator const_iterator;
+ const_iterator begin() const {
+ return Iterator(d_head, d_entries);
+ }
+ const_iterator end() const {
+ return Iterator(ENTRYID_SENTINEL, d_entries);
+ }
+
+ EntryID getHead() const { return d_head; }
+
+ uint32_t getSize() const { return d_size; }
+
+ void insert(EntryID newId){
+ if(isRow){
+ d_entries->get(newId).setNextRowEntryID(d_head);
+
+ if(d_head != ENTRYID_SENTINEL){
+ d_entries->get(d_head).setPrevRowEntryID(newId);
+ }
+ }else{
+ d_entries->get(newId).setNextColEntryID(d_head);
+
+ if(d_head != ENTRYID_SENTINEL){
+ d_entries->get(d_head).setPrevColEntryID(newId);
+ }
+ }
+
+ d_head = newId;
+ ++d_size;
+ }
+ void remove(EntryID id){
+ Assert(d_size > 0);
+ --d_size;
+ if(isRow){
+ EntryID prevRow = d_entries->get(id).getPrevRowEntryID();
+ EntryID nextRow = d_entries->get(id).getNextRowEntryID();
+
+ if(d_head == id){
+ d_head = nextRow;
+ }
+ if(prevRow != ENTRYID_SENTINEL){
+ d_entries->get(prevRow).setNextRowEntryID(nextRow);
+ }
+ if(nextRow != ENTRYID_SENTINEL){
+ d_entries->get(nextRow).setPrevRowEntryID(prevRow);
+ }
+ }else{
+ EntryID prevCol = d_entries->get(id).getPrevColEntryID();
+ EntryID nextCol = d_entries->get(id).getNextColEntryID();
+
+ if(d_head == id){
+ d_head = nextCol;
+ }
+
+ if(prevCol != ENTRYID_SENTINEL){
+ d_entries->get(prevCol).setNextColEntryID(nextCol);
+ }
+ if(nextCol != ENTRYID_SENTINEL){
+ d_entries->get(nextCol).setPrevColEntryID(prevCol);
+ }
+ }
+ }
+}; /* class MatrixVector<T, isRow> */
+
+template <class T>
+ class RowVector : public MatrixVector<T, true>
+{
+private:
+ typedef MatrixVector<T, true> SuperT;
+public:
+ typedef typename SuperT::const_iterator const_iterator;
+
+ RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
+};
+
+template <class T>
+ class ColumnVector : public MatrixVector<T, false>
+{
+private:
+ typedef MatrixVector<T, false> SuperT;
+public:
+ typedef typename SuperT::const_iterator const_iterator;
+
+ ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
+};
+
+template <class T>
+class Matrix {
+protected:
+
+ typedef MatrixEntry<T> Entry;
+
+ typedef CVC4::theory::arith::RowVector<T> RowVectorT;
+ typedef typename RowVectorT::const_iterator RowIterator;
+
+ typedef CVC4::theory::arith::ColumnVector<T> ColumnVectorT;
+ typedef typename ColumnVectorT::const_iterator ColIterator;
+
+ // RowTable : RowID |-> RowVector
+ typedef std::vector< RowVectorT > RowTable;
+ RowTable d_rows;
+
+ // ColumnTable : ArithVar |-> ColumnVector
+ typedef std::vector< ColumnVectorT > ColumnTable;
+ ColumnTable d_columns;
+
+ /* The merge buffer is used to store a row in order to optimize row addition. */
+ typedef std::pair<EntryID, bool> PosUsedPair;
+ typedef DenseMap< PosUsedPair > RowToPosUsedPairMap;
+ RowToPosUsedPairMap d_mergeBuffer;
+
+ /* The row that is in the merge buffer. */
+ RowIndex d_rowInMergeBuffer;
+
+ uint32_t d_entriesInUse;
+ MatrixEntryVector<T> d_entries;
+
+ T d_zero;
+
+public:
+ /**
+ * Constructs an empty Matrix.
+ */
+ Matrix()
+ : d_rows(),
+ d_columns(),
+ d_mergeBuffer(),
+ d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
+ d_entriesInUse(0),
+ d_entries(),
+ d_zero(0)
+ {}
+
+ Matrix(const T& zero)
+ : d_rows(),
+ d_columns(),
+ d_mergeBuffer(),
+ d_rowInMergeBuffer(ROW_INDEX_SENTINEL),
+ d_entriesInUse(0),
+ d_entries(),
+ d_zero(zero)
+ {}
+
+
+protected:
+
+ void addEntry(RowIndex row, ArithVar col, const T& coeff){
+ Assert(coeff != 0);
+
+ EntryID newId = d_entries.newEntry();
+ Entry& newEntry = d_entries.get(newId);
+ newEntry = Entry(row, col, coeff);
+
+ Assert(newEntry.getCoefficient() != 0);
+
+ Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
+
+ ++d_entriesInUse;
+
+ d_rows[row].insert(newId);
+ d_columns[col].insert(newId);
+ }
+
+ void removeEntry(EntryID id){
+ Assert(d_entriesInUse > 0);
+ --d_entriesInUse;
+
+ Entry& entry = d_entries.get(id);
+
+ RowIndex ridx = entry.getRowIndex();
+ ArithVar col = entry.getColVar();
+
+ Assert(d_rows[ridx].getSize() > 0);
+ Assert(d_columns[col].getSize() > 0);
+
+ d_rows[ridx].remove(id);
+ d_columns[col].remove(id);
+
+ entry.markBlank();
+
+ d_entries.freeEntry(id);
+}
+
+public:
+
+ size_t getNumRows() const {
+ return d_rows.size();
+ }
+
+ size_t getNumColumns() const {
+ return d_columns.size();
+ }
+
+ void increaseSize(){
+ d_columns.push_back(ColumnVector<T>(&d_entries));
+ }
+
+ const RowVector<T>& getRow(RowIndex r) const {
+ Assert(r < d_rows.size());
+ return d_rows[r];
+ }
+
+ const ColumnVector<T>& getColumn(ArithVar v) const {
+ Assert(v < d_columns.size());
+ return d_columns[v];
+ }
+
+ uint32_t getRowLength(RowIndex r) const{
+ return getRow(r).getSize();
+ }
+
+ uint32_t getColLength(ArithVar x) const{
+ return getColumn(x).getSize();
+ }
+
+ /**
+ * Adds a row to the matrix.
+ * The new row is equivalent to:
+ * \f$\sum_i\f$ coeffs[i] * variables[i]
+ */
+ RowIndex addRow(const std::vector<T>& coeffs,
+ const std::vector<ArithVar>& variables){
+ RowIndex ridx = d_rows.size();
+ d_rows.push_back(RowVectorT(&d_entries));
+
+ std::vector<Rational>::const_iterator coeffIter = coeffs.begin();
+ std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+ std::vector<ArithVar>::const_iterator varsEnd = variables.end();
+
+ for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
+ const Rational& coeff = *coeffIter;
+ ArithVar var_i = *varsIter;
+ addEntry(ridx, var_i, coeff);
+ }
+
+ return ridx;
+ }
+
+
+ void loadRowIntoBuffer(RowIndex rid){
+ Assert(d_mergeBuffer.empty());
+ Assert(d_rowInMergeBuffer == ROW_INDEX_SENTINEL);
+
+ RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end();
+ for(; i != i_end; ++i){
+ EntryID id = i.getID();
+ const MatrixEntry<T>& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ d_mergeBuffer.set(colVar, std::make_pair(id, false));
+ }
+
+ d_rowInMergeBuffer = rid;
+ }
+
+ void clearBuffer() {
+ Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
+
+ d_rowInMergeBuffer = ROW_INDEX_SENTINEL;
+ d_mergeBuffer.purge();
+ }
+
+ /** to += mult * buffer. */
+ void rowPlusBufferTimesConstant(RowIndex to, const T& mult){
+ Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL);
+ Assert(to != ROW_INDEX_SENTINEL);
+
+ Debug("tableau") << "rowPlusRowTimesConstant("
+ << to << "," << mult << "," << d_rowInMergeBuffer << ")"
+ << std::endl;
+
+ Assert(debugNoZeroCoefficients(to));
+ Assert(debugNoZeroCoefficients(d_rowInMergeBuffer));
+
+ Assert(mult != 0);
+
+
+ RowIterator i = getRow(to).begin();
+ RowIterator i_end = getRow(to).end();
+ while(i != i_end){
+ EntryID id = i.getID();
+ Entry& entry = d_entries.get(id);
+ ArithVar colVar = entry.getColVar();
+
+ ++i;
+
+ if(d_mergeBuffer.isKey(colVar)){
+ EntryID bufferEntry = d_mergeBuffer[colVar].first;
+ Assert(!d_mergeBuffer[colVar].second);
+ d_mergeBuffer.get(colVar).second = true;
+
+ const Entry& other = d_entries.get(bufferEntry);
+ entry.getCoefficient() += mult * other.getCoefficient();
+
+ if(entry.getCoefficient() == d_zero){
+ removeEntry(id);
+ }
+ }
+ }
+
+ i = getRow(d_rowInMergeBuffer).begin();
+ i_end = getRow(d_rowInMergeBuffer).end();
+
+ for(; i != i_end; ++i){
+ const Entry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+
+ if(d_mergeBuffer[colVar].second){
+ d_mergeBuffer.get(colVar).second = false;
+ }else{
+ Assert(!(d_mergeBuffer[colVar]).second);
+ T newCoeff = mult * entry.getCoefficient();
+ addEntry(to, colVar, newCoeff);
+ }
+ }
+
+ Assert(mergeBufferIsClear());
+
+ if(Debug.isOn("matrix")) { printMatrix(); }
+ }
+
+ bool mergeBufferIsClear() const{
+ RowToPosUsedPairMap::const_iterator i = d_mergeBuffer.begin();
+ RowToPosUsedPairMap::const_iterator i_end = d_mergeBuffer.end();
+ for(; i != i_end; ++i){
+ RowIndex rid = *i;
+ if(d_mergeBuffer[rid].second){
+ return false;
+ }
+ }
+ return true;
+ }
+
+protected:
+
+ EntryID findOnRow(RowIndex rid, ArithVar column){
+ RowIterator i = d_rows[rid].begin(), i_end = d_rows[rid].end();
+ for(; i != i_end; ++i){
+ EntryID id = i.getID();
+ const MatrixEntry<T>& entry = *i;
+ ArithVar colVar = entry.getColVar();
+
+ if(colVar == column){
+ return id;
+ }
+ }
+ return ENTRYID_SENTINEL;
+ }
+
+ EntryID findOnCol(RowIndex rid, ArithVar column){
+ ColIterator i = d_columns[column].begin(), i_end = d_columns[column].end();
+ for(; i != i_end; ++i){
+ EntryID id = i.getID();
+ const MatrixEntry<T>& entry = *i;
+ RowIndex currRow = entry.getRowIndex();
+
+ if(currRow == rid){
+ return id;
+ }
+ }
+ return ENTRYID_SENTINEL;
+ }
+
+ MatrixEntry<T> d_failedFind;
+public:
+
+ /** If the find fails, isUnused is true on the entry. */
+ const MatrixEntry<T>& findEntry(RowIndex rid, ArithVar col){
+ bool colIsShorter = getColLength(col) < getRowLength(rid);
+ EntryID id = colIsShorter ? findOnCol(rid, col) : findOnRow(rid,col);
+ if(id == ENTRYID_SENTINEL){
+ return d_failedFind;
+ }else{
+ return d_entries.get(id);
+ }
+ }
+
+ /**
+ * Prints the contents of the Matrix to Debug("matrix")
+ */
+ void printMatrix() const {
+ Debug("matrix") << "Matrix::printMatrix" << std::endl;
+
+ for(RowIndex i = 0, N = d_rows.size(); i < N; ++i){
+ printRow(i);
+ }
+ }
+
+ void printRow(RowIndex rid) const {
+ Debug("matrix") << "{" << rid << ":";
+ const RowVector<T>& row = getRow(rid);
+ RowIterator i = row.begin();
+ RowIterator i_end = row.end();
+ for(; i != i_end; ++i){
+ printEntry(*i);
+ Debug("matrix") << ",";
+ }
+ Debug("matrix") << "}" << std::endl;
+ }
+
+ void printEntry(const MatrixEntry<T>& entry) const {
+ Debug("matrix") << entry.getColVar() << "*" << entry.getCoefficient();
+ }
+
+
+protected:
+
+ // static bool bufferPairIsNotEmpty(const PosUsedPair& p){
+ // return !(p.first == ENTRYID_SENTINEL && p.second == false);
+ // }
+
+ // static bool bufferPairIsEmpty(const PosUsedPair& p){
+ // return (p.first == ENTRYID_SENTINEL && p.second == false);
+ // }
+ // bool mergeBufferIsEmpty() const {
+ // return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(),
+ // d_mergeBuffer.end(),
+ // bufferPairIsNotEmpty);
+ // }
+
+public:
+ uint32_t size() const {
+ return d_entriesInUse;
+ }
+ uint32_t getNumEntriesInTableau() const {
+ return d_entries.size();
+ }
+ uint32_t getEntryCapacity() const {
+ return d_entries.capacity();
+ }
+
+ void removeRow(RowIndex rid){
+ RowIterator i = getRow(rid).begin();
+ RowIterator i_end = getRow(rid).end();
+ for(; i != i_end; ++i){
+ EntryID id = i.getID();
+ removeEntry(id);
+ }
+ }
+
+
+ Node rowAsEquality(RowIndex rid, const ArithVarToNodeMap& map){
+ using namespace CVC4::kind;
+
+ Assert(getRowLength(rid) >= 2);
+
+ std::vector<Node> pairs;
+ for(RowIterator i = getRow(rid); !i.atEnd(); ++i){
+ const Entry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+
+ Node var = (map.find(colVar))->second;
+ Node coeff = mkRationalNode(entry.getCoefficient());
+
+ Node mult = NodeBuilder<2>(MULT) << coeff << var;
+ pairs.push_back(mult);
+ }
+
+ Node sum = Node::null();
+ if(pairs.size() == 1 ){
+ sum = pairs.front();
+ }else{
+ Assert(pairs.size() >= 2);
+ NodeBuilder<> sumBuilder(PLUS);
+ sumBuilder.append(pairs);
+ sum = sumBuilder;
+ }
+ return NodeBuilder<2>(EQUAL) << sum << mkRationalNode(d_zero);
+ }
+
+ double densityMeasure() const{
+ Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
+ Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
+
+ uint32_t n = getNumRows();
+ if(n == 0){
+ return 1.0;
+ }else {
+ uint32_t s = numNonZeroEntries();
+ uint32_t m = d_columns.size();
+ uint32_t divisor = (n *(m - n + 1));
+
+ Assert(n >= 1);
+ Assert(m >= n);
+ Assert(divisor > 0);
+ Assert(divisor >= s);
+
+ return (double(s)) / divisor;
+ }
+ }
+
+protected:
+ uint32_t numNonZeroEntries() const { return size(); }
+
+ uint32_t numNonZeroEntriesByRow() const {
+ uint32_t rowSum = 0;
+ for(RowIndex rid = 0, N = d_rows.size(); rid < N; ++rid){
+ rowSum += getRowLength(rid);
+ }
+ return rowSum;
+ }
+
+ uint32_t numNonZeroEntriesByCol() const {
+ uint32_t colSum = 0;
+ for(ArithVar v = 0, N = d_columns.size(); v < N; ++v){
+ colSum += getColLength(v);
+ }
+ return colSum;
+ }
+
+
+ bool debugNoZeroCoefficients(RowIndex ridx){
+ for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+ const Entry& entry = *i;
+ if(entry.getCoefficient() == 0){
+ return false;
+ }
+ }
+ return true;
+ }
+ bool debugMatchingCountsForRow(RowIndex ridx){
+ for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+ const Entry& entry = *i;
+ ArithVar colVar = entry.getColVar();
+ uint32_t count = debugCountColLength(colVar);
+ Debug("tableau") << "debugMatchingCountsForRow "
+ << ridx << ":" << colVar << " " << count
+ <<" "<< getColLength(colVar) << std::endl;
+ if( count != getColLength(colVar) ){
+ return false;
+ }
+ }
+ return true;
+ }
+
+ uint32_t debugCountColLength(ArithVar var){
+ Debug("tableau") << var << " ";
+ uint32_t count = 0;
+ for(ColIterator i=getColumn(var).begin(); !i.atEnd(); ++i){
+ const Entry& entry = *i;
+ Debug("tableau") << "(" << entry.getRowIndex() << ", " << i.getID() << ") ";
+ ++count;
+ }
+ Debug("tableau") << std::endl;
+ return count;
+ }
+ uint32_t debugCountRowLength(RowIndex ridx){
+ uint32_t count = 0;
+ for(RowIterator i=getRow(ridx).begin(); !i.atEnd(); ++i){
+ ++count;
+ }
+ return count;
+ }
+
+};/* class Matrix<T> */
+
+
+/**
+ * A Tableau is a Rational matrix that keeps its rows in solved form.
+ * Each row has a basic variable with coefficient -1 that is solved.
+ * Tableau is optimized for pivoting.
+ * The tableau should only be updated via pivot calls.
+ */
+class Tableau : public Matrix<Rational> {
+public:
+private:
+ typedef DenseMap<RowIndex> BasicToRowMap;
+ // Set of all of the basic variables in the tableau.
+ // ArithVarMap<RowIndex> : ArithVar |-> RowIndex
+ BasicToRowMap d_basic2RowIndex;
+ // RowIndex |-> Basic Variable
+ std::vector<ArithVar> d_rowIndex2basic;
+
+public:
+
+ Tableau() : Matrix<Rational>(Rational(0)) {}
+
+ typedef Matrix<Rational>::ColIterator ColIterator;
+ typedef Matrix<Rational>::RowIterator RowIterator;
+ typedef BasicToRowMap::const_iterator BasicIterator;
+
+ typedef MatrixEntry<Rational> Entry;
+
+ bool isBasic(ArithVar v) const{
+ return d_basic2RowIndex.isKey(v);
+ }
+
+ BasicIterator beginBasic() const {
+ return d_basic2RowIndex.begin();
+ }
+ BasicIterator endBasic() const {
+ return d_basic2RowIndex.end();
+ }
+
+ RowIndex basicToRowIndex(ArithVar x) const {
+ return d_basic2RowIndex[x];
+ }
+
+ ArithVar rowIndexToBasic(RowIndex rid) const {
+ Assert(rid < d_rowIndex2basic.size());
+ return d_rowIndex2basic[rid];
+ }
+
+ ColIterator colIterator(ArithVar x) const {
+ return getColumn(x).begin();
+ }
+
+ RowIterator basicRowIterator(ArithVar basic) const {
+ return getRow(basicToRowIndex(basic)).begin();
+ }
+
+ // RowIterator rowIterator(RowIndex r) const {
+ // return getRow(r).begin();
+ // }
+
+ /**
+ * Adds a row to the tableau.
+ * The new row is equivalent to:
+ * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
+ * preconditions:
+ * basicVar is already declared to be basic
+ * basicVar does not have a row associated with it in the tableau.
+ *
+ * Note: each variables[i] does not have to be non-basic.
+ * Pivoting will be mimicked if it is basic.
+ */
+ void addRow(ArithVar basicVar,
+ const std::vector<Rational>& coeffs,
+ const std::vector<ArithVar>& variables);
+
+ /**
+ * preconditions:
+ * x_r is basic,
+ * x_s is non-basic, and
+ * a_rs != 0.
+ */
+ void pivot(ArithVar basicOld, ArithVar basicNew);
+
+ void removeBasicRow(ArithVar basic);
+
+
+private:
+ /* Changes the basic variable on the row for basicOld to basicNew. */
+ void rowPivot(ArithVar basicOld, ArithVar basicNew);
+
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){
ArithVar slack = ARITHVAR_SENTINEL;
- for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){
- const TableauEntry& entry = *iter;
+ for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
+ const Tableau::Entry& entry = *iter;
ArithVar nonbasic = entry.getColVar();
if(nonbasic == x_i) continue;
bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold;
if(!useVarOrderPivot){
- d_pivotsInRound.addMultiset(x_i);
+ d_pivotsInRound.add(x_i);
}
NodeBuilder<> conflict(kind::AND);
bool anyWeakenings = false;
- for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
+ for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
+ const Tableau::Entry& entry = *i;
ArithVar v = entry.getColVar();
const Rational& coeff = entry.getCoefficient();
bool weakening = false;
#include "theory/arith/arithvar.h"
#include "theory/arith/arith_priority_queue.h"
-#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/linear_equality.h"
#include "context/cdlist.h"
+#include "util/dense_map.h"
#include "util/options.h"
#include "util/stats.h"
NodeCallBack& d_conflictChannel;
/** Maps a variable to how many times they have been used as a pivot in the simplex search. */
- ArithVarMultiset d_pivotsInRound;
+ DenseMultiset d_pivotsInRound;
/** Stores to the DeltaRational constant 0. */
DeltaRational d_DELTA_ZERO;
+++ /dev/null
-/********************* */
-/*! \file tableau.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-#include "theory/arith/tableau.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
-
-/*
-void Tableau::addRow(ArithVar basicVar,
- const std::vector<Rational>& coeffs,
- const std::vector<ArithVar>& variables){
-
- Assert(coeffs.size() == variables.size());
-
- //The new basic variable cannot already be a basic variable
- Assert(!d_basicVariables.isMember(basicVar));
- d_basicVariables.add(basicVar);
- ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount, d_columnMatrix);
- d_rowsTable[basicVar] = row_current;
-
- //A variable in the row may have been made non-basic already.
- //If this is the case we fake pivoting this variable
- vector<ArithVar>::const_iterator varsIter = variables.begin();
- vector<ArithVar>::const_iterator varsEnd = variables.end();
-
- for( ; varsIter != varsEnd; ++varsIter){
- ArithVar var = *varsIter;
-
- if(d_basicVariables.isMember(var)){
- EntryID varID = find(basicVar, var);
- TableauEntry& entry = d_entryManager.get(varID);
- const Rational& coeff = entry.getCoefficient();
-
- loadRowIntoMergeBuffer(var);
- rowPlusRowTimesConstant(coeff, basicVar, var);
- emptyRowFromMergeBuffer(var);
- }
- }
-}
-*/
-
-/*
-ReducedRowVector* Tableau::removeRow(ArithVar basic){
- Assert(isBasic(basic));
-
- ReducedRowVector* row = d_rowsTable[basic];
-
- d_basicVariables.remove(basic);
- d_rowsTable[basic] = NULL;
-
- return row;
-}
-*/
-
-void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic){
- Assert(isBasic(oldBasic));
- Assert(!isBasic(newBasic));
- Assert(mergeBufferIsEmpty());
-
- Debug("tableau") << "Tableau::pivot(" << oldBasic <<", " << newBasic <<")" << endl;
-
- rowPivot(oldBasic, newBasic);
- loadRowIntoMergeBuffer(newBasic);
-
- ColIterator colIter = colIterator(newBasic);
- while(!colIter.atEnd()){
- EntryID id = colIter.getID();
- TableauEntry& entry = d_entryManager.get(id);
-
- ++colIter; //needs to be incremented before the variable is removed
- if(entry.getRowVar() == newBasic){ continue; }
-
- ArithVar basicTo = entry.getRowVar();
- Rational coeff = entry.getCoefficient();
-
- rowPlusRowTimesConstant(basicTo, coeff, newBasic);
- }
- emptyRowFromMergeBuffer(newBasic);
-
- //Clear the column for used for this variable
-
- Assert(mergeBufferIsEmpty());
- Assert(!isBasic(oldBasic));
- Assert(isBasic(newBasic));
- Assert(getColLength(newBasic) == 1);
-}
-
-Tableau::~Tableau(){}
-
-void Tableau::setColumnUnused(ArithVar v){
- ColIterator colIter = colIterator(v);
- while(!colIter.atEnd()){
- ++colIter;
- }
-}
-void Tableau::printTableau() const {
- Debug("tableau") << "Tableau::d_activeRows" << endl;
-
- ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
- for(; basicIter != endIter; ++basicIter){
- ArithVar basic = *basicIter;
- printRow(basic);
- }
-}
-
-void Tableau::printRow(ArithVar basic) const {
- Debug("tableau") << "{" << basic << ":";
- for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){
- const TableauEntry& entry = *entryIter;
- printEntry(entry);
- Debug("tableau") << ",";
- }
- Debug("tableau") << "}" << endl;
-}
-
-void Tableau::printEntry(const TableauEntry& entry) const {
- Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
-}
-
-uint32_t Tableau::numNonZeroEntriesByRow() const {
- uint32_t rowSum = 0;
- ArithVarSet::const_iterator i = d_basicVariables.begin(), end = d_basicVariables.end();
- for(; i != end; ++i){
- ArithVar basic = *i;
- rowSum += getRowLength(basic);
- }
- return rowSum;
-}
-
-uint32_t Tableau::numNonZeroEntriesByCol() const {
- uint32_t colSum = 0;
- VectorSizeTable::const_iterator i = d_colLengths.begin();
- VectorSizeTable::const_iterator end = d_colLengths.end();
- for(; i != end; ++i){
- colSum += *i;
- }
- return colSum;
-}
-
-
-EntryID Tableau::findOnRow(ArithVar row, ArithVar col){
- for(RowIterator i = rowIterator(row); !i.atEnd(); ++i){
- EntryID id = i.getID();
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
-
- if(colVar == col){
- return id;
- }
- }
- return ENTRYID_SENTINEL;
-}
-
-EntryID Tableau::findOnCol(ArithVar row, ArithVar col){
- for(ColIterator i = colIterator(col); !i.atEnd(); ++i){
- EntryID id = i.getID();
- const TableauEntry& entry = *i;
- ArithVar rowVar = entry.getRowVar();
-
- if(rowVar == row){
- return id;
- }
- }
- return ENTRYID_SENTINEL;
-}
-
-const TableauEntry& Tableau::findEntry(ArithVar row, ArithVar col){
- bool colIsShorter = getColLength(col) < getRowLength(row);
- EntryID id = colIsShorter ? findOnCol(row,col) : findOnRow(row,col);
- if(id == ENTRYID_SENTINEL){
- return d_failedFind;
- }else{
- return d_entryManager.get(id);
- }
-}
-
-void Tableau::removeRow(ArithVar basic){
- RowIterator i = rowIterator(basic);
- while(!i.atEnd()){
- EntryID id = i.getID();
- ++i;
- removeEntry(id);
- }
- d_basicVariables.remove(basic);
-}
-
-void Tableau::loadRowIntoMergeBuffer(ArithVar basic){
- Assert(mergeBufferIsEmpty());
- for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
- EntryID id = i.getID();
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
- d_mergeBuffer[colVar] = make_pair(id, false);
- }
-}
-
-void Tableau::emptyRowFromMergeBuffer(ArithVar basic){
- Assert(isBasic(basic));
- for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
- Assert(d_mergeBuffer[colVar].first == i.getID());
- d_mergeBuffer[colVar] = make_pair(ENTRYID_SENTINEL, false);
- }
-
- Assert(mergeBufferIsEmpty());
-}
-
-
-/**
- * Changes basic to newbasic (a variable on the row).
- */
-void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){
- Assert(mergeBufferIsEmpty());
- Assert(isBasic(basicOld));
- Assert(!isBasic(basicNew));
-
- EntryID newBasicID = findOnRow(basicOld, basicNew);
-
- Assert(newBasicID != ENTRYID_SENTINEL);
-
- TableauEntry& newBasicEntry = d_entryManager.get(newBasicID);
- Rational negInverseA_rs = -(newBasicEntry.getCoefficient().inverse());
-
- for(RowIterator i = rowIterator(basicOld); !i.atEnd(); ++i){
- EntryID id = i.getID();
- TableauEntry& entry = d_entryManager.get(id);
-
- entry.getCoefficient() *= negInverseA_rs;
- entry.setRowVar(basicNew);
- }
-
- d_rowHeads[basicNew] = d_rowHeads[basicOld];
- d_rowHeads[basicOld] = ENTRYID_SENTINEL;
-
- d_rowLengths[basicNew] = d_rowLengths[basicOld];
- d_rowLengths[basicOld] = 0;
-
- d_basicVariables.remove(basicOld);
- d_basicVariables.add(basicNew);
-}
-
-void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){
- Assert(coeff != 0);
-
- EntryID newId = d_entryManager.newEntry();
- TableauEntry& newEntry = d_entryManager.get(newId);
- newEntry = TableauEntry( row, col,
- d_rowHeads[row], d_colHeads[col],
- ENTRYID_SENTINEL, ENTRYID_SENTINEL,
- coeff);
- Assert(newEntry.getCoefficient() != 0);
-
- Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << endl;
-
- ++d_entriesInUse;
-
- if(d_rowHeads[row] != ENTRYID_SENTINEL)
- d_entryManager.get(d_rowHeads[row]).setPrevRowID(newId);
-
- if(d_colHeads[col] != ENTRYID_SENTINEL)
- d_entryManager.get(d_colHeads[col]).setPrevColID(newId);
-
- d_rowHeads[row] = newId;
- d_colHeads[col] = newId;
- ++d_rowLengths[row];
- ++d_colLengths[col];
-}
-
-void Tableau::removeEntry(EntryID id){
- Assert(d_entriesInUse > 0);
- --d_entriesInUse;
-
- TableauEntry& entry = d_entryManager.get(id);
-
- ArithVar row = entry.getRowVar();
- ArithVar col = entry.getColVar();
-
- Assert(d_rowLengths[row] > 0);
- Assert(d_colLengths[col] > 0);
-
-
- --d_rowLengths[row];
- --d_colLengths[col];
-
- EntryID prevRow = entry.getPrevRowID();
- EntryID prevCol = entry.getPrevColID();
-
- EntryID nextRow = entry.getNextRowID();
- EntryID nextCol = entry.getNextColID();
-
- if(d_rowHeads[row] == id){
- d_rowHeads[row] = nextRow;
- }
- if(d_colHeads[col] == id){
- d_colHeads[col] = nextCol;
- }
-
- entry.markBlank();
-
- if(prevRow != ENTRYID_SENTINEL){
- d_entryManager.get(prevRow).setNextRowID(nextRow);
- }
- if(nextRow != ENTRYID_SENTINEL){
- d_entryManager.get(nextRow).setPrevRowID(prevRow);
- }
-
- if(prevCol != ENTRYID_SENTINEL){
- d_entryManager.get(prevCol).setNextColID(nextCol);
- }
- if(nextCol != ENTRYID_SENTINEL){
- d_entryManager.get(nextCol).setPrevColID(prevCol);
- }
-
- d_entryManager.freeEntry(id);
-}
-
-void Tableau::rowPlusRowTimesConstant(ArithVar basicTo, const Rational& c, ArithVar basicFrom){
-
- Debug("tableau") << "rowPlusRowTimesConstant("
- << basicTo << "," << c << "," << basicFrom << ")"
- << endl;
-
- Assert(debugNoZeroCoefficients(basicTo));
- Assert(debugNoZeroCoefficients(basicFrom));
-
- Assert(c != 0);
- Assert(isBasic(basicTo));
- Assert(isBasic(basicFrom));
- Assert( d_usedList.empty() );
-
-
- RowIterator i = rowIterator(basicTo);
- while(!i.atEnd()){
- EntryID id = i.getID();
- TableauEntry& entry = d_entryManager.get(id);
- ArithVar colVar = entry.getColVar();
-
- ++i;
- if(bufferPairIsNotEmpty(d_mergeBuffer[colVar])){
- d_mergeBuffer[colVar].second = true;
- d_usedList.push_back(colVar);
-
- EntryID inOtherRow = d_mergeBuffer[colVar].first;
- const TableauEntry& other = d_entryManager.get(inOtherRow);
- entry.getCoefficient() += c * other.getCoefficient();
-
- if(entry.getCoefficient().sgn() == 0){
- removeEntry(id);
- }
- }
- }
-
- for(RowIterator i = rowIterator(basicFrom); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
-
- if(!(d_mergeBuffer[colVar]).second){
- Rational newCoeff = c * entry.getCoefficient();
- addEntry(basicTo, colVar, newCoeff);
- }
- }
-
- clearUsedList();
-
- if(Debug.isOn("tableau")) { printTableau(); }
-}
-
-void Tableau::clearUsedList(){
- ArithVarArray::iterator i, end;
- for(i = d_usedList.begin(), end = d_usedList.end(); i != end; ++i){
- ArithVar pos = *i;
- d_mergeBuffer[pos].second = false;
- }
- d_usedList.clear();
-}
-
-void Tableau::addRow(ArithVar basic,
- const std::vector<Rational>& coefficients,
- const std::vector<ArithVar>& variables)
-{
- Assert(coefficients.size() == variables.size() );
- Assert(!isBasic(basic));
-
- d_basicVariables.add(basic);
-
- if(Debug.isOn("tableau")){ printTableau(); }
-
- addEntry(basic, basic, Rational(-1));
-
- vector<Rational>::const_iterator coeffIter = coefficients.begin();
- vector<ArithVar>::const_iterator varsIter = variables.begin();
- vector<ArithVar>::const_iterator varsEnd = variables.end();
-
- for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
- const Rational& coeff = *coeffIter;
- ArithVar var_i = *varsIter;
- addEntry(basic, var_i, coeff);
- }
-
- varsIter = variables.begin();
- coeffIter = coefficients.begin();
- for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
- ArithVar var = *varsIter;
-
- if(isBasic(var)){
- Rational coeff = *coeffIter;
-
- loadRowIntoMergeBuffer(var);
- rowPlusRowTimesConstant(basic, coeff, var);
- emptyRowFromMergeBuffer(var);
- }
- }
-
- if(Debug.isOn("tableau")) { printTableau(); }
-
- Assert(debugNoZeroCoefficients(basic));
-
- Assert(debugMatchingCountsForRow(basic));
- Assert(getColLength(basic) == 1);
-}
-
-bool Tableau::debugNoZeroCoefficients(ArithVar basic){
- for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- if(entry.getCoefficient() == 0){
- return false;
- }
- }
- return true;
-}
-bool Tableau::debugMatchingCountsForRow(ArithVar basic){
- for(RowIterator i=rowIterator(basic); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
- uint32_t count = debugCountColLength(colVar);
- Debug("tableau") << "debugMatchingCountsForRow "
- << basic << ":" << colVar << " " << count
- <<" "<< d_colLengths[colVar] << endl;
- if( count != d_colLengths[colVar] ){
- return false;
- }
- }
- return true;
-}
-
-
-uint32_t Tableau::debugCountColLength(ArithVar var){
- Debug("tableau") << var << " ";
- uint32_t count = 0;
- for(ColIterator i=colIterator(var); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- Debug("tableau") << "(" << entry.getRowVar() << ", " << i.getID() << ") ";
- ++count;
- }
- Debug("tableau") << endl;
- return count;
-}
-
-uint32_t Tableau::debugCountRowLength(ArithVar var){
- uint32_t count = 0;
- for(RowIterator i=rowIterator(var); !i.atEnd(); ++i){
- ++count;
- }
- return count;
-}
-
-/*
-void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{
- for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){
- ArithVar var = (*i).getArithVar();
- const Rational& q = (*i).getCoefficient();
- if(var != basic()){
- variables.push_back(var);
- coefficients.push_back(q);
- }
- }
- }*/
-
-Node Tableau::rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map){
- using namespace CVC4::kind;
-
- Assert(getRowLength(basic) >= 2);
-
- vector<Node> nonBasicPairs;
- for(RowIterator i = rowIterator(basic); !i.atEnd(); ++i){
- const TableauEntry& entry = *i;
- ArithVar colVar = entry.getColVar();
- if(colVar == basic) continue;
- Node var = (map.find(colVar))->second;
- Node coeff = mkRationalNode(entry.getCoefficient());
-
- Node mult = NodeBuilder<2>(MULT) << coeff << var;
- nonBasicPairs.push_back(mult);
- }
-
- Node sum = Node::null();
- if(nonBasicPairs.size() == 1 ){
- sum = nonBasicPairs.front();
- }else{
- Assert(nonBasicPairs.size() >= 2);
- NodeBuilder<> sumBuilder(PLUS);
- sumBuilder.append(nonBasicPairs);
- sum = sumBuilder;
- }
- Node basicVar = (map.find(basic))->second;
- return NodeBuilder<2>(EQUAL) << basicVar << sum;
-}
-
-double Tableau::densityMeasure() const{
- Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
- Assert(numNonZeroEntriesByCol() == numNonZeroEntries());
-
- uint32_t n = getNumRows();
- if(n == 0){
- return 1.0;
- }else {
- uint32_t s = numNonZeroEntries();
- uint32_t m = d_colHeads.size();
- uint32_t divisor = (n *(m - n + 1));
-
- Assert(n >= 1);
- Assert(m >= n);
- Assert(divisor > 0);
- Assert(divisor >= s);
-
- return (double(s)) / divisor;
- }
-}
-
-void TableauEntryManager::freeEntry(EntryID id){
- Assert(get(id).blank());
- Assert(d_size > 0);
-
- d_freedEntries.push(id);
- --d_size;
-}
-
-EntryID TableauEntryManager::newEntry(){
- EntryID newId;
- if(d_freedEntries.empty()){
- newId = d_entries.size();
- d_entries.push_back(TableauEntry());
- }else{
- newId = d_freedEntries.front();
- d_freedEntries.pop();
- }
- ++d_size;
- return newId;
-}
+++ /dev/null
-/********************* */
-/*! \file tableau.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#include "expr/node.h"
-#include "expr/attribute.h"
-
-#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
-#include "theory/arith/normal_form.h"
-
-#include <queue>
-#include <vector>
-#include <utility>
-
-#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
-#define __CVC4__THEORY__ARITH__TABLEAU_H
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-typedef uint32_t EntryID;
-#define ENTRYID_SENTINEL std::numeric_limits<ArithVar>::max()
-
-class TableauEntry {
-private:
- ArithVar d_rowVar;
- ArithVar d_colVar;
-
- EntryID d_nextRow;
- EntryID d_nextCol;
-
- EntryID d_prevRow;
- EntryID d_prevCol;
-
- Rational d_coefficient;
-
-public:
- TableauEntry():
- d_rowVar(ARITHVAR_SENTINEL),
- d_colVar(ARITHVAR_SENTINEL),
- d_nextRow(ENTRYID_SENTINEL),
- d_nextCol(ENTRYID_SENTINEL),
- d_prevRow(ENTRYID_SENTINEL),
- d_prevCol(ENTRYID_SENTINEL),
- d_coefficient(0)
- {}
-
- TableauEntry(ArithVar row, ArithVar col,
- EntryID nextRowEntry, EntryID nextColEntry,
- EntryID prevRowEntry, EntryID prevColEntry,
- const Rational& coeff):
- d_rowVar(row),
- d_colVar(col),
- d_nextRow(nextRowEntry),
- d_nextCol(nextColEntry),
- d_prevRow(prevRowEntry),
- d_prevCol(prevColEntry),
- d_coefficient(coeff)
- {}
-
-private:
- bool unusedConsistent() const {
- return
- (d_rowVar == ARITHVAR_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
- (d_rowVar != ARITHVAR_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
- }
-
-public:
-
- EntryID getNextRowID() const {
- return d_nextRow;
- }
-
- EntryID getNextColID() const {
- return d_nextCol;
- }
- EntryID getPrevRowID() const {
- return d_prevRow;
- }
-
- EntryID getPrevColID() const {
- return d_prevCol;
- }
-
- void setNextRowID(EntryID id) {
- d_nextRow = id;
- }
- void setNextColID(EntryID id) {
- d_nextCol = id;
- }
- void setPrevRowID(EntryID id) {
- d_prevRow = id;
- }
- void setPrevColID(EntryID id) {
- d_prevCol = id;
- }
-
- void setRowVar(ArithVar newRowVar){
- d_rowVar = newRowVar;
- }
-
- ArithVar getRowVar() const{
- return d_rowVar;
- }
- ArithVar getColVar() const{
- return d_colVar;
- }
-
- const Rational& getCoefficient() const {
- return d_coefficient;
- }
-
- Rational& getCoefficient(){
- return d_coefficient;
- }
-
- void markBlank() {
- d_rowVar = ARITHVAR_SENTINEL;
- d_colVar = ARITHVAR_SENTINEL;
- }
-
- bool blank() const{
- Assert(unusedConsistent());
-
- return d_rowVar == ARITHVAR_SENTINEL;
- }
-};
-
-class TableauEntryManager {
-private:
- typedef std::vector<TableauEntry> EntryArray;
-
- EntryArray d_entries;
- std::queue<EntryID> d_freedEntries;
-
- uint32_t d_size;
-
-public:
- TableauEntryManager():
- d_entries(), d_freedEntries(), d_size(0)
- {}
-
- const TableauEntry& get(EntryID id) const{
- Assert(inBounds(id));
- return d_entries[id];
- }
-
- TableauEntry& get(EntryID id){
- Assert(inBounds(id));
- return d_entries[id];
- }
-
- void freeEntry(EntryID id);
-
- EntryID newEntry();
-
- uint32_t size() const{ return d_size; }
- uint32_t capacity() const{ return d_entries.capacity(); }
-
-
-private:
- bool inBounds(EntryID id) const{
- return id < d_entries.size();
- }
-};
-
-class Tableau {
-private:
-
- // VectorHeadTable : ArithVar |-> EntryID of the head of the vector
- typedef std::vector<EntryID> VectorHeadTable;
- VectorHeadTable d_rowHeads;
- VectorHeadTable d_colHeads;
-
- // VectorSizeTable : ArithVar |-> length of the vector
- typedef std::vector<uint32_t> VectorSizeTable;
- VectorSizeTable d_colLengths;
- VectorSizeTable d_rowLengths;
-
- // Set of all of the basic variables in the tableau.
- ArithVarSet d_basicVariables;
-
- typedef std::pair<EntryID, bool> PosUsedPair;
- typedef std::vector<PosUsedPair> PosUsedPairArray;
- PosUsedPairArray d_mergeBuffer;
-
- typedef std::vector<ArithVar> ArithVarArray;
- ArithVarArray d_usedList;
-
-
- uint32_t d_entriesInUse;
- TableauEntryManager d_entryManager;
-
-public:
- /**
- * Constructs an empty tableau.
- */
- Tableau() : d_entriesInUse(0) {}
- ~Tableau();
-
-private:
- void addEntry(ArithVar row, ArithVar col, const Rational& coeff);
- void removeEntry(EntryID id);
-
- template <bool isRowIterator>
- class Iterator {
- private:
- EntryID d_curr;
- const TableauEntryManager& d_entryManager;
-
- public:
- Iterator(EntryID start, const TableauEntryManager& manager) :
- d_curr(start), d_entryManager(manager)
- {}
-
- public:
-
- EntryID getID() const {
- return d_curr;
- }
-
- const TableauEntry& operator*() const{
- Assert(!atEnd());
- return d_entryManager.get(d_curr);
- }
-
- Iterator& operator++(){
- Assert(!atEnd());
- const TableauEntry& entry = d_entryManager.get(d_curr);
- d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID();
- return *this;
- }
-
- bool atEnd() const {
- return d_curr == ENTRYID_SENTINEL;
- }
- };
-
-public:
- typedef Iterator<true> RowIterator;
- typedef Iterator<false> ColIterator;
-
- double densityMeasure() const;
-
- size_t getNumRows() const {
- return d_basicVariables.size();
- }
-
- void increaseSize(){
- d_basicVariables.increaseSize();
-
- d_rowHeads.push_back(ENTRYID_SENTINEL);
- d_colHeads.push_back(ENTRYID_SENTINEL);
-
- d_colLengths.push_back(0);
- d_rowLengths.push_back(0);
-
- d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false));
- }
-
- bool isBasic(ArithVar v) const {
- return d_basicVariables.isMember(v);
- }
-
- ArithVarSet::const_iterator beginBasic() const{
- return d_basicVariables.begin();
- }
-
- ArithVarSet::const_iterator endBasic() const{
- return d_basicVariables.end();
- }
-
- RowIterator rowIterator(ArithVar v) const {
- Assert(v < d_rowHeads.size());
- EntryID head = d_rowHeads[v];
- return RowIterator(head, d_entryManager);
- }
-
- ColIterator colIterator(ArithVar v) const {
- Assert(v < d_colHeads.size());
- EntryID head = d_colHeads[v];
- return ColIterator(head, d_entryManager);
- }
-
-
- uint32_t getRowLength(ArithVar x) const{
- Assert(x < d_rowLengths.size());
- return d_rowLengths[x];
- }
-
- uint32_t getColLength(ArithVar x) const{
- Assert(x < d_colLengths.size());
- return d_colLengths[x];
- }
-
- /**
- * Adds a row to the tableau.
- * The new row is equivalent to:
- * basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
- * preconditions:
- * basicVar is already declared to be basic
- * basicVar does not have a row associated with it in the tableau.
- *
- * Note: each variables[i] does not have to be non-basic.
- * Pivoting will be mimicked if it is basic.
- */
- void addRow(ArithVar basicVar,
- const std::vector<Rational>& coeffs,
- const std::vector<ArithVar>& variables);
-
- /**
- * preconditions:
- * x_r is basic,
- * x_s is non-basic, and
- * a_rs != 0.
- */
- void pivot(ArithVar basicOld, ArithVar basicNew);
-private:
- void rowPivot(ArithVar basicOld, ArithVar basicNew);
- /** Requires merge buffer to be loaded with basicFrom and used to be empty. */
- void rowPlusRowTimesConstant(ArithVar basicTo, const Rational& coeff, ArithVar basicFrom);
-
- EntryID findOnRow(ArithVar basic, ArithVar find);
- EntryID findOnCol(ArithVar basic, ArithVar find);
-
- TableauEntry d_failedFind;
-public:
-
- /** If the find fails, isUnused is true on the entry. */
- const TableauEntry& findEntry(ArithVar row, ArithVar col);
-
- /**
- * Prints the contents of the Tableau to Debug("tableau::print")
- */
- void printTableau() const;
- void printRow(ArithVar basic) const;
- void printEntry(const TableauEntry& entry) const;
-
-
-private:
- void loadRowIntoMergeBuffer(ArithVar basic);
- void emptyRowFromMergeBuffer(ArithVar basic);
- void clearUsedList();
-
- static bool bufferPairIsNotEmpty(const PosUsedPair& p){
- return !(p.first == ENTRYID_SENTINEL && p.second == false);
- }
-
- static bool bufferPairIsEmpty(const PosUsedPair& p){
- return (p.first == ENTRYID_SENTINEL && p.second == false);
- }
- bool mergeBufferIsEmpty() const {
- return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(),
- d_mergeBuffer.end(),
- bufferPairIsNotEmpty);
- }
-
- void setColumnUnused(ArithVar v);
-
-public:
- uint32_t size() const {
- return d_entriesInUse;
- }
- uint32_t getNumEntriesInTableau() const {
- return d_entryManager.size();
- }
- uint32_t getEntryCapacity() const {
- return d_entryManager.capacity();
- }
-
- void removeRow(ArithVar basic);
- Node rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map);
-private:
- uint32_t numNonZeroEntries() const { return size(); }
- uint32_t numNonZeroEntriesByRow() const;
- uint32_t numNonZeroEntriesByCol() const;
-
-
- bool debugNoZeroCoefficients(ArithVar basic);
- bool debugMatchingCountsForRow(ArithVar basic);
- uint32_t debugCountColLength(ArithVar var);
- uint32_t debugCountRowLength(ArithVar var);
-
-};/* class Tableau */
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__ARITH__TABLEAU_H */
#include "util/rational.h"
#include "util/integer.h"
#include "util/boolean_simplification.h"
+#include "util/dense_map.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
-#include "theory/arith/arithvar_set.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/constraint.h"
Tableau::ColIterator basicIter = d_tableau.colIterator(variable);
for(; !basicIter.atEnd(); ++basicIter){
- const TableauEntry& entry = *basicIter;
+ const Tableau::Entry& entry = *basicIter;
Assert(entry.getColVar() == variable);
- ArithVar basic = entry.getRowVar();
- uint32_t rowLength = d_tableau.getRowLength(basic);
+ RowIndex ridx = entry.getRowIndex();
+ ArithVar basic = d_tableau.rowIndexToBasic(ridx);
+ uint32_t rowLength = d_tableau.getRowLength(ridx);
if((rowLength < bestRowLength) ||
(rowLength == bestRowLength && basic < bestBasic)){
bestBasic = basic;
if(d_updatedBounds.empty()){ return; }
- PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
- PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
+ DenseSet::const_iterator i = d_updatedBounds.begin();
+ DenseSet::const_iterator end = d_updatedBounds.end();
for(; i != end; ++i){
ArithVar var = *i;
if(d_tableau.isBasic(var) &&
- d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){
+ d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= Options::current()->arithPropagateMaxLength){
d_candidateBasics.softAdd(var);
}else{
Tableau::ColIterator basicIter = d_tableau.colIterator(var);
for(; !basicIter.atEnd(); ++basicIter){
- const TableauEntry& entry = *basicIter;
- ArithVar rowVar = entry.getRowVar();
+ const Tableau::Entry& entry = *basicIter;
+ RowIndex ridx = entry.getRowIndex();
+ ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
Assert(entry.getColVar() == var);
Assert(d_tableau.isBasic(rowVar));
- if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){
+ if(d_tableau.getRowLength(ridx) <= Options::current()->arithPropagateMaxLength){
d_candidateBasics.softAdd(rowVar);
}
}
d_updatedBounds.purge();
while(!d_candidateBasics.empty()){
- ArithVar candidate = d_candidateBasics.pop_back();
+ ArithVar candidate = d_candidateBasics.back();
+ d_candidateBasics.pop_back();
Assert(d_tableau.isBasic(candidate));
propagateCandidate(candidate);
}
#include "context/cdqueue.h"
#include "expr/node.h"
+#include "util/dense_map.h"
+
#include "theory/arith/arithvar.h"
-#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
-#include "theory/arith/tableau.h"
+#include "theory/arith/matrix.h"
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/linear_equality.h"
Node AssertDisequality(Constraint constraint);
/** Tracks the bounds that were updated in the current round. */
- PermissiveBackArithVarSet d_updatedBounds;
+ DenseSet d_updatedBounds;
/** Tracks the basic variables where propagatation might be possible. */
- PermissiveBackArithVarSet d_candidateBasics;
+ DenseSet d_candidateBasics;
bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
void clearUpdates(){ d_updatedBounds.purge(); }
language.h \
lemma_input_channel.h \
lemma_output_channel.h \
+ dense_map.h \
channel.h \
language.cpp \
ntuple.h \
ite_removal.cpp \
pseudoboolean.h \
pseudoboolean.cpp \
- node_visitor.h
+ node_visitor.h \
+ index.h
libutil_la_LIBADD = \
@builddir@/libutilcudd.la
--- /dev/null
+/********************* */
+/*! \file dense_map.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is an abstraction of a Map from unsigned integers to elements of type T.
+ **
+ ** This is an abstraction of a Map from an unsigned integer to elements of type T.
+ ** This class is designed to provide constant time insertion, deletion, element_of,
+ ** and fast iteration. This is done by storing backing vectors of size greater than
+ ** the maximum key. This datastructure is appropraite for heavy use datastructures
+ ** where the Keys are a dense set of integers.
+ **
+ ** T must support T(), and operator=().
+ **
+ ** The derived utility classes DenseSet and DenseMultiset are also defined.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include <boost/integer_traits.hpp>
+#include "util/index.h"
+
+namespace CVC4 {
+
+template <class T>
+class DenseMap {
+public:
+ typedef Index Key;
+ typedef std::vector<Key> KeyList;
+ typedef KeyList::const_iterator const_iterator;
+
+private:
+ //List of the keys in the dense map.
+ KeyList d_list;
+
+ typedef Index Position;
+ typedef std::vector<Position> PositionMap;
+ static const Position POSITION_SENTINEL = boost::integer_traits<Position>::const_max;
+
+ //Each Key in the set is mapped to its position in d_list.
+ //Each Key not in the set is mapped to KEY_SENTINEL
+ PositionMap d_posVector;
+
+ typedef std::vector<T> ImageMap;
+ //d_image : Key |-> T
+ ImageMap d_image;
+
+public:
+
+ DenseMap() : d_list(), d_posVector(), d_image() {}
+
+ /** Returns the number of elements in the set. */
+ size_t size() const {
+ return d_list.size();
+ }
+
+ /** Returns true if the map is empty(). */
+ bool empty() const {
+ return d_list.empty();
+ }
+
+ /**
+ * Similar to a std::vector::clear().
+ *
+ * Invalidates iterators.
+ */
+ void clear() {
+ d_list.clear();
+ d_posVector.clear();
+ d_image.clear();
+ Assert(empty());
+ }
+
+ /**
+ * Similar to a clear(), but the datastructures are not reset in size.
+ * Invalidates iterators.
+ */
+ void purge() {
+ while(!empty()){
+ pop_back();
+ }
+ Assert(empty());
+ }
+
+ /** Returns true if k is a key of this datastructure. */
+ bool isKey(Key x) const{
+ if( x >= allocated()){
+ return false;
+ }else{
+ Assert(x < allocated());
+ return d_posVector[x] != POSITION_SENTINEL;
+ }
+ }
+
+ /**
+ * Maps the key to value in the map.
+ * Invalidates iterators.
+ */
+ void set(Key key, const T& value){
+ if( key >= allocated()){
+ increaseSize(key);
+ }
+
+ if(!isKey(key)){
+ d_posVector[key] = size();
+ d_list.push_back(key);
+ }
+ d_image[key] = value;
+ }
+
+ /** Returns a mutable reference to the element mapped by key. */
+ T& get(Key key){
+ Assert(isKey(key));
+ return d_image[key];
+ }
+
+ /** Returns a const reference to the element mapped by key.*/
+ const T& operator[](Key key) const {
+ Assert(isKey(key));
+ return d_image[key];
+ }
+
+ /** Returns an iterator over the keys of the map. */
+ const_iterator begin() const{ return d_list.begin(); }
+ const_iterator end() const{ return d_list.end(); }
+
+ const KeyList& getKeys() const{
+ return d_list;
+ }
+
+ /**
+ * Removes the mapping associated with key.
+ * This changes the order of the keys.
+ *
+ * Invalidates iterators.
+ */
+ void remove(Key x){
+ Assert(isKey(x));
+ swapToBack(x);
+ Assert(d_list.back() == x);
+ pop_back();
+ }
+
+ Key back() const {
+ return d_list.back();
+ }
+
+ /** Removes the element associated with the last Key from the map. */
+ void pop_back() {
+ Assert(!empty());
+ Key atBack = back();
+ d_posVector[atBack] = POSITION_SENTINEL;
+ d_image[atBack] = T();
+ d_list.pop_back();
+ }
+
+ private:
+
+ size_t allocated() const {
+ Assert(d_posVector.size() == d_image.size());
+ return d_posVector.size();
+ }
+
+ void increaseSize(Key max){
+ Assert(max >= allocated());
+ d_posVector.resize(max+1, POSITION_SENTINEL);
+ d_image.resize(max+1);
+ }
+
+ /** Swaps a member x to the back of d_list. */
+ void swapToBack(Key x){
+ Assert(isKey(x));
+
+ Position currentPos = d_posVector[x];
+ Key atBack = back();
+
+ d_list[currentPos] = atBack;
+ d_posVector[atBack] = currentPos;
+
+ Position last = size() - 1;
+
+ d_list[last] = x;
+ d_posVector[x] = last;
+ }
+}; /* class DenseMap<T> */
+
+/**
+ * This provides an abstraction for a set of unsigned integers with similar capabilities
+ * as DenseMap. This is implemented as a light wrapper for DenseMap<bool> with an
+ * interface designed for use as a set instead of a map.
+ */
+class DenseSet {
+private:
+ typedef DenseMap<bool> BackingMap;
+ BackingMap d_map;
+public:
+ typedef BackingMap::const_iterator const_iterator;
+ typedef BackingMap::Key Element;
+
+ size_t size() const { return d_map.size(); }
+ bool empty() const { return d_map.empty(); }
+
+ /** See DenseMap's documentation. */
+ void purge() { d_map.purge(); }
+ void clear() { d_map.clear(); }
+
+ bool isMember(Element x) const{ return d_map.isKey(x); }
+
+ /**
+ * Adds an element that is not a member of the set to the set.
+ */
+ void add(Element x){
+ Assert(!isMember(x));
+ d_map.set(x, true);
+ }
+
+ /** Adds an element to the set even if it is already an element of the set. */
+ void softAdd(Element x){ d_map.set(x, true); }
+
+ /** Removes an element from the set. */
+ void remove(Element x){ d_map.remove(x); }
+
+ const_iterator begin() const{ return d_map.begin(); }
+ const_iterator end() const{ return d_map.end(); }
+
+ Element back() { return d_map.back(); }
+ void pop_back() { d_map.pop_back(); }
+}; /* class DenseSet */
+
+/**
+ * This provides an abstraction for a multiset of unsigned integers with similar
+ * capabilities as DenseMap.
+ * This is implemented as a light wrapper for DenseMap<bool> with an
+ * interface designed for use as a set instead of a map.
+ */
+class DenseMultiset {
+public:
+ typedef uint32_t CountType;
+
+private:
+ typedef DenseMap<CountType> BackingMap;
+ BackingMap d_map;
+
+public:
+ typedef BackingMap::const_iterator const_iterator;
+ typedef BackingMap::Key Element;
+
+ DenseMultiset() : d_map() {}
+
+ size_t size() const { return d_map.size(); }
+ bool empty() const { return d_map.empty(); }
+
+ void purge() { d_map.purge(); }
+ void clear() { d_map.clear(); }
+
+ bool isMember(Element x) const{ return d_map.isKey(x); }
+
+ void add(Element x){
+ if(d_map.isKey(x)){
+ d_map.set(x, d_map.get(x)+1);
+ }else{
+ d_map.set(x,1);
+ }
+ }
+
+ void remove(Element x){ return d_map.remove(x); }
+
+ CountType count(Element x) const {
+ if(d_map.isKey(x)){
+ return d_map[x];
+ }else {
+ return 0;
+ }
+ }
+
+ const_iterator begin() const{ return d_map.begin(); }
+ const_iterator end() const{ return d_map.end(); }
+ Element back() { return d_map.back(); }
+ void pop_back() { d_map.pop_back(); }
+}; /* class DenseMultiset */
+
+}/* CVC4 namespace */
--- /dev/null
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <stdint.h>
+#include <boost/static_assert.hpp>
+
+namespace CVC4 {
+
+/**
+ * Index is an unsigned integer used for array indexing.
+ *
+ * This gives a standardized type for independent pieces of code to use as an agreement.
+ */
+typedef uint32_t Index;
+
+BOOST_STATIC_ASSERT(sizeof(Index) <= sizeof(size_t));
+BOOST_STATIC_ASSERT(!std::numeric_limits<Index>::is_signed);
+
+/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)?
+ *
+ * size_t is a more appropraite choice than uint32_t as the choice is dictated by
+ * uniqueness in arrays and vectors. These correspond to size_t.
+ * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticably
+ * slower. (Limited testing suggests a ~1/16 of running time.)
+ * (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!)
+ */
+
+}; /* namespace CVC4 */
projects / cvc5.git / commitdiff