projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
More fixes and improvements for query generator (#7988)
[cvc5.git] / src / expr /
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... tree | commitdiff
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923) tree | commitdiff
2022-01-12 Andrew ReynoldsEliminate use of subtyping from results of quantifier... tree | commitdiff
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` for type constants (#7920) tree | commitdiff
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` (#7916) tree | commitdiff
2022-01-04 Aina NiemetzReorder NodeManager class according to code guidelines... tree | commitdiff
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) tree | commitdiff
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) tree | commitdiff
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818) tree | commitdiff
2021-12-14 Andrew ReynoldsConnecting the core array solver in strings (#7800) tree | commitdiff
2021-12-13 mudathirmahgoubA more efficient implementation for bag.card operator... tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-10 Andrew ReynoldsRefactor and fixes related to getSpecializedConstructor... tree | commitdiff
2021-12-09 Andrew ReynoldsConsider polarity in relevance manager (#7768) tree | commitdiff
2021-12-03 Andres NoetzliFaster hasing for `cvc5::String` (#7742) tree | commitdiff
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) tree | commitdiff
2021-11-30 Andrew ReynoldsProper check for first-class types in datatype subfield... tree | commitdiff
2021-11-24 Andres NoetzliRemove dependency of `TypeNode` on `Node` (#7690) tree | commitdiff
2021-11-23 Gereon KremerPush output language inside the printing code (#7683) tree | commitdiff
2021-11-23 Andres NoetzliMake `node_value.h` not depend on `node_manager.h`... tree | commitdiff
2021-11-22 Gereon KremerRefactor IO stream manipulators (#7555) tree | commitdiff
2021-11-19 Andres NoetzliClean up relationship of metakind and node_manager... tree | commitdiff
2021-11-17 Haniel BarbosaImprove naming in term canonization when handling HO... tree | commitdiff
2021-11-17 Andrew ReynoldsPreparations for eliminating arithmetic subtyping ... tree | commitdiff
2021-11-16 Andres NoetzliRefactor `metakind` (#7639) tree | commitdiff
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-12 Andres NoetzliFix redundant definitions of `NodeValue::getConst`... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-11 Andrew ReynoldsGeneralize front-end checks to check for shadowed varia... tree | commitdiff
2021-11-09 Aina Niemetzregex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match... tree | commitdiff
2021-11-08 mudathirmahgoubexpand bag.choose operator (#7481) tree | commitdiff
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... tree | commitdiff
2021-11-06 Haniel Barbosabetter traces in node converter (#7590) tree | commitdiff
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) tree | commitdiff
2021-11-03 Andrew ReynoldsRefactor skolem construction (#7561) tree | commitdiff
2021-11-03 Andrew ReynoldsFormalize more string skolems (#7554) tree | commitdiff
2021-10-29 Andrew ReynoldsImprovements for LFSC proof conversion (#7524) tree | commitdiff
2021-10-25 mudathirmahgoubAdd inference for count map (#7264) tree | commitdiff
2021-10-22 Andrew ReynoldsRemove `--uf-ho` option (#7463) tree | commitdiff
2021-10-21 Andrew ReynoldsMake cardinality constraint a nullary operator (#7333) tree | commitdiff
2021-10-20 Andrew ReynoldsMove variadic trie utility to its own file (#7410) tree | commitdiff
2021-10-20 Andrew ReynoldsUse codatatype bound variables for codatatype values... tree | commitdiff
2021-10-12 Aina NiemetzClean up occurrences of SmtEngine in comments. (#7349) tree | commitdiff
2021-10-12 Ouyanchengfix deprecation of std::iterator (#7332) tree | commitdiff
2021-10-11 Andrew ReynoldsAdd cardinality constraint utilities (#7286) tree | commitdiff
2021-10-05 Gereon KremerFirst round of refactoring on NlModel (#7255) tree | commitdiff
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
next