Summary:
Similarly to terms, use the Comparar interface of Sets to defined
formulas using recursive types instead of recursive modules.
Reviewed By: jvillard
Differential Revision: D26250512
fbshipit-source-id: 84f0ae8c0
Summary: No functional change, just to make the interface easier to read
Reviewed By: jvillard
Differential Revision: D26250513
fbshipit-source-id: f3b07bccc
Summary:
Terms include Arithmetic terms, which are polynomials over terms
themselves. Monomials are represented as maps from
terms (multiplicative factors) to integers (their powers). Polynomials
are represented as maps from monomials (indeterminates) to
rationals (coefficients). In particular, terms are represented using
maps whose keys are terms themselves. This is currently implemented
using recursive modules.
This diff uses the Comparer-based interface of Maps to express this
cycle as recursive *types* rather than recursive *modules*, see the
very beginning of trm.ml. The rest of the changes are driven by the
need to expose the Arithmetic.t type at toplevel, outside the functor
that defines the arithmetic operations, and changes to stage the
definition of term and polynomial operations to remove unnecessary
recursion.
One might hope that these changes are just moving code around, but due
to how recursive modules are implemented, this refactoring is
motivated by performance profiling. In every cycle between recursive
modules, at least one of the modules must be "safe". A "safe" module
is one where all exposed values have function type. This allows the
compiler to initialize that module with functions that immediately
raise an exception, define the other modules using it, and then tie
the recursive knot by backpatching the safe module with the actual
functions at the end. This implementation works, but has the
consequence that the compiler must treat calls to functions of safe
recursive modules as indirect calls to unknown functions. This means
that they are not inlined or even called by symbol, and instead
calling them involves spilling registers if needed, loading their
address from memory, calling them by address, and restoring any
spilled registers. For operations like Trm.compare that are a handful
of instructions on the hot path, this is a significant
difference. Since terms are the keys of maps and sets in the core of
the first-order equality solver, those map operations are very very
hot.
Reviewed By: jvillard
Differential Revision: D26250533
fbshipit-source-id: f79334c68
Summary:
No functional change, apart from a minor change in invariant checking
for core constructors. Only to reduce diffs of upcoming changes.
Reviewed By: jvillard
Differential Revision: D26250518
fbshipit-source-id: a731e4fd6
Summary:
Inline functor applications, principally those involved in the
representation of (arithmetic) terms. This enables direct calls to
functions in the result of functor applications, instead of indirect
via an offset from the start of the module block resulting from the
functor appication. This also then enables further inlining
opportunities.
Reviewed By: jvillard
Differential Revision: D26338016
fbshipit-source-id: 27b770fa3
Summary:
Currently there is a direct cycle of dependencies Var -> Trm ->
Var. Inside Trm, these two modules are defined as mutually recursive
modules, so at some level this is ok. Due to internals of how
recursive modules are compiled, recursive modules that are
"unsafe" (that is, export some value of non-function type) are
compiled more efficiently. This diff moves Var from being defined
recursively with Trm to being a submodule of Trm. This eliminates that
Var -> Trm -> Var cycle and enables making Trm an "unsafe"
module. (Trm is still mutually recursive with Arith (and Arith0), but
they are "safe".)
The difference between how "safe" and "unsafe" recursive modules are
compiled, in this context, is that the safe ones are first initialized
to a block containing dummy function closures that immediately raise,
then the unsafe ones are initialized as normal modules, and then the
safe ones are back-patched. A consequence of this is that calls to
functions in safe recursive modules are "unknown" calls, and they are
implemented as loading from a pointer to a closure and calling the
generic caml_apply function. In contrast, calls to functions in normal
or "unsafe" modules can be known, and get compiled to direct assembly
calls to the statically resolved callee. The second case is
faster. Additionally, in the indirect case, the callee is unknown, and
so some register spilling and restoring is also potentially
involved. Normally (I guess), this difference in performance is not
significant, but it can be significant for e.g. compare or hash
functions of modules used as container keys / elements, where the
container data structure is very hot.
Reviewed By: ngorogiannis
Differential Revision: D26250517
fbshipit-source-id: ecef49b32
Summary:
Variable ids are currently unique non-negative integers, and register
ids are unique positive integers, so using register ids negated as
variable ids yields a situation where all variable ids are unique.
Reviewed By: jvillard
Differential Revision: D26250544
fbshipit-source-id: 9e47e9776
Summary:
`Sh.and_ b q` normalizes `b` using the equality context of `q` and
then conjoins the result to `q`. This is incorrect in case normalizing
`b` results in expressing it using existentials of `q`, which takes
the existentials out of their scope. So this diff changes from
essentially
`(∃x.Q) ∧ B = (∃x.Q) ∧ (∃x.Bρ)`
to
`(∃x.Q) ∧ B = (∃x'.Q[x'/x] ∧ Bρ)`
where `ρ` is the substitution that normalizes with respect to the
equality context.
Reviewed By: jvillard
Differential Revision: D26250536
fbshipit-source-id: 05f5c48c0
Summary:
Add assertion to detect if the variable a function call modifies
appears in the actual parameters. In this case, the implementation is
incomplete.
Reviewed By: jvillard
Differential Revision: D26250527
fbshipit-source-id: d2e81a467
Summary:
Instructions and terminators are not themselves unique, there can be
two instructions that compare equal in distinct blocks, and likewise
for terminators. Such clashes make the coverage statistics report
incorrectly low coverage. This diff fixes this by also considering the
parent blocks.
Reviewed By: jvillard
Differential Revision: D26250514
fbshipit-source-id: 93f916eab
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
Josh Berdine