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

Age	Commit message (Collapse)	Author
2019-09-12	Update to standard implementation of contains term (#3270)	Andrew Reynolds

2019-09-04	More details in substitution function documentation (#3244)	yoni206

2019-07-22	Get operators in node (#3094)	yoni206
	This commit adds a function to node_algorithm.{h,cpp} that returns the operators that occur in a given node.
2019-06-05	Prevent letification from shadowing variables (#3042)	Andres Noetzli
	Fixes #3005. When printing nodes, we introduce `let` expressions on the fly. However, when doing that, we have to be careful that we don't shadow existing variables with the same name. When quantifiers are involved, we do not descend into the quantifiers to avoid letifying terms with bound variables that then go out of scope (see #1863). Thus, to avoid shadowing variables appearing in quantifiers, we have to collect all the variables appearing in that term to make sure that the let does not shadow them. In #3005, the issue was caused by a `let` that was introduced outside of a quantifier and then was shadowed in the body of the quantifier by another `let` introduced for that body.
2019-04-24	Do not use __ prefix for header guards. (#2974)	Mathias Preiner
	Fixes 2887.
2019-03-26	Update copyright headers.	Aina Niemetz

2019-03-15	Adding capture avoiding substitution (#2867)	Haniel Barbosa

2019-03-14	Add getFreeVariables method to node algorithm (#2852)	Andrew Reynolds

2018-10-12	Improvements to rewrite rules from inputs (#2625)	Andrew Reynolds

2018-09-05	Finer-grained inference of substitutions in incremental mode (#2403)	Andrew Reynolds

2018-08-16	Move node algorithms to separate file (#2311)	Andres Noetzli