| Age | Commit message (Collapse) | Author |
|---|
|
|
|
There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.
Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Commit 629824db3911ab11ae286e4b14151a537602ba5a added options when
introducing the pseudo boolean processor that were never used. This
commit removes them.
|
|
|
|
|
|
|
|
|
|
(#1757)
|
|
|
|
|
|
|
|
|
|
This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).
|
|
|
|
|
|
|
|
|
|
This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).
|
|
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.
This includes improvements to the robustness of the sygus solver.
|
|
If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.
The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
|
|
|
|
(#1742)
|
|
|
|
|
|
|
|
|
|
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
|
|
TypeCheckingExceptionPrivate. (#1733)
While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.
|
|
|
|
|
|
(#1726)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
While reviewing #1695, I realized that bvminisat is leaking memory for
each call to setNotify(). This commit uses std::unique_ptr to fix the
issue. It also adds std::unique_ptr to manage d_minisat.
|
|
Our current build scripts did not work with Automake 1.16. At configure
time, the .swig_deps target in src/bindings/Makefile.am was executed due
to the `@mk_include@ .swig_deps` (which is not the case with older
versions of Automake). This ultimately caused configure to fail because
SWIG was complaining about missing files (generated source files, such
as src/expr/expr.h). This commit fixes the issue by adding
`-ignoremissing` to the call to SWIG. With that option, SWIG is not
complaining about the missing files and the dependency generation
completes successfully.
Currently, the src/bindings/compat/java/create_impl.py script is not
compatible with Python 3, which leads to errors when building on systems
where `python` links to Python 3 (e.g. on Arch Linux). This commit makes
the script compatible with both Python 2 and 3.
Our build scripts were using old -source/-target versions when calling
`javac`. Those are not supported by newer Java versions (e.g. Java 9).
This commit updates the version to 1.6, which is still fairly old, so
should be broadly supported.
Finally, some systems (e.g. Arch Linux' AUR package for SWIG 2) refer to
SWIG 2 as `swig-2`. This commit adds support for detecting this at
configure time.
|
|
|
|
|
|
|
|
This commit adds a rewrite for substrings of strings of length one to
the empty string if it can be shown that it is not possible that the
start position and the length are both greater than zero:
```
(str.substr "A" x y) --> "" if x = 0 |= 0 >= y
```
The commit introduces a set of functions to check such entailments
with assumptions.
|
|
|
