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

Age	Commit message (Collapse)	Author
2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-09	Rename CVC4_ macros to CVC5_. (#6327)	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	Some more cleanup of includes (#6083)	Gereon Kremer
	This PR does some more cleanup of the includes.
2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2021-03-04	Add proper define for libpoly usage (#6050)	Gereon Kremer
	When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.
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.
2021-02-24	(proof-new) Add proofs for CAD solver (#5981)	Gereon Kremer
	This PR adds proofs for the CAD solver, based on the proof generator from the previous PR. Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work. Thus, the CAD proof rules are both trusted rules for now.
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-09-04	Use arith::InferenceManager for CAD lemmas (#5015)	Gereon Kremer
	This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
2020-08-19	(cad solver) Add a partial check method. (#4904)	Gereon Kremer
	This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead. It also fixes some confusion in excluding_interval_to_lemma...
2020-08-04	Add CAD-based solver (#4834)	Gereon Kremer
	Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail: add --nl-cad option add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation add new Inference types for the NlLemma class use CadSolver in NonlinearExtension (if --nl-cad is given)