projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
New C++ Api: Rename and move checks.h. (#6306)
[cvc5.git] / src / expr /
2021-04-07 Andrew Reynolds(proof-new) Proper implementation of proof node cloning... tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) tree | commitdiff
2021-04-05 Andrew ReynoldsAdd interface for skolem functions in SkolemManager... tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-30 Andrew ReynoldsMake SEXPR simply typed (#6160) tree | commitdiff
2021-03-25 Gereon KremerAdd missing includes. (#6207) tree | commitdiff
2021-03-23 Abdalrhman MohamedReplace old sygus term reconstruction algorithm with... tree | commitdiff
2021-03-22 Gereon KremerMove statistics from the driver into the SmtEngine... tree | commitdiff
2021-03-22 Andrew Reynolds Function types are always first-class (#6167) tree | commitdiff
2021-03-22 Andrew ReynoldsGuard for non-unique skolems in term formula removal... tree | commitdiff
2021-03-16 Mathias Preinercmake: Generate cvc4_export.h and set visibility to... tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) tree | commitdiff
2021-03-12 Andrew Reynolds(proof-new) Miscellaneous sync to master (#6129) tree | commitdiff
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-11 Aina NiemetzClean up ownership of Datatypes in NodeManager. (#6113) tree | commitdiff
2021-03-11 Aina NiemetzRefactor Node::getOperator() to fix compiler warning... tree | commitdiff
2021-03-10 Haniel Barbosa[proof-new] Clarifying doc (#6108) tree | commitdiff
2021-03-10 Aina NiemetzMove ExprManager::isNAryKind to NodeManager. (#6107) tree | commitdiff
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Replace witness form by original form in... tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-09 Aina NiemetzNew C++ API: Migrate to Node layer. (#6070) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-26 Andrew ReynoldsOptionally permit creation of non-flat function types... tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-23 Mathias PreinerSwitch to C++17. (#5959) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for monomial bounds check (#5965) tree | commitdiff
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964) tree | commitdiff
2021-02-23 Gereon KremerAdd trans secant proofs. (#5957) tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for exponential functions (... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Option to automatically add SYMM steps... tree | commitdiff
2021-02-22 Haniel Barbosa[proof-new] Optionally print conclusion in the AST... tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for sine lemmas in the transcend... tree | commitdiff
2021-02-12 Andrew Reynolds(proof-new) Option to not automatically consider symmet... tree | commitdiff
2021-02-09 Haniel Barbosa[quantifiers] Fix prenex computation (#5879) tree | commitdiff
2021-02-02 Andrew Reynolds(proof-new) Miscellaneous fixes and regressions (#5841) tree | commitdiff
2021-01-29 Andrew Reynolds(proof-new) Distinguish pre vs post rewrites in term... tree | commitdiff
2021-01-26 Haniel BarbosaReestablishing support for define-sort (#5810) tree | commitdiff
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) tree | commitdiff
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710) tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) tree | commitdiff
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof... tree | commitdiff
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) tree | commitdiff
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671) tree | commitdiff
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655) tree | commitdiff
2020-12-10 Gereon KremerRefactor KindMap (#5646) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) tree | commitdiff
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641) tree | commitdiff
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating... tree | commitdiff
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... tree | commitdiff
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own... tree | commitdiff
2020-12-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601) tree | commitdiff
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) tree | commitdiff
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... tree | commitdiff
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530) tree | commitdiff
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (... tree | commitdiff
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... tree | commitdiff
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-16 Andrew ReynoldsCleaning up scopes in preparation for symbol manager... tree | commitdiff
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434) tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in... tree | commitdiff
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic... tree | commitdiff
2020-11-12 Andrew ReynoldsMake symbol manager context dependent (#5424) tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsAdd simple substitution utility (#5397) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398) tree | commitdiff
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-03 Andrew ReynoldsAdd scope methods constructing types in API (#5393) tree | commitdiff
2020-11-02 Andrew ReynoldsAvoid dynamic allocation in symbol table implementation... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-29 Gereon KremerAdd NodeManager::mkOr() (#5360) tree | commitdiff
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... tree | commitdiff
next