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

Age	Commit message (Collapse)	Author
2020-04-28	Support the SMT-LIB Unicode string standard by default (#4378)	Andrew Reynolds
	This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml. I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards. This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.
2020-03-31	Support char smt-lib syntax (#4188)	Andrew Reynolds
	Towards support for the strings standard. Adds support to (_ char #x ... ) syntax for characters.
2020-03-27	Support unicode internal representation and escape sequences (#3852)	Andrew Reynolds
	Work towards support for the strings standard. This updates the string solver and parser such that: The internal representation of strings is vectors of code points, Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models, The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings, Handle unicode escape sequences according to the SMT-LIB standard in String, Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary, Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.