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

Age	Commit message (Collapse)	Author
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-03	More cleanup of includes to reduce compilation times (#6037)	Gereon Kremer
	Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2020-12-17	Simplify and fix check models (#5685)	Andrew Reynolds
	Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true. However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base. Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not. This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions. A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators. Fixes #5645.
2020-12-16	Move ownership of term formula removal to theory preprocessor (#5670)	Andrew Reynolds
	This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion. This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move. The next step will move the TheoryPreprocessor inside prop::TheoryProxy. There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.
2020-12-02	Update copyright headers.	Aina Niemetz

2020-11-26	Removing infrastructure related to SMT model (#5527)	Andrew Reynolds
	Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine. The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
2020-11-10	Do not mark extended functions as reduced based on decomposing contains (#5407)	Andrew Reynolds
	Fixes #5381.
2020-10-20	Split CheckModels utility to its own file (#5303)	Andrew Reynolds
	This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file. There are no major code changes in this PR, a few things were changed to be consistent to the coding standard.