summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
2021-03-22Move statistics from the driver into the SmtEngine (#6170)Gereon Kremer
2021-03-22 Function types are always first-class (#6167)Andrew Reynolds
2021-03-22Guard for non-unique skolems in term formula removal (#6179)Andrew Reynolds
2021-03-16cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)Mathias Preiner
2021-03-16[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)Haniel Barbosa
2021-03-15Replace HistogramStat by IntegralHistogramStat (#6126)Gereon Kremer
2021-03-12(proof-new) Miscellaneous sync to master (#6129)Andrew Reynolds
2021-03-11arith proof rules shuffle & add ARITH_SUM_UB (#6118)Alex Ozdemir
2021-03-11First refactoring of statistics classes (#6105)Gereon Kremer
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-11Clean up ownership of Datatypes in NodeManager. (#6113)Aina Niemetz
2021-03-11Refactor Node::getOperator() to fix compiler warning. (#6110)Aina Niemetz
2021-03-10[proof-new] Clarifying doc (#6108)Haniel Barbosa
2021-03-10Move ExprManager::isNAryKind to NodeManager. (#6107)Aina Niemetz
2021-03-10Improve arithmetic proofs (#6106)Gereon Kremer
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
2021-03-10(proof-new) Replace witness form by original form in the internal proof calcu...Andrew Reynolds
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback