Summary:
Instead of passing the Var.strength across interfaces, pass the Trm.pp
partially applied to the Var.strength. This hides the type of
Var.strength, and thereby removes the need for `Arithmetic.S.var`.
Reviewed By: jvillard
Differential Revision: D26250516
fbshipit-source-id: 64dbd3870
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:
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
Summary:
The current implementation of quantifier elimination in Sh.simplify is
tightly coupled with the details of what the Context operations
support. In particular, successfully eliminating variables with
Context.elim effectively relies on being given a context that has been
transformed by Context.apply_subst. These operations are sound
independently, but achieving the desired result is delicate.
To simplify this situation, this diff refactors the tightly coupled
usage into a Context.apply_and_elim operation that hides the details
of the interaction inside the Context module. This enables an accurate
specification of apply_and_elim to be given much more simply than can
be done for the separate operations. This also simplifies the
implementation of Sh.simplify.
Reviewed By: jvillard
Differential Revision: D25756577
fbshipit-source-id: b344b3da6
Summary:
The current implementation of Context.elim crudely removes oriented
equations from terms involving the given variables. This is easy to
use in a way that violates the representation invariants of Context,
as well as destroys completeness. This diff resolves this by making
Context.elim remove the desired variables by rearranging the existing
equality classes, in particular promoting a new representative term
when the existing representative is to be removed. Also, since this
basic approach is incomplete for interpreted terms, they are detected
and not removed. As a result, the interface changes to return the set
of variables that have been removed.
Reviewed By: jvillard
Differential Revision: D25756573
fbshipit-source-id: 0eead9281
Summary:
Context.fold_uses_of should enumerate the transitive subterms of a
term rather than only the immediate subterms.
Reviewed By: jvillard
Differential Revision: D25756553
fbshipit-source-id: a3911d9f5
Summary:
Sh operations usually detect inconsistency where needed. But some
operations such as Context.inter must treat the unsat case
specially. This diff increases robustness by not relying on Sh to
detect inconsistency in order to get the correct context or pure
constraints, or to use the fast-paths through Context or Formula
operations.
Reviewed By: jvillard
Differential Revision: D25756550
fbshipit-source-id: 091439ff6
Josh Berdine