summaryrefslogtreecommitdiff
path: root/test/unit/theory
AgeCommit message (Expand)Author
2020-07-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
2020-07-15Use TypeNode in UninterpretedConstant (#4748)Andres Noetzli
2020-07-14Use TypeNode in EmptySet (#4740)Andres Noetzli
2020-07-13Use TypeNode/Node in ArrayStoreAll (#4728)Andres Noetzli
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-06-29Make ExprManager constructor private (#4669)Andres Noetzli
2020-06-19Convert more uses of strings to words (#4584)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-10Add support for str.replace_re/str.replace_re_all (#4594)Andres Noetzli
2020-06-01Incorporate sequences into the word interface (#4543)Andrew Reynolds
2020-04-30Remove skolem share involving pre_first_ctn. (#4423)Andrew Reynolds
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-04-03Split sequences rewriter (#4194)Andrew Reynolds
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-03-27Move string utility file (#4164)Andrew Reynolds
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-03-16SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)Aina Niemetz
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-03Refactoring and cleaning the type enumerator for sets (#3908)mudathirmahgoub
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-24Utilities for words (#3797)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-03Rewrite `str.contains` used for character matching (#3519)Andres Noetzli
2019-12-01Prevent ref count from reaching zero in BV instantiator (#3512)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-08-29Infer conflicts based on regular expression inclusion (#3234)Andres Noetzli
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-05-17Fix BV ITE rewrite (#3004)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2019-03-23Strip non-matching beginning from indexof operator (#2885)Andres Noetzli
2019-03-22Fix stripConstantEndpoints in strings rewriter (#2883)Andres Noetzli
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
2018-11-28Improve skolem caching by normalizing skolem args (#2723)Andres Noetzli
2018-11-21Add rewrite for (str.substr s x y) --> "" (#2695)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback