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

Age	Commit message (Collapse)	Author
2020-07-12	Add support for string/sequence update (#4725)	Andrew Reynolds
	This adds basic support for string/sequence updating, which has a semantics that is length preserving.
2020-07-12	Remove ExprSequence (#4724)	Andres Noetzli
	Now that we can break the old API, we don't need an ExprSequence anymore. This commit removes ExprSequence and replaces all of its uses with Sequence. Note that I had to temporarily make sequence.h public because we currently include it in a "public" header because we still generate the code for Expr::mkConst<Sequence>().
2020-06-16	Update copyright headers.	Aina Niemetz

2020-05-27	Add the Expr-level sequence datatype (#4526)	Andrew Reynolds
	This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
2020-05-23	Add the sequence datatype (#4153)	Andrew Reynolds
	This class is the Node-level representation of a sequence. It is analogous to CVC4::String.