Summary:
Currently there is an implicit assumption in Sh.simplify that
variables do not occur free in an equality relation which makes no
constraint on their values. This diff adds a step to formula
simplification that explicitly removes eliminated existentials from
equality relations.
Reviewed By: jvillard
Differential Revision: D20726960
fbshipit-source-id: 7109aa479
Summary:
Fix the crash in
```
(And_eq () (Var (id 10) (name v))
(Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1)))
((xs ()) (sat true) (rep ())))
```
The solver for interpreted functions relies on the solution
substitutions containing mappings from variables to interpreted
applications, and never in the reverse. When solving equations
involving polynomials, this constraint is specifically
established. But for equalities involving only monomials, it could
happen that e.g. `x` was chosen as the representative of `a × b`,
which violates this constraint.
Reviewed By: jvillard
Differential Revision: D20596422
fbshipit-source-id: 69b026f03
Summary: Term.compare already ignores Var names, make Term.equal do so as well.
Reviewed By: jvillard
Differential Revision: D20663961
fbshipit-source-id: 59e7aa880
Summary:
Generate output on stderr containing lines such as:
```
solve_for_vars time: 0.105 ms 0.871 ms 79 calls
```
which indicates that the current maximal time of a single
`solve_for_vars` query is `0.105 ms` and so far the total time spent in
`solve_for_vars` over `79` queries is `0.871 ms`.
At program exit, there is also a line for each timer indicating the
max query time and final accumulated duration and number of queries:
```
solve_for_vars time: 0.173 ms 17.242 ms 1108 calls
```
Additionally, replay sexp are dumped interactively. A query exceeding
1 sec is dumped, then one exceeding 2 sec, then 4 sec, etc.
Reviewed By: jvillard
Differential Revision: D20852160
fbshipit-source-id: 0a316891e
Summary:
Rename and clarify documentation to indicate that the stronger
specification wrt physical equality is due to requiring the mapped
function to be an endofunction.
Reviewed By: jvillard
Differential Revision: D20863524
fbshipit-source-id: 74dabeb5c
Summary:
Otherwise there is an alias `'a t` for `'a option` polluting the
global namespace, which causes e.g. merlin to produce confusing types.
Reviewed By: jvillard
Differential Revision: D20831349
fbshipit-source-id: dff7b4f15
Summary:
Many Equality functions accept and return a set of variables, document
their function.
Reviewed By: ngorogiannis
Differential Revision: D20596492
fbshipit-source-id: b91ae7197
Summary:
Passing info that affects the build through environment variables is
bad since it is not very visible, e.g. in log files. Also, those
settings are not recorded in .merlin files, leading to merlin using
the default configuration.
This diff changes ppx_trace to use a 'cookie' instead of an
environment variable, and configures dune to set this cookie based on
the selected profile. This has the benefit of using command line
arguments such as `--cookie 'ppx_trace_enabled="1"'` which appear in
build logs and .merlin files.
Reviewed By: jvillard
Differential Revision: D20590515
fbshipit-source-id: d2daceaa3
Summary:
Previously building would spew:
```
Warning 58: no cmx file was found in path for module Build_info__Build_info_data, and its interface was not compiled with -opaque
```
This is from compilation of the generated `build_info_data.ml-gen`. It
does not have an interface, so I don't how to resolve this other than
disabling the warning.
See also https://github.com/ocaml/dune/issues/3277 .
Reviewed By: jvillard
Differential Revision: D20589879
fbshipit-source-id: fcd86fb3b
Summary:
Now that the containers use functorial interfaces with representations
that do not include closures for the comparison functions, it is not
necessary to enable closure support when Marshaling the IR between the
frontend and backend. This should be slightly faster, but more
importantly, it means that the serialized form is stable across
changes to the analyzer that do not change the representation of the
IR types, and in particular, the dbg and opt binaries can use the same
serialized form.
Reviewed By: jvillard
Differential Revision: D20589880
fbshipit-source-id: 63f07335e
Summary:
If both the library and binary are named `sledge`, then compilation
works fine and resolves the names correctly, but merlin gets confused
and cannot find the sledge library modules used in the bin sources. So
the binary and library need different names. The name of the library
gets exposed to clients, while the name of the binary only determines
the name of some files in the _build directory, which can be renamed
as desired. Therefore, use the `sledge` name for the library module,
and rename the binary module to `sledge_cli`, but still have dune
install it as `sledge.exe`.
Reviewed By: jvillard
Differential Revision: D20589431
fbshipit-source-id: 14b65907d
Summary:
Integer `div` and `rem` are a pair of functions that satisfy the
division rule, where the result of `div` is truncated toward zero:
```
| Div (** Division, for integers result is truncated toward zero *)
| Rem
(** Remainder of division, satisfies [a = b * div a b + rem a b] and
for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
```
Reviewed By: jvillard
Differential Revision: D20584626
fbshipit-source-id: fa02a3a98
Summary:
This diff adds wrappers for Equality entry points that augment
exceptions escaping out of Equality with an sexp that can be given
back to Equality.replay in order to reexecute the function call that
failed.
A (bogus) example could be raising:
```
((Failure "domains intersect: ((u8) %x_5)")
(And_eq () (Ap1 (Unsigned (bits 8)) (Var (id 5) (name x)))
(Var (id 6) (name y))
((xs ()) (sat true)
(rep (((Var (id 6) (name y)) (Var (id 5) (name x))))))))
```
and then calling `Equality.replay {|(And_eq ...)|}`.
Reviewed By: jvillard
Differential Revision: D20583753
fbshipit-source-id: 80d855950
Summary:
It is more convenient, and harder to misunderstand, if the verbose
tracing setting comes commented-out after the default non-verbose
setting.
Reviewed By: jvillard
Differential Revision: D20583755
fbshipit-source-id: 06ecb0e9a
Summary:
Work on the containers revealed that 1b8746d21 was premature, and this
diff is in part a revert of that. The objectives for the global
namespace are:
- self-consistent as much as possible
- rich data type operations
- does not require maintaining lots of tedious library wrapping code
- has Marshalable containers
- has containers with functorial interfaces
For these aims, it's best to stick with Core. Base isn't enough to
define functorial interfaces for collections (without a lot of tedious
wrapping code to keep in sync manually), and since a few modules not
in Core_kernel are needed anyhow.
Reviewed By: ngorogiannis
Differential Revision: D20583756
fbshipit-source-id: d939be7d0
Summary:
This diff defines Map as a functorover the underlying implementation
of Core.Map. This results in map values that are just trees, with no
comparison function closures, and with the same interface (almost) and
underlying data structure implementation as Core.Map.
Reviewed By: ngorogiannis
Differential Revision: D20583758
fbshipit-source-id: 5a4997b51
Summary:
This diff defines Set as a functorover the underlying implementation
of Core.Set. This results in set values that are just trees, with no
comparison function closures, and with the same interface (almost) and
underlying data structure implementation as Core.Set.
Reviewed By: ngorogiannis
Differential Revision: D20583754
fbshipit-source-id: 79aa7477a
Summary:
- Rename to `combine_adjacent` for clarity
- Reimplement without needing to filter out a dummy value, by keeping
track of the numer of adjacent pairs that have been combined
together
- Use this counting to replace the probably-confusing lazy copy with
explicit eager copy at the right time
- Remove the now-unneeded dummy value argument
Reviewed By: jvillard
Differential Revision: D20482752
fbshipit-source-id: db80bbbe3
Summary:
`dune build fmt` applies to all contexts, but we only need one, so
use `dune build @_build/dbg/fmt` instead. Also swallow stderr as it's
useless with `--auto-promote`.
Reviewed By: ngorogiannis
Differential Revision: D20482767
fbshipit-source-id: a7642f65d
Summary:
The term "vector" evokes expectations of being automatically growable,
and these are just immutable arrays.
Reviewed By: ngorogiannis
Differential Revision: D20482762
fbshipit-source-id: 0cd2c9c23
Summary:
The base containers have inconvenient interfaces due to lacking
support for functors, which also leads to the representation of values
of containers including closures for the comparison functions. This
causes problems when `Marshal`ing these values.
This diff is one step toward not using the base containers.
Reviewed By: ngorogiannis
Differential Revision: D20482756
fbshipit-source-id: 0312c422d
Summary:
The base containers have inconvenient interfaces due to lacking
support for functors, which also leads to the representation of values
of containers including closures for the comparison functions. This
causes problems when `Marshal`ing these values.
This diff is one step toward not using the base containers.
Reviewed By: ngorogiannis
Differential Revision: D20482763
fbshipit-source-id: f55f91bf2
Summary:
Move definitions of profiles from `dune-workspace` to `dune` since it
seems to be ok to use profiles in `dune-workspace` that are only
defined in `dune`. Since the `dune` but not `dune-workspace` file is
used when building as a vendored dependency, this seems to be
preferable.
Also, change the `opt` profile into a wildcard, which seems to be
preferable from the vendored-building perspective.
Also, set library public names such that including `sledge` in the
`libraries` phrase of `dune` files works.
Reviewed By: ngorogiannis
Differential Revision: D20376179
fbshipit-source-id: f2b634716
Summary:
Define a `ppx_sledge` ppx rewriter that composes all the ppx rewriters
used, so that the list needs to be specified only once.
Reviewed By: jvillard
Differential Revision: D20322874
fbshipit-source-id: f15540b7f
Summary:
It seems to currently not be possible to make dune `preprocess`
stanzas vary across contexts, without essentially generating the dune
files. A consequence is that it is not possible to pass
context-dependent command line arguments to ppx rewriters. So add
support for an environment variable instead.
Reviewed By: jvillard
Differential Revision: D20322871
fbshipit-source-id: f3f3ea413
Summary:
Move files, adjust build system, etc.
This also separates out the ppx_trace conditional compilation debug
tracing machinery into an independent package and library.
Reviewed By: jvillard
Differential Revision: D20322876
fbshipit-source-id: a50522462
Summary:
`Reg.demangle` is implemented by calling the `_cxa_demangle` C++
runtime system function. This will be linked into the sledge binary,
due to being linked with llvm, but will not necessarily be available
in the sledge library. So make it a dynamically-set function to avoid
calling an undefined function from the library.
Reviewed By: jvillard
Differential Revision: D20323791
fbshipit-source-id: bda9afd37
Summary:
The convenience symlinks from sledge/bin to the built binaries of
various build modes under sledge/_build/_install conflict with
upcoming code rearrangements, so remove them.
Reviewed By: jvillard
Differential Revision: D20322872
fbshipit-source-id: 1a7c99ae0
Summary:
Formulate the canonizer for Extract from Concat terms uniformly as a
concatenation of extracts.
Reviewed By: jvillard
Differential Revision: D20303064
fbshipit-source-id: a45bc45dd
Summary:
Change constructor for solver goals to enforce variable context
conditions, and simplify other context manipulations that are now
unneeded.
Reviewed By: jvillard
Differential Revision: D20248543
fbshipit-source-id: a255c792b
Summary:
In a few places, implicitly witnessed existential variables could
remain in the existential context. This led to weakness in the solver,
where occurrences bound by the existential context would be not known
to be constrained by their witnesses.
Reviewed By: jvillard
Differential Revision: D20248542
fbshipit-source-id: 44f62839c
Summary: In preparation for enforcing invariants in the constructor.
Reviewed By: jvillard
Differential Revision: D20248541
fbshipit-source-id: 41f7d36e5
Summary:
Program (and global) variables are only distinct when considering
their string names, but logical variables need only their ids.
Reviewed By: jvillard
Differential Revision: D20214528
fbshipit-source-id: f7892c3ad
Summary:
When extracting from a concatenation, drop a prefix of the concat with
length equal to the offset of the extraction:
```
(α₀^…^αᵢ^…) [0+n₀+…+nᵢ₋₁, l) ==> (αᵢ^…)[0,l) where nₓ ≡ |αₓ|
```
Reviewed By: jvillard
Differential Revision: D20192874
fbshipit-source-id: cd015aa36
Summary:
Fix unstated assumptions Sh.or_ made on the universal and existential
contexts of disjuncts.
Reviewed By: jvillard
Differential Revision: D20192873
fbshipit-source-id: 945623e57
Summary:
This diff changes `Sh.simplify` from a logically-weakening syntactic
simplification to an equivalence-preserving rewrite. The
implementation is based on `Equality.solve_for_vars` which is also
used by `Solver` to witness existential variables.
Reviewed By: jvillard
Differential Revision: D20120274
fbshipit-source-id: 5e11659ea
Summary:
Just fix accumulated mis-formatting that is swallowed by the
inline-test promotion implementation.
Reviewed By: ngorogiannis
Differential Revision: D20120262
fbshipit-source-id: 0e387dc55
Summary:
Add `Sh.pp_raw` which is closer to the representation, for use when
tracing `Sh` operations.
Reviewed By: ngorogiannis
Differential Revision: D20120281
fbshipit-source-id: e3b1b531a
Summary:
Due to strengthened existential witnessing, the incomplete ad hoc
witness guessing is no longer needed.
Reviewed By: ngorogiannis
Differential Revision: D20120277
fbshipit-source-id: 8ee1656dd
Summary:
Strengthen computation of solution substitutions used for existential
witnessing by using the solver for the memory contents theory. This
uses a generalization of the equation solver implementation which
accepts a predicate used as a filter for equations added to the
solution substitution. When used for solving for a given set of
variables, this filter excludes equations which do not meet the
desired variable conditions.
Reviewed By: jvillard
Differential Revision: D20120275
fbshipit-source-id: 4203d5e41
Summary:
Strengthen existential quantifier witnessing to enable witnessing an
existential with a term containing another existential if no universal
witness is available. Additionally, strengthen existential witnessing
to enable terms of interpreted theories to witness existential
variables.
Also strengthen and simplify the representation invariant checking for
existential witnessing code.
Reviewed By: jvillard
Differential Revision: D20120271
fbshipit-source-id: 4c44fe9ef
Summary:
Handle the case the universal context of a goal does not stay in sync
with that of the minuend.
The need for this indicates that there is some problematic redundancy
in the representation of solver goals.
Reviewed By: ngorogiannis
Differential Revision: D20120268
fbshipit-source-id: 44a4d6260
Summary:
It can happen that canonizing subterms can change the classification
of a term e.g. to the literal true. In such cases, it is not useful or
correct use `Equality.lookup` (which expects to only be used on
uninterpreted applications) to search for some other equation equal to
the literal and use its representative instead.
Reviewed By: ngorogiannis
Differential Revision: D20120279
fbshipit-source-id: 3e2160233
Summary: When equating Concat terms, drop any common prefix or suffix.
Reviewed By: ngorogiannis
Differential Revision: D20120264
fbshipit-source-id: afdeb990e
Summary: No code change, only reordering definitions in prep for later changes.
Reviewed By: ngorogiannis
Differential Revision: D20120263
fbshipit-source-id: b312dfc9a
Summary: Add `Equality.and_term` and replace most of `Sh.pure` with it.
Reviewed By: ngorogiannis
Differential Revision: D20029742
fbshipit-source-id: 07c2f1fe6
Summary:
Replace `Equality.Subst.trim` with `partition_valid` which has a
logical specification (and unsurprisingly fixes some corner case
bugs):
```
val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
(** Partition ∃xs. σ into equivalent ∃xs. τ ∧ ∃ks. ν where ks and ν
are maximal where ∃ks. ν is universally valid, xs ⊇ ks and ks ∩
fv(τ) = ∅. *)
```
Reviewed By: ngorogiannis
Differential Revision: D20004974
fbshipit-source-id: 5cb3b3835
Summary:
Sh.var_strength determines, in part, if an existential variable has
only a single occurrence. The objective of this is to determine that a
variable is merely a placeholder and not used to express additional
constraints. For this, it suffices to check the weaker condition that
there is a single occurrence in each branch of a DNF expansion.
Reviewed By: ngorogiannis
Differential Revision: D19973779
fbshipit-source-id: 2c90c61f4
Summary:
The result of promoting expect tests is not necessarily formatted, so
try to reduce iterations by formatting after testing.
Reviewed By: ngorogiannis
Differential Revision: D20004973
fbshipit-source-id: 53af4c034
Summary:
Changing `pps` to `staged_pps` was needed for `import_ppx`, but it has
since been removed.
Reviewed By: jvillard
Differential Revision: D19973778
fbshipit-source-id: 5e2d83157
Summary:
Currently the free variables of the equality relation of a formula are
contained in the free variables of the rest of the formula, so Sh.fv
ignores them. Propagating equality facts across the star-or structure
of a formula, as necessary for quantifier elimination, breaks this
invariant. Some use cases, such as detecting which variables survive
applying a witness substitution, need to ignore the variables that
appear in the equality relation. This diff adds an argument to
conditionally ignore the variables in the equality relations.
Reviewed By: ngorogiannis
Differential Revision: D19580430
fbshipit-source-id: 2d417d89b
Josh Berdine
Jules Villard