Skip to content

Commit

Permalink
Added vector expressions. [#263]
Browse files Browse the repository at this point in the history
  • Loading branch information
@pietercollins
pietercollins committed Nov 30, 2024
1 parent 84ff7d2 commit 2c0a30b
Show file tree
Hide file tree
Showing 11 changed files with 700 additions and 110 deletions.
26 changes: 26 additions & 0 deletions source/algebra/vector.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,14 @@ struct DeclareVectorOperations {
template<class X1, class X2> friend Vector<InplaceDifferenceType<X1,X2>>& operator-=(Vector<X1>& v1, const Vector<X2>& v2);
template<class X1, class X2> friend Vector<InplaceProductType<X1,X2>>& operator*=(Vector<X1>& v1, X2 const& x2);
template<class X1, class X2> friend Vector<InplaceQuotientType<X1,X2>>& operator/=(Vector<X1>& v1, X2 const& x2);
template<class X> friend Vector<X> nul(Vector<X> const& v);
template<class X> friend Vector<X> pos(Vector<X> const& v);
template<class X> friend Vector<NegationType<X>> neg(Vector<X> const& v);
template<class X1, class X2> friend Vector<SumType<X1,X2>> add(Vector<X1> const& v1, Vector<X2> const& v2);
template<class X1, class X2> friend Vector<DifferenceType<X1,X2>> sub(Vector<X1> const& v1, Vector<X2> const& v2);
template<class X1, class X2> friend Vector<ProductType<Scalar<X1>,X2>> mul(X1 const& x1, Vector<X2> const& v2);
template<class X1, class X2> friend Vector<ProductType<X1,Scalar<X2>>> mul(Vector<X1> const& v1, X2 const& x2);
template<class X1, class X2> friend Vector<QuotientType<X1,Scalar<X2>>> div(Vector<X1> const& v1, X2 const& x2);
template<class X> friend decltype(abs(declval<X>())) norm(Vector<X> const& v);
template<class X> friend decltype(mag(declval<X>())) sup_norm(Vector<X> const& v);
template<class X> friend decltype(sqrt(sqr(declval<X>()))) two_norm(Vector<X> const& v);
Expand Down Expand Up @@ -297,6 +305,15 @@ class Vector
//! \brief %Scalar division.
friend template<class X1, class X2> Vector<decltype(declval<X1>()+declval<X2>())>(const Vector<X1>& v, const X2& s);

friend template<class X> Vector<X> nul(Vector<X> const& v);
friend template<class X> decltype(auto) pos(Vector<X> const& v) { return +v; }
friend template<class X> decltype(auto) neg(Vector<X> const& v) { return -v; }
friend template<class X1, class X2> decltype(auto) add(Vector<X1> const& v1, Vector<X2> const& v2) { return v1+v2; }
friend template<class X1, class X2> decltype(auto) sub(Vector<X1> const& v1, Vector<X2> const& v2) { return v1-v2; }
friend template<class X1, class X2> decltype(auto) mul(X1 const& s1, Vector<X2> const& v2) { return s1*v2; }
friend template<class X1, class X2> decltype(auto) mul(Vector<X1> const& v1, X2 const& s2) { return v1*s2; }
friend template<class X1, class X2> decltype(auto) div(Vector<X1> const& v1, X2 const& s2) { return v1/s2; }

//! \brief The supremum norm.
friend template<class X> X norm(const Vector<X>& v);
//! \brief The inner product.
Expand Down Expand Up @@ -403,6 +420,15 @@ struct ProvideVectorOperations {
for(SizeType i=0; i!=v1.size(); ++i) { v1[i]/=s2; } return v1;
}

template<class X> friend Vector<X> nul(Vector<X> const& v) { return Vector<X>(v.size(),v.zero_element()); }
template<class X> friend Vector<X> pos(Vector<X> const& v) { return +v; }
template<class X> friend Vector<NegationType<X>> neg(Vector<X> const& v) { return -v; }
template<class X1, class X2> friend Vector<SumType<X1,X2>> add(Vector<X1> const& v1, Vector<X2> const& v2) { return v1+v2; }
template<class X1, class X2> friend Vector<DifferenceType<X1,X2>> sub(Vector<X1> const& v1, Vector<X2> const& v2) { return v1-v2; }
template<class X1, class X2> friend Vector<ProductType<Scalar<X1>,X2>> mul(X1 const& s1, Vector<X2> const& v2) { return s1*v2; }
template<class X1, class X2> friend Vector<ProductType<X1,Scalar<X2>>> mul(Vector<X1> const& v1, X2 const& s2) { return v1*s2; }
template<class X1, class X2> friend Vector<QuotientType<X1,Scalar<X2>>> div(Vector<X1> const& v1, X2 const& s2) { return v1/s2; }

template<class X1, class X2> friend ArithmeticType<X1,X2> dot(const Vector<X1>& v1, const Vector<X2>& v2) {
ARIADNE_PRECONDITION(v1.size()==v2.size());
ArithmeticType<X1,X2> r=v1.zero_element()*v2.zero_element();
Expand Down
2 changes: 2 additions & 0 deletions source/numeric/operators.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,8 @@ enum class Operator::Code : ComparableEnumerationType {
XOR, // Logical exclusive or
IMPL, // Logical implication
ITOR, // Conversion of Int to Real
GET, // Subscript operator
VEC, // Vectorisation operator
PUSH,
PULL,
EQ=-6, // Equal
Expand Down
106 changes: 93 additions & 13 deletions source/symbolic/expression.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,6 @@ template<> Expression<Real>::operator ElementaryAlgebra<Real>() const {
return ElementaryAlgebra<Real>(new ElementaryAlgebraWrapper<Expression<Real>,Real>(*this));
}


template class Expression<Boolean>;
template class Expression<Kleenean>;
template class Expression<String>;
Expand Down Expand Up @@ -206,14 +205,78 @@ Expression<Real> min(Expression<Real> const& e1, Expression<Real> const& e2) {
Expression<Real> abs(Expression<Real> const& e) {
return make_expression<Real>(Abs(),e); }

Expression<RealVector> operator+(Expression<RealVector> const& e1, Expression<RealVector> const& e2) {
return make_expression<RealVector>(Add(),e1,e2); }
Expression<RealVector> operator-(Expression<RealVector> const& e1, Expression<RealVector> const& e2) {
return make_expression<RealVector>(Sub(),e1,e2); }
Expression<RealVector> operator*(Expression<Real> const& e1, Expression<RealVector> const& e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> operator*(Expression<RealVector> const& e1, Expression<Real> const& e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> operator/(Expression<RealVector> const& e1, Expression<Real> const& e2) {
return make_expression<RealVector>(Div(),e1,e2); }

Expression<RealVector>::Expression(RealVector v)
: _root(new ExpressionNode<T>(Constant<T>(v))) { }
Expression<RealVector>::Expression(Constant<RealVector> cnst)
: Expression(std::make_shared<ExpressionNode<T>>(cnst)) { }
Expression<RealVector>::Expression(Variable<RealVector> var)
: Expression(std::make_shared<ExpressionNode<T>>(var)) { }
Expression<RealVector>::Expression(Vector<Expression<Real>> ve)
: _root(std::make_shared<ExpressionNode<T>>(ve)) { }
Expression<RealVector>::Expression(RealVariables vars)
: Expression(Vector<Expression<Real>>(vars)) { }
Expression<RealVector>::Expression(InitializerList<Expression<Real>> vars)
: Expression(Vector<Expression<Real>>(vars)) { }
Operator Expression<RealVector>::op() const {
return this->node_ptr()->op(); }
SizeType Expression<RealVector>::size() const {
return this->node_ref().accept([](auto en){return _size_impl(en);}); }
Expression<Real> Expression<RealVector>::get(SizeType i) const {
return make_expression<Real>(OperatorType<Real(RealVector,SizeType)>(Get()),*this,i); }
Set<UntypedVariable> Expression<RealVector>::arguments() const {
return this->node_ref().accept([](auto s){return _arguments(s);}); }
Expression<RealVector> nul(Expression<RealVector> e) {
return make_expression<RealVector>(Nul(),e); }
Expression<RealVector> pos(Expression<RealVector> e) {
return make_expression<RealVector>(Pos(),e); }
Expression<RealVector> neg(Expression<RealVector> e) {
return make_expression<RealVector>(Neg(),e); }
Expression<RealVector> add(Expression<RealVector> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Add(),e1,e2); }
Expression<RealVector> sub(Expression<RealVector> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Sub(),e1,e2); }
Expression<RealVector> mul(Expression<Real> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> mul(Expression<RealVector> e1, Expression<Real> e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> div(Expression<RealVector> e1, Expression<Real> e2) {
return make_expression<RealVector>(Div(),e1,e2); }
Expression<RealVector> operator+(Expression<RealVector> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Add(),e1,e2); }
Expression<RealVector> operator-(Expression<RealVector> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Sub(),e1,e2); }
Expression<RealVector> operator*(Expression<Real> e1, Expression<RealVector> e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> operator*(Expression<RealVector> e1, Expression<Real> e2) {
return make_expression<RealVector>(Mul(),e1,e2); }
Expression<RealVector> operator/(Expression<RealVector> e1, Expression<Real> e2) {
return make_expression<RealVector>(Div(),e1,e2); }

OutputStream& Expression<RealVector>::_write(OutputStream& os) const {
auto writer=OperationExpressionWriter(); return os << writer(*this); }


template String evaluate(const Expression<String>& e, const Valuation<String>& x);
template Integer evaluate(const Expression<Integer>& e, const Valuation<Integer>& x);
template Real evaluate(const Expression<Real>& e, const Valuation<Real>& x);
template Boolean evaluate(const Expression<Boolean>& e, const Valuation<String>& x);
template Boolean evaluate(const Expression<Boolean>& e, const Valuation<Integer>& x);
template Kleenean evaluate(const Expression<Kleenean>& e, const Valuation<Real>& x);
template RealVector evaluate(const Expression<RealVector>& e, const Valuation<Real>& x);

template Real evaluate(Expression<Real> const&, Map<Identifier, Real> const&);
template RealVector evaluate(Expression<RealVector> const&, Map<Identifier, Real> const&);


template Set<Identifier> arguments(const Expression<Boolean>& e);
Expand All @@ -225,11 +288,13 @@ template Expression<Kleenean> substitute(const Expression<Kleenean>& e, const Va
template Expression<Kleenean> substitute(const Expression<Kleenean>& e, const Variable<Real>& v, const Real& c);
template Expression<Real> substitute(const Expression<Real>& e, const Variable<Real>& v, const Real& c);
template Expression<Real> substitute(const Expression<Real>& e, const Variable<Real>& v, const Expression<Real>& c);
template Expression<Vector<Real>> substitute(const Expression<Vector<Real>>& e, const Variable<Real>& v, const Expression<Real>& c);
template Expression<Real> substitute(const Expression<Real>& e, const List< Assignment< Variable<Real>, Expression<Real> > >& c);
template Vector<Expression<Real>> substitute(const Vector<Expression<Real>>& e, const List< Assignment< Variable<Real>, Expression<Real> > >& c);
template Expression<Kleenean> substitute(const Expression<Kleenean>& e, const List< Assignment< Variable<Real>, Expression<Real> > >& c);

template Expression<Real> simplify(const Expression<Real>& e);
template Expression<RealVector> simplify(const Expression<RealVector>& e);
template Expression<Kleenean> simplify(const Expression<Kleenean>& e);

template Void eliminate_common_subexpressions(Expression<Real>&);
Expand Down Expand Up @@ -290,6 +355,9 @@ template Bool is_variable(const Expression<Real>&, const Variable<Real>&);
template Bool identical(const Expression<Real>&, const Expression<Real>&);

template Bool is_constant_in(const Expression<Real>& e, const Set<Variable<Real>>& spc);
template Bool is_constant_in(const Expression<Vector<Real>>& e, const Set<Variable<Real>>& spc);
template Bool is_constant_in(const Vector<Expression<Real>>& e, const Set<Variable<Real>>& spc);
template Bool component_is_constant_in(const Expression<Vector<Real>>& e, SizeType i, const Set<Variable<Real>>& spc);

Bool is_affine_in(const Expression<Real>& e, const Set<Variable<Real>>& spc) {
return e.node_ref().accept([&spc](auto en){return is_affine_in(en,spc);});
Expand All @@ -301,6 +369,9 @@ Bool is_affine_in(const Vector<Expression<Real>>& e, const Set<Variable<Real>>&
}
return true;
}
Bool is_affine_in(const Expression<Vector<Real>>& ve, const Set<Variable<Real>>& spc) {
return ve.node_ref().accept([&spc](auto en){return is_affine_in(en,spc);});
}

Bool is_polynomial_in(const Expression<Real>& e, const Set<Variable<Real>>& spc) {
return e.node_ref().accept([&spc](auto en){return is_polynomial_in(en,spc);});
Expand All @@ -319,23 +390,25 @@ namespace {
typedef Expression<Real> RE; typedef Expression<Real> const& REcr;
typedef Variable<Real> const& RVcr; typedef Constant<Real> const& RCcr;

inline Bool _is_additive_in(Add, REcr e1, REcr e2, RVcr var) {
inline Bool _is_additive_in_impl(Add, REcr e1, REcr e2, RVcr var) {
return (is_additive_in(e1,var) && is_constant_in(e2,var)) || (is_constant_in(e1,var) && is_additive_in(e2,var)); }
inline Bool _is_additive_in(Sub, REcr e1, REcr e2, RVcr var) {
inline Bool _is_additive_in_impl(Sub, REcr e1, REcr e2, RVcr var) {
return is_additive_in(e1,var) && is_constant_in(e2,var); }
inline Bool _is_additive_in(Variant<Mul,Div,Max,Min>, REcr e1, REcr e2, RVcr var) { return false; }
template<class... OPS> inline Bool _is_additive_in(OperatorVariant<OPS...> const& ops, REcr e1, REcr e2, RVcr var) {
return ops.accept([&](auto op){return _is_additive_in(op,e1,e2,var);}); }

inline Bool is_additive_in(RCcr c, RVcr var) { return true; }
inline Bool is_additive_in(RVcr v, RVcr var) { return true; }
template<class OP> inline Bool is_additive_in(Symbolic<OP,RE> const&, RVcr var) { return false; }
template<class OP> inline Bool is_additive_in(Symbolic<OP,RE,Int> const&, RVcr var) { return false; }
template<class OP> inline Bool is_additive_in(Symbolic<OP,RE,RE> const& e, RVcr var) { return _is_additive_in(e._op,e._arg1,e._arg2,var); }
inline Bool _is_additive_in_impl(Variant<Mul,Div,Max,Min>, REcr e1, REcr e2, RVcr var) { return false; }
template<class... OPS> inline Bool _is_additive_in_impl(OperatorVariant<OPS...> const& ops, REcr e1, REcr e2, RVcr var) {
return ops.accept([&](auto op){return _is_additive_in_impl(op,e1,e2,var);}); }

inline Bool _is_additive_in(RCcr c, RVcr var) { return true; }
inline Bool _is_additive_in(RVcr v, RVcr var) { return true; }
template<class OP> inline Bool _is_additive_in(Symbolic<OP,RE> const&, RVcr var) { return false; }
template<class OP> inline Bool _is_additive_in(Symbolic<OP,RE,RE> const& e, RVcr var) { return _is_additive_in_impl(e._op,e._arg1,e._arg2,var); }
template<class OP> requires AGraded<OP> inline Bool _is_additive_in(Symbolic<OP,RE,Int> const&, RVcr var) { return false; }
template<class OP> requires AGetter<OP> inline Bool _is_additive_in(Symbolic<OP,Expression<RealVector>,SizeType> const&, RVcr var) {
ARIADNE_NOT_IMPLEMENTED; }
}

Bool is_additive_in(const Expression<Real>& e, const Variable<Real>& var) {
return e.node_ref().accept([&](auto en){return is_additive_in(en,var);});
return e.node_ref().accept([&](auto en){return _is_additive_in(en,var);});
}


Expand Down Expand Up @@ -436,6 +509,10 @@ template<class SPC,class CACHE> Formula<Y> _cached_make_formula_impl(const Binar
template<class SPC,class CACHE> Formula<Y> _cached_make_formula_impl(const GradedExpressionNode<R>& e, const SPC& spc, CACHE& cache) {
return make_formula<Y>(e.op(),_cached_make_formula(e.arg(),spc,cache),e.num()); }

template<class SPC,class CACHE> Formula<Y> _cached_make_formula_impl(const SymbolicType<Real(RealVector,SizeType)>& e, const SPC& spc, CACHE& cache) {
ARIADNE_NOT_IMPLEMENTED;
}

const Formula<EffectiveNumber>& _cached_make_formula(const Expression<Real>& e, const Map<Identifier,SizeType>& spc, Map< const Void*, Formula<EffectiveNumber> >& cache)
{
const ExpressionNode<Real>* eptr=&e.node_ref();
Expand Down Expand Up @@ -532,4 +609,7 @@ template OutputStream& OperatorExpressionWriter::_write(OutputStream& os, Expres
template OutputStream& OperatorExpressionWriter::_write(OutputStream& os, Expression<String> const& e) const;
template OutputStream& OperatorExpressionWriter::_write(OutputStream& os, Expression<Boolean> const& e) const;

template<> String class_name<RealVariables>() { return "RealVariables"; }
template<> String class_name<Expression<RealVector>>() { return "Expression<Vector<Real>>"; }

} // namespace Ariadne
11 changes: 9 additions & 2 deletions source/symbolic/expression.decl.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,11 @@ template<class T> class Vector;

class Identifier;

template<class T> class Vector;
template<class T> class Matrix;
using RealVector = Vector<Real>;
using RealMatrix = Matrix<Real>;

template<class T> class Constant;
template<class T> class Variable;
template<class T> class Variables;
Expand Down Expand Up @@ -74,6 +79,7 @@ using RealVariable = Variable<Real>; //!< <p/>
//! \relates Variables
//! \name Type synonyms
using RealVariables = Variables<Real>; //!< <p/>
using RealVectorVariable = Variable<RealVector>; //!< <p/>
//!@}

//!@{
Expand Down Expand Up @@ -107,6 +113,9 @@ using IntegerExpression = Expression<Integer>; //!< <p/>
using RealExpression = Expression<Real>; //!< <p/>
using RealExpressions = List<Expression<Real>>; //!< <p/>
using RealExpressionVector = Vector<Expression<Real>>; //!< <p/>
using RealVectorExpression = Expression<RealVector>;
using RealMatrixExpression = Expression<RealMatrix>;


using DiscretePredicate = Expression<Boolean>; //!< \brief A decidable predicate over discrete variables.
using ContinuousPredicate = Expression<Kleenean>; //!< \brief A quasidecidable predicate over continuous variables.
Expand Down Expand Up @@ -145,8 +154,6 @@ class DiscreteValuation;
template<class X> class ContinuousValuation;




template<class UB> class Interval;
using RealInterval = Interval<Real>;

Expand Down
Loading

0 comments on commit 2c0a30b

Please sign in to comment.