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:
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:
Require Exp clients to provide the type of the result of arithmetic
operations.
Reviewed By: mbouaziz
Differential Revision: D12854511
fbshipit-source-id: cc91a39ca
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
Josh Berdine
Mehdi Bouaziz