search

TorXakis / TorXakis

A tool for Model Based Testing
BSD 3-Clause "New" or "Revised" License
47 stars 13 forks source link

String comparison operators missing #883

Open pjljvandelaar opened 5 years ago

pjljvandelaar commented 5 years ago

As a user I would like to lexically sort strings, e.g. to make a dictionary. However, TorXakis lacks the operators <=, <, >, and >= for strings.

pjljvandelaar commented 5 years ago

Z3, CVC4 & SMTLIB also lacks these operators.

pjljvandelaar commented 5 years ago

Is part of new proposal for strings: 

  ; Lexicographic ordering
  (str.< String String Bool :chainable)

For more details, see http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

pjljvandelaar commented 5 years ago

The nightly build of z3 could be used to experiment: See https://github.com/Z3Prover/z3/commit/218edbe9c68c7906971e1660510a6e7afe933ca6

pjljvandelaar commented 5 years ago

Also cvc4 supports str.< and str.<=.