|
smats
0.0.1
Satisfability Modulo Arithmetic Theories Symbols
|
|
|
smats
0.0.1
Satisfability Modulo Arithmetic Theories Symbols
|
#include <expression.h>
Public Member Functions | |
| Expression () | |
| Expression (const T &constant) | |
| Expression (const Variable &var) | |
| ExpressionKind | kind () const |
| Variables | variables () const |
| bool | equal_to (const Expression< T > &e) const |
| bool | less (const Expression< T > &e) const |
| bool | is_polynomial () const |
| T | evaluate (const Environment< T > &env={}) const |
| Expression< T > | evaluate_partial (const Environment< T > &env) const |
| bool | is_expanded () const |
Static Public Member Functions | |
| static Expression< T > | zero () |
| static Expression< T > | one () |
| static Expression< T > | pi () |
| static Expression< T > | e () |
| static Expression< T > | NaN () |
Friends | |
| class | ExpressionCell< T > |
| class | ExpressionAddFactory< T > |
| class | ExpressionMulFactory< T > |
Represents a symbolic form of an expression.
Its syntax tree is as follows:
E := Var | Constant | E + ... + E | E * ... * E | E / E | log(E)
| abs(E) | exp(E) | sqrt(E) | pow(E, E) | sin(E) | cos(E) | tan(E)
| asin(E) | acos(E) | atan(E) | atan2(E, E) | sinh(E) | cosh(E) | tanh(E)
| min(E, E) | max(E, E) | ceil(E) | floor(E) | if_then_else(F, E, E)
| NaN | uninterpreted_function(name, {v_1, ..., v_n})
In the implementation, Expression directly stores a shared pointer to a const ExpressionCell class that is a super-class of different kinds of symbolic expressions (i.e., ExpressionAdd, ExpressionMul, ExpressionLog, ExpressionSin), which makes it efficient to copy, move, and assign to an Expression.
The following simple simplifications are implemented:
E + 0 -> E 0 + E -> E E - 0 -> E E - E -> 0 E * 1 -> E 1 * E -> E E * 0 -> 0 0 * E -> 0 E / 1 -> E E / E -> 1 pow(E, 0) -> 1 pow(E, 1) -> E E * E -> E^2 (= pow(E, 2)) sqrt(E * E) -> |E| (= abs(E)) sqrt(E) * sqrt(E) -> E
Constant folding is implemented:
E(c1) + E(c2) -> E(c1 + c2) // c1, c2 are constants E(c1) - E(c2) -> E(c1 - c2) E(c1) * E(c2) -> E(c1 * c2) E(c1) / E(c2) -> E(c1 / c2) f(E(c)) -> E(f(c)) // c is a constant, f is a math function
For the math functions which are only defined over a restricted domain (namely, log, sqrt, pow, asin, acos), we check the domain of argument(s), and throw std::domain_error exception if a function is not well-defined for a given argument(s).
Relational operators over expressions (==, !=, <, >, <=, >=) return symbolic::Formula instead of bool. Those operations are declared in formula.h file. To check structural equality between two expressions a separate function, Expression::EqualTo, is provided.
Regarding the arithmetic of an Expression when operating on NaNs, we have the following rules:
isnan in order to fail-fast. So we provide isnan(const Expression&) for the common case of non-NaN value returning False. This way, code can fail-fast with mpq_class yet still compile with Expression.if_then_else), some of the sub-expressions may be not used in evaluation when they are in the not-taken case (for NaN reasons or any other reason). Bad values within those not-taken branches does not cause exceptions.| smats::Expression< T >::Expression | ( | ) |
Construct a new expression, Default to zero object.
| smats::Expression< T >::Expression | ( | const Variable & | var | ) |
Constructs an expression from var.
var is not a BOOLEAN variable.
|
nodiscard |
Checks structural equality.
Two expressions e1 and e2 are structurally equal when they have the same internal AST(abstract-syntax tree) representation. Please note that we can have two computationally (or extensionally) equivalent expressions which are not structurally equal. For example, consider:
\[ e1 = 2 * (x + y) \\ e2 = 2x + 2y \]
Obviously, we know that e1 and e2 are evaluated to the same value for all assignments to x and y. However, e1 and e2 are not structurally equal by the definition. Note that e1 is a multiplication expression (is_multiplication(e1) is true) while e2 is an addition expression (is_addition(e2) is true).
One main reason we use structural equality in EqualTo is due to Richardson's Theorem. It states that checking ∀x. E(x) = F(x) is undecidable when we allow sin, asin, log, exp in E and F. Read https://en.wikipedia.org/wiki/Richardson%27s_theorem for details.
Note that for polynomial cases, you can use Expand method and check if two polynomial expressions p1 and p2 are computationally equal. To do so, you check the following:
|
nodiscard |
Evaluates using a given environment (by default, an empty environment).
| std::exception | if there exists a non-random variable in this expression whose assignment is not provided by env |
| std::exception | if an unassigned random variable is detected while random_generator is nullptr |
| std::exception | if NaN is detected during evaluation. |
|
nodiscard |
Partially evaluates this expression using an environment env.
Internally, this method uses env to substitute (Variable → Constant) and call Evaluate::Substitute with it.
| std::exception | if NaN is detected during evaluation. |
|
nodiscard |
Returns true if this symbolic expression is already expanded. Expression::Expand() uses this flag to avoid calling ExpressionCell::Expand() on an pre-expanded expressions. Expression::Expand() also sets this flag before returning the result.
false does not always indicate that the expression is not expanded. This is because exact checks can be costly and we want to avoid the exact check at the construction time.
|
nodiscard |
Check whether the expression is polynomial.
|
nodiscard |
Get read-only access to the kind of the expression.
|
nodiscard |
Compare two expressions to determine the order between them.
| o | other object to compare against |
|
nodiscard |
Get read-only access to the variables of the expression.
1.11.0