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

interact with SMT solver #130

Closed
Smattr opened this issue Jun 1, 2019 · 3 comments
Closed

interact with SMT solver #130

Smattr opened this issue Jun 1, 2019 · 3 comments

Comments

@Smattr
Copy link
Owner

Smattr commented Jun 1, 2019

One way of implementing #13 would be to ask an SMT solver if two rules satisfy the necessary POR side conditions. For this, we'll first have to teach Rumur how to speak to an SMT solver. A good preliminary step would be implementing some type of DCE using this.
Smattr added a commit that referenced this issue Jun 19, 2019
@Smattr
add a model for testing SMT simplification
5a33d50 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 21, 2019
@Smattr
FIXME: add wrapper for managing forked+execed processes
0208f46 
Needs some testing plus termination functionality.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 23, 2019
@Smattr
add support for running an external command
bc56159 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 23, 2019
@Smattr
add SMT solver options
62d6a27 
Not yet exposed via the command line.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 23, 2019
@Smattr
add an API for interacting with an SMT solver
3ea9335 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 23, 2019
@Smattr
add an API for translating Rumur expressions into SMTLIB expressions
b97827e 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 23, 2019
@Smattr
add an API for SMT-powered simplification
b196f50 
This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 24, 2019
@Smattr
add support for running an external command
e646835 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 24, 2019
@Smattr
add SMT solver options
b682457 
Not yet exposed via the command line.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 24, 2019
@Smattr
add an API for interacting with an SMT solver
ff99762 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 24, 2019
@Smattr
add an API for translating Rumur expressions into SMTLIB expressions
3d9af51 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 24, 2019
@Smattr
add an API for SMT-powered simplification
ffd9eda 
This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
add an API for interacting with an SMT solver
572e469 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
add an API for translating Rumur expressions into SMTLIB expressions
4818ee0 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
add an API for SMT-powered simplification
393e088 
This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
plumb SMT functionality to command line options
c8fd06e 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
don't bail out from SMT simplification on encountering the built-in b…
d10491d 
…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"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
skip SMT simplification of unsupported expressions, and continue
3356509 
We were aborting SMT simplification whenever we hit an unsupported expression.
This was unnecessarily conservative as one unsupported expression does not mean
that every later expression in the model will be unsupported. Note that we still
*do* need to abort on unsupported definitions and similar constructs while
traversing the model because skipping these can affect the correctness of later
simplification decisions.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
enable now-passing SMT solver test
04bea03 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
when encountering an SMT-unsupported expression, include it in the de…
c62f26b 
…bug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"
@Smattr Smattr mentioned this issue Jun 25, 2019
Closed
Smattr added a commit that referenced this issue Jun 25, 2019
@Smattr
add some pieces for inspecting the SMT bridge during development
34458f7 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
add an API for interacting with an SMT solver
92f691a 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
add an API for translating Rumur expressions into SMTLIB expressions
23a3712 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
add an API for SMT-powered simplification
11af4fe 
This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
plumb SMT functionality to command line options
4ee77c6 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
don't bail out from SMT simplification on encountering the built-in b…
16ddf49 
…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"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
skip SMT simplification of unsupported expressions, and continue
2f96793 
We were aborting SMT simplification whenever we hit an unsupported expression.
This was unnecessarily conservative as one unsupported expression does not mean
that every later expression in the model will be unsupported. Note that we still
*do* need to abort on unsupported definitions and similar constructs while
traversing the model because skipping these can affect the correctness of later
simplification decisions.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
enable now-passing SMT solver test
9ce928c 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
when encountering an SMT-unsupported expression, include it in the de…
939480f 
…bug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 26, 2019
@Smattr
add some pieces for inspecting the SMT bridge during development
4145340 
Github: related to #130 "interact with SMT solver"
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 27, 2019
@Smattr
add support for running an external command
45f56b3 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add SMT solver options
1c75eef 
Not yet exposed via the command line.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add an API for interacting with an SMT solver
0f8c1aa 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add an API for translating Rumur expressions into SMTLIB expressions
9aa75f1 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add an API for SMT-powered simplification
dce3565 
This implementation is pretty minimal and simply bails out (throwing
smt::Unsupported) when it encounters any complicated feature. However, it's
already enough to simplify the example in tests/disabled/smt-simplify.m.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
plumb SMT functionality to command line options
4a0b72a 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
don't bail out from SMT simplification on encountering the built-in b…
4bf443d 
…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"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
skip SMT simplification of unsupported expressions, and continue
c66061f 
We were aborting SMT simplification whenever we hit an unsupported expression.
This was unnecessarily conservative as one unsupported expression does not mean
that every later expression in the model will be unsupported. Note that we still
*do* need to abort on unsupported definitions and similar constructs while
traversing the model because skipping these can affect the correctness of later
simplification decisions.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
enable now-passing SMT solver test
f01aab1 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
when encountering an SMT-unsupported expression, include it in the de…
3e4ac29 
…bug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add some pieces for inspecting the SMT bridge during development
627fff3 
Github: related to #130 "interact with SMT solver"
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
enable now-passing SMT solver test
20794d6 
Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
when encountering an SMT-unsupported expression, include it in the de…
7dfd442 
…bug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"
Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
add some pieces for inspecting the SMT bridge during development
d4c0731 
Github: related to #130 "interact with SMT solver"
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
Copy link
Owner Author

Smattr commented Jun 27, 2019

@yurivict, I'm intending to merge the feature/smt-solver branch in the next few days that contains commits related to this issue. 20794d6 adds a Python script that the test suite ends up causing Rumur to call as python <path>/misc/toy-smt.py .... I think it may cause shebangfix-related problems for the FreeBSD package. Is it simpler for you if I chmod +x this script, call it as <path>/misc/toy-smt.py ... and let you shebangfix-patch its shebang?

Smattr added a commit that referenced this issue Jun 27, 2019
@Smattr
name-mangle variables used in SMT queries
c32ed61 
This avoids collision with SMT solver keywords.

Github: related to #130 "interact with SMT solver"
@Smattr
Copy link
Owner Author

Smattr commented Jul 19, 2019

This is essentially done. What is required for #13 is some evolution of the SMT bridge to get it to understand aggregate types (arrays and records) and the effect of statements/functions. The latter will probably require some internal implementation of SSA.

For posterity, the previous comment is no longer relevant because the toy SMT solver was removed in 81d4123 and the test suite now simply calls Z3 or CVC4 if they're available.

@Smattr Smattr closed this as completed Jul 19, 2019
@yurivict
Copy link

Thanks for warning me about shebangs!
I'll handle them. -)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Smattr @yurivict