[CN] Pure term (partial) evaluation #447

ZippeyKeys12 · 2024-07-30T02:51:49Z

Evaluates terms (IndexTerms.t). Can be used for term simplification.
It is needed to evaluate terms when generating test cases in OCaml-land.

Potential issues

It's supposed to get stuck on errors, but it still might throw exceptions due to the functions used (ex: List.combine)
- Some of these checks could be omitted, assuming the term is well-typed.

Other

No sets, pointer ops, casts and a few other operations

dc-mak · 2024-07-30T09:10:13Z

It would be useful if you could explain why as well as what. I'm off on holiday for until 12th, so I'll let Christopher handle this.

backend/cn/lib/eval.ml

cp526 · 2024-07-30T14:43:27Z

backend/cn/lib/eval.ml

+  let eval_num_binop = eval_num_binop eval_aux bt here in
+  match t_ with
+  | Const _ -> return it
+  | Sym x -> Result.error (Sym.pp_string x ^ " is free")


If we want to be able to use eval to simplify quantified constraints or assertions, then it can't crash on free variables.

It doesn't crash, it returns Error, which partial_eval accounts for (and is what would be used for simplification).

backend/cn/lib/eval.ml

ZippeyKeys12 added the cn label Jul 30, 2024

ZippeyKeys12 requested review from cp526 and dc-mak July 30, 2024 02:51

dc-mak removed their request for review July 30, 2024 09:08