| Age | Commit message (Collapse) | Author |
|---|
|
LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.
|
|
For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.
|
|
[LFSC] Minor fixes/improvements
|
|
- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions
|
|
In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).
|
|
|
|
child arguments after successful comparison).
|
|
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
|
|
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
|
|
(mostly whitespace differences).
|
|
|
|
|
|
|
|
(problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.
|
|
|
|
|
