projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[Rewrite Synthesis] Fix args for non-chaining ops (#7996)
[cvc5.git]
/
src
/
expr
/
2022-01-13
Andres Noetzli
Unify abstract values and uninterpreted constants ...
tree
|
commitdiff
2022-01-12
Gereon Kremer
Add mkRealAlgebraicNumber (#7923)
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Eliminate use of subtyping from results of quantifier...
tree
|
commitdiff
2022-01-11
Andres Noetzli
Fix `TypeNode::substitute()` for type constants (#7920)
tree
|
commitdiff
2022-01-11
Andres Noetzli
Fix `TypeNode::substitute()` (#7916)
tree
|
commitdiff
2022-01-04
Aina Niemetz
Reorder NodeManager class according to code guidelines...
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Add utility expr::isBooleanConnective (#7869)
tree
|
commitdiff
2021-12-21
Andrew Reynolds
Support get-abduct-next (#7850)
tree
|
commitdiff
2021-12-16
Andres Noetzli
Explicitly disallow `mkConst(Rational)` (#7818)
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Connecting the core array solver in strings (#7800)
tree
|
commitdiff
2021-12-13
mudathirmahgoub
A more efficient implementation for bag.card operator...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-10
Andrew Reynolds
Refactor and fixes related to getSpecializedConstructor...
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Consider polarity in relevance manager (#7768)
tree
|
commitdiff
2021-12-03
Andres Noetzli
Faster hasing for `cvc5::String` (#7742)
tree
|
commitdiff
2021-12-02
mudathirmahgoub
add bag.fold operator (#7718)
tree
|
commitdiff
2021-11-30
Andrew Reynolds
Proper check for first-class types in datatype subfield...
tree
|
commitdiff
2021-11-24
Andres Noetzli
Remove dependency of `TypeNode` on `Node` (#7690)
tree
|
commitdiff
2021-11-23
Gereon Kremer
Push output language inside the printing code (#7683)
tree
|
commitdiff
2021-11-23
Andres Noetzli
Make `node_value.h` not depend on `node_manager.h`...
tree
|
commitdiff
2021-11-22
Gereon Kremer
Refactor IO stream manipulators (#7555)
tree
|
commitdiff
2021-11-19
Andres Noetzli
Clean up relationship of metakind and node_manager...
tree
|
commitdiff
2021-11-17
Haniel Barbosa
Improve naming in term canonization when handling HO...
tree
|
commitdiff
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
tree
|
commitdiff
2021-11-16
Andres Noetzli
Refactor `metakind` (#7639)
tree
|
commitdiff
2021-11-12
mudathirmahgoub
bags: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-12
Andres Noetzli
Fix redundant definitions of `NodeValue::getConst`...
tree
|
commitdiff
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
tree
|
commitdiff
2021-11-11
Andrew Reynolds
Generalize front-end checks to check for shadowed varia...
tree
|
commitdiff
2021-11-09
Aina Niemetz
regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match...
tree
|
commitdiff
2021-11-08
mudathirmahgoub
expand bag.choose operator (#7481)
tree
|
commitdiff
2021-11-08
Aina Niemetz
sets: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-06
Haniel Barbosa
better traces in node converter (#7590)
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Formalize more string skolems (#7554)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Improvements for LFSC proof conversion (#7524)
tree
|
commitdiff
2021-10-25
mudathirmahgoub
Add inference for count map (#7264)
tree
|
commitdiff
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
tree
|
commitdiff
2021-10-21
Andrew Reynolds
Make cardinality constraint a nullary operator (#7333)
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Move variadic trie utility to its own file (#7410)
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Use codatatype bound variables for codatatype values...
tree
|
commitdiff
2021-10-12
Aina Niemetz
Clean up occurrences of SmtEngine in comments. (#7349)
tree
|
commitdiff
2021-10-12
Ouyancheng
fix deprecation of std::iterator (#7332)
tree
|
commitdiff
2021-10-11
Andrew Reynolds
Add cardinality constraint utilities (#7286)
tree
|
commitdiff
2021-10-05
Gereon Kremer
First round of refactoring on NlModel (#7255)
tree
|
commitdiff
2021-09-23
Andrew Reynolds
Implement alpha equivalence proofs (#7066)
tree
|
commitdiff
2021-09-22
Mathias Preiner
Remove CVC language support (#7219)
tree
|
commitdiff
2021-09-17
Andres Noetzli
Use a single `NodeManager` per thread (#7204)
tree
|
commitdiff
2021-09-14
Andrew Reynolds
Utilities in preparation for print benchmark utility...
tree
|
commitdiff
2021-09-02
Andrew Reynolds
Add LFSC node converter (#6944)
tree
|
commitdiff
2021-08-31
Andrew Reynolds
Make regular expression sort not closed enumerable...
tree
|
commitdiff
2021-08-27
Andrew Reynolds
Add n-ary match trie utility (#6909)
tree
|
commitdiff
2021-08-26
Gereon Kremer
Consolidate language types (#7065)
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Split higher-order term database (#7045)
tree
|
commitdiff
2021-08-23
Andrew Reynolds
Fix single invocation partition for higher-order (...
tree
|
commitdiff
2021-08-05
Andrew Reynolds
Generalize term canonizer for type classes (#6895)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Miscellaneous fixes from proof-new (#6914)
tree
|
commitdiff
2021-07-18
Andrew Reynolds
Add n-ary term utilities (#6896)
tree
|
commitdiff
2021-07-15
Andrew Reynolds
Add node converter utility (#6878)
tree
|
commitdiff
2021-07-13
Mathias Preiner
bv: Do not rewrite below BV leafs in BBProof's TConvPro...
tree
|
commitdiff
2021-07-02
Andres Noetzli
Add reverse iterators to `Node`/`TNode` (#6825)
tree
|
commitdiff
2021-06-28
Ouyancheng
Further fix #6453 (#6804)
tree
|
commitdiff
2021-06-21
Andres Noetzli
[Attributes] Remove parameter `context_dependent` ...
tree
|
commitdiff
2021-06-09
Andres Noetzli
Update CVC4 URLs/macros (#6666)
tree
|
commitdiff
2021-06-09
Haniel Barbosa
Removing spurious HO checks (#6707)
tree
|
commitdiff
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Better formalization of regular expression unfolding...
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Formalize 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 Reynolds
Add utility to get all types occurring in a term (...
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth respons...
tree
|
commitdiff
2021-05-21
Andres Noetzli
Support braced-init-lists with `mkNode()` (#6580)
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-20
Alex Ozdemir
Expand arith's farkas lemma rule as a macro (#6577)
tree
|
commitdiff
2021-05-19
Andres Noetzli
Remove unused methods from `NodeManager` (#6578)
tree
|
commitdiff
2021-05-19
Andres Noetzli
Improve handling of `:named` attributes (#6549)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-12
Andrew Reynolds
Ensure sequences of Booleans generate Boolean term...
tree
|
commitdiff
2021-05-08
Andrew Reynolds
Add 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 Reynolds
Add internal support for datatype update (#6450)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Fix refutational soundness bug in quantifier prenexing...
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Simplify making function types (#6447)
tree
|
commitdiff
2021-04-27
Gereon Kremer
Use std::hash for API types (#6432)
tree
|
commitdiff
2021-04-24
Mathias Preiner
Add assumption-based unsat cores. (#6427)
tree
|
commitdiff
2021-04-23
Andrew Reynolds
Add new substitution apply methods fixpoint, sequential...
tree
|
commitdiff
2021-04-23
Aina Niemetz
BV: Add proof logging for bit-blasting. (#6373)
tree
|
commitdiff
2021-04-21
Aina Niemetz
Datatypes: Move implementation of type rules to cpp...
tree
|
commitdiff
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
tree
|
commitdiff
2021-04-20
Aina Niemetz
Add guards to disable clang-format around placeholders...
tree
|
commitdiff
2021-04-16
Andrew Reynolds
Fix ONCE for post-rewrite (#6372)
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-15
Gereon Kremer
Fix printing of stats when aborted. (#6362)
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename 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 Reynolds
Formalize more skolems (#6307)
tree
|
commitdiff
2021-04-12
Andrew Reynolds
Fix computation of whether a type is finite (#6312)
tree
|
commitdiff
next