diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-27 12:24:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-27 17:24:17 +0000 |
| commit | 3a180a2f8ffe8ad5756119ce0cbe61ab4ab28127 (patch) | |
| tree | 228409a37f4cd24c752244a5f71bea4e8199490b /src/proof | |
| parent | 119516a98c052e79ad55e126d13ce1ded38f90af (diff) | |
Track instantiation reasons in proofs (#6935)
This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.
Also simplifies an old argument modEq which was unused.
FYI @MikolasJanota
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/proof_rule.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 4b95b47da..173e4df9a 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -827,10 +827,16 @@ enum class PfRule : uint32_t SKOLEMIZE, // ======== Instantiate // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) - // Arguments: (t1 ... tn) + // Arguments: (t1 ... tn, (id (t)?)? ) // ---------------------------------------- // Conclusion: F*sigma - // sigma maps x1 ... xn to t1 ... tn. + // where sigma maps x1 ... xn to t1 ... tn. + // + // The optional argument id indicates the inference id that caused the + // instantiation. The term t indicates an additional term (e.g. the trigger) + // associated with the instantiation, which depends on the id. If the id + // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that + // generated the instantiation. INSTANTIATE, // ======== (Trusted) quantifiers preprocess // Children: ? |