| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
This commit fixes an issue with calling make clean && make.
The final doc/libcvc4.3 is now generated during ./autogen.sh and should not
be deleted with make clean.
|
|
|
|
|
|
|
|
invariant synthesis (#1703)
|
|
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.
The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.
This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
|
|
|
|
|
|
|
|
|
|
NonLinearExtension (#1633)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Cryptominisat has name conflicts with the other Minisat implementations since
the Minisat implementations export var_Undef, l_True, ... as macro whereas
Cryptominisat uses static const. In order to avoid these conflicts we
forward declare CMSat::SATSolver and include the cryptominisat header only
in cryptominisat.cpp.
Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.
|
|
make units does not fail if we have compile error for a unit test, however, make check does.
-Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings.
Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds.
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
|
|
|
|
This commit removes the unused printf functions from the output utilities. It also adds `const` keywords where possible. Finally, it removes overloaded `const char*` functions if the same function existed for `const std::string&` and the `const char*` version was only casting the `const char*` to an `std::string`. This conversion happens implicitly, so the `const char*` version is not needed.
|
|
|
|
Adds missing override keywords.
|
|
|
|
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
|
|
|
|
|
