projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add term pools utility (#6243)
[cvc5.git]
/
src
/
expr
/
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
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 Barbosa
Reestablishing support for define-sort (#5810)
tree
|
commitdiff
2021-01-19
Alex Ozdemir
Implement proofs for arith BRAB lemmas (#5784)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Add bags inference generator (#5731)
tree
|
commitdiff
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
tree
|
commitdiff
2020-12-21
Gereon Kremer
Add proof for pi bound lemma (#5709)
tree
|
commitdiff
2020-12-21
Gereon Kremer
Add 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 Reynolds
Fix 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 Kremer
Refactor KindMap (#5646)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-09
Aina Niemetz
google test: expr: Migrate kind_map_black. (#5640)
tree
|
commitdiff
2020-12-09
Aina Niemetz
kind_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 Preiner
Add 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 Reynolds
Fix bugs in getFreeVariables (#5601)
tree
|
commitdiff
2020-12-04
Andrew Reynolds
Fix bug in hasBoundVar (#5600)
tree
|
commitdiff
2020-12-03
Andrew Reynolds
Refactor handling of global declarations (#5577)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Remove Record object and convert to Node-level API...
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Add 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 Reynolds
Remove 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 Reynolds
Fully 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 Reynolds
Add 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 Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Add nested quantifier elimination module (#5422)
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
tree
|
commitdiff
2020-11-18
Aina Niemetz
FloatingPoint: Clean up and document header, format...
tree
|
commitdiff
2020-11-16
Andrew Reynolds
Cleaning up scopes in preparation for symbol manager...
tree
|
commitdiff
2020-11-13
Andrew Reynolds
Add 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 Reynolds
Make symbol manager context dependent (#5424)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Move symbol manager to src/expr/ (#5420)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Add simple substitution utility (#5397)
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Add getSubtermKinds to node algorithm (#5398)
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Migrate some documentation about attributes (#5390)
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
tree
|
commitdiff
2020-11-03
Andrew Reynolds
Add scope methods constructing types in API (#5393)
tree
|
commitdiff
2020-11-02
Andrew Reynolds
Avoid dynamic allocation in symbol table implementation...
tree
|
commitdiff
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
tree
|
commitdiff
2020-10-29
mudathirmahgoub
Add mkInteger to the API (#5274)
tree
|
commitdiff
2020-10-29
Gereon Kremer
Add NodeManager::mkOr() (#5360)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Convert symbol table from Expr-level to Term-level...
tree
|
commitdiff
2020-10-27
Andrew Reynolds
Add missing methods involving datatype sorts to the...
tree
|
commitdiff
next