Age | Commit message (Collapse) | Author |
|
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
|
|
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
|
|
|
|
|
|
|
|
* 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").
|
|
|
|
Removing more miscellaneous throw specifiers.
|
|
|
|
Print statistics if CVC4 gets a SIGTERM signal.
|
|
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
|
|
This adds option --copyright which displays copyright information for CVC4. It further extends --show-config with copyright information and adds a banner with copyright information in interactive mode.
|
|
The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.
|
|
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.
|
|
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.
|
|
|
|
sygus), update regressions.
|
|
With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.
|
|
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
|
|
|