Parser improvement #18
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is required for a our Model to function properly. Previously, it would just create a term "(distinct 0 1 2)", instead of directly simplifying that to "true".
It seems that LASolver was always setting `has_explanation` flag to true, but never to false. This, in combination with inverted solver schedule in UFLA, led to a subtle bug where UF would detect conflict, but LA solver would also signal that it has a conflict (even though this would not be true) and then return an empty explanation. This resulted in incorrect UNSAT answers.
Before the change regarding the T-solvers schedule, in UFLA, UF solver was always checked before the LA solver. However, it seems that the solver schedule in UFLATHandler had LA solver scheduled before UF solver. This commit schedules UF solver first. I believe that in general UF solver should always be scheduled first. However, for model building, values for LA variables must be known before UF can compute values for other terms, so here the model building in LA must happen before model building in UF.
Previously, in `collectSingleEqualitySubstitutions`, the variables were processed in order as stored in `unordered_map`. Additionally, UF terms are treated as variables in ArithLogic. This meant that from an equality f(x) = x (with x being Real), the code could derive a substitution "x -> f(x)". However, such substitution results in an infinite cycle in the function that computes transitive closure of substitutions. We fix this by forcing an order in which variables are checked, starting from variables with higher PTRef, which mean they they were created later. This ensures for the above case, that f(x) will be considered before x, so the computed substitution will be "f(x) -> x".
ArithLogic::mkNeg is a simpler operation now than ArithLogic::mkTimes. In fact the latter uses the former as a subprocedure. Thus, to negate the second argument of `minus`, it is better to directly call mkNeg. Additional benefit is that this avoids allocation of a temporary vector.
The first branch before the change did not make sense, because it was trying to get sort from the first term in an empty list. Since this method is internal to ArithLogic.cc, we have control about how it is called. It is better to just assert that the input will never be an empty list.
Current master checks for redundant "parallel" let bindings of the form `(let ((l a) (l b)) f)` and gives an error if one is present. The smt-lib standard does not forbid these constructs and other solvers seem to parse them without errors. Hence one can argue that the checking in opensmt unnecessarily introduces complication in the code and in principle also a performance overhead (I haven't measured this) This commit introduces a semantic in which the last binding prevails (in the example above `(l b)`).
It starts to look like using a reentrant parser with custom name is not supported by flex/bison combination. This is the last commit where I still have an attempt at writing the system like that.
It looks like flex + bison combination does not support at the same time having a custom name for a parser and a reentrant parser. This commit removes the custom name for a parser so that we can use reentrancy.
aehyvari
force-pushed
the
parser-improvement
branch
from
a5c5733 to
406e76d
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.