Summary:
Make the relationship between Sh.is_empty and Sh.pure_approx stronger
and more precise. In particular:
> If [is_empty q], then [pure_approx q] is equivalent to
> [pure (pure_approx q)].
This enables replacing Solver.excise_pure with a simpler pure_entails
function. In particular, the heavy reliance on normalization of pure
formulas to true or false literals is eliminated, and only pure
entailment is needed.
Reviewed By: jvillard
Differential Revision: D22571146
fbshipit-source-id: 2fca64a61
Summary:
Generalize Fol interface to allow checking if a context implies any
formula, rather than restricting to only equalities.
Reviewed By: jvillard
Differential Revision: D22571144
fbshipit-source-id: 726bd87fd
Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.
Reviewed By: jvillard
Differential Revision: D22571150
fbshipit-source-id: 8952f0301
Summary:
In Ses, the constant term of a polynomial is represented as a
redundant multiplication by 1. Fix Fol.of_ses to recognize and
normalize this.
Reviewed By: jvillard
Differential Revision: D22571131
fbshipit-source-id: 3e1a12e5f
Summary:
The Ses constructors might simplify terms when called from
Fol.to_ses. Fix Fol.ses_map to account for this.
Reviewed By: jvillard
Differential Revision: D22571151
fbshipit-source-id: 1d573ac5f
Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.
Reviewed By: jvillard
Differential Revision: D22455725
fbshipit-source-id: 6f0059873
Summary:
In preparation for more smoothly interoperating with ICS's functional
array theory.
Reviewed By: jvillard
Differential Revision: D22401039
fbshipit-source-id: 4de39c38a
Summary:
It is not needed or very meaningful since the addition of type-based
disambiguation.
Reviewed By: jvillard
Differential Revision: D22401035
fbshipit-source-id: 31996f946
Summary:
The first-order context is induced by the pure part, so no need to
compare it.
Reviewed By: jvillard
Differential Revision: D22381645
fbshipit-source-id: 29fff13a3
Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.
The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.
Reviewed By: jvillard
Differential Revision: D22170506
fbshipit-source-id: a014ee7d7
Summary:
The eventual aim is for the conversion of Llair to Fol to be external
to Fol. Fol should not need to depend on Llair, nor vice versa. This
is not yet possible, but a step forward is to move the conversion
functions into separate modules outside the core Fol modules.
Reviewed By: ngorogiannis
Differential Revision: D22170522
fbshipit-source-id: 4860b4c07
Summary:
The `Subst` module is not used by `Ses`, so move it out of the
Ses-internal APIs.
Reviewed By: ngorogiannis
Differential Revision: D22170513
fbshipit-source-id: a189a1440
Summary:
Change Term and Equality rename functions to accept a partial
application of Var.Subst.apply to the renaming substitution.
Reviewed By: ngorogiannis
Differential Revision: D22170520
fbshipit-source-id: 003d8b27e
Summary:
The convention is for modules that are intended to be `open`ed, that
define syntax and infix operations, are named `Import`. This diff
combines the `Option.Monad_infix` and `Option.Monad_syntax` modules
into `Option.Import` to follow this convention.
Reviewed By: ngorogiannis
Differential Revision: D22170507
fbshipit-source-id: 44378fd56
Summary:
Exponents in polynomials are represented by rationals for code reuse
purposes, but only integral exponents are supported. Strengthen the
invariant check to clarify this.
Reviewed By: ngorogiannis
Differential Revision: D22170517
fbshipit-source-id: 81ae38f4e
Summary:
Refactor `Equality.ppx_classes_diff` into `diff_classes` to construct
the difference between classes maps explicitly, and change
`ppx_classes` to accept such a difference instead of computing it
internally.
This more flexibly composable interface allows elimination of extra
calls to `Equality.entails` to check if the difference is empty.
Reviewed By: jvillard
Differential Revision: D22038488
fbshipit-source-id: c19c18fc8
Summary:
The list interpreted as a conjunction of individual terms in `Sh.pure`
is now redundant with `Term.And`. This patch removes the redundant
list.
Reviewed By: jvillard
Differential Revision: D22035852
fbshipit-source-id: 49c01a078
Summary:
With the current handling of fresh variable generation during symbolic
execution, it is now possible to delay generating fresh variables in
individual small axioms until the precondition is known. In
particular, the existential variables of the precondition formula can
be bound, and then the small axiom can be generated with variables
fresh with respect to them. Previously, the small axioms were
generated with fresh variables that could later clash with the
precondition's existentials, necessitating renaming. This
double-freshening is now eliminated.
Reviewed By: jvillard
Differential Revision: D21974022
fbshipit-source-id: f217bfb9f
Summary:
When fresh variables are generated to name the overwritten value in an
assignment, they should be included in the ghost variables of the
resulting small axiom. This change should have been included in the
elimination of SSA.
Also strengthen assertion checking of small specs during symbolic
execution.
Reviewed By: jvillard
Differential Revision: D21974019
fbshipit-source-id: a66d8dac6
Summary:
Currently the symbolic execution code in `Exec` manually threads
universal and existential variable contexts through virtually every
function. It is easy to mistakenly pass on a context that is not the
latest-extended one, or to forget to add generated variables to the
contexts.
This patch adds a state monad, `Fresh`, to manage the generation of
fresh variables in `Exec`. This is a standard state monad where the
state is two sets of variables: those to which fresh variables must be
chosen fresh, and those which have been generated. This yields an
abstraction where an `'a Fresh.t` value represents a value of type
`'a` which may contain as-yet-unnamed variables, and `Fresh.gen ~wrt
a` generates names that are fresh with respect to `wrt` for all
unnamed variables in `a`, and yields the set of generated variables
together with `a` expressed in terms of those variables.
Reviewed By: jvillard
Differential Revision: D21974018
fbshipit-source-id: 1917e82c0
Summary: Minor code simplification and optimization of `extend_us` in no-op case.
Reviewed By: jvillard
Differential Revision: D21974021
fbshipit-source-id: a8b12b564
Summary:
Change the `Var.Subst` `freshen` and `restrict` constructors to return
the domain and range of the substitution explicitly. Clients generally
need to compute them immediately, and they are at least partially
constructed during the initial substitution construction anyhow. This
may be an incidental minor optimization.
This allows removing the `apply_set` operation, as it's use can be
handled directly from the domain and range sets.
This also allows `Sh.rename` to be split into a function that assumes
that the substitution is restricted to the vocabulary of the formula,
and a wrapper that does this restriction and calls through. This
allows `Sh.freshen_xs` to be simplified slightly, and avoids some
redundant restriction, domain, and range computations.
Reviewed By: jvillard
Differential Revision: D21974017
fbshipit-source-id: aa8b3db24
Summary:
`Domain_sh.from_call.subst` is a substitution that replaces shadowed
variables with fresh ones, which is constructed by `Domain_sh.call`
and used by `Domain_sh.retn`, after inverting it. This patch changes
the stored substitution to the inverted one, and renames it to
`unshadow` for clarity.
After this change, the stored substitutions have the property that
they map variables to program variables. This is desirable since it
avoids the question about the uninverted substitution of whether the
variables in the range of the uninverted substitution are "fresh".
Reviewed By: jvillard
Differential Revision: D21974020
fbshipit-source-id: d469c89f9
Summary:
Logically there is nothing specific to memory contents (as
byte-arrays) or aggregate (struct/array) values, the theory is for
sequences of non-fixed sized elements.
Reviewed By: jvillard
Differential Revision: D21721019
fbshipit-source-id: b2b730a50
Summary:
`Term.eq_concat` is not primitive and complicates the `Term`
interface. Move it to a couple clients as a convenience wrapper.
Reviewed By: jvillard
Differential Revision: D21721026
fbshipit-source-id: 0d74aa251
Summary:
Previously `null` and `zero` had different sorts/types, but now they
are equivalent.
Reviewed By: jvillard
Differential Revision: D21721023
fbshipit-source-id: 485219f6a
Summary:
Multiplication by a constant is primitive in the linear arithmetic
solver, while general multiplication is not, so for clarity and
predictability, use constants where possible.
Reviewed By: jvillard
Differential Revision: D21721020
fbshipit-source-id: 3497d06c9
Josh Berdine