projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f15059) | patch
Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 Sep 2020 16:45:38 +0000 (11:45 -0500)
committerGitHub <noreply@github.com>
Tue, 8 Sep 2020 16:45:38 +0000 (11:45 -0500)
commitbe3543ef7e01eb32aab3161fa2778953fabc988d
treed821c034199aad91fddaa27d9baf3792c91463a6tree
parent3f150596fe2186aea1c40b3210e8a0d59dc1ba94commit | diff
Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)

This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history