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.


Last updated on 2010/05/19 15h:56