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

Age	Commit message (Collapse)	Author
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-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.
2021-03-02	Clean up includes to reduce compile times (#6031)	Gereon Kremer
	This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2020-12-02	Update copyright headers.	Aina Niemetz

2020-10-21	(proof-new) Updates to lazy proof chain (#5317)	Andrew Reynolds
	Support for a default proof generator, which is optionally not called recursively. This is required for preprocessing.
2020-09-28	[proof-new] Adds a proof manager for the SAT solver (#5140)	Haniel Barbosa
	Tracks the refutation proof built by Minisat. See the header for extensive explanations. This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).
2020-09-16	[proof-new] Adds Lazy CDProof chain data-structure (#5060)	Haniel Barbosa
	A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.