Summary: The wrapper functions do not get inlined enough to avoid excess allocations.
Reviewed By: jvillard
Differential Revision: D25946110
fbshipit-source-id: 8dc3d8259
Summary:
This diff replaces Fml.fold_dnf, which eagerly enumerates a
disjunctive-normal form expansion, with iter_dnf which can be iterated
lazily. Fml.iter_dnf is then used in Context.dnf. This means that the
full DNF expansion does not need to be allocated by
e.g. Smtlib.check_sat, which yields huge peak memory savings.
Reviewed By: jvillard
Differential Revision: D25946111
fbshipit-source-id: e6d179e9f
Summary:
Currently detection and propagation of consequences of newly added
equality constraints is implemented using some operations that
traverse the entire representation of the equality relation. This
implementation strategy makes it relatively easy and robust to ensure
that the consequences of constraints are treated in a sound and
complete way. It does have the drawback that adding a constraint
involves work that is proportional (nonlinearly even) to the number of
all constraints. This can become a performance bottleneck.
This diff reimplements the core operations using an additional data
structure that essentially tracks the "super-term" relation between
terms, which can be used to look up the existing constraints that
might be involved in deriving new consequences when adding
equalities. This means that adding new equalities no longer takes time
proportional to the size of the entire equality context
representation, but only to the number of existing constraints that
might interact with the new constraint. Also, rewriting terms
into canonical form no longer takes time proportional to size of the
whole context, but only performs table lookups on the subterms of the
term to canonize.
Reviewed By: jvillard
Differential Revision: D25883705
fbshipit-source-id: b3f266533
Summary:
This diff changes Context.extend to not only add terms and their
subterms to the carrier, but to simultaneously normalize the added
term. The normalized form is currently ignored, but it will be needed
when adding use lists.
Reviewed By: jvillard
Differential Revision: D25883709
fbshipit-source-id: bfe06f2a8
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:
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
Josh Berdine