projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add missing InferenceIds to toString (#6320)
2021-04-09
Gereon Kremer
Add missing InferenceIds to toString (#6320)
commit
|
commitdiff
|
tree
2021-04-08
Gereon Kremer
Use newer version of update-pr-branch action. (#6315)
commit
|
commitdiff
|
tree
2021-04-02
Gereon Kremer
Add cache for new dependencies folder. (#6265)
commit
|
commitdiff
|
tree
2021-04-02
Gereon Kremer
New statistics registry (#6210)
commit
|
commitdiff
|
tree
2021-04-02
Gereon Kremer
Minor refactoring (#6273)
commit
|
commitdiff
|
tree
2021-04-02
Gereon Kremer
FindCaDiCaL: Avoid redirect to file (#6272)
commit
|
commitdiff
|
tree
2021-04-01
Gereon Kremer
Add utility classes for new statistics (#6178)
commit
|
commitdiff
|
tree
2021-04-01
Gereon Kremer
Refactor CLN dependency & Cleanup (#6251)
commit
|
commitdiff
|
tree
2021-04-01
Gereon Kremer
Make ResetCommand go through APISolver (#6172)
commit
|
commitdiff
|
tree
2021-03-31
Gereon Kremer
Refactor GMP and Poly dependencies (#6245)
commit
|
commitdiff
|
tree
2021-03-31
Gereon Kremer
Refactor dependencies for external SAT solvers (#6215)
commit
|
commitdiff
|
tree
2021-03-31
Gereon Kremer
Refactor SymFPU dependency (#6218)
commit
|
commitdiff
|
tree
2021-03-30
Gereon Kremer
Fix total time statistic (#6233)
commit
|
commitdiff
|
tree
2021-03-29
Gereon Kremer
Add external project to install gtest (#6229)
commit
|
commitdiff
|
tree
2021-03-27
Gereon Kremer
Refactor ANTLR3 dependency (#6202)
commit
|
commitdiff
|
tree
2021-03-25
Gereon Kremer
Ensure nonlinear extensions properly reconsiders its...
commit
|
commitdiff
|
tree
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
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-22
Gereon Kremer
Move statistics from the driver into the SmtEngine...
commit
|
commitdiff
|
tree
2021-03-18
Gereon Kremer
Move stats registry to env. (#6173)
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-12
Gereon Kremer
Add missing includes for statistics (#6124)
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
Make linear arithmetic use its inference manager (...
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
commit
|
commitdiff
|
tree
2021-03-10
Gereon Kremer
Improve arithmetic proofs (#6106)
commit
|
commitdiff
|
tree
2021-03-09
Gereon Kremer
Add missing include if GLPK is enabled. (#6084)
commit
|
commitdiff
|
tree
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
commit
|
commitdiff
|
tree
2021-03-08
Gereon Kremer
Fix justification heuristic again (#6074)
commit
|
commitdiff
|
tree
2021-03-05
Gereon Kremer
Reimplement time limit mechanism for windows (#6049)
commit
|
commitdiff
|
tree
2021-03-04
Gereon Kremer
Add proper define for libpoly usage (#6050)
commit
|
commitdiff
|
tree
2021-03-04
Gereon Kremer
Add cmake scripts for iwyu targets. (#6042)
commit
|
commitdiff
|
tree
2021-03-04
Gereon Kremer
Ignore isInConflict when adding conflicts (#5995)
commit
|
commitdiff
|
tree
2021-03-03
Gereon Kremer
Remove obsolete gcc check. (#6041)
commit
|
commitdiff
|
tree
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
commit
|
commitdiff
|
tree
2021-03-02
Gereon Kremer
Improve handling of utf8 encoded inputs (#5694)
commit
|
commitdiff
|
tree
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
commit
|
commitdiff
|
tree
2021-03-01
Gereon Kremer
Refactor collection of debug and trace tags (#5996)
commit
|
commitdiff
|
tree
2021-02-26
Gereon Kremer
Store Node instead of TNode (#5993)
commit
|
commitdiff
|
tree
2021-02-25
Gereon Kremer
Move (optional) rewrite from TrustSubstitutionMap to...
commit
|
commitdiff
|
tree
2021-02-25
Gereon Kremer
Add regression. (#5994)
commit
|
commitdiff
|
tree
2021-02-24
Gereon Kremer
Ensure static-learning adds rewritten assertions. ...
commit
|
commitdiff
|
tree
2021-02-24
Gereon Kremer
(proof-new) Add proofs for CAD solver (#5981)
commit
|
commitdiff
|
tree
2021-02-23
Gereon Kremer
Add proof for mult sign lemma (#5966)
commit
|
commitdiff
|
tree
2021-02-23
Gereon Kremer
Add proof for monomial bounds check (#5965)
commit
|
commitdiff
|
tree
2021-02-23
Gereon Kremer
(proof-new) Add proof generator for CAD solver (#5964)
commit
|
commitdiff
|
tree
2021-02-23
Gereon Kremer
Add trans secant proofs. (#5957)
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
(proof-new) Add proofs for exponential functions (...
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
Add the LazyTreeProofGenerator. (#5948)
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE...
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
(proof-new) Add proofs for sine lemmas in the transcendental...
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
Cleanup in transcendental solver, add ApproximationBounds...
commit
|
commitdiff
|
tree
2021-02-22
Gereon Kremer
add pruneRedundantIntervals (#5950)
commit
|
commitdiff
|
tree
2021-02-19
Gereon Kremer
Cleanup of inferences in arithmetic theory (#5927)
commit
|
commitdiff
|
tree
2021-02-18
Gereon Kremer
Add statistic for InferenceId to TheoryInferenceManager...
commit
|
commitdiff
|
tree
2021-02-18
Gereon Kremer
Add InferenceIds for sets theory. (#5900)
commit
|
commitdiff
|
tree
2021-02-18
Gereon Kremer
New InferenceIds for BV theory (#5909)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Use InferenceId in sep theory. (#5912)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
TheoryIds for UF theory. (#5901)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add InferenceIds for theory of arrays (#5910)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add InferenceId to buffered inference manager (#5911)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add new IntegralHistogramStat (#5898)
commit
|
commitdiff
|
tree
2021-02-15
Gereon Kremer
Remove now obsolete sendLemmas and inferences stat...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Make most methods of TheoryInferenceManager expect...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Add InferenceId member to TheoryInference, adapt all...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
commit
|
commitdiff
|
tree
2021-01-07
Gereon Kremer
Make sure polynomials are properly factorized in nl...
commit
|
commitdiff
|
tree
2020-12-23
Gereon Kremer
Add proofs for nonlinear sign lemmas. (#5707)
commit
|
commitdiff
|
tree
2020-12-21
Gereon Kremer
Add proof for pi bound lemma (#5709)
commit
|
commitdiff
|
tree
2020-12-21
Gereon Kremer
Add proof for sine shift lemmas. (#5710)
commit
|
commitdiff
|
tree
2020-12-21
Gereon Kremer
(proof-new) Make nl-ext factoring lemmas proof producing...
commit
|
commitdiff
|
tree
2020-12-18
Gereon Kremer
(proof-new) Setup proof infrastructure for transcendental...
commit
|
commitdiff
|
tree
2020-12-18
Gereon Kremer
Add proof checker for nl tangent lemma (#5704)
commit
|
commitdiff
|
tree
2020-12-18
Gereon Kremer
(proof-new) Add proof for tangent plane lemmas (#5700)
commit
|
commitdiff
|
tree
2020-12-18
Gereon Kremer
Add proof for split zero check. (#5699)
commit
|
commitdiff
|
tree
2020-12-17
Gereon Kremer
Always consider rewritten lemmas for caching. (#5696)
commit
|
commitdiff
|
tree
2020-12-17
Gereon Kremer
(proof-new) Prepare nonlinear extension and nl-ext...
commit
|
commitdiff
|
tree
2020-12-15
Gereon Kremer
Add getters to retrieve constants from api::Term (...
commit
|
commitdiff
|
tree
2020-12-10
Gereon Kremer
Refactor KindMap (#5646)
commit
|
commitdiff
|
tree
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
commit
|
commitdiff
|
tree
2020-12-09
Gereon Kremer
Split initial exp lemma into separate lemmas. (#5622)
commit
|
commitdiff
|
tree
2020-12-08
Gereon Kremer
Add regression from #1978. (#5552)
commit
|
commitdiff
|
tree
2020-12-07
Gereon Kremer
Refactor initial phase of transcendental solver (#5599)
commit
|
commitdiff
|
tree
2020-12-07
Gereon Kremer
Add regression from #4927 (#5556)
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Make run_regression.py executable. (#5588)
commit
|
commitdiff
|
tree
2020-12-02
Gereon Kremer
Add regressions from #3687. (#5553)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Refactor transcendental solver (#5539)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regressions from #5099 (#5557)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regression for #4335. (#5554)
commit
|
commitdiff
|
tree
2020-12-01
Gereon Kremer
Add regressions for #4707. (#5555)
commit
|
commitdiff
|
tree
2020-11-26
Gereon Kremer
Make CAD solver work for empty set of assertions (...
commit
|
commitdiff
|
tree
2020-11-25
Gereon Kremer
Fix transcendental secant plane lemmas (#5525)
commit
|
commitdiff
|
tree
2020-11-25
Gereon Kremer
Refactor transcendental solver (#5514)
commit
|
commitdiff
|
tree
2020-11-23
Gereon Kremer
Add get-info :time. (#5485)
commit
|
commitdiff
|
tree
2020-11-20
Gereon Kremer
(proof-new) Replace LazyCDProofSet by generic CDProofSet...
commit
|
commitdiff
|
tree
2020-11-20
Gereon Kremer
Allow to pass ProofGenerator to arithmetic inference...
commit
|
commitdiff
|
tree
2020-11-17
Gereon Kremer
Fix tangent plane lemmas (#5455)
commit
|
commitdiff
|
tree
2020-11-16
Gereon Kremer
Refactor tangent plane lemmas (#5449)
commit
|
commitdiff
|
tree
next