projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Eliminate Output macro in favor of simple Env functions (#7223)
[cvc5.git] / src / expr /
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-22 Mathias PreinerRemove CVC language support (#7219) tree | commitdiff
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204) tree | commitdiff
2021-09-14 Andrew ReynoldsUtilities in preparation for print benchmark utility... tree | commitdiff
2021-09-02 Andrew ReynoldsAdd LFSC node converter (#6944) tree | commitdiff
2021-08-31 Andrew ReynoldsMake regular expression sort not closed enumerable... tree | commitdiff
2021-08-27 Andrew ReynoldsAdd n-ary match trie utility (#6909) tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-24 Andrew ReynoldsSplit higher-order term database (#7045) tree | commitdiff
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... tree | commitdiff
2021-08-05 Andrew ReynoldsGeneralize term canonizer for type classes (#6895) tree | commitdiff
2021-07-27 Andrew ReynoldsMiscellaneous fixes from proof-new (#6914) tree | commitdiff
2021-07-18 Andrew ReynoldsAdd n-ary term utilities (#6896) tree | commitdiff
2021-07-15 Andrew ReynoldsAdd node converter utility (#6878) tree | commitdiff
2021-07-13 Mathias Preinerbv: Do not rewrite below BV leafs in BBProof's TConvPro... tree | commitdiff
2021-07-02 Andres NoetzliAdd reverse iterators to `Node`/`TNode` (#6825) tree | commitdiff
2021-06-28 OuyanchengFurther fix #6453 (#6804) tree | commitdiff
2021-06-21 Andres Noetzli[Attributes] Remove parameter `context_dependent` ... tree | commitdiff
2021-06-09 Andres NoetzliUpdate CVC4 URLs/macros (#6666) tree | commitdiff
2021-06-09 Haniel BarbosaRemoving spurious HO checks (#6707) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-24 Andrew ReynoldsBetter formalization of regular expression unfolding... tree | commitdiff
2021-05-21 Andrew ReynoldsFormalize shared selectors as skolem functions (#6591) tree | commitdiff
2021-05-21 Andrew Reynolds(proof-new) Minor documentation sync (#6592) tree | commitdiff
2021-05-21 Andrew ReynoldsAdd utility to get all types occurring in a term (... tree | commitdiff
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth respons... tree | commitdiff
2021-05-21 Andres NoetzliSupport braced-init-lists with `mkNode()` (#6580) tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-20 Alex OzdemirExpand arith's farkas lemma rule as a macro (#6577) tree | commitdiff
2021-05-19 Andres NoetzliRemove unused methods from `NodeManager` (#6578) tree | commitdiff
2021-05-19 Andres NoetzliImprove handling of `:named` attributes (#6549) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-12 Andrew ReynoldsEnsure sequences of Booleans generate Boolean term... tree | commitdiff
2021-05-08 Andrew ReynoldsAdd support for datatype update (#6449) tree | commitdiff
2021-05-06 Haniel Barbosa[proof-new] Updating documentation for Subs/Rw ids... tree | commitdiff
2021-04-27 Andrew ReynoldsAdd internal support for datatype update (#6450) tree | commitdiff
2021-04-27 Andrew ReynoldsFix refutational soundness bug in quantifier prenexing... tree | commitdiff
2021-04-27 Andrew ReynoldsSimplify making function types (#6447) tree | commitdiff
2021-04-27 Gereon KremerUse std::hash for API types (#6432) tree | commitdiff
2021-04-24 Mathias PreinerAdd assumption-based unsat cores. (#6427) tree | commitdiff
2021-04-23 Andrew ReynoldsAdd new substitution apply methods fixpoint, sequential... tree | commitdiff
2021-04-23 Aina NiemetzBV: Add proof logging for bit-blasting. (#6373) tree | commitdiff
2021-04-21 Aina NiemetzDatatypes: Move implementation of type rules to cpp... tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-20 Aina NiemetzAdd guards to disable clang-format around placeholders... tree | commitdiff
2021-04-16 Andrew ReynoldsFix ONCE for post-rewrite (#6372) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-15 Gereon KremerFix printing of stats when aborted. (#6362) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-14 Haniel Barbosa[proof-new] Fix explanation of literals in SAT proof... tree | commitdiff
2021-04-13 Andrew ReynoldsFormalize more skolems (#6307) tree | commitdiff
2021-04-12 Andrew ReynoldsFix computation of whether a type is finite (#6312) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-09 Haniel Barbosa[proof-new] Optimizing sat proof (#6324) tree | commitdiff
2021-04-08 Andrew ReynoldsUse exceptions when constructing malformed datatypes... tree | commitdiff
2021-04-08 Andrew ReynoldsInitial support for parametric datatypes in sygus ... tree | commitdiff
2021-04-07 Haniel Barbosa[proof-new] Fixing SMT post-processor's handling of... tree | commitdiff
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
next