projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Remove regex header from cvc4cpp.cpp (#5826)
[cvc5.git]
/
src
/
expr
/
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
2020-10-26
Andrew Reynolds
(proof-new) Add datatypes proof checker (#5340)
tree
|
commitdiff
2020-10-21
Andrew Reynolds
(proof-new) Updates to lazy proof chain (#5317)
tree
|
commitdiff
2020-10-21
mudathirmahgoub
Add operator MakeBagOp for constructing bags (#5209)
tree
|
commitdiff
2020-10-21
Andrew Reynolds
(proof-new) Fixes for proofs in rewriter (#5307)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Fix for CDProof::isSame (#5297)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-19
Haniel Barbosa
[proof-new] Fixing resolution proof checker (#5262)
tree
|
commitdiff
2020-10-19
Haniel Barbosa
[proof-new] Improving cycle checking in lazycdproofchai...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Refactoring cyclic checks (#5291)
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Witness axiom reconstruction for purificat...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Implementation of trust substitution (...
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Simplifications for proof rule checker...
tree
|
commitdiff
2020-10-13
Andrew Reynolds
(proof-new) New rules for Booleans (#5243)
tree
|
commitdiff
2020-10-13
Andrew Reynolds
(proof-new) Change merge policy for proof node updater...
tree
|
commitdiff
2020-10-11
Mathias Preiner
SyGuS instantiation modes (#5228)
tree
|
commitdiff
2020-10-09
Andrew Reynolds
(proof-new) Add lazy proof set utility (#5221)
tree
|
commitdiff
2020-10-08
Andrew Reynolds
(proof-new) Fixes and improvements for smt proof postpr...
tree
|
commitdiff
2020-10-06
Andrew Reynolds
(proof-new) Allow null proofs from generators in LazyCD...
tree
|
commitdiff
2020-10-06
mudathirmahgoub
Remove subtyping for sets (#5205)
tree
|
commitdiff
2020-10-04
mudathirmahgoub
Remove subtyping for sets theory (#5179)
tree
|
commitdiff
2020-10-02
Andrew Reynolds
(proof-new) Fixes for theory preprocessing proofs ...
tree
|
commitdiff
2020-09-30
Andrew Reynolds
(proof-new) Add the term conversion sequence generator...
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Updates to proof node updater (#5156)
tree
|
commitdiff
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof node hash function (#5154)
tree
|
commitdiff
2020-09-28
Andrew Reynolds
Minor fixes to quantifiers proofs (#5151)
tree
|
commitdiff
2020-09-28
Haniel Barbosa
[proof-new] Adds a proof manager for the SAT solver...
tree
|
commitdiff
2020-09-24
Andrew Reynolds
Modify lemma vs fact policy for datatype equalities...
tree
|
commitdiff
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-21
Andrew Reynolds
(proof-new) Add the arrays proof checker (#5047)
tree
|
commitdiff
2020-09-18
Andrew Reynolds
(proof-new) Updates to proof node updater algorithm...
tree
|
commitdiff
2020-09-18
Andrew Reynolds
(proof-new) Rewrites involving operators in term conver...
tree
|
commitdiff
2020-09-17
Haniel Barbosa
[proof-new] Have mkScope agnostic to True assumptions...
tree
|
commitdiff
2020-09-16
Haniel Barbosa
[proof-new] Adds Lazy CDProof chain data-structure...
tree
|
commitdiff
2020-09-16
Haniel Barbosa
[proof-new] Resolution rules and checkers (#5070)
tree
|
commitdiff
2020-09-16
Haniel Barbosa
[proof-new] A simple proof generator for buffered proof...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
(proof-new) Handle mismatched assumptions in proof...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
(proof-new) Use deep copy for final lemma step in proof...
tree
|
commitdiff
2020-09-09
Andrew Reynolds
(proof-new) Minor changes to proof node updater (#5011)
tree
|
commitdiff
2020-09-03
Andrew Reynolds
(proof-new) Improve debugging infrastructure for open...
tree
|
commitdiff
2020-09-02
Gereon Kremer
Remove #line directives from generated files. (#5005)
tree
|
commitdiff
2020-09-02
Andrew Reynolds
(proof-new) Updates to builtin proof checker (#4962)
tree
|
commitdiff
2020-09-02
Andrew Reynolds
(proof-new) Add proof support in TheoryUF (#5002)
tree
|
commitdiff
2020-09-02
Andrew Reynolds
(proof-new) Make term conversion proof generator option...
tree
|
commitdiff
2020-08-31
Andrew Reynolds
Basic proof support in inference manager (#4975)
tree
|
commitdiff
2020-08-29
Andrew Reynolds
(proof-new) More term context utilities. (#4912)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
next