projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-03-27
Gereon Kremer
Refactor ANTLR3 dependency (#6202)
commit
|
commitdiff
|
tree
2021-03-27
Aina Niemetz
Use color output to print configuration. (#6219)
commit
|
commitdiff
|
tree
2021-03-26
Aina Niemetz
FloatingPointLiteral: Make constructors that shouldn...
commit
|
commitdiff
|
tree
2021-03-26
Andrew Reynolds
Pass term registry to quantifiers modules (#6216)
commit
|
commitdiff
|
tree
2021-03-25
Gereon Kremer
Ensure nonlinear extensions properly reconsiders its...
commit
|
commitdiff
|
tree
2021-03-25
Aina Niemetz
FP: Refactor FloatingPointLiteral in preparation for...
commit
|
commitdiff
|
tree
2021-03-25
Andrew Reynolds
Refactor construction of triggers (#6209)
commit
|
commitdiff
|
tree
2021-03-25
Mathias Preiner
Do not use Configuration class in API black tests....
commit
|
commitdiff
|
tree
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
commit
|
commitdiff
|
tree
2021-03-25
Haniel Barbosa
Deleting old LFSC signatures (#6194)
commit
|
commitdiff
|
tree
2021-03-24
Andrew Reynolds
Use inference manager to access intantiate utility...
commit
|
commitdiff
|
tree
2021-03-24
Gereon Kremer
Only consider relevant terms for integer branches ...
commit
|
commitdiff
|
tree
2021-03-24
Gereon Kremer
Refactor our integration of LFSC (#6201)
commit
|
commitdiff
|
tree
2021-03-23
Andrew Reynolds
Remove unused code for axioms (#6197)
commit
|
commitdiff
|
tree
2021-03-23
Haniel Barbosa
Removing unused build options and deprecated proof...
commit
|
commitdiff
|
tree
2021-03-23
Andrew Reynolds
Passing term registry to ematching utilities (#6190)
commit
|
commitdiff
|
tree
2021-03-23
Aina Niemetz
Remove internal includes of Api header. (#6193)
commit
|
commitdiff
|
tree
2021-03-23
Abdalrhman...
Replace old sygus term reconstruction algorithm with...
commit
|
commitdiff
|
tree
2021-03-23
Andrew Reynolds
Moving instantiate and skolemize into quantifiers infer...
commit
|
commitdiff
|
tree
2021-03-22
Gereon Kremer
Move statistics from the driver into the SmtEngine...
commit
|
commitdiff
|
tree
2021-03-22
Andrew Reynolds
Move equality query utility into quantifiers model...
commit
|
commitdiff
|
tree
2021-03-22
Andrew Reynolds
Function types are always first-class (#6167)
commit
|
commitdiff
|
tree
2021-03-22
Andrew Reynolds
Add skolem definition manager (#6187)
commit
|
commitdiff
|
tree
2021-03-22
Aina Niemetz
FP: Add documentation for FloatingPointLiteral construc...
commit
|
commitdiff
|
tree
2021-03-22
Andrew Reynolds
Guard for non-unique skolems in term formula removal...
commit
|
commitdiff
|
tree
2021-03-21
Andrew Reynolds
Simplify strings term registration (#6174)
commit
|
commitdiff
|
tree
2021-03-21
Andrew Reynolds
Clean up remaining raw uses of output channel (#6161)
commit
|
commitdiff
|
tree
2021-03-20
Andrew Reynolds
Improved tracing for equivalence classes of EE (#6169)
commit
|
commitdiff
|
tree
2021-03-20
mudathirmahgoub
Generate cvc/Kind.java for the java API (#6143)
commit
|
commitdiff
|
tree
2021-03-19
Andrew Reynolds
Refactor initialization of quantifiers model and builde...
commit
|
commitdiff
|
tree
2021-03-19
Aina Niemetz
BitVector: Change setBit to set the bit in place. ...
commit
|
commitdiff
|
tree
2021-03-19
Aina Niemetz
FP: Use setBit instead of bv or in conversion from...
commit
|
commitdiff
|
tree
2021-03-18
Haniel Barbosa
When giving an SMT-LIB version, defaulting to SMT-LIB...
commit
|
commitdiff
|
tree
2021-03-18
Gereon Kremer
Move stats registry to env. (#6173)
commit
|
commitdiff
|
tree
2021-03-18
Andrew Reynolds
Eliminate dependency on quantifiers engine in quantifie...
commit
|
commitdiff
|
tree
2021-03-18
Abdalrhman...
Eliminate more uses of SExpr. (#6149)
commit
|
commitdiff
|
tree
2021-03-18
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-17
Andrew Reynolds
(proof-new) Fixes to set defaults (#6163)
commit
|
commitdiff
|
tree
2021-03-17
Andrew Reynolds
Move utilities for inferred bounds on quantifers to...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename test/unit/expr to test/unit/node. (#6156)
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename fixtures in test/unit/context to conform to...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename fixtures in test/unit/base to conform to naming...
commit
|
commitdiff
|
tree
2021-03-16
Mathias Preiner
ci: Enable checking of proofs + unsat cores. (#6088)
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Activating proofs when dumping proofs ...
commit
|
commitdiff
|
tree
2021-03-16
Andrew Reynolds
Further standardization of strings statistics (#6128)
commit
|
commitdiff
|
tree
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Disabling proofs on regressions with known...
commit
|
commitdiff
|
tree
2021-03-16
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Fix rewrite for double replace (#6152)
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Gereon Kremer
Replace HistogramStat by IntegralHistogramStat (#6126)
commit
|
commitdiff
|
tree
2021-03-15
Gereon Kremer
Disable sqlite (#6145)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Make nonlinear extension account for relevant term...
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Split inst match generator class to own file (#6125)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Letify quantifier bodies independently (#6112)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Reorganizing initialization of term registry in quantif...
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-14
Diego Della...
[proof-new] Adding a dot printer for proof nodes (...
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
New C++ Api: Move checks to separate file. (#6138)
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
New C++ API: Rename TRY CATCH macros. (#6135)
commit
|
commitdiff
|
tree
2021-03-12
Andres Noetzli
Schedule preregistration lemmas to be satisfied after...
commit
|
commitdiff
|
tree
2021-03-12
Mathias Preiner
cmake: Remove install rules for old API headers. (...
commit
|
commitdiff
|
tree
2021-03-12
Andrew Reynolds
(proof-new) Miscellaneous sync to master (#6129)
commit
|
commitdiff
|
tree
2021-03-12
Haniel Barbosa
[proof-new] Fix arity check when building equality...
commit
|
commitdiff
|
tree
2021-03-12
Gereon Kremer
Add missing includes for statistics (#6124)
commit
|
commitdiff
|
tree
2021-03-12
Andrew Reynolds
Simplify instantiation match generator interface (...
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
Add more unit tests for api::Sort. (#6122)
commit
|
commitdiff
|
tree
2021-03-12
Mathias Preiner
ci: Replace debug builds with assertion enabled product...
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
Make linear arithmetic use its inference manager (...
commit
|
commitdiff
|
tree
2021-03-11
Alex Ozdemir
arith proof rules shuffle & add ARITH_SUM_UB (#6118)
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
Introduce inference ids for quantifier instantiation...
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
commit
|
commitdiff
|
tree
2021-03-11
MikolasJanota
Improvements and refactoring for enumeratative strategy...
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
(proof-new) Clean up uses of witness with skolem lemmas...
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
Direct lemmas and inference ids for sygus extension...
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Fix compile warnings when compiling with GLPK. (#6115)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Remove obsolete test/api/statistics.cpp. (#6116)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Clean up ownership of Datatypes in NodeManager. (#6113)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Refactor Node::getOperator() to fix compiler warning...
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Add GitHub action to automatically update approved...
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
Use Assert instead of assert. (#6095)
commit
|
commitdiff
|
tree
2021-03-10
Aina Niemetz
New C++ Api: Add missing argument checks in Solver...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Add Env class (#6093)
commit
|
commitdiff
|
tree
2021-03-10
Andrew V. Jones
Improved handing of 'lib64' vs. 'lib' for glpk-cut...
commit
|
commitdiff
|
tree
2021-03-10
Haniel Barbosa
[proof-new] Clarifying doc (#6108)
commit
|
commitdiff
|
tree
2021-03-10
Aina Niemetz
Move ExprManager::isNAryKind to NodeManager. (#6107)
commit
|
commitdiff
|
tree
2021-03-10
Gereon Kremer
Improve arithmetic proofs (#6106)
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
cmake: Fix optimization level for debug builds. (#6097)
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
(proof-new) Update ppRewrite to use skolem lemmas ...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Fix extended equality rewrite involving replace. (...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Fix term registration and non-theory-preprocessed terms...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Add quant elim regression (#6103)
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
(proof-new) Replace witness form by original form in...
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
test: Fix missing std::. (#6096)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ Api: Use const ref for arguments when possible...
commit
|
commitdiff
|
tree
next