inline static Expr_ptr
trace_evaluate_define(
const Trace_ptr trace,
const TraceIter step,
node_ptr define,
hash_ptr cache
)
- Evaluates a define in a given environment. Missing
dependencies are represented by FAILURE nodes.
This function is a private service of
Trace_evaluate_defines
- Side Effects None
- See Also
Trace_evaluate_defines
Expr_ptr
trace_evaluate_expr_recur(
const Trace_ptr trace,
const TraceIter step,
Expr_ptr expr,
boolean in_next,
hash_ptr cache
)
- This function is a private service of
Trace_evaluate_expr
- Side Effects None
- See Also
Trace_evaluate_expr
node_ptr
trace_make_failure(
const char* tmpl,
node_ptr symbol
)
- Private service of trace_evaluate_expr_recur
- See Also
Private
service
of
trace_evaluate_expr_recur
Expr_ptr
trace_simplify_expr(
const SymbTable_ptr st,
Expr_ptr expr
)
- MathSAT is currently required to evaluate expressions
over reals
void
trace_step_evaluate_defines(
Trace_ptr self,
const TraceIter step
)
- Evaluates define for a trace, based on assignments to
state, frozen and input variables.
If a previous value exists for a define, The mismatch
is reported to the caller by appending a failure node
describing the error to the "failures" list. If
"failures" is NULL failures are silently discarded. If
no previous value exists for a given define, assigns
the define to the calculated value according to vars
assignments. The "failures" list must be either NULL
or a valid, empty list.
0 is returned if no mismatching were detected, 1
otherwise
- Side Effects The trace is filled with defines, failures list is
populated as necessary.