summaryrefslogtreecommitdiff
path: root/src/main
AgeCommit message (Collapse)Author
2020-03-12New C++ API: Remove support for (reset). (#4037)Aina Niemetz
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.
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
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>
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio build but there were some leftovers. This commit removes them.
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
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.
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
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.
2019-08-14Remove option --continued-execution. (#3189)Mathias Preiner
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-11-08cmake: Add option to explicitely enable/disable static binaries. (#2698)Mathias Preiner
2018-10-22CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)Andres Noetzli
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
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-09-24cmake: Add program prefix option. (#2515)Mathias Preiner
2018-09-22cmake: Build fully static binaries with option --static.Mathias Preiner
2018-09-22cmake: More documentation, clean up.Aina Niemetz
2018-09-22cmake: Add make install rule.Mathias Preiner
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
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.
2018-09-22cmake: Add portfolio support.Mathias Preiner
2018-09-22cmake: Add support for CxxTest.Aina Niemetz
2018-09-22cmake: Do not set global output directories for binaries and libraries.Mathias Preiner
2018-09-22cmake: Add module finder for readline.Mathias Preiner
2018-09-22cmake: Generate token headers.Mathias Preiner
2018-09-22cmake: Cleanup CMakeLists.txt files, remove SHARED.Mathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
TODO: cvc4autoconfig.h
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-10Fix portfolio command executor for changes from #2240. (#2294)Aina Niemetz
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-07Require Swig 3 (#2283)Andres Noetzli
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
2018-08-07Delete functions instead of using CVC4_UNDEFINED (#1794)Andres Noetzli
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.
2018-08-02Remove Subversion build info (#2250)Andres Noetzli
2018-08-01 InteractiveShell: Remove redundant options argument. (#2244)Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
* 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").
2018-02-02Restoring ostream format. Resolves a few CIDs 1362780. (#1543)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
Removing more miscellaneous throw specifiers.
2018-01-04Removing miscellaneous throw specifiers. (#1474)Tim King
2017-12-12Add SIGTERM handler. (#1440)Mathias Preiner
Print statistics if CVC4 gets a SIGTERM signal.
2017-11-03Sygus clean main (#1297)Andrew Reynolds
* Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field.
2017-10-10Add copyright information. (#1201)Aina Niemetz
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.
2017-09-20Fix issue #1081, memory leak in cmd executor (#1109)Andres Noetzli
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.
2017-08-31Replace CVC4_THREADLOCAL in interactive_shell (#1065)Andres Noetzli
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.
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
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.
2017-08-24Add include to fix buildAndres Noetzli
2017-08-04Set default language to smt lib 2.6 (including as a base language for ↵ajreynol
sygus), update regressions.
2017-07-17Remove PtrCloser (#198)Andres Noetzli
With C++11, we don't need PtrCloser anymore because we can just use std::unique_ptr.
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
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.
2017-07-07Update copyright headers.Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback