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-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-01-07	Make sure polynomials are properly factorized in nl-cad (#5733)	Gereon Kremer
	CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726. Fixes #5726.
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-17	(cad-solver) Fix square-free-basis computation (#5085)	Gereon Kremer
	This PR fixes a subtle issue when making the polynomials of two subsequent (overlapping) intervals relative square-free. We now make sure that the resulting polynomials are ignored (if constant) or pushed to the lower dimension (if lower main variable). Also, we now appropriately update the main polynomials of the corresponding intervals.
2020-07-30	Adds the interface for the CAD-based arithmetic solver. (#4773)	Gereon Kremer
	This PR adds some utilities and, most importantly, the interface of the new CAD-based solver. The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code structure follows the paper rather closely.
2020-07-21	Preparations for a CAD-based arithmetic solver (#4762)	Gereon Kremer
	Based on #4679, this PR contains further preparations for a CAD-based arithmetic solver that extends the current NonlinearExtension. In detail, it provides: a Constraints class that manages all (polynomial) constraints visible to the cad solver, a collection of methods used for cad projections, a VariableOrdering class that provides different variable ordering heuristics tailored to cad, an extension to the NlModel class, allowing for witness terms, further conversion methods, in particular between Node and poly::Polynomial, poly::Value and RealAlgebraicNumber.