From: Tim King Date: Fri, 27 Apr 2012 14:47:10 +0000 (+0000) Subject: This merges in the branch cvc4/branches/arithmetic/matrix into trunk. X-Git-Tag: cvc5-1.0.0~8217 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f813ed144b0945334e03bfd769ea3c2cf8b75843;p=cvc5.git This merges in the branch cvc4/branches/arithmetic/matrix into trunk. - 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! --- diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 13a151ffc..d979a9c16 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -25,4 +25,5 @@ libcontext_la_SOURCES = \ cdvector.h \ cdmaybe.h \ stacking_map.h \ - stacking_vector.h + stacking_vector.h \ + cddense_set.h \ No newline at end of file diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h new file mode 100644 index 000000000..592925705 --- /dev/null +++ b/src/context/cddense_set.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \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 + +#include "context/context.h" +#include "context/cdlist_forward.h" +#include "context/cdlist.h" + +#include "util/index.h" + +namespace CVC4 { +namespace context { + +template > +class CDDenseSet { +public: + typedef Index Element; + +private: + + class RemoveIntCleanup { + private: + std::vector& d_set; + + /** + * The CleanUp functor. + */ + CleanUp d_cleanUp; + public: + RemoveIntCleanup(std::vector& 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 ElementList; + ElementList d_list; + + std::vector 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 */ diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index f9c423ef7..a029bc97b 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -27,9 +27,8 @@ libarith_la_SOURCES = \ 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 \ diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 9dd8e588a..e11a8ba53 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -25,7 +25,7 @@ #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" @@ -136,7 +136,7 @@ private: */ ArithVarArray d_varOrderQueue; - PermissiveBackArithVarSet d_varSet; + DenseSet d_varSet; /** * Reference to the arithmetic partial model for checking if a variable diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 432f9f0c2..924e91bf5 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -14,7 +14,7 @@ ** \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. **/ @@ -25,16 +25,18 @@ #define __CVC4__THEORY__ARITH__ARITHVAR_H #include -#include #include #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::max(); //Maps from Nodes -> ArithVars, and vice versa diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h deleted file mode 100644 index b9ae48b16..000000000 --- a/src/theory/arith/arithvar_set.h +++ /dev/null @@ -1,372 +0,0 @@ -/********************* */ -/*! \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 -#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 -class ArithVarSetImpl { -public: - typedef std::vector 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 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 ArithVarSet; -typedef ArithVarSetImpl PermissiveBackArithVarSet; - - -/** - * ArithVarMultiset - */ -class ArithVarMultiset { -public: - typedef std::vector 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 d_posVector; - - //Count of the number of elements in the array - std::vector 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& d_set; - public: - RemoveIntCleanup(std::vector& set) - : d_set(set) - {} - - void operator()(ArithVar* p){ - ArithVar x = *p; - Assert(d_set[x]); - d_set[x] = false; - } - }; - - std::vector d_set; - context::CDList 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 */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index e70773030..a72989498 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -5,7 +5,6 @@ #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" @@ -18,6 +17,7 @@ #include "context/cdmaybe.h" #include "util/stats.h" +#include "util/dense_map.h" namespace CVC4 { namespace theory { @@ -32,7 +32,7 @@ private: * 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; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index c5a0f534f..b92aced4e 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -23,7 +23,7 @@ #include "context/context.h" -#include "theory/arith/tableau.h" +#include "theory/arith/matrix.h" #include "theory/arith/partial_model.h" #include "util/rational.h" diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index ca7cd69c4..964d27464 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -58,10 +58,10 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){ //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); @@ -76,7 +76,6 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){ 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); @@ -90,7 +89,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio 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()); @@ -111,10 +111,11 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio //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); @@ -126,15 +127,12 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio // 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(); } } @@ -142,8 +140,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRatio 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(); @@ -168,15 +166,15 @@ void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){ * } */ 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; @@ -195,8 +193,8 @@ void LinearEqualityModule::debugCheckTableau(){ 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(); @@ -220,8 +218,8 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ 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(); @@ -233,8 +231,8 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ } 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; @@ -267,9 +265,9 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ vector 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; diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index b5d439769..7cac4c871 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -35,7 +35,7 @@ #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" diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp new file mode 100644 index 000000000..18fbf395e --- /dev/null +++ b/src/theory/arith/matrix.cpp @@ -0,0 +1,564 @@ +/********************* */ +/*! \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& coeffs, + const std::vector& 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::const_iterator varsIter = variables.begin(); + vector::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& coefficients, + const std::vector& variables) +{ + Assert(coefficients.size() == variables.size() ); + Assert(!isBasic(basic)); + + RowIndex newRow = Matrix::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::const_iterator coeffIter = coefficients.begin(); + vector::const_iterator varsIter = variables.begin(); + vector::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 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 */ diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h new file mode 100644 index 000000000..b1be48828 --- /dev/null +++ b/src/theory/arith/matrix.h @@ -0,0 +1,915 @@ +/********************* */ +/*! \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, 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 +#include +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +typedef Index EntryID; +const EntryID ENTRYID_SENTINEL = std::numeric_limits::max(); + +typedef Index RowIndex; +const RowIndex ROW_INDEX_SENTINEL = std::numeric_limits::max(); + +template +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 */ + +template +class MatrixEntryVector { +private: + typedef MatrixEntry EntryType; + typedef std::vector EntryArray; + + EntryArray d_entries; + std::queue 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()); + }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 */ + +template +class MatrixVector { +private: + EntryID d_head; + uint32_t d_size; + + MatrixEntryVector* d_entries; + + class Iterator { + private: + EntryID d_curr; + const MatrixEntryVector* d_entries; + + public: + Iterator(EntryID start, const MatrixEntryVector* entries) : + d_curr(start), d_entries(entries) + {} + + public: + + EntryID getID() const { + return d_curr; + } + + const MatrixEntry& operator*() const{ + Assert(!atEnd()); + return (*d_entries)[d_curr]; + } + + Iterator& operator++(){ + Assert(!atEnd()); + const MatrixEntry& 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::Iterator */ + +public: + MatrixVector(MatrixEntryVector* mev) + : d_head(ENTRYID_SENTINEL), d_size(0), d_entries(mev) + {} + + MatrixVector(EntryID head, uint32_t size, MatrixEntryVector* 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 */ + +template + class RowVector : public MatrixVector +{ +private: + typedef MatrixVector SuperT; +public: + typedef typename SuperT::const_iterator const_iterator; + + RowVector(MatrixEntryVector* mev) : SuperT(mev){} +}; + +template + class ColumnVector : public MatrixVector +{ +private: + typedef MatrixVector SuperT; +public: + typedef typename SuperT::const_iterator const_iterator; + + ColumnVector(MatrixEntryVector* mev) : SuperT(mev){} +}; + +template +class Matrix { +protected: + + typedef MatrixEntry Entry; + + typedef CVC4::theory::arith::RowVector RowVectorT; + typedef typename RowVectorT::const_iterator RowIterator; + + typedef CVC4::theory::arith::ColumnVector 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 PosUsedPair; + typedef DenseMap< PosUsedPair > RowToPosUsedPairMap; + RowToPosUsedPairMap d_mergeBuffer; + + /* The row that is in the merge buffer. */ + RowIndex d_rowInMergeBuffer; + + uint32_t d_entriesInUse; + MatrixEntryVector 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(&d_entries)); + } + + const RowVector& getRow(RowIndex r) const { + Assert(r < d_rows.size()); + return d_rows[r]; + } + + const ColumnVector& 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& coeffs, + const std::vector& variables){ + RowIndex ridx = d_rows.size(); + d_rows.push_back(RowVectorT(&d_entries)); + + std::vector::const_iterator coeffIter = coeffs.begin(); + std::vector::const_iterator varsIter = variables.begin(); + std::vector::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& 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& 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& entry = *i; + RowIndex currRow = entry.getRowIndex(); + + if(currRow == rid){ + return id; + } + } + return ENTRYID_SENTINEL; + } + + MatrixEntry d_failedFind; +public: + + /** If the find fails, isUnused is true on the entry. */ + const MatrixEntry& 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& 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& 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 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 */ + + +/** + * 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 { +public: +private: + typedef DenseMap BasicToRowMap; + // Set of all of the basic variables in the tableau. + // ArithVarMap : ArithVar |-> RowIndex + BasicToRowMap d_basic2RowIndex; + // RowIndex |-> Basic Variable + std::vector d_rowIndex2basic; + +public: + + Tableau() : Matrix(Rational(0)) {} + + typedef Matrix::ColIterator ColIterator; + typedef Matrix::RowIterator RowIterator; + typedef BasicToRowMap::const_iterator BasicIterator; + + typedef MatrixEntry 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& coeffs, + const std::vector& 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 */ + diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 9f48dad77..d3092c044 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -176,8 +176,8 @@ template 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; @@ -344,7 +344,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold; if(!useVarOrderPivot){ - d_pivotsInRound.addMultiset(x_i); + d_pivotsInRound.add(x_i); } @@ -476,8 +476,8 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar 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; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 7ad7734c7..6dcfccb8e 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -52,14 +52,14 @@ #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" @@ -98,7 +98,7 @@ private: 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; diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp deleted file mode 100644 index 567d8215e..000000000 --- a/src/theory/arith/tableau.cpp +++ /dev/null @@ -1,571 +0,0 @@ -/********************* */ -/*! \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& coeffs, - const std::vector& 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::const_iterator varsIter = variables.begin(); - vector::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& coefficients, - const std::vector& variables) -{ - Assert(coefficients.size() == variables.size() ); - Assert(!isBasic(basic)); - - d_basicVariables.add(basic); - - if(Debug.isOn("tableau")){ printTableau(); } - - addEntry(basic, basic, Rational(-1)); - - vector::const_iterator coeffIter = coefficients.begin(); - vector::const_iterator varsIter = variables.begin(); - vector::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 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; -} diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h deleted file mode 100644 index 1fcbdf13d..000000000 --- a/src/theory/arith/tableau.h +++ /dev/null @@ -1,409 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#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::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 EntryArray; - - EntryArray d_entries; - std::queue 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 VectorHeadTable; - VectorHeadTable d_rowHeads; - VectorHeadTable d_colHeads; - - // VectorSizeTable : ArithVar |-> length of the vector - typedef std::vector VectorSizeTable; - VectorSizeTable d_colLengths; - VectorSizeTable d_rowLengths; - - // Set of all of the basic variables in the tableau. - ArithVarSet d_basicVariables; - - typedef std::pair PosUsedPair; - typedef std::vector PosUsedPairArray; - PosUsedPairArray d_mergeBuffer; - - typedef std::vector 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 - 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 RowIterator; - typedef Iterator 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& coeffs, - const std::vector& 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 */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bc8861996..e183e0e1b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -28,13 +28,13 @@ #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" @@ -632,10 +632,11 @@ ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){ 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; @@ -1762,21 +1763,22 @@ void TheoryArith::propagateCandidates(){ 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); } } @@ -1785,7 +1787,8 @@ void TheoryArith::propagateCandidates(){ 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); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 3ed1d1941..aa7740c37 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -27,10 +27,11 @@ #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" @@ -380,10 +381,10 @@ private: 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(); } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index d52f23a9c..4945f6339 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -52,6 +52,7 @@ libutil_la_SOURCES = \ language.h \ lemma_input_channel.h \ lemma_output_channel.h \ + dense_map.h \ channel.h \ language.cpp \ ntuple.h \ @@ -73,7 +74,8 @@ libutil_la_SOURCES = \ ite_removal.cpp \ pseudoboolean.h \ pseudoboolean.cpp \ - node_visitor.h + node_visitor.h \ + index.h libutil_la_LIBADD = \ @builddir@/libutilcudd.la diff --git a/src/util/dense_map.h b/src/util/dense_map.h new file mode 100644 index 000000000..a687985f9 --- /dev/null +++ b/src/util/dense_map.h @@ -0,0 +1,294 @@ +/********************* */ +/*! \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 +#include +#include "util/index.h" + +namespace CVC4 { + +template +class DenseMap { +public: + typedef Index Key; + typedef std::vector 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 PositionMap; + static const Position POSITION_SENTINEL = boost::integer_traits::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 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 */ + +/** + * This provides an abstraction for a set of unsigned integers with similar capabilities + * as DenseMap. This is implemented as a light wrapper for DenseMap with an + * interface designed for use as a set instead of a map. + */ +class DenseSet { +private: + typedef DenseMap 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 with an + * interface designed for use as a set instead of a map. + */ +class DenseMultiset { +public: + typedef uint32_t CountType; + +private: + typedef DenseMap 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 */ diff --git a/src/util/index.h b/src/util/index.h new file mode 100644 index 000000000..0c8b0a307 --- /dev/null +++ b/src/util/index.h @@ -0,0 +1,29 @@ +#include "cvc4_private.h" + +#pragma once + +#include +#include + +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::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 */