Summary:
The SLEdge internal first-order theory solver targets the "word
problem", where a query has the form `C ⊢ L` where `C` is a
conjunction of literals and `L` is a single literal. This can be
abused to implement a naive SMT solver using an expansion to
disjunctive-normal form and checking `C ⊢ false` for each branch `C`
of the DNF. This is not useful as an SMT solver, but can be used for
testing.
Reviewed By: ngorogiannis
Differential Revision: D23459524
fbshipit-source-id: 5483e5a84
Summary: Formula.disjuncts was a quickly written approximation of DNF.
Reviewed By: ngorogiannis
Differential Revision: D23459513
fbshipit-source-id: 79fd60a7b
Summary:
It was incorrect in case any but the first of of the Formula.disjuncts
was inconsistent.
Reviewed By: ngorogiannis
Differential Revision: D23459519
fbshipit-source-id: 394677e38
Summary:
The only use of the ill-specified Sh.with_pure function is to ignore
the pure part when computing free variables. So add an argument to
Sh.fv to achieve that explicitly and remove Sh.with_pure.
Reviewed By: ngorogiannis
Differential Revision: D23459517
fbshipit-source-id: 8767799ca
Summary:
Strengthen normalization performed by Term and Formula constructors to
eliminate literal 0 subterms and true or false subformulas, as well as
cases where subterms or subformulas are either equal or opposite.
This strengthens the ability of Context.implies to prove formulas that
involve embedding or projecting between terms and formulas, as the
added normalization sometimes reduces if-then-else formulas to
literals that are then directly provable.
Reviewed By: ngorogiannis
Differential Revision: D23459512
fbshipit-source-id: 6d4d90399
Summary:
The dune build info embedded into executables is broken with dune <
2.7 and an flambda compiler.
Reviewed By: ngorogiannis
Differential Revision: D23459510
fbshipit-source-id: 18b3e3e15
Summary:
`Sh.norm` relies on `Eq (v, v)` formulas for `v` a variable to be
normalized to `Tt`, which is how eliminated variables are actually
removed from the representation.
Reviewed By: jvillard
Differential Revision: D22571132
fbshipit-source-id: 6d5f3efd7
Summary:
Move normalization that is necessary for `embed_into_fml` to be left
inverse to `embed_into_cnd` into the general `Fml` constructors.
Reviewed By: jvillard
Differential Revision: D22571137
fbshipit-source-id: 575c6bc45
Summary:
In order to ensure that the normalizing constructors are not
circumvented.
Reviewed By: jvillard
Differential Revision: D22571139
fbshipit-source-id: 32032c6fa
Summary:
The default printer is `pp_classes`, while `pp` is for debugging the
internal representation manipulation, so it is renamed to `pp_raw`.
Reviewed By: jvillard
Differential Revision: D22571135
fbshipit-source-id: 2d624e279
Summary:
`Formula.is_true` and `is_false` are now trivial one-line wrappers,
remove them for clarity.
Reviewed By: jvillard
Differential Revision: D22571143
fbshipit-source-id: 3f058eab4
Summary:
It is more confusing than necessary to use logical formula terminology
for the Context interface, considering that Formula represents
formulas and Context represents a (solver state resulting from a) set
of assumptions.
Reviewed By: jvillard
Differential Revision: D22571136
fbshipit-source-id: 087c97a02
Summary:
The unary forms are primitive in ICS, and in uncoming changes which
involve considering the product of a term and an equality relation, it
is more efficient to have unary constructors since the product is then
linear instead of quadratic in the size of the equality relation.
Reviewed By: jvillard
Differential Revision: D22571138
fbshipit-source-id: e0b745cc8
Summary:
Add a Predsym module for uninterpreted (unary) predicate symbols, and
positive and negative literals applying them to a term. As with
uninterpreted functions, tuple terms are used to represent predicates
of other arities.
Using this support, change the Ord and Uno formulas to uninterpreted
literals.
Reviewed By: jvillard
Differential Revision: D22571140
fbshipit-source-id: 5022a91e2
Summary:
`Context.difference` is now just a convenience function that does not
need to be defined internally.
Reviewed By: jvillard
Differential Revision: D22571141
fbshipit-source-id: 58aea9488
Summary: Also, when printing in raw mode, do not print the context.
Reviewed By: jvillard
Differential Revision: D22571145
fbshipit-source-id: b3596d9cc
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
Josh Berdine