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

Age	Commit message (Collapse)	Author
2021-04-14	Rename public and private headers in src/include. (#6352)	Aina Niemetz

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	Update copyright headers to 2021. (#6081)	Aina Niemetz

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-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-06-19	Convert more uses of strings to words (#4584)	Andrew Reynolds
	Towards theory of sequences. This PR also adds support for sequences in default sygus grammars. Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
2020-06-16	Update copyright headers.	Aina Niemetz

2020-06-01	Incorporate sequences into the word interface (#4543)	Andrew Reynolds
	Also renames a function mkWord -> mkWordFlatten.
2020-04-15	Convert more cases of strings to words (#4206)	Andrew Reynolds

2020-04-03	Split sequences rewriter (#4194)	Andrew Reynolds
	This is in preparation for making the strings rewriter configurable for stats. This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas. No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.
2020-03-31	Convert more uses of string-specific functions (#4158)	Andrew Reynolds
	Towards theory of sequences.
2020-03-09	Convert more uses of strings to words (#3921)	Andrew Reynolds
	Towards theory of sequences. Also adds documentation to strncmp/rstrncmp and adds them to the Word interface.
2020-02-26	Some initial work on using words (#3819)	Andrew Reynolds
	Towards support for sequences (CVC4/cvc4-projects#23.)
2020-02-24	Utilities for words (#3797)	Andrew Reynolds
	This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23. Also improves documentation in regexp.h.