Hi smt-scope developers,
I have been recently updating verus's quantifier profiler from z3tracer to smt-scope (smt-scope works way better!). I'm mostly done with the update, but have some questions about how smt-scope computed the cost of a quantifier. In Verus, we computed the cost following the Computing with Triggers paper https://github.com/verus-lang/smt2utils/blob/main/z3tracer/src/model.rs#L402-L423.
It seems like each node in the smt-scope instantiation graph also has a cost, https://docs.rs/smt-scope/latest/smt_scope/analysis/raw/struct.Node.html. Is that something computed similarly? I'm not sure I followed what the source code is doing there.
Hi smt-scope developers,
I have been recently updating verus's quantifier profiler from
z3tracertosmt-scope(smt-scope works way better!). I'm mostly done with the update, but have some questions about how smt-scope computed the cost of a quantifier. In Verus, we computed the cost following the Computing with Triggers paper https://github.com/verus-lang/smt2utils/blob/main/z3tracer/src/model.rs#L402-L423.It seems like each node in the smt-scope instantiation graph also has a cost, https://docs.rs/smt-scope/latest/smt_scope/analysis/raw/struct.Node.html. Is that something computed similarly? I'm not sure I followed what the source code is doing there.