Strings - Revision history

Ajreynol: /* Extended Functions */

2018-12-11T18:35:47Z

‎Extended Functions

2018-12-11T18:34:01Z

2018-12-11T18:31:58Z

2018-12-11T18:31:22Z

2018-12-11T18:30:58Z

‎Extended Functions

2018-12-11T18:30:36Z

‎Theory Signature

2018-12-11T18:29:50Z

2018-12-11T18:29:34Z

‎Options

2018-12-11T18:28:01Z

‎Options

2018-12-11T18:27:28Z

‎Options

@@ Line 313: / Line 313: @@
 ==Extended Functions==
 Following functions are available when using the --strings-exp option.
 String Char-At:

@@ Line 509: / Line 509: @@
 =References=
 * Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. [http://dl.acm.org/citation.cfm?id=2994123 An efficient SMT solver for string constraints]. Formal Methods in System Design. 2016.
 * Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. [http://link.springer.com/chapter/10.1007/978-3-319-24246-0_9 A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings]. In Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), Wroclaw, Poland, 2015.
 * Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters. [http://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_43 A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions].In Proceedings of the 26th International Conference on Computer Aided Verification (CAV'14), Vienna, Austria, 2014.
 * Tianyi Liang. [http://ir.uiowa.edu/etd/1478/ Automated reasoning over string constraints]. PhD Dissertation, Department of Computer Science, The University of Iowa, Dec 2014.

@@ Line 362: / Line 362: @@
   (int.to.str i)
 where i is an integer term. It returns the corresponding string if i is a natural number; otherwise, it returns an empty string.
 =Limitations=

@@ Line 255: / Line 255: @@
 where s is a string term.
-==Escape Sequences for Regular Expressions==
+==Regular Expression Memberships==
-Currently, it is for CVC format only. (Coming soon.)
-−
-==Symbolic Regular Expression==
 Membership Constraint:
    (str.in.re s r)

@@ Line 316: / Line 316: @@
 ==Extended Functions==
 Following functions are available when using the --strings-exp option.
 String Char-At:

@@ Line 208: / Line 208: @@
 '''Note:''' The alphabet will change to the one prescribed by the SMT-LIB standard
 once there is one.
 ==Escape Sequences in String Constants==

@@ Line 199: / Line 199: @@
 to find a solution with a reasonably large timeout.
-By default, the strings solver uses the standard ASCII alphabet, which has cardinality 256.
+Currently, the solver's theory is based on an alphabet consisting of the 256
-A ''printable'' character is any character with numerical value between 0x20 and 0x7e
+characters from (8-bit) Extended ASCII.
-in the standard US ASCII encoding.
+Since there are several versions of Extended ASCII, we allow string constants
 To limit the alphabet of the strings solver to the 128 printable ASCII characters, use:
    (set-option :--strings-print-ascii)
 ==Alphabet==