essential-constraint-vm

基本约束检查虚拟机。

lib.rs:

基本约束检查实现。

检查谓词

此crate的主要入口点是check_predicate函数，它允许并行检查与单个谓词相关联的约束契约与提供的解决方案数据和状态槽变异。

检查单个约束

还公开了检查单个约束的函数。

• exec_bytecode、exec_bytecode_iter和exec_ops函数允许执行约束并返回结果Stack。
• eval_bytecode、eval_bytecode_iter和eval_ops函数与它们的exec_*对应函数类似，但期望栈顶包含一个布尔值，指示约束是否得到满足（0表示false，1表示true）并返回此值。