summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/simp/SimpSolver.cc
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-31 15:34:36 -0500
committerGitHub <noreply@github.com>2020-08-31 15:34:36 -0500
commit09b3b246ad0328a163b0e3825531ccf82ea4013d (patch)
treec4a2b560e63e0fbe06861d7051c97194c66cbcca /src/prop/bvminisat/simp/SimpSolver.cc
parent52bab1414d41a4beb301f3c8a4165fa972f71a93 (diff)
(new theory) Update TheoryStrings to new standard (#4963)
This updates theory of strings to the new standard. This makes strings use the standard template for check and collectModelInfo. It also updates its inference manager to the standard and makes use of assertFactInternal for processing internal facts. This now enables preNotifyFact and notifyFact to be defined in TheoryStrings instead of inside inference manager, which is clearer and eliminates some dependencies within inference manager. Note that the inference manager of strings for now inherits from TheoryInferenceManager. Further standardization will make it inherit from the new InferenceManagerBuffered class. This design will be merged into proof-new, which also has significant changes to strings inference manager.
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.cc')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback