git.libre-soc.org Git - cvc5.git/search

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
2020-11-16	Gereon Kremer	Improve accuracy of resource limitation (#4763)	commit \| commitdiff \| tree
2020-11-09	Gereon Kremer	Properly clear interrupt for solve() as well. (#5403)	commit \| commitdiff \| tree
next

RSS Atom