ocaml - 代入 Z3 表达式中的操作

Question

我有一个形式的 Z3 公式(> Expr1 Expr2)，我想将其更改为(< Expr1 Expr2)，同时保留Expr1and的结构Expr2。据我了解，substitute用其他人替换变量是有帮助的；但我不确定如果可能的话，我应该给出哪些参数来更改运算符。是否可以使用substitute或通过其他方法？

我正在使用 OCaml 绑定。

提前感谢您的回答:)

标签： ocamlz3

Answer 1

您可以只创建一个新表达式，例如，

let ult_of_ugt ctxt exp = match Expr.get_args exp with
  | [x; y] -> BitVector.mk_ult ctxt x y
  | _ -> invalid_arg "expected two operands"