summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08New C++ API: Migrate to Node layer. (#6070)Aina Niemetz
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-26Optionally permit creation of non-flat function types (#6010)Andrew Reynolds
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2021-02-23Switch to C++17. (#5959)Mathias Preiner
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
2021-02-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
2021-02-22(proof-new) Add proofs for exponential functions (#5956)Gereon Kremer
2021-02-22(proof-new) Option to automatically add SYMM steps during proof node update. ...Andrew Reynolds
2021-02-22[proof-new] Optionally print conclusion in the AST proof (#5954)Haniel Barbosa
2021-02-22(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)Gereon Kremer
2021-02-12(proof-new) Option to not automatically consider symmetry in CDProof (#5895)Andrew Reynolds
2021-02-09[quantifiers] Fix prenex computation (#5879)Haniel Barbosa
2021-02-02(proof-new) Miscellaneous fixes and regressions (#5841)Andrew Reynolds
2021-01-29(proof-new) Distinguish pre vs post rewrites in term conversion proof generat...Andrew Reynolds
2021-01-26Reestablishing support for define-sort (#5810)Haniel Barbosa
2021-01-19Implement proofs for arith BRAB lemmas (#5784)Alex Ozdemir
2021-01-11Further simplifications in preparation for removing Expr layer (#5756)Andrew Reynolds
2021-01-08Add bags inference generator (#5731)mudathirmahgoub
2021-01-05Remove a few miscellaneous references to the expr layer (#5661)Andrew Reynolds
2020-12-21Add proof for pi bound lemma (#5709)Gereon Kremer
2020-12-21Add proof for sine shift lemmas. (#5710)Gereon Kremer
2020-12-18(proof-new) Add proof for tangent plane lemmas (#5700)Gereon Kremer
2020-12-17(proof-new) Minor updates to term conversion proof generator (#5691)Andrew Reynolds
2020-12-16(proof-new) Use bound variable manager (#5679)Andrew Reynolds
2020-12-15Fix datatypes compute ground value (#5671)Andrew Reynolds
2020-12-14(proof-new) Add bound variable manager (#5655)Andrew Reynolds
2020-12-10Refactor KindMap (#5646)Gereon Kremer
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-09google test: expr: Migrate kind_map_black. (#5640)Aina Niemetz
2020-12-09kind_map: Remove unused Accessor class. (#5641)Aina Niemetz
2020-12-07[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)Haniel Barbosa
2020-12-07Add support for BV proofs with the simple bitblasting solver. (#5603)Mathias Preiner
2020-12-07 (proof-new) Split proof ensure closed checks to own file (#5522)Andrew Reynolds
2020-12-07Fix bugs in getFreeVariables (#5601)Andrew Reynolds
2020-12-04Fix bug in hasBoundVar (#5600)Andrew Reynolds
2020-12-03Refactor handling of global declarations (#5577)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Remove Record object and convert to Node-level API (#5575)Andrew Reynolds
2020-12-02Add associative utilities to node manager (#5530)Andrew Reynolds
2020-12-02(proof-new) Proofs for expand definitions (#5562)Andrew Reynolds
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
2020-11-30(proof-new) Proofs for regular expression elimination (#5361)Andrew Reynolds
2020-11-25Fully decouple SmtEngine and the Expr layer (#5532)Andrew Reynolds
2020-11-23(proof-new) Miscellaneous changes from proof-new (#5445)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback