Summary:
Context.solve_uninterp_eqs uses `not Theory.is_interpreted` where
`Theory.is_noninterpreted` is more correct, since it operates on terms
that are class elements, which cannot be `Z _ | Q _ | Concat [||]`.
Reviewed By: jvillard
Differential Revision: D25883732
fbshipit-source-id: 5d060b338
Summary:
Currently `not Theory.is_interpreted` is used to terms should be added
to classes, or delayed to pending equations. This diff changes this to
use `Theory.is_noninterpreted` instead. They only differ on `Z _ | Q _
| Concat [||]`, which do not make it to this test, and
`is_noninterpreted` is more correct since classes may only contain
solvables.
Reviewed By: jvillard
Differential Revision: D25883706
fbshipit-source-id: 3b7b94065
Summary:
Use Theory.solvable_trms for a minor strengthening and simplification
of Context.is_valid_eq.
Reviewed By: jvillard
Differential Revision: D25883735
fbshipit-source-id: 3d0f3fcfe
Summary:
The current Context.max_solvables differs from Theory.solvables in
that it incorrectly includes `Z _ | Q _ | Concat [||]` terms.
Reviewed By: jvillard
Differential Revision: D25883728
fbshipit-source-id: f39f67622
Summary:
Currently when Arith.map encounters a noninterpreted polynomial, it
does not descend to its subterms. This diff fixes this bug, and
documents that the `map` and `trms` operations agree on the set of
subterms.
Reviewed By: jvillard
Differential Revision: D25883725
fbshipit-source-id: 1dc06f1fc
Summary:
For arithmetic terms that are a single monomial, Arith.trms is
currently the singleton iterator containing the term itself. In
particular, Arith.trms is not the *sub*terms in this case. In this
case the principal constructor is multiplication. This diff fixes
these cases and defines Arith.trms to contain the factors of a
singleton monomial.
Reviewed By: jvillard
Differential Revision: D25883719
fbshipit-source-id: a88611bba
Summary:
No functional change. Mostly reorder definitions. Add some
tracing. Some documentation improvement. Remove a few unneeded
identifiers in patterns.
Reviewed By: jvillard
Differential Revision: D25883712
fbshipit-source-id: 1449a7f54
Summary:
Currently the equality classes are computed from the representatives
solution substitution when needed. This diff instead maintains them as
part of the representation of the context. By itself this does not
make a huge difference, but it is necessary to make other operations
incremental.
Reviewed By: jvillard
Differential Revision: D25883715
fbshipit-source-id: 1b444a0dc
Summary:
The solver for single equations no longer needs access to the internal
representation of the context.
Reviewed By: jvillard
Differential Revision: D25883722
fbshipit-source-id: 4ccd97674
Summary:
When `no_fresh` is true, then no fresh variables will be generated
while solving. So it is not necessary to provide a set with respect to
which variables must be generated fresh.
Reviewed By: jvillard
Differential Revision: D25883724
fbshipit-source-id: fd886067f
Summary:
Currently when solving an equation requires solving one or more other
equations, they are handled recursively. This diff reworks the solver
to instead queue pending equations in a list rather than eagerly
solving them eagerly. The pending list will be needed when changing
the Context.t representation since some equations will need to be
delayed until representation invariants are re-established.
Additionally, the solution is accumulated as an association list
rather than being eagerly incorporated into the context
representation. This enables the uses in equality solving and
quantifier elimination to use different representations.
Reviewed By: jvillard
Differential Revision: D25883727
fbshipit-source-id: 2f6b5efa3
Summary:
When used by the first-order solver, solve_extract may generate fresh
variables to express the solution substitutions, but when used by
quantifier elimination via solve_for_vars, fresh variables should not
be generated. This diff makes the difference between these use cases
simpler and clearer by replacing the obscure filter predicate argument
that is passed eventually to compose1 with a boolean indicating
whether fresh variables may be generated.
Reviewed By: jvillard
Differential Revision: D25756562
fbshipit-source-id: 53a35b71c
Summary:
Context.solve_for_vars returns a solution substitution consisting of
oriented equalities that are implied by the given context. It is
logically valid to express these equations using terms that are
normalized with respect to the solution substitution itself. This diff
normalizes uninterpreted terms with the solution substitution when
extending it. This preserves the logical strength of the solutions,
and strengthens other purely syntactic operations on the substitution,
such as Context.Subst.is_valid_eq.
Reviewed By: jvillard
Differential Revision: D25756582
fbshipit-source-id: cd997c46b
Summary:
- Fix clamping of percentage change of memory quantities
- Improve sorting of coverage changes relative to unchanged error
results
- Filter out results for invalid LLVM code
- Fix printing multiple status values
- Fix passing args to sledge, different subcommands need different
args
- Fix cleaning commands
- Add an unknown error status to the report if sledge exits without
producing a status in the report
- Internalize globals for tests, as otherwise C++ tests are unreadable
due to the runtime system models
Reviewed By: jvillard
Differential Revision: D25756567
fbshipit-source-id: 3b4c003f4
Summary:
The ~20% hit in compilation time is dominated by the time saved
running the tests. This also makes the memory allocation numbers more
robust to inconsequential changes. Note that `make check` is still
fast.
Note that normally dune passes `-g` to ocamlopt itself, but not if the
build profile includes an `ocamlopt_flags` entry. So add it explicitly
to ensure that compilation includes debug symbols.
(Also remove `-error-style short` that was missed in 9c4f263.)
Reviewed By: jvillard
Differential Revision: D25756570
fbshipit-source-id: 94d18bac2
Summary:
When a stem has an occurrence of an existential, say x, and x is
substituted out by different witnesses, say a and b, in two disjuncts,
then the connection to other occurrences of a and b are lost.
This diff fixes this problem by propagating the solved variables that
survive normalization down to subformulas, and not removing those
variables from subformulas.
Reviewed By: jvillard
Differential Revision: D25756583
fbshipit-source-id: dabda743f
Summary:
Trade a bit more code for lowering complexity from linear to
logarithmic.
Reviewed By: jvillard
Differential Revision: D25756569
fbshipit-source-id: 83ad575fe
Summary:
Composing two substitutions does not need to require that their
domains are disjoint.
Leave disjointness check for composing a single mapping just to check
expected usage.
Reviewed By: jvillard
Differential Revision: D25756557
fbshipit-source-id: 04e92b864
Summary:
The overall operation of the quantifier elimination algorithm in
Sh.simplify is to first descend through the disjunctive structure of a
symbolic heap formula, process the leaves, and then proceed back up
the formula. At each point on the way back up, the first-order solver
is used to compute a solution substitution representing witnesses of
existential variables. This substitution is then used to normalize the
entire subformula at that point. Note that this results in
substituting and normalizing each subformula a number of times
proportional to its depth in the disjunctive structure.
This diff removes this redundancy and substitutes through each
subformula once. This is done by changing from an overall bottom-up to
top-down algorithm, and involves composing solution substitutions
rather than substituting multiple times. This change also heavily
relies on the strengthened Context.apply_and_elim operation, where the
bottom-up many-substitutions approach relies on the internal details
of repeated substitutions.
Reviewed By: jvillard
Differential Revision: D25756549
fbshipit-source-id: ca7cd814a
Josh Berdine