Summary:
This patch adds an embarrassingly inefficient implementation of a
decision procedure for equality in the theories of uninterpreted
functions and linear arithmetic. A Shostak-style approach, where a
single congruence closure structure is shared by all theories, is
used. This is mostly based on the corrected variant of Shostak's
algorithm from:
Harald Rueβ and Natarajan Shankar. 2001. Deconstructing Shostak. In
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer
Science (LICS '01).
Reviewed By: jvillard
Differential Revision: D14251655
fbshipit-source-id: 8a080145f
Summary:
Now with rational coefficients, dividing a polynomial by an integer
can be simplified.
Reviewed By: jvillard
Differential Revision: D14251656
fbshipit-source-id: 01094bc61
Summary:
Exp simplification must not generate fresh subexpressions in its
output that do not appear in its input, lest congruence closure gets
confused. Previously this check only considered immediate
subexpressions, which is overly restrictive.
Reviewed By: ngorogiannis
Differential Revision: D14251653
fbshipit-source-id: f8d5d9756
Summary:
Trace.report is essentially redundant with Trace.fail, and does not
behave as well wrt flushing when raising exceptions.
Reviewed By: ngorogiannis
Differential Revision: D14251657
fbshipit-source-id: 69a61c915
Summary:
Represent Add and Mul directly as associative and commutative nary
operations, rather than have Add and Mul operators and a separate AppN
nary application.
Reviewed By: ngorogiannis
Differential Revision: D14231544
fbshipit-source-id: 4fb7a06cf
Summary:
- Add nary expressions implemented using a form of multisets which
support any integer multiplicity
- Reimplement polynomials using new nary expressions
- Move the decomposition of exps into "base plus offset" form into
Exp, to enforce simplification invariants
- Revise expression simplification to cooperate with congruence
closure (mainly: simplification should not invent new
subexpressions)
- Reimplement congruence closure plus integer offsets to
+ cope with new representation of polynomials using nary expression forms
+ be diligent about maintaining which expressions are in the relation
+ add lots of invariant checking for the correlations between the
componnents of the congruence closure data structures
Reviewed By: jvillard
Differential Revision: D14075512
fbshipit-source-id: 2dbaf3d11
Summary:
Even pretty-printed congruence relations are verbose, and most
operations do not change much of the relation. So on return, print
only the symmetric difference between input and output relations.
Reviewed By: mbouaziz
Differential Revision: D14075513
fbshipit-source-id: b1f0ae6d0
Summary:
This is significant for operations involving the NULL pointer, which
is an integer of pointer type.
Reviewed By: mbouaziz
Differential Revision: D14075516
fbshipit-source-id: b727cb4c8
Summary:
Trace.parse is exposed across a module boundary, so handle its own
exceptions and return an `error`.
Reviewed By: mbouaziz
Differential Revision: D14081602
fbshipit-source-id: 4087c5d5b
Summary:
This allows exposing `Trace.parse`, which can be used to call
`Trace.init` in test code.
Reviewed By: mbouaziz
Differential Revision: D14075522
fbshipit-source-id: 4715c643f
Summary:
This makes it convenient to call
`Trace.init ~margin:70 ~config:all ()`
in test modules.
Reviewed By: mbouaziz
Differential Revision: D14075515
fbshipit-source-id: 3d3940eb1
Summary:
Comparison operations always return Typ.bool, and Add/Mul/Integer exps
are typed. Use these types to check that arguments are type correct up
to Typ.castable.
Reviewed By: mbouaziz
Differential Revision: D12854504
fbshipit-source-id: fff1426d5
Summary:
Require Exp clients to provide the type of the result of arithmetic
operations.
Reviewed By: mbouaziz
Differential Revision: D12854511
fbshipit-source-id: cc91a39ca
Summary:
Previously only the arguments of binary operations on integers were
clamped to the given bitwidth, but the results could overflow. This
was incorrect.
Also, use a clamped version of equality to simplify equality
expressions. This was previously overlooked.
Reviewed By: mbouaziz
Differential Revision: D12854502
fbshipit-source-id: 8786b4217
Summary:
Running `dune build check` while `dune build --watch` is running
intermittently produces strange errors due to race conditions between
the two.
Reviewed By: mbouaziz
Differential Revision: D12854510
fbshipit-source-id: 348a902bc
Summary:
Types of integer constants, in particular their bit-width, are
necessary for:
- correctly interpreting bitwise operations (e.g. `-1 xor 1` at type
`i1` is `0` while without the type the result is `-2`), and;
- distinguishing between integers and booleans, which are one-bit
integers, since booleans admit stronger algebraic simplification.
Note that code does genuinely treat 1-bit integers interchangeably as
booleans and integers, e.g. with expressions such as `e + (b != 42)`.
Therefore a lighter-weight early syntactic distinction between boolean
and bitwise operations is nontrivial/impossible to make robust.
This patch:
- adds the type to the representation of Exp.Integer;
- adds checks that Integer values fit within their specified bit-width
- factors out code handling 1-bit integers as booleans into `Z`, as it
is easy to make mistakes when forgetting that `-1`, not `1`, is the
representation of `true`;
- corrects the treatment of Exp.Convert in some cases involving
treating negative integers as unsigned;
- corrects and strengthens Exp simplification based on the bit-width
information;
- removes the `e - e ==> 0` simplification, due to not having the type
for `0`.
Reviewed By: mbouaziz
Differential Revision: D10488407
fbshipit-source-id: ff4320a29
Summary:
The main motivation is to factor out the code that determines the test
condition, e.g. to uniformly test `!= 0` vs `= 1`.
Also a convenience, and there are enough uses to make it worthwhile
and a readability improvement.
Reviewed By: mbouaziz
Differential Revision: D10488408
fbshipit-source-id: 520e843f3
Summary:
Just a convenience, but there are enough uses to make it worthwhile,
and a readability improvement.
Reviewed By: mbouaziz
Differential Revision: D10488404
fbshipit-source-id: 30cca06d5
Summary:
`sledge -c foo.bc` generates a binary file `foo.bc.llair` which can be
analyzed with `sledge foo.bc.llair`, and converted to textual form
with `sledge -c foo.bc.llair -o foo.llair`. Binary files are not
compatible between debug and release builds.
Reviewed By: mbouaziz
Differential Revision: D10389473
fbshipit-source-id: dfcabf33b
Josh Berdine
Mehdi Bouaziz