Skip to content

Commit

Permalink
use True and False to construct new booleans in SMT simplification
Browse files Browse the repository at this point in the history
Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
  • Loading branch information
Smattr committed Jun 27, 2019
1 parent 51cb346 commit 91aceea
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions rumur/src/smt/simplify.cc
Original file line number Diff line number Diff line change
Expand Up @@ -453,16 +453,12 @@ namespace { class Simplifier : public BaseTraversal {

// invent a reference to "true"
static Ptr<Expr> make_true(void) {
auto n = Ptr<Number>::make(1, location());
auto cd = Ptr<ConstDecl>::make("boolean", n, Boolean, location());
return Ptr<ExprID>::make("true", cd, location());
return Ptr<Expr>(True);
}

// invent a reference to "false"
static Ptr<Expr> make_false(void) {
auto n = Ptr<Number>::make(0, location());
auto cd = Ptr<ConstDecl>::make("boolean", n, Boolean, location());
return Ptr<ExprID>::make("false", cd, location());
return Ptr<Expr>(False);
}

// declare a variable/type to the solver
Expand Down

0 comments on commit 91aceea

Please sign in to comment.