summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/extended_rewrite.cpp
AgeCommit message (Expand)Author
2021-10-27Avoid non-terminating check with assumptions in strings rewriter (#7503)Andrew Reynolds
2021-09-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)Andrew Reynolds
2021-09-08Towards standard usage of ExtendedRewriter (#7145)Andrew Reynolds
2021-07-28Make extended rewriter methods const (#6948)Andrew Reynolds
2021-05-24Fix instance of no rewrite in extended rewriter (#6610)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-25Add missing includes. (#6207)Gereon Kremer
2021-03-10Move ExprManager::isNAryKind to NodeManager. (#6107)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
2021-01-11Remove extended rewrite for arithmetic (#5760)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-06-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-02Fix scope issue with pulling ITEs in extended rewriter. (#4547)Andrew Reynolds
2020-04-12Fixes for extended rewriter (#4278)Andrew Reynolds
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2018-12-15Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)Andres Noetzli
2018-12-14 Fix extended rewriter for binary associative operators. (#2751)Andrew Reynolds
2018-11-21Move ss-combine rewrite to extended rewriter (#2703)Andres Noetzli
2018-09-28Rewrites for (= "" _) and (= (str.replace _) _) (#2546)Andres Noetzli
2018-09-25Fix warnings uncovered by cmake build (#2521)Andrew Reynolds
2018-09-24Refactor strings equality rewriting (#2513)Andrew Reynolds
2018-09-05 More extended rewrites for strings equality (#2431)Andrew Reynolds
2018-09-05 Extended rewriter for string equalities (#2427)Andrew Reynolds
2018-08-27Refactor extended rewriter, move rewrites to aggressive (#2387)Andrew Reynolds
2018-07-06 sygusComp2018: improve extended rewriter for Bool (#2107)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-04-27Core improvements to extended rewriter (#1820)Andrew Reynolds
2018-04-25Equality resolution in the extended rewriter (#1811)Andrew Reynolds
2018-04-02Improvements to extended rewriter for Booleans and ITE (#1705)Andrew Reynolds
2018-02-12Option to use extended rewriter as a preprocessing pass (#1600)Andrew Reynolds
2018-01-28Sort children of all commutative operators for sygus. (#1544)Andrew Reynolds
2018-01-02Improve rewriter for string equality (#1427)Andrew Reynolds
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback