Skip to content

Commit

Permalink
don't bail out from SMT simplification on encountering the built-in b…
Browse files Browse the repository at this point in the history
…oolean enum

Rather interesting screw up there. We were bailing out of SMT simplification
when encountering an enum, as we don't support it yet. However, every model
begins with the implicit definition of the built-in type boolean. So SMT
simplification was previously useless as it would bail out on every single
model.

We still don't handle full enums, but we can at least cope with boolean now.

Github: related to #130 "interact with SMT solver"
  • Loading branch information
Smattr committed Jun 25, 2019
1 parent c8fd06e commit d10491d
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion rumur/src/smt/simplify.cc
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,12 @@ namespace { class Simplifier : public BaseTraversal {
simplify(n.index);
}

void visit_enum(Enum&) final {
void visit_enum(Enum &n) final {

// boolean is an SMT built-in we don't need to declare
if (n == *Boolean)
return;

throw Unsupported();
}

Expand Down

0 comments on commit d10491d

Please sign in to comment.