projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Rename getAntecedent to getPremises (#5754)
[cvc5.git]
/
src
/
theory
/
strings
/
2021-01-08
mudathirmahgoub
Rename getAntecedent to getPremises (#5754)
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Add bags inference generator (#5731)
tree
|
commitdiff
2020-12-24
Haniel Barbosa
[proof-new] Only use old proofs for unsat cores if...
tree
|
commitdiff
2020-12-23
Andrew Reynolds
(proof-new) Miscelleneous fixes from proof-new (#5714)
tree
|
commitdiff
2020-12-16
mudathirmahgoub
Renamed InferInfo::getAntecedant to InferInfo::getAntec...
tree
|
commitdiff
2020-12-16
Andrew Reynolds
(proof-new) Use bound variable manager (#5679)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Fix SAT-context dependent issue in strings preregistrat...
tree
|
commitdiff
2020-12-11
Andrew Reynolds
Fix length assumption for deq norm emp rule (#5623)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-09
Aina Niemetz
Fix compiler warnings. (#5644)
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Make term indices in the strings base solver aware...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Proper implementation of expand definitions for sequenc...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Fix collect model values for sequences of sequences...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-01
Andres Noetzli
Improve rewriting of str.<= (#4848)
tree
|
commitdiff
2020-11-30
Andrew Reynolds
(proof-new) Proofs for regular expression elimination...
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Fix regular expression consume for nested star (#5518)
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Fix quantifiers scope issue in strings preprocessor...
tree
|
commitdiff
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
tree
|
commitdiff
2020-11-14
Andrew Reynolds
Fix double conflict in extended string solver (#5435)
tree
|
commitdiff
2020-11-13
Andrew Reynolds
Make regular expression difference left associative...
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Do not mark extended functions as reduced based on...
tree
|
commitdiff
2020-11-06
Andrew Reynolds
(proof-new) Miscellaneous changes to strings for proofs...
tree
|
commitdiff
2020-11-04
Andres Noetzli
Add constants from equality engine evaluation to model...
tree
|
commitdiff
2020-11-02
Andrew Reynolds
Update strings proxy variable map to be context indepen...
tree
|
commitdiff
2020-10-29
Andrew Reynolds
Set strings pending conflict flag (#5364)
tree
|
commitdiff
2020-10-29
Andrew Reynolds
(proof-new) Update the strings inference manager for...
tree
|
commitdiff
2020-10-23
Andrew Reynolds
Fix related to preregistering boolean term variables...
tree
|
commitdiff
2020-10-20
yoni206
Expand `seq.nth` lazily (#5287)
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Simplifications for proof rule checker...
tree
|
commitdiff
2020-10-07
Andrew Reynolds
(proof-new) Add the strings proof constructor (#4903)
tree
|
commitdiff
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
tree
|
commitdiff
2020-09-23
Andrew Reynolds
Allow E-matching by default when strings are enabled...
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-18
Andres Noetzli
[Strings] Fix extended equality rewriter (#5092)
tree
|
commitdiff
2020-09-16
Andres Noetzli
Only rewrite replace_re(_all) if regexp is const (...
tree
|
commitdiff
2020-09-09
Andrew Reynolds
(proof-new) Generalize single step helper in eager...
tree
|
commitdiff
2020-09-03
Andrew Reynolds
Make ExtTheory independent of Theory (#5010)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Andrew Reynolds
(new theory) Update TheoryStrings to new standard ...
tree
|
commitdiff
2020-08-31
Andrew Reynolds
Simplify interface for computing relevant terms. (...
tree
|
commitdiff
2020-08-28
Andrew Reynolds
Replace Theory::Set with TheoryIdSet (#4959)
tree
|
commitdiff
2020-08-24
Andrew Reynolds
Extend the standard Theory template based on equality...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Remove spurious theory methods calls (#4931)
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
tree
|
commitdiff
2020-08-19
Andrew Reynolds
Make sets and strings solver states inherit from Theory...
tree
|
commitdiff
2020-08-19
Andres Noetzli
Require `--strings-exp` when using `str.substr` (#4916)
tree
|
commitdiff
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-08-17
Andrew Reynolds
(proof-new) Prepare the theory of strings for proof...
tree
|
commitdiff
2020-08-16
Andrew Reynolds
Add non-emptiness to conclusion of positive RE star...
tree
|
commitdiff
2020-08-15
Andrew Reynolds
Minor cleanup related to notifications (#4898)
tree
|
commitdiff
2020-08-15
Andrew Reynolds
(proof-new) Add the strings proof checker (#4858)
tree
|
commitdiff
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Proof support in the strings term registry...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Make valuation class more robust to null underlying...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
(proof-new) Refactor regular expression operation ...
tree
|
commitdiff
2020-08-05
Andres Noetzli
[Strings] Add eager context-dependent evaluation (...
tree
|
commitdiff
2020-08-02
Andres Noetzli
Ensure strict length constraint for decompose rule...
tree
|
commitdiff
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
tree
|
commitdiff
2020-07-28
yoni206
Supporting seq.nth (#4723)
tree
|
commitdiff
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
tree
|
commitdiff
2020-07-16
Andrew Reynolds
Make ExtTheory a utility and not a member of Theory...
tree
|
commitdiff
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
tree
|
commitdiff
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
tree
|
commitdiff
2020-07-13
Andres Noetzli
Remove ExprSequence (#4724)
tree
|
commitdiff
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
tree
|
commitdiff
2020-07-01
Andrew Reynolds
Inferences and model construction taking into account...
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
tree
|
commitdiff
2020-06-28
Andrew Reynolds
Fix non-termination issues in simpleRegExpConsume ...
tree
|
commitdiff
2020-06-20
Andrew Reynolds
(proof-new) Make static methods in re-elim (#4623)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
(proof-new) Updates to strings term registry (#4599)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Clean the header file of TheoryStrings (#4272)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-15
Andrew Reynolds
Do RE derivation inference only for concrete constant...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
(proof-new) Minor updates to strings base solver (...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
Cardinality-related inferences per type in theory of...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
Add rewrite for str.replace_re. (#4601)
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Theory strings preprocess (#4534)
tree
|
commitdiff
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
tree
|
commitdiff
2020-05-30
Andrew Reynolds
Add the sequence type (#4539)
tree
|
commitdiff
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
tree
|
commitdiff
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
tree
|
commitdiff
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
tree
|
commitdiff
2020-05-26
Andrew Reynolds
(proof-new) Updates to strings skolem cache. (#4524)
tree
|
commitdiff
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expres...
tree
|
commitdiff
2020-05-22
Andrew Reynolds
(proof-new) Minor update to strings solver state (...
tree
|
commitdiff
2020-05-21
Andrew Reynolds
Throw logic exception for equality between regular...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Normal form equality conflicts and uniqueness check...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-04-30
Andrew Reynolds
Remove skolem share involving pre_first_ctn. (#4423)
tree
|
commitdiff
2020-04-30
Andrew Reynolds
Do not mark congruent terms are reduced (#4419)
tree
|
commitdiff
next