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

Age	Commit message (Collapse)	Author
2021-07-01	Add option to limit the number of instantiation rounds (#6818)	Andrew Reynolds
	This adds an option to limit the number of instantiation rounds used by quantifiers engine. This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions. This PR also makes minor improvements to the quantifier utility infrastructure.
2021-04-12	Refactor and update copyright headers. (#6316)	Aina Niemetz

2021-04-08	Add identifiers for sources of incompleteness (#6311)	Andrew Reynolds
	This PR classifies all internal kinds of incompleteness as identifiers. It makes it so TheoryEngine records an identifier when its incomplete flag is set. The next step will be to possibly communicate this value to the user.