summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-11-30Proper check for first-class types in datatype subfields (#7712)Andrew Reynolds
2021-11-29Fix minor issues (#7704)Gereon Kremer
2021-11-24Remove dependency of `TypeNode` on `Node` (#7690)Andres Noetzli
2021-11-24Fix potential for cycles in trust substitutions (#7687)Andrew Reynolds
2021-11-24Minor fixes (#7691)Andres Noetzli
2021-11-23Make difficulty manager only consider lemmas at full effort (#7685)Andrew Reynolds
2021-11-23Enable model-based reduction technique for strings (#7680)Andrew Reynolds
2021-11-23Add rewrite rule for bag.card operator using bag.map and lambda (#7643)mudathirmahgoub
2021-11-22Refactor IO stream manipulators (#7555)Gereon Kremer
2021-11-22Add rewrite for repeated re.allchar (#7681)Andrew Reynolds
2021-11-22Improve error for check theory assertions with model (#7679)Andrew Reynolds
2021-11-21Fix const RE test for internal regexp rv kind (#7678)Andrew Reynolds
2021-11-20bv2int module: translation of more cases (#7653)yoni206
2021-11-18Refactor CAD option for linear model seed (#7657)Gereon Kremer
2021-11-17Preparations for eliminating arithmetic subtyping (#7637)Andrew Reynolds
2021-11-17Revert change and clean datatypes cons candidate generator (#7645)Andrew Reynolds
2021-11-17Implement aggressive pruning in CAD solver (#7650)Gereon Kremer
2021-11-15[Strings] Minor refactor of eager solver (#7628)Andres Noetzli
2021-11-15Add documentation for theory_bags_type_rules.h (#7642)mudathirmahgoub
2021-11-13Skip `str.code` inferences for sequence eqcs (#7644)Andres Noetzli
2021-11-13Fix type error for rewriting bag.map bag.union_disjoint (#7640)mudathirmahgoub
2021-11-13Add operator set.map to theory of sets (#7641)mudathirmahgoub
2021-11-12bags: Rename kinds with a more consistent naming scheme (#7611)mudathirmahgoub
2021-11-12Add some basic rewrites for regular expression intersection (#7629)Andrew Reynolds
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-11Add lazy approach for handling lambdas in the HO extension (#7625)Andrew Reynolds
2021-11-11Fixes for update/nth over constant sequences (#7631)Andrew Reynolds
2021-11-10Fix soundness issue of missing premises for count bag lemmas (#7615)mudathirmahgoub
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
2021-11-09Minor optimizations for term database (#7600)Andrew Reynolds
2021-11-09Preparation for non-constant lambda models (#7604)Andrew Reynolds
2021-11-09Make secant points user context dependent (#7567)Gereon Kremer
2021-11-09regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)Aina Niemetz
2021-11-09Remove `CVC5Message` (#7610)Gereon Kremer
2021-11-09Remove more static option accesses (#7582)Gereon Kremer
2021-11-08expand bag.choose operator (#7481)mudathirmahgoub
2021-11-08Add lambda lift utility (#7601)Andrew Reynolds
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-08Evaluate cast-to-real operator (#7599)Andrew Reynolds
2021-11-06Do not use extended rewrites on recursive function definitions (#7549)Andrew Reynolds
2021-11-06Remove `Notice()` in favor of new `verbose()` (#7588)Gereon Kremer
2021-11-05Fix exclusion criteria for codatatype model values (#7546)Andrew Reynolds
2021-11-05Eliminate a level of nesting of traversals in theory preprocessing (#7345)Andrew Reynolds
2021-11-05Move functions and lambdas from builtin to uf (#7570)Andrew Reynolds
2021-11-05[FP] Do not assert that model has shared term (#7585)Andres Noetzli
2021-11-05Minor changes to circuit propagator (#7584)Haniel Barbosa
2021-11-05Remove many static calls to rewrite (#7580)Andrew Reynolds
2021-11-05Remove quadratic solving in NlModel (#7542)Gereon Kremer
2021-11-05Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)Gereon Kremer
2021-11-05Remove a bunch of debugging/logging code from the linear solver (#7576)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback