summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--impl/Expression.hpp49
-rw-r--r--impl/Makefile2
-rw-r--r--impl/MaxStrategy.hpp110
-rw-r--r--impl/VariableAssignment.hpp53
-rw-r--r--impl/main.cpp41
-rw-r--r--impl/systems/example.eqns4
-rw-r--r--impl/test/run5
7 files changed, 161 insertions, 103 deletions
diff --git a/impl/Expression.hpp b/impl/Expression.hpp
index c005fd6..dcf7201 100644
--- a/impl/Expression.hpp
+++ b/impl/Expression.hpp
@@ -4,6 +4,7 @@
#include <string>
#include <vector>
#include <sstream>
+#include <set>
#include "IdMap.hpp"
#include "Operator.hpp"
@@ -33,6 +34,10 @@ struct Expression {
virtual Domain eval(VariableAssignment<Domain>&) const = 0;
virtual Domain eval(VariableAssignment<Domain>& rho,
+ const MaxStrategy<Domain>&) const {
+ return eval(rho);
+ }
+ virtual Domain eval(VariableAssignment<Domain>& rho,
MaxStrategy<Domain>&) const {
return eval(rho);
}
@@ -40,6 +45,9 @@ struct Expression {
virtual void mapTo(Variable<Domain>&, IdMap<MaxExpression<Domain>, Variable<Domain>*>&) const {
}
+ virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>&) const {
+ }
+
virtual void print(std::ostream&) const = 0;
};
@@ -100,6 +108,16 @@ struct OperatorExpression : public Expression<Domain> {
return _operator.eval(argumentValues);
}
+ virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+ std::vector<Domain> argumentValues;
+ for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
+ it != _arguments.end();
+ ++it) {
+ argumentValues.push_back((*it)->eval(rho, strat));
+ }
+ return _operator.eval(argumentValues);
+ }
+
virtual Domain eval(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
std::vector<Domain> argumentValues;
for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
@@ -130,6 +148,14 @@ struct OperatorExpression : public Expression<Domain> {
}
}
+ virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>& exprs) const {
+ for (unsigned int i = 0, length = _arguments.size();
+ i < length;
+ ++i) {
+ _arguments[i]->subMaxExprs(exprs);
+ }
+ }
+
void print(std::ostream& cout) const {
cout << _operator << "(";
for (unsigned int i = 0, length = _arguments.size();
@@ -161,27 +187,33 @@ struct MaxExpression : public OperatorExpression<Domain> {
return this;
}
+ virtual Domain eval(VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+ log::fixpoint << "const MaxExpression eval" << std::endl;
+ return this->_arguments[strat.get(*this)]->eval(rho, strat);
+ }
+
virtual Domain eval(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
+ log::strategy << "const MaxExpression eval" << std::endl;
return this->_arguments[strat.get(*this)]->eval(rho, strat);
}
unsigned int bestStrategy(VariableAssignment<Domain>& rho, MaxStrategy<Domain>& strat) const {
- Domain bestValue = this->eval(rho, strat);
- unsigned int bestIndex = strat.get(*this);
+ unsigned int bestIndex = const_cast<const MaxStrategy<Domain>&>(strat).get(*this);
+ Domain bestValue = this->_arguments[bestIndex]->eval(rho, strat);
for (unsigned int i = 0, length = this->_arguments.size();
i < length;
++i) {
const Domain value = this->_arguments[i]->eval(rho, strat);
if (bestValue < value) {
- bestValue = value;
bestIndex = i;
+ bestValue = value;
}
}
return bestIndex;
}
- virtual void mapTo(Variable<Domain>& v, IdMap<MaxExpression<Domain>, Variable<Domain>*>& m) const {
+ virtual void mapTo(Variable<Domain>& v, IdMap<MaxExpression<Domain>,Variable<Domain>*>& m) const {
m[*this] = &v;
for (unsigned int i = 0, length = this->_arguments.size();
i < length;
@@ -190,6 +222,15 @@ struct MaxExpression : public OperatorExpression<Domain> {
}
}
+ virtual void subMaxExprs(std::set<const MaxExpression<Domain>*>& exprs) const {
+ exprs.insert(this);
+ for (unsigned int i = 0, length = this->_arguments.size();
+ i < length;
+ ++i) {
+ this->_arguments[i]->subMaxExprs(exprs);
+ }
+ }
+
unsigned int id() const {
return _id;
}
diff --git a/impl/Makefile b/impl/Makefile
index 6fc6f3b..ca0b37d 100644
--- a/impl/Makefile
+++ b/impl/Makefile
@@ -2,7 +2,7 @@ CC=gcc
CPP=g++
BUILD=build
PARSER=parser
-FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions
+FLAGS=-Wall -Werror -Wextra -pedantic -lantlr3c -fno-exceptions -lrt
NORMAL_FLAGS=$(FLAGS) -g -pg
OPTIMISED_FLAGS=$(FLAGS) -O3
diff --git a/impl/MaxStrategy.hpp b/impl/MaxStrategy.hpp
index d908c7b..5534597 100644
--- a/impl/MaxStrategy.hpp
+++ b/impl/MaxStrategy.hpp
@@ -9,7 +9,10 @@
template<typename Domain>
struct MaxStrategy {
virtual ~MaxStrategy() { }
- virtual unsigned int get(const MaxExpression<Domain>& e) = 0;
+ virtual unsigned int get(const MaxExpression<Domain>& e) {
+ return const_cast<const MaxStrategy<Domain>*>(this)->get(e);
+ }
+ virtual unsigned int get(const MaxExpression<Domain>& e) const = 0;
};
unsigned int stack_depth = 1;
@@ -39,44 +42,60 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
_var_influence(system.variableCount(),
IdSet<MaxExpression<Domain> >(system.maxExpressionCount())),
- _frozen(false)
+ _changed(false)
{}
- void freeze() {
- _frozen = true;
+ void setRho(DynamicVariableAssignment<Domain>& rho) {
+ _rho = &rho;
}
- void thaw() {
- _frozen = false;
+ void hasChanged(bool c) {
+ _changed = c;
}
- bool is_frozen() {
- return _frozen;
+ bool hasChanged() const {
+ return _changed;
}
- void setRho(DynamicVariableAssignment<Domain>& rho) {
- _rho = &rho;
+ unsigned int get(const MaxExpression<Domain>& e) const {
+ log::strategy << indent() << "Look up " << e << std::endl;
+ return _values[e];
}
unsigned int get(const MaxExpression<Domain>& e) {
- if (!_frozen)
- solve(e);
+ log::strategy << indent() << "Solve for " << e << std::endl;
+ solve(e);
return _values[e];
}
void invalidate(const Variable<Domain>& v) {
log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
- _stable.filter(_var_influence[v]);
+ //log::debug << indent() << " var-influence sets " << _var_influence << std::endl;
IdSet<MaxExpression<Domain> > infl = _var_influence[v];
- _var_influence[v].clear();
-
for (typename IdSet<MaxExpression<Domain> >::iterator
it = infl.begin(),
end = infl.end();
it != end;
++it) {
- solve(_system.maxExpression(*it));
+ invalidate(_system.maxExpression(*it));
+ }
+ }
+
+ void invalidate(const MaxExpression<Domain>& v) {
+ if (_stable.contains(v)) {
+ log::strategy << indent() << "Invalidating " << v << std::endl;
+ //log::debug << indent() << " influence sets " << _influence << std::endl;
+ _stable.remove(v);
+
+ IdSet<MaxExpression<Domain> > infl = _influence[v];
+ for (typename IdSet<MaxExpression<Domain> >::iterator
+ it = infl.begin(),
+ end = infl.end();
+ it != end;
+ ++it) {
+ invalidate(_system.maxExpression(*it));
+ }
}
}
@@ -96,16 +115,13 @@ private:
log::strategy << x << " => " << *x.arguments()[val] << std::endl;
IdSet<MaxExpression<Domain> > oldInfluence = _influence[x];
- _influence[x].clear();
+ //_influence[x].clear();
_values[x] = val;
+ _changed = true;
_rho->invalidate(*_system.varFromExpr(x));
-
- _rho->thaw();
- this->freeze();
- _rho->stabilise();
- _rho->freeze();
- this->thaw();
+
+ //_rho->stabilise();
_stable.filter(oldInfluence);
@@ -136,15 +152,11 @@ private:
_current(strat._system.variableCount()) {
}
const Domain operator[](const Variable<Domain>& var) {
+ // solve the strategy for this variable, too
+ _strat.solve(*_strat._system[var]);
_strat._var_influence[var].insert(_expr);
- if (_current.contains(var)) {
- return _rho[var];
- } else {
- _current.insert(var);
- Domain val = _strat._system[var]->eval(_rho, _strat);
- _current.remove(var);
- return val;
- }
+ _strat._influence[*_strat._system[var]].insert(_expr);
+ return _rho[var];
}
private:
DynamicMaxStrategy& _strat;
@@ -158,11 +170,13 @@ private:
: _strat(strat),
_expr(expr) {
}
+ unsigned int get(const MaxExpression<Domain>& e) const {
+ _strat._influence[e].insert(_expr);
+ return _strat._values[e];
+ }
unsigned int get(const MaxExpression<Domain>& e) {
_strat.solve(e);
- if (&_expr != &e) {
- _strat._influence[e].insert(_expr);
- }
+ _strat._influence[e].insert(_expr);
return _strat._values[e];
}
private:
@@ -177,7 +191,7 @@ private:
IdSet<MaxExpression<Domain> > _stable;
IdMap<MaxExpression<Domain>,IdSet<MaxExpression<Domain> > > _influence;
IdMap<Variable<Domain>,IdSet<MaxExpression<Domain> > > _var_influence;
- bool _frozen;
+ bool _changed;
};
@@ -193,19 +207,25 @@ struct Solver {
Domain solve(Variable<Domain>& var) {
MaxExpression<Domain>& rhs = *_system[var];
- do {
- _rho.has_changed(false);
+ // _rho automatically keeps up to date with changes made to the
+ // strategy, so you don't need to stabilise it
+
+ _strategy.get(rhs);
- // improve strategy
- _rho.freeze();
- _strategy.thaw();
- _strategy.get(rhs);
- // iterate fixpoint
- _strategy.freeze();
- _rho.thaw();
+ /*
+ do {
+ _strategy.hasChanged(false);
+
+ log::debug << "Stabilise assignment (toplevel)" << std::endl;
_rho.stabilise();
- } while (_rho.has_changed());
+
+ log::debug << "Improve strategy (toplevel)" << std::endl;
+ // improve strategy
+ _strategy.get(rhs);
+ log::debug << (_strategy.hasChanged() ? "Strategy has changed - loop again" : "Strategy has not changed - terminate") << std::endl;
+ } while (_strategy.hasChanged());
+ */
return _rho[var];
}
diff --git a/impl/VariableAssignment.hpp b/impl/VariableAssignment.hpp
index e074f6f..2e081e6 100644
--- a/impl/VariableAssignment.hpp
+++ b/impl/VariableAssignment.hpp
@@ -26,54 +26,31 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
_values(system.variableCount(), value),
_unstable(system.variableCount()),
_influence(system.variableCount(),
- IdSet<Variable<Domain> >(system.variableCount())),
- _frozen(false),
- _changed(false)
- {
- }
-
- void freeze() {
- _frozen = true;
- }
-
- void thaw() {
- _frozen = false;
- }
-
- bool is_frozen() const {
- return _frozen;
- }
-
- void has_changed(bool c) {
- _changed = c;
- }
-
- bool has_changed() const {
- return _changed;
- }
+ IdSet<Variable<Domain> >(system.variableCount()))
+ { }
const Domain operator[](const Variable<Domain>& var) {
- if (!_frozen)
- solve(var);
+ solve(var);
return _values[var];
}
- void stabilise() {
+ /*void stabilise() {
if (!_unstable.empty()) {
Variable<Domain>& var = _system.variable(*_unstable.begin());
solve(var);
}
- }
+ }*/
void invalidate(const Variable<Domain>& x) {
- log::fixpoint << indent() << "Invalidating " << x << std::endl;
if (!_unstable.contains(x)) {
+ log::fixpoint << indent() << "Invalidating " << x << std::endl;
+
_unstable.insert(x);
_values[x] = infinity<Domain>();
- _changed = true;
-
+
IdSet<Variable<Domain> > infl = _influence[x];
_influence[x].clear();
+
for (typename IdSet<Variable<Domain> >::iterator
it = infl.begin(),
ei = infl.end();
@@ -92,19 +69,21 @@ private:
log::fixpoint << indent() << "Stabilise " << x << std::endl;
stack_depth++;
+ // we don't want the assignment to affect the strategy, so we're
+ // going to use a const reference here
+ const DynamicMaxStrategy<Domain>& const_strat = _strategy;
DependencyAssignment assignment(*this, x);
- Domain val = _system[x]->eval(assignment, _strategy);
+ Domain val = _system[x]->eval(assignment, const_strat);
stack_depth--;
if (val != _values[x]) {
log::fixpoint << x << " = " << val << std::endl;
+
+ _strategy.invalidate(x);
IdSet<Variable<Domain> > oldInfluence = _influence[x];
_influence[x].clear();
_values[x] = val;
- _changed = true;
-
- _strategy.invalidate(x);
_unstable.absorb(oldInfluence);
@@ -141,8 +120,6 @@ private:
IdMap<Variable<Domain>, Domain> _values;
IdSet<Variable<Domain> > _unstable;
IdMap<Variable<Domain>,IdSet<Variable<Domain> > > _influence;
- bool _frozen;
- bool _changed;
};
#endif
diff --git a/impl/main.cpp b/impl/main.cpp
index 94351ec..1fed389 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -1,5 +1,6 @@
#include "Log.hpp"
#include <iostream>
+#include <iomanip>
#include <vector>
#include <sstream>
#include "Complete.hpp"
@@ -9,6 +10,8 @@
#include "MaxStrategy.hpp"
#include "VariableAssignment.hpp"
+#include <ctime>
+
extern "C" {
#include "parser/EquationSystemParser.h"
#include "parser/EquationSystemLexer.h"
@@ -134,44 +137,58 @@ int main (int argc, char* argv[]) {
EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
+ std::cerr << "Parse complete." << std::endl;
+
EquationSystem<ZBar> system;
treeToSystem<ZBar>(ret.tree, system);
log::debug << system << endl;
system.indexMaxExpressions(); // make reverse-lookup O(1) instead of O(n)
+ std::cerr << "System created and indexed." << std::endl;
+
Solver<ZBar> solver(system); // local *and* lazy. I love it!
+
+ timespec start, finish;
+ clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &start);
if (variables.size() > 0) {
- for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
- Variable<ZBar>& var = system.variable(i);
- if (variables.find(var.name()) != variables.end())
- cout << var.name() << " = " << solver.solve(var) << endl;
+ for (set<string>::iterator it = variables.begin(), ei = variables.end();
+ it != ei;
+ ++it) {
+ solver.solve(system.variable(*it));
}
} else {
for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
Variable<ZBar>& var = system.variable(i);
- cout << var.name() << " = " << solver.solve(var) << endl;
+ solver.solve(var);
}
}
+ clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &finish);
- /*
- DynamicMaxStrategy<ZBar> strategy(system);
- DynamicVariableAssignment<ZBar> rho(system, strategy);
- strategy.setRho(rho);
+ std::cerr << "System solved." << std::endl;
if (variables.size() > 0) {
for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
Variable<ZBar>& var = system.variable(i);
if (variables.find(var.name()) != variables.end())
- cout << var.name() << " = " << rho[var] << endl;
+ cout << var.name() << " = " << solver.solve(var) << endl;
}
} else {
for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
Variable<ZBar>& var = system.variable(i);
- cout << var.name() << " = " << rho[var] << endl;
+ cout << var.name() << " = " << solver.solve(var) << endl;
}
}
- */
+
+ timespec temp;
+ if ((finish.tv_nsec-start.tv_nsec)<0) {
+ temp.tv_sec = finish.tv_sec-start.tv_sec-1;
+ temp.tv_nsec = 1000000000+finish.tv_nsec-start.tv_nsec;
+ } else {
+ temp.tv_sec = finish.tv_sec-start.tv_sec;
+ temp.tv_nsec = finish.tv_nsec-start.tv_nsec;
+ }
+ cerr << "Time taken: " << temp.tv_sec << "." << setfill('0') << setw(9) << temp.tv_nsec << " seconds." << endl;
parser -> free(parser);
tokens -> free(tokens);
diff --git a/impl/systems/example.eqns b/impl/systems/example.eqns
index 71ee74a..dc59a01 100644
--- a/impl/systems/example.eqns
+++ b/impl/systems/example.eqns
@@ -1,3 +1,3 @@
-x1 = max(0, min(x1-1, x2))
+x1 = max(0, min(x1 - 1, x2))
x2 = max(0, 5+x1, x1)
-x3 = max(0, 1+x3, 0+x1)
+x3 = max(0, 1 + x3, 0 + x1)
diff --git a/impl/test/run b/impl/test/run
index 0c1886d..169edda 100644
--- a/impl/test/run
+++ b/impl/test/run
@@ -7,7 +7,10 @@ FAILED=0
echo "Testing binary: $1 in directory $DIR"
while [ -f "$DIR/$NUM.eqns" ]
do
- OUTPUT=$($1 "$DIR/$NUM.eqns")
+ OUTPUT=$(timeout 5s $1 "$DIR/$NUM.eqns" 2> /dev/null)
+ if [ $? -eq 124 ]; then
+ OUTPUT="did not terminate"
+ fi
DIFF=$(echo "$OUTPUT" | diff - "$DIR/$NUM.soln")
if [ ! -z "$DIFF" ]; then
echo "=================="
generated by cgit v1.2.3 (git 2.46.2) at 2024-12-25 06:22:13 +0000