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

Age	Commit message (Collapse)	Author
2021-09-09	Remove `TheoryState::options()` (#7148)	Andres Noetzli
	This commit removes TheoryState::options() by changing more classes to EnvObjs.
2021-08-20	Use Env class in nonlinear extension (#7039)	Gereon Kremer
	This PR refactors the nonlinear extension(s) to access options only via the environment class.
2021-05-13	Add std::hash overloads for Node, TNode and TypeNode. (#6534)	Mathias Preiner
	Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-12	Refactor and update copyright headers. (#6316)	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-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-07	Add bitwise refinement mode for IAND (#5328)	makaimann
	Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits. For example, with a 1-bit granularity, you might learn a lemma like: ((_ iand 4) x y), value = 1 actual (2, 3) = 2 bv-value = #b0001 bv-actual (#b0010, #b0011) = #b0010 IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y))) (and (and true (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0))) (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0)))) ; BITWISE_REFINE which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.
2020-12-02	Update copyright headers.	Aina Niemetz

2020-10-14	bv2int: implementing the iand-sum mode (#5265)	yoni206
	There are 3 potential modes to lazily treat the iand operator: (1) by value (typical CEGAR loop) (2) by sum (lazily expanding each iand node into a sum of ITEs) (3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities) This PR implements (2). The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
2020-09-23	Make IAND solver use inference manager. (#5126)	Gereon Kremer
	This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.
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-07-01	Add solver for integer AND (#4681)	Andrew Reynolds
	This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.