| Age | Commit message (Collapse) | Author |
|---|
|
* Remove support for conversions between uint32/uint16 and string.
* Temporarily disable regression.
|
|
Until now, all travis builds where built with gmp. This commit adds an additional debug build built with cln.
|
|
This commit adds two jobs (debug, with portfolio, test groups 0 and 1) to Travis.
Both jobs are added using matrix.include, based on the example in the documentation:
https://docs.travis-ci.com/user/languages/cpp/#GCC-on-Linux . This
unfortunately requires some code duplication but there does not seem to be a
way to do it in a much better fashion.
|
|
Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.
|
|
constraints from user input, add regressions. (#1060)
|
|
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
|
|
Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.
There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).
This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.
There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.
The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.
|
|
Coverity works without the SSL certificate workaround and is not needed anymore. Note that we don't require sudo anymore and we could switch to container-based Travis builds (instead of VM-based). However, container-based environments only provide 4G of memory (instead of 7.5G for VMs) , which is not enough for the current CVC4 build environment.
|
|
|
|
|
|
|
|
Before this commit, we were downloading cxxtest from Sourceforge. This commit
instead installs the Ubuntu package, which is easier and more reliable. Instead
of adding the package to the list of packages for Coverity and the common list
of packages, this commit changes the Coverity package list to just refer to the
common list of packages.
|
|
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
|
|
Algorithm was previously removed from src/util/regexp.h which broke
compilation on some platforms.
|
|
|
|
|
|
Cleaning up the CVC4::String class.
|
|
|
|
|
|
|
|
|
|
|
|
As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
|
|
|
|
|
|
|
|
|
|
Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.
|
|
* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4.
|
|
Fix compiler warnings in theory/arith/nonlinear_extension.cpp
|
|
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
|
|
|
|
|
|
|
|
|
|
Previous help message broke syntax highlighting in vim.
|
|
* Guard use of AigBitblaster with CVC4_USE_ABC.
This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.
|
|
|
|
|
|
|
|
Fix compiler warning in theory/quantifiers/term_database_sygus.cpp
|
|
To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sygus), update regressions.
|
|
|
