Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

avoid calling SMT solver for "true" and "false" #139

Closed
Smattr opened this issue Jun 25, 2019 · 0 comments
Closed

avoid calling SMT solver for "true" and "false" #139

Smattr opened this issue Jun 25, 2019 · 0 comments
Labels
enhancement

Comments

@Smattr
Copy link
Owner

Smattr commented Jun 25, 2019

In relation to #130, the implementation in the feature/smt-solver branch is pretty unintelligent and calls the SMT solver for any boolean expression. This includes the literals true and false, which is a waste of time as the algorithm is only capable of replacing these with themselves. We should just detect this and avoid calling the solver in this case.
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
add reusable boolean constants
4138714 
This will save us having to reconstruct these repeatedly when we just want to
ask the question "is the expression I have the literal true or false?"

Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
use True and False to construct new booleans in SMT simplification
364cb45 
Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
avoid SMT simplification of "true" and "false"
b995eb1 
These literals are already as simple as they can be. Any attempt to ask the SMT
solver to simplify them just produces themselves. So avoid calling the solver
altogether in these cases.

Github: closes #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add reusable boolean constants
51cb346 
This will save us having to reconstruct these repeatedly when we just want to
ask the question "is the expression I have the literal true or false?"

Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
use True and False to construct new booleans in SMT simplification
91aceea 
Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
avoid SMT simplification of "true" and "false"
b507abb 
These literals are already as simple as they can be. Any attempt to ask the SMT
solver to simplify them just produces themselves. So avoid calling the solver
altogether in these cases.

Github: closes #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add reusable boolean constants
dcb3559 
This will save us having to reconstruct these repeatedly when we just want to
ask the question "is the expression I have the literal true or false?"

Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
use True and False to construct new booleans in SMT simplification
ec7afdc 
Github: related to #130 "interact with SMT solver"
Github: related to #139 "avoid calling SMT solver for "true" and "false""
@Smattr Smattr closed this as completed in 349c455 Jun 29, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Smattr