summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-29Move decision manager into theory inference manager (#6231)Andrew Reynolds
2021-03-21Simplify strings term registration (#6174)Andrew Reynolds
2021-03-20Improved tracing for equivalence classes of EE (#6169)Andrew Reynolds
2021-03-16Further standardization of strings statistics (#6128)Andrew Reynolds
2021-03-15Fix rewrite for double replace (#6152)Andrew Reynolds
2021-03-15Replace HistogramStat by IntegralHistogramStat (#6126)Gereon Kremer
2021-03-11First refactoring of statistics classes (#6105)Gereon Kremer
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-11(proof-new) Clean up uses of witness with skolem lemmas (#6109)Andrew Reynolds
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
2021-03-10Fix extended equality rewrite involving replace. (#6104)Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08(proof-new) Separating optimizations for strings skolem caching (#6064)Andrew Reynolds
2021-03-08Do not process conjunctions as facts in strings (#6065)Andrew Reynolds
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-25(proof-new) Fix regular expression unfolding under substitution (#5958)Andrew Reynolds
2021-02-22Require length-in-conclusion form for strings inferences (#5953)Andrew Reynolds
2021-02-19Refactoring theory inference process (#5920)Andrew Reynolds
2021-02-19Fix rewrite for contains over replace (#5924)Andrew Reynolds
2021-02-19Remove string stat for inferences (#5932)Andrew Reynolds
2021-02-18Add statistic for InferenceId to TheoryInferenceManager. (#5913)Gereon Kremer
2021-02-11Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)Gereon Kremer
2021-02-11Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)Gereon Kremer
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
2021-02-11Fix spurious assertion failure in regexp normalization (#5852)Andrew Reynolds
2021-02-10Simplify method for inferring proxy lemmas in strings (#5789)Andrew Reynolds
2021-02-08Fix disequality between seq.unit terms (#5880)Andrew Reynolds
2021-02-08Avoid spurious traversal of terms during preregistration (#5860)Andrew Reynolds
2021-01-24rename InferInfo::d_newSkolem to InferInfo::d_skolems (#5799)mudathirmahgoub
2021-01-15Implement --no-strings-lazy-pp as a preprocessing pass (#5777)Andrew Reynolds
2021-01-13Split eager solver from strings solver state (#5775)Andrew Reynolds
2021-01-08Rename getAntecedent to getPremises (#5754)mudathirmahgoub
2021-01-08Add bags inference generator (#5731)mudathirmahgoub
2020-12-24[proof-new] Only use old proofs for unsat cores if no proof new (#5725)Haniel Barbosa
2020-12-23(proof-new) Miscelleneous fixes from proof-new (#5714)Andrew Reynolds
2020-12-16Renamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)mudathirmahgoub
2020-12-16(proof-new) Use bound variable manager (#5679)Andrew Reynolds
2020-12-14Fix SAT-context dependent issue in strings preregistration (#5564)Andrew Reynolds
2020-12-11Fix length assumption for deq norm emp rule (#5623)Andrew Reynolds
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-09Fix compiler warnings. (#5644)Aina Niemetz
2020-12-08Make term indices in the strings base solver aware of types (#5589)Andrew Reynolds
2020-12-08Proper implementation of expand definitions for sequences (#5616)Andrew Reynolds
2020-12-07Fix collect model values for sequences of sequences (#5579)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-12-01Improve rewriting of str.<= (#4848)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback