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

Age	Commit message (Collapse)	Author
2020-02-13	Update sygus v1 parser to use ParseOp utility (#3756)	Andrew Reynolds

2019-09-25	Use separate CMake project for CVC4 examples. (#3196)	Mathias Preiner

2019-09-06	Remove 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-14	cmake: Export CVC4 library interface. (#3179)	Mathias Preiner

2019-08-13	Introduce smt2 parsing utility ParseOp and refactor (#3165)	Andrew Reynolds

2019-06-21	Fix and simplify handling of --force-logic (#3062)	Andres Noetzli
	The `--force-logic` command line argument can be used to override a logic specified in an input file or to set a logic when none is given. Before this commit, both the `SmtEngine` and the parser were aware of that argument. However, there were two issues if an input file didn't specify a logic but `--force-logic` was used: - Upon parsing `--force-logic`, the `SmtEngine` was informed about it and set the logic to the forced logic. Then, the parser detected that there was no `set-logic` command, so it set the logic to `ALL` and emitted a corresponding warning. Finally, `SmtEngine::setDefaults()` detected that `forceLogic` was set by the user and changed the logic back to the forced logic. The warning was confusing and setting the logic multiple times was not elegant. - For eager bit-blasting, the logic was checked before resetting the logic to the forced logic, so it would emit an error that eager bit-blasting couldn't be used with the logic (which was `ALL` at that point of the execution). This was a problem in the competition because our runscript parses the `set-logic` command to decide on the appropriate arguments to use and passes the logic to CVC4 via `--force-logic`. This commit moves the handling of `--force-logic` entirely into the parser. The rationale for that is that this is not an API-level issue (if you use the API you simply set the logic you want, forcing a different logic in addition doesn't make sense) and simplifies the handling of the option (no listeners need to be installed and the logic is set only once). This commit also removes the option to set the logic via `(set-option :cvc4-logic ...)` because it complicates matters (e.g. which method of setting the logic takes precedence?). For the CVC and the TPTP languages the commit creates a command to set the logic in `SmtEngine` when the logic is forced in the parser instead of relying on `SmtEngine` to figure it out itself.
2018-10-20	Remove antlr_undefines.h. (#2664)	Mathias Preiner
	Is not required anymore since we don't use autotools anymore.
2018-09-22	cmake: Enable -Wall.	Mathias Preiner

2018-09-22	cmake: Add support for cross-compiling for Windows.	Mathias Preiner

2018-09-22	cmake: More documentation, clean up.	Aina Niemetz

2018-09-22	cmake: FindANTLR: Check if antlr3FileStreamNew is available.	Mathias Preiner

2018-09-22	cmake: Add make install rule.	Mathias Preiner

2018-09-22	cmake: 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-22	cmake: Move find_package to where it is actually needed.	Mathias Preiner

2018-09-22	cmake: Add library versioning for libcvc4.so.	Mathias Preiner

2018-09-22	cmake: Fix some includes.	Mathias Preiner

2018-09-22	cmake: Cleanup CMakeLists.txt files, remove SHARED.	Mathias Preiner

2018-09-22	cmake: Working build infrastructure.	Mathias Preiner
	TODO: cvc4autoconfig.h
2018-09-22	cmake: Added initial build infrastructure.	Aina Niemetz