| Age | Commit message (Collapse) | Author |
|---|
|
This moves .cpp files to directory test/unit/api/cpp and python files in
test/python/unit/api to test/unit/api/python.
|
|
Previously, on CI, unit tests and api tests were run twice since we use
a ctest exclude rule based on labels (-LE) which includes unit and api
tests, but then run them separately again. This cleans up the CI test
configuration.
Further, unit gtest unit tests were added with gtest_add_tests, which
adds every test of a unit test binary as a single test target to ctest.
In theory, this may speed up testing (because more parallelism) but in
practice it slows it down due to the start up overhead. It also clutters
CI output. This cleans up the gtest configuration to add the gtest unit
tests per test binary rather then per test of a test binary.
|
|
This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.
|
|
This PR resolves that issue by checking that a -W<error-class> flag exists before trying to use the -Wno-<error-class> flag.
|
|
This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).
|
|
Fixes #6866. The `theory_airth_cad_white` unit test has been failing on
some platforms (e.g., macOS) due to statically linking libpoly in
libcvc5 and then separately linking it in the unit tests. This resulted
in issues with `static` variables. This commit fixes the issue by
avoiding linking libpoly in the unit tests and instead relying solely on
libcvc5.
Co-authored-by: Ouyancheng <1024842937@qq.com>
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
|
|
|
|
This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system.
Also, it does a bit of cleanup.
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
This PR enables us to build gtest ourselves if it is not already installed.
|
|
|
|
This is in preparation for renaming src/expr to src/node.
|
|
|
|
|
|
This fixes some issues that break the nightly ASAN builds with clang.
|
|
|
|
This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.
|
|
In the new SMT-LIB string standard, re.loop and re.^ are indexed
operators but the printer was not updated to print them correctly. This
commit adds support for printing re.loop and re.^.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
|
|
* [proof] Eliminate the side condition in er.plf
By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.
* [proof] Changed er_proof.cpp in line with signature
The new signature requires slightly different proof printing.
* [proof] clang-format er_proof.cpp
* Fix tests
* [proof] Actually delete the SC
* Apply suggestions from code review
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof
* Gate the lfsc invocation on the build system
* Properly gate the lfsc check on the build system
* gate the plf_signatures forward def on the build system
|
|
CxxTest's generator has one of three names, depending on the CxxTest
version:
* `cxxtestgen.py`, a python program
* `cxxtestgen`, some kind of program with a shebang
* `cxxtestgen.pl`, a perl program
We were mistakenly assuming that the `cxxtestgen` form was always a
python program.
Now, if we find that form on the system, we assume that it is has a
shebang, and is executable.
|
|
Adds option --ninja to configure.sh.
|
|
|
|
* Copied old DRAT data-structure files.
Next step: clean up the code, and adapt them to our current usage plans.
* Polished the DRAT class.
Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.
More explicit about whether methods handle binary or text.
Better constructor patterns
* Added implementation of textual DRAT output
* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction
* use emplace_back
* Addressing Yoni's first review
* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation
* Removed aside about std::string
* Addressed Mathias' comments
Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.
* Unit tests for binary DRAT parsing
* Added text output test
* s/white/black/ derp
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
|
|
|
|
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
