projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
arrays: Move type enumerator implementation to .cpp. (#7216)
[cvc5.git]
/
src
/
expr
/
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
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename 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 Reynolds
Use exceptions when constructing malformed datatypes...
tree
|
commitdiff
2021-04-08
Andrew Reynolds
Initial 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 Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
tree
|
commitdiff
2021-04-06
Aina Niemetz
New C++ Api: Rename and move headers. (#6292)
tree
|
commitdiff
2021-04-05
Andrew Reynolds
Add interface for skolem functions in SkolemManager...
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Make SEXPR simply typed (#6160)
tree
|
commitdiff
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
tree
|
commitdiff
2021-03-23
Abdalrhman Mohamed
Replace old sygus term reconstruction algorithm with...
tree
|
commitdiff
2021-03-22
Gereon Kremer
Move 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 Reynolds
Guard for non-unique skolems in term formula removal...
tree
|
commitdiff
2021-03-16
Mathias Preiner
cmake: 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 Kremer
Replace HistogramStat by IntegralHistogramStat (#6126)
tree
|
commitdiff
2021-03-12
Andrew Reynolds
(proof-new) Miscellaneous sync to master (#6129)
tree
|
commitdiff
2021-03-11
Alex Ozdemir
arith proof rules shuffle & add ARITH_SUM_UB (#6118)
tree
|
commitdiff
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Clean up ownership of Datatypes in NodeManager. (#6113)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Refactor Node::getOperator() to fix compiler warning...
tree
|
commitdiff
2021-03-10
Haniel Barbosa
[proof-new] Clarifying doc (#6108)
tree
|
commitdiff
2021-03-10
Aina Niemetz
Move ExprManager::isNAryKind to NodeManager. (#6107)
tree
|
commitdiff
2021-03-10
Gereon Kremer
Improve 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 Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-09
Aina Niemetz
New C++ API: Migrate to Node layer. (#6070)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-26
Andrew Reynolds
Optionally permit creation of non-flat function types...
tree
|
commitdiff
2021-02-25
Mathias Preiner
Enable -Werror. (#5969)
tree
|
commitdiff
2021-02-23
Mathias Preiner
Switch to C++17. (#5959)
tree
|
commitdiff
2021-02-23
Gereon Kremer
Add proof for mult sign lemma (#5966)
tree
|
commitdiff
2021-02-23
Gereon Kremer
Add 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 Kremer
Add 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
next