projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Add new interfaces to term formula removal and theory preprocess (#5717)
[cvc5.git]
/
src
/
theory
/
strings
/
2020-04-28
Andrew Reynolds
Update cardinality in strings to unicode standard ...
tree
|
commitdiff
2020-04-23
Andres Noetzli
Introduce best content heuristic for strings (#4382)
tree
|
commitdiff
2020-04-23
Andres Noetzli
Strings: Register skolems before sending lemma (#4381)
tree
|
commitdiff
2020-04-22
Andrew Reynolds
Ensure disequality splits are processed as lemmas ...
tree
|
commitdiff
2020-04-22
Andres Noetzli
Reinstantiate support for conjunctions in facts (#4377)
tree
|
commitdiff
2020-04-20
Andrew Reynolds
Refactor inference manager in strings to be amenable...
tree
|
commitdiff
2020-04-18
Andrew Reynolds
Track inference id for pending facts in strings (#4331)
tree
|
commitdiff
2020-04-16
Andrew Reynolds
Eliminate remaining references to parent TheoryStrings...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Move regular expression inclusion test to RegExpEntail...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Split TermRegistry object from TheoryStrings (#4312)
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Do not mark string extended functions as eliminated...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Convert more cases of strings to words (#4206)
tree
|
commitdiff
2020-04-14
Andrew Reynolds
Remove a few options (#4295)
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Explain non-emptiness by non-zero length in strings...
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Add a few stats to strings (#4252)
tree
|
commitdiff
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
tree
|
commitdiff
2020-04-07
Andrew Reynolds
Enum for all remaining string inferences (#4220)
tree
|
commitdiff
2020-04-06
Andres Noetzli
Refactor disequality processing in string solver (...
tree
|
commitdiff
2020-04-05
Andrew Reynolds
Add missing stat for lemmas based on inferences (#4214)
tree
|
commitdiff
2020-04-05
Andrew Reynolds
Type-independent preregistration of empty word (#4205)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-03
Andrew Reynolds
Split sequences rewriter (#4194)
tree
|
commitdiff
2020-04-02
Andrew Reynolds
Introduce enums for all string inferences, excluding...
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-31
Andrew Reynolds
Convert more uses of string-specific functions (#4158)
tree
|
commitdiff
2020-03-30
Andrew Reynolds
Rewrites for all remaining return statements in strings...
tree
|
commitdiff
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
tree
|
commitdiff
2020-03-29
Andrew Reynolds
Enumeration for String rewrites (#4173)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Add stats for string reductions, lemmas and conflicts...
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Generalize more string-specific functions (#4152)
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Care graphs based on polymorphic operators in strings...
tree
|
commitdiff
2020-03-25
Andres Noetzli
Support async-signal-safe printing of inferences (...
tree
|
commitdiff
2020-03-25
Andrew Reynolds
Generalize more uses of string-specific functions...
tree
|
commitdiff
2020-03-23
Andres Noetzli
Collect statistics about normal form inferences (#4127)
tree
|
commitdiff
2020-03-21
Andres Noetzli
Simplify heuristic in `processNEqc` (#4129)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Generalize mkConcat for types (#4123)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewri...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Refactor enumerator for strings (#4014)
tree
|
commitdiff
2020-03-19
Andres Noetzli
Only apply testConstStringInRegExp to const regexp...
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Removing a few deprecated options (#4052)
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Generalize type rules for strings to sequences (#3987)
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Convert more uses of strings to words (#3921)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-03-02
Andrew Reynolds
Split collect model info by types in strings (#3847)
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Convert more uses of string to word (#3834)
tree
|
commitdiff
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Fix large models for strings (#3835)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression differe...
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Some initial work on using words (#3819)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Move equivalence class info to its own file in strings...
tree
|
commitdiff
2020-02-24
Andrew Reynolds
Utilities for words (#3797)
tree
|
commitdiff
2020-02-23
Andrew Reynolds
Minor refactoring of equality notifications (#3798)
tree
|
commitdiff
2020-02-22
Andrew Reynolds
Move check memberships to reg exp solver (#3793)
tree
|
commitdiff
2020-02-22
Andrew Reynolds
Move cardinality inference scheme to base solver in...
tree
|
commitdiff
2020-02-21
Andrew Reynolds
Split extended functions solver in strings (#3768)
tree
|
commitdiff
2020-02-16
Andres Noetzli
Activate reverse variant of F-Split inference (#3745)
tree
|
commitdiff
2020-02-15
Andrew Reynolds
Move proxy variables to InferenceManager in strings...
tree
|
commitdiff
2020-02-11
Andres Noetzli
Remove `--strings-binary-csp` option (#3743)
tree
|
commitdiff
2020-02-11
Andres Noetzli
Refactor `CoreSolver::processSimpleNEq()` (#3736)
tree
|
commitdiff
2020-02-08
Andrew Reynolds
Split strings finite model finding strategy (#3727)
tree
|
commitdiff
2020-02-08
Andrew Reynolds
Split core solver from the theory of strings (#3713)
tree
|
commitdiff
2020-02-04
Andrew Reynolds
Split base solver from the theory of strings (#3680)
tree
|
commitdiff
2020-02-04
Andres Noetzli
Revert semantic change from refactoring (#3711)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Move disequality list to solver state in strings (...
tree
|
commitdiff
2020-01-30
Andres Noetzli
Better heuristics for marking congruent variables ...
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Modularize more steps in the strings strategy (#3676)
tree
|
commitdiff
2020-01-30
Andrew Reynolds
Minor updates to string utilities (#3675)
tree
|
commitdiff
2020-01-10
Andres Noetzli
Optimize str.substr reduction (#3595)
tree
|
commitdiff
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Simplify rewrite for character matching (#3545)
tree
|
commitdiff
2019-12-07
Andres Noetzli
Use str.subtr in str.to.int/int.to.str reduction (...
tree
|
commitdiff
2019-12-06
Andres Noetzli
Add lemma for str.to.int/int.to.str (#3541)
tree
|
commitdiff
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
tree
|
commitdiff
2019-12-04
Andres Noetzli
Fix corner case in model construction of strings (...
tree
|
commitdiff
2019-12-03
Andres Noetzli
Rewrite `str.contains` used for character matching...
tree
|
commitdiff
2019-11-27
Andrew Reynolds
Fix indexof range lemma (#3499)
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Move more string utility functions (#3398)
tree
|
commitdiff
2019-11-01
Andres Noetzli
Fix and refactor TheoryStrings::checkFlatForms() (...
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-23
Andrew Reynolds
Fixes for SyGuS + regular expressions (#3313)
tree
|
commitdiff
2019-10-16
Andrew Reynolds
Solver state for theory of strings (#3181)
tree
|
commitdiff
2019-10-14
Andrew Reynolds
Minor refactor in strings rewriter (#3387)
tree
|
commitdiff
2019-10-08
Piotr Trojanek
prefer prefix ++ operator for iterators
tree
|
commitdiff
2019-10-06
Andrew Reynolds
Fix str to int reduction (#3358)
tree
|
commitdiff
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
tree
|
commitdiff
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
tree
|
commitdiff
2019-09-27
Andrew Reynolds
Fix case of disjunctive conclusion in strings (#3254)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Fix off by one error in strings flat form explanation...
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
tree
|
commitdiff
2019-08-30
Andres Noetzli
Fix out-of-bounds access in regexp inclusion test ...
tree
|
commitdiff
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Infer emptiness instead of splitting when a string...
tree
|
commitdiff
2019-08-22
Andrew Reynolds
Local substitutions for context-depdendent simplificat...
tree
|
commitdiff
next