summaryrefslogtreecommitdiff
path: root/src/theory/booleans/theory_bool_rewriter.cpp
AgeCommit message (Expand)Author
2020-06-19Always rewrite boolean ITEs with constant then/else-branches (#4619)Haniel Barbosa
2020-06-16Update copyright headers.Aina Niemetz
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-24Make lambda rewriter more robust (#3806)Andres Noetzli
2019-10-22NodeValue: Eliminate redundant NBITS macros. (#3400)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-07Update copyright headers.Mathias Preiner
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-10-19Fix minor bug and typo in boolean rewriterfix_rewriteAndres Notzli
2016-04-20update from the masterPaulMeng
2014-07-01Update copyrights.Morgan Deters
2014-06-19Fix rewriter typo.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-25Substantial Changes:Tim King
2013-04-17bool flatten: node num_children workaroundKshitij Bansal
2013-04-17boolean flatten: bug fix in dfs searchKshitij Bansal
2013-04-16boolean flatten rewrite: dont re-rewriteKshitij Bansal
2013-04-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-04-01fixed TheoryBool rewriter buglianah
2013-03-13Added a rewrite for iff:Clark Barrett
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-05-11Added some ITE rewrites,Clark Barrett
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-02-26Commit to fix bug 241 (improper "using namespace std" in a header). This cau...Morgan Deters
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback