cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2021-09-02	Driver & Options cleanup (#7109)	Gereon Kremer
	This PR does some cleanup in the driver and the options. It removes the now obsolete public attribute that allowed using the options in the driver, and removes a bunch of includes from the driver that are no longer necessary.
2021-09-01	No longer use direct access to options in driver (#7094)	Gereon Kremer
	This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().
2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-09	Rename CVC4__ header guards to CVC5__. (#6326)	Aina Niemetz

2021-04-01	Rename namespace CVC5 to cvc5. (#6258)	Aina Niemetz

2021-03-31	Rename namespace CVC4 to CVC5. (#6249)	Aina Niemetz

2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-03-05	Reimplement time limit mechanism for windows (#6049)	Gereon Kremer
	As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this. Fixes #5034.
2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	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.
2020-07-13	Implement --tlimit for windows (#4716)	Gereon Kremer
	The new mechanism for --tlimit only works for POSIX compatible systems (that implement setitimer). This PR implements an alternative (though roughly equivalent) approach for windows, based on SetWaitableTimer(). To make this work (without code duplication) we need to call the timeout_handler function from time_limit.cpp as the windows solution employs an asynchronous callback instead of signals. I used the opportunity to rename util.cpp to signal_handlers.cpp (as it really does not do anything else) and reformat the file. As I do not have a windows system at hand, I have not been able to actually test this apart from making sure that it compiles with the mingw setup.
2020-07-08	Re-implement handling of --tlimit (#4655)	Gereon Kremer
	As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed. In more detail, this PR: removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager) adds a new TimeLimitListener that lives in src/main uses TimeLimitListener directly in runCvc4() adds a signal handler for SIGALRM (that also uses the existing timeout_handler)