Summary:
Term.const_of is misleading as it is easy to expect it checks if a
term is a constant, or to expect that it returns the constant part of
a term. Instead, Term.split_const is clearer:
```
val split_const : t -> t * Q.t
(** Splits a term into the sum of its constant and non-constant parts.
That is, [split_const a] is [(b, c)] such that [a = b + c] and the
absolute value of [c] is maximal. *)
```
Reviewed By: ngorogiannis
Differential Revision: D24306065
fbshipit-source-id: ba15958ad
Summary:
The treatment of comparison and exceptions in Core/Core_kernel/Base
makes them questionable as the default. This diff changes nonstdlib so
that Core is no longer opened in the global namespace, and makes a few
changes to handle the resulting minor API changes. This leads to a
lighter-touch nonstdlib, which makes a few definitions of its own, and
selects and extends modules from several libraries, including base,
core_kernel, containers, iter.
Reviewed By: jvillard
Differential Revision: D24306090
fbshipit-source-id: 42c91bd1b
Summary: Now elapsed time and the info in Unix.process_times is treated uniformly.
Reviewed By: jvillard
Differential Revision: D24306049
fbshipit-source-id: 09ab734ea
Summary:
The unary comparison to zero predicates are confusing to read since
whether the 0 is the left or right argument of the naturally infix
comparison is ambiguous. So replace Gt0 with Pos, meaning the argument
is positive, and remove the rest.
Reviewed By: jvillard
Differential Revision: D24306067
fbshipit-source-id: 2bd30dbe4
Summary:
Checking whether a formula is negative now only needs to inspect the
principle connective.
Reviewed By: ngorogiannis
Differential Revision: D24306061
fbshipit-source-id: 1f110e7f1
Summary:
Add a negation formula that will be used on atomic formulas instead of
ensuring the set of literals is closed under negation. This is in
preparation for more efficient negation and negation-normal form
preservation, which explicitly tracks whether literals are positive or
negative.
Reviewed By: ngorogiannis
Differential Revision: D24306055
fbshipit-source-id: 9300d6aee
Summary:
Change the representation of Fol terms to use polynomials for
arithmetic. This is a generalization and simplification of those used
in Ses. In particular, the treatment of division is stronger as it
captures associativity, commutativity, and unit laws, plus being the
inverse of multiplication.
Also, the interface is staged and factored so that the implementation
of polynomials and arithmetic is separate from the rest of terms.
Reviewed By: jvillard
Differential Revision: D24306108
fbshipit-source-id: 78589a8ec
Summary:
Function symbols when applied to literal values can be simplified by
evaluating them. This can be done even for function symbols that are
otherwise uninterpreted. This is not very strong, but is important in
some cases, and can prevent accumulating large complex terms that are
equal to literal constants.
Reviewed By: jvillard
Differential Revision: D24306044
fbshipit-source-id: 8c34d1ef2
Summary: In preparation for generalizing the type of multiplicities.
Reviewed By: jvillard
Differential Revision: D24306052
fbshipit-source-id: ddb71499e
Summary:
The form of the Base containers interface, in particular the way
comparison functions are passed using Comparators, is slower than
standard functors. Also Base.Map is missing some operations, such as
efficient merge and union.
Reviewed By: jvillard
Differential Revision: D24306047
fbshipit-source-id: e1623b693
Summary: Hopefully only transitional until Fol.Var and Ses.Var are conflated.
Reviewed By: jvillard
Differential Revision: D24306039
fbshipit-source-id: 5c3be8d4d
Summary:
Clarify the translation of 1-bit integer operations to formulas, and
add a few missing cases.
Reviewed By: ngorogiannis
Differential Revision: D24306057
fbshipit-source-id: 626a27997
Summary:
The translation from Llair to Fol can now be implemented using only
the external interface of Fol, so move it to a separate module. This
makes Fol not depend on Llair and vice versa, as appropriate.
Reviewed By: jvillard
Differential Revision: D24306087
fbshipit-source-id: fc68a588b
Summary:
Instead of relying on tuple terms, make function symbol applications
and predicate symbol literals n-ary directly.
Reviewed By: jvillard
Differential Revision: D24306078
fbshipit-source-id: 2863dceb4
Summary:
Move the punting between arrays and lists out of the clients of the
n-ary application normalizing constructors.
Reviewed By: jvillard
Differential Revision: D24306071
fbshipit-source-id: f3d2cb5df
Summary:
References from a record to one of its ancestor records are used to
represent cyclic or recursive record values. While the current
interpretation is weak, these logically are part of the record theory
and should be interpreted with the rest of the record terms.
Reviewed By: jvillard
Differential Revision: D24306091
fbshipit-source-id: 41553741d
Summary:
The empty record term is only used as the base of a sequence of
updates for an interval of indices from 0 to some N. A more direct
representation is to combine such sequences of updates into a flat
record term listing the elements.
Reviewed By: jvillard
Differential Revision: D24306048
fbshipit-source-id: d1b4900c8
Summary:
The uses of record terms only require indices that are literal
integers. This is a significant logical simplification from the
perspective of the backend solver.
Reviewed By: jvillard
Differential Revision: D24306093
fbshipit-source-id: 083dcc6b5
Summary:
Conversions between types are uninterpreted, so use uninterpreted
function symbols for them.
Reviewed By: jvillard
Differential Revision: D24306077
fbshipit-source-id: 49937fdbb
Summary:
Label values are uninterpreted, so use an uninterpreted function
symbol for them.
Reviewed By: jvillard
Differential Revision: D24306097
fbshipit-source-id: e139c70ba
Summary:
Floating point values are uninterpreted, so use an uninterpreted
function symbol for them.
Reviewed By: jvillard
Differential Revision: D24306096
fbshipit-source-id: 8c10dd3fd
Summary:
Convert from Llair.Exp to Fol.Term directly instead of going via
Ses.Term. This is a step on the way to removing Ses.
There are currently some term simplifications done in Ses.Term that
are missing in Fol.Term. This means that converting directly from
Llair.Exp to Fol.Term instead of via Ses.Term is not exactly the same
as the indirect conversion. The missing simplifications will be added
to Fol.Term in upcoming diffs.
Reviewed By: jvillard
Differential Revision: D24306053
fbshipit-source-id: 4ec5620a9
Summary:
Generalize Fol.Predsym to separate Predsym module for arbitrary
uninterpreted predicate symbols.
Add uninterpreted predicate literals to Ses.Term.
Use uninterpreted predicates to represent "ord" and "uno".
Reviewed By: jvillard
Differential Revision: D24306105
fbshipit-source-id: bdd72a8be
Summary: Funsym does not need to be defined as a submodule of Fol.
Reviewed By: jvillard
Differential Revision: D24306092
fbshipit-source-id: 7875f45f0
Summary:
A number of function symbols are not interpreted. This diff adds
generic uninterpreted function symbols, which will be used later to
avoid treating different uninterpreted functions separately.
Reviewed By: jvillard
Differential Revision: D24306076
fbshipit-source-id: b70ed10aa
Summary:
With the implementation of variables defined parametrically over their
representation, the implementation can also be used for Fol.Var.
Reviewed By: ngorogiannis
Differential Revision: D23703054
fbshipit-source-id: d27bdbbe8
Summary:
Variables are represented as a subtype of terms. The implementation of
the operations on variables is largely independent of this. This diff
generalizes the implementation over the concrete representation, and
moves it to a separate module.
Reviewed By: ngorogiannis
Differential Revision: D23660290
fbshipit-source-id: 90d8c3ca4
Summary:
Increase the fidelity of the status in the analysis report slightly by
including the number of analysis steps taken.
Reviewed By: jvillard
Differential Revision: D23648493
fbshipit-source-id: 8050b7829
Summary:
When equal_or_separate returns Unknown, it is common to sort the args,
which is wasteful since computing equal_or_separate already had to
test if the args are equal, which is most if not all of the work of
comparing them.
Reviewed By: jvillard
Differential Revision: D23636205
fbshipit-source-id: 5b2bcdd8f
Summary:
`Fol.equal_or_opposite p q` naively constructs the negation of `q` in
most cases, only to test if it is equal to `p`. This is an inefficient
method of computing if one formula is the negation of another. This
diff implements this directly. The drawback is some duplication of the
negation logic from `_Not`.
Reviewed By: ngorogiannis
Differential Revision: D23487500
fbshipit-source-id: 100f95edc
Summary:
Normalize conditional formulas to ensure that their "condition"
formula is not "negative". This avoids redundant formulas such as `(x
= 0 ? p : q)` and `(x ≠ 0 ? q : p)`. The choice of which formulas are
"negative" for this purpose is mostly arbitrary, with the only real
constraint being that negating a negative formula should produce a
positive one.
Note that conditional formulas themselves are considered to be
"positive" since negating them produces another conditional formula
with the same condition formula.
Reviewed By: ngorogiannis
Differential Revision: D23487502
fbshipit-source-id: 63606d89c
Summary:
Sort the subterms or subformulas of binary formulas that are
symmetric. This avoids redundant formulas such as both `x = y` and `y
= x`.
Reviewed By: ngorogiannis
Differential Revision: D23487501
fbshipit-source-id: 7e2295aba
Summary:
Add a Report.status type to represent the overall status of an
analysis run, and revise handling of backtraces to preserve the trace
of the originally-raised exception in more cases.
Reviewed By: ngorogiannis
Differential Revision: D23459518
fbshipit-source-id: a99fe0d14
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:
`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
Josh Berdine