diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-26 16:03:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-26 21:03:48 +0000 |
| commit | 9a098337f9f25e7e2df07e493e6a120f6b8ce520 (patch) | |
| tree | 8953168e00fd442e350ab9af1fec2564f3cb70b0 /src/theory/theory_inference_manager.h | |
| parent | e4e19cd62b3eebed2de5b9b627509df0ffec23e1 (diff) | |
Enable default equality proofs for sets (#6931)
This enables default support for equality proofs in the theory of sets.
This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.
Diffstat (limited to 'src/theory/theory_inference_manager.h')
| -rw-r--r-- | src/theory/theory_inference_manager.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index b11f21f1e..cea0e698b 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -300,6 +300,8 @@ class TheoryInferenceManager * Theory's preNotifyFact and notifyFact method have been called with * isInternal = true. * + * Note this method should never be used when proofs are enabled. + * * @param atom The atom of the fact to assert * @param pol Its polarity * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid. |