Code

String theory support#165

Code

Draft

raf-nr wants to merge 65 commits intoUnitTestBot:mainUnitTestBot/ksmt:mainfrom raf-nr:string-theoryraf-nr/ksmt:string-theoryCopy head branch name to clipboard

+5,411-75

Commits

Commits on Dec 3, 2024

• Add string sort to core

  raf-nr

  committed
  183449f

• Add regex sort to core

  raf-nr

  committed
  25db759

• Add string and regex sorts to context

  raf-nr

  committed
  3b52e78

• Implement string literal's expr and decl

  raf-nr

  committed
  6815d4d

• Implement regex literal's expr and decl

  raf-nr

  committed
  e98b386

• Implement strings concatenation

  raf-nr

  committed
  c52235a

• Implement strings length expr and decl

  raf-nr

  committed
  2bdb945

• Implement expr and decl for translation string to a regex

  raf-nr

  committed
  779b5c2

• Implement regular expressions concatenation

  raf-nr

  committed
  4b8d5ad

• Implement regular expressions union

  raf-nr

  committed
  0099dc3

• Implement regular expressions intersection

  raf-nr

  committed
  ce1a550

• Implement regular expressions difference and Kleene closure

  raf-nr

  committed
  743b758

• Implement regular expressions Kleene cross

  raf-nr

  committed
  3a1c7c1

• Implement prefixOf and suffixOf strings' operations

  raf-nr

  committed
  5a139cd

Commits on Dec 4, 2024

• Implement operation to check whether a string belongs to a regex

  raf-nr

  committed
  fd259a5

• Implement operations for comparing strings

  raf-nr

  committed
  2a500d7

• Implement regular expression complement operation

  raf-nr

  committed
  d771e78

• Fix imports

  raf-nr

  committed
  c8cb6bf

• Add regular expression constants

  raf-nr

  committed
  844db59

• Implement operation to make regex optional

  raf-nr

  committed
  4182e5a

• Implement strings' contains operation

  raf-nr

  committed
  79b6f20

Commits on Dec 8, 2024

• Describe operations on strings and regex that have not yet been implemented

  raf-nr

  committed
  0837aa9

• Syntactic sugar for comparing string expressions

  raf-nr

  committed
  45bd801

• Syntactic sugar for strings and regex concatenation

  raf-nr

  committed
  f9da6a6

• Syntactic sugar for strings literals and length expr

  raf-nr

  committed
  ee0ff54

• Syntactic sugar for suffixOf, prefixOf, contains operations

  raf-nr

  committed
  eb068cc

• Syntactic sugar for inRegex, toRegex operations

  raf-nr

  committed
  1b38d12

• Implement replace operations for strings

  raf-nr

  committed
  f42d7eb

• Implement regex range operation

  raf-nr

  committed
  01a57ef

• Implement operations, that maps strings to and from integers

  raf-nr

  committed
  1d22225

• Implement strings' replace operations based on regex

  raf-nr

  committed
  4363af9

Commits on Dec 9, 2024

• Implement remaining operations on strings and transformers for strings

  raf-nr

  committed
  7cfad2e

• Describe and implement transformers interfaces for regex

  raf-nr

  committed
  98f82c9

• Add string and regex declarations in visitor

  raf-nr

  committed
  8e0fafb

• Add exceptions that Bitwuzla does not support string theory

  raf-nr

  committed
  889642f

• Add string theory to KTheory class

  raf-nr

  committed
  c8958dc

• Fix str name in KTheory class

  raf-nr

  committed
  c5b9f7e

• Implement string and regex sorts cvc5 internalizer

  raf-nr

  committed
  2e2286d

Commits on Dec 10, 2024

• Add string and regex expressions internalizer for cvc5

  raf-nr

  committed
  eac27d5

• Add cvc5 internalizer for substrings and indexOf expressions

  raf-nr

  committed
  3dc16f8

• Implement converter from cvc5 to ksmt

  raf-nr

  committed
  62b1a6a

• Implement string/regex methods for cvc5 uninterpreted sort collector

  raf-nr

  committed
  811d531

• Add exceptions that Yices does not support string theory

  raf-nr

  committed
  97bead4

• Fix typo in exceptions' messages

  raf-nr

  committed
  b3ecd8a

Commits on Dec 11, 2024

• Fix yices solver configuration after adding string theory

  raf-nr

  committed
  81ac05f

• Delete regex literal expression

  raf-nr

  committed
  ca8bff6

• Fix string theory name in KTheory class

  raf-nr

  committed
  b54264f

Commits on Dec 12, 2024

• Change the names of classes and methods, do the code formatting

  raf-nr

  committed
  6daeecc

• Update sort visitor implementation for theory requirement

  raf-nr

  committed
  ce19526

• Add string and regex sorts to z3 sort internalizer

  raf-nr

  committed
  c9e2e19

• Implement z3 internalizer some methods for strings

  raf-nr

  committed
  07bdf4b

• Add string literals printer with quotes

  raf-nr

  committed
  18d690d

• Implement toLower, toUpper and reverse string operations

  raf-nr

  committed
  3e7f8bd

Commits on Dec 14, 2024

• Add string and regex default values

  raf-nr

  committed
  a124b8b

• Fix bug with regex constants in cvc5

  raf-nr

  committed
  ceb95a2

Commits on Dec 17, 2024

• Add string and regex sorts serializer and deserializer

  raf-nr

  committed
  9c2e89b

• Add string and regex expressions serializer/deserializer

  raf-nr

  committed
  1e31092

• Partially implement z3 string internalizer/converter

  raf-nr

  committed
  17d40f5

Commits on Dec 18, 2024

• Fully implement z3 converter

  raf-nr

  committed
  8f0921e

• Implement regex power and loop operations

  raf-nr

  committed
  d16f8d9

• Fix regex power and loop expr deserializer

  raf-nr

  committed
  57db57a

• Add stubs in symfpu visitors

  raf-nr

  committed
  4f3c819

Commits on Dec 19, 2024

• Fix typo in z3 converter

  raf-nr

  committed
  0c22147

• Describe functions for further simplification of expressions

  raf-nr

  committed
  dbb8531

• Fix cvc5 sort converter

  raf-nr

  committed
  a865074