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

Age	Commit message (Collapse)	Author
2020-10-19	(proof-new) Update preprocessing pass context for proofs (#5298)	Andrew Reynolds
	This sets up the preprocessing pass context in preparation for proof production. This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs. This PR also makes the "apply subst" preprocessing pass proof producing.
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-16	Dump commands in internal code using command printing functions. (#5040)	Abdalrhman Mohamed
	This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
2020-08-06	Split preprocessor from SmtEngine (#4854)	Andrew Reynolds
	This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal). It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.