summaryrefslogtreecommitdiff
path: root/src/theory/logic_info.cpp
diff options
context:
space:
mode:
authormudathirmahgoub <mudathirmahgoub@gmail.com>2020-09-22 16:59:41 -0500
committerGitHub <noreply@github.com>2020-09-22 16:59:41 -0500
commite4a29a6033ecc7ba5ec266f37e8f151f09ead020 (patch)
tree26dff55bd5121dc311185dcd3071a6e8751f9f5e /src/theory/logic_info.cpp
parent524c879720779abc3bc529459da8734f2eb3e3ad (diff)
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets). It acts as a basis for future commits. It includes straightforward implementation for typing rules an enumerator for bags.
Diffstat (limited to 'src/theory/logic_info.cpp')
-rw-r--r--src/theory/logic_info.cpp5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 4bbbdc322..73cd920d2 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -338,6 +338,11 @@ std::string LogicInfo::getLogicString() const {
ss << "FS";
++seen;
}
+ if (d_theories[THEORY_BAGS])
+ {
+ ss << "FB";
+ ++seen;
+ }
if(seen != d_sharingTheories) {
Unhandled()
<< "can't extract a logic string from LogicInfo; at least one "
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback