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-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-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-15
Gereon Kremer
Remove now obsolete sendLemmas and inferences stat...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
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-15
Gereon Kremer
Add getters to retrieve constants from api::Term (...
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
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
2020-10-30
Gereon Kremer
Use BoundInference in nonlinear extension (#5359)
commit
|
commitdiff
|
tree
2020-10-29
Gereon Kremer
Add NodeManager::mkOr() (#5360)
commit
|
commitdiff
|
tree
2020-10-28
Gereon Kremer
Split NlSolver in multiple subsolvers (#5315)
commit
|
commitdiff
|
tree
2020-10-27
Gereon Kremer
Disable --nl-cad option by default (#5350)
commit
|
commitdiff
|
tree
2020-10-27
Gereon Kremer
Enable --nl-cad by default (#5345)
commit
|
commitdiff
|
tree
2020-10-22
Gereon Kremer
Use theoryof-mode=type for QF_NRA (#5326)
commit
|
commitdiff
|
tree
2020-10-21
Gereon Kremer
(proof-new) Make circuit propagator proof producing...
commit
|
commitdiff
|
tree
2020-10-20
Gereon Kremer
(proof-new) Add proofs for circuit propagator (#5301)
commit
|
commitdiff
|
tree
2020-10-20
Gereon Kremer
Handle rewrite to bool in BoundInference (#5311)
commit
|
commitdiff
|
tree
2020-10-11
Gereon Kremer
Add conversion of poly polynomial to cvc node. (#5218)
commit
|
commitdiff
|
tree
2020-10-07
Gereon Kremer
Make sure conflicts are not rewritten (in arithmetic...
commit
|
commitdiff
|
tree
2020-10-02
Gereon Kremer
Allow for theory combination of strings with nonlinear...
commit
|
commitdiff
|
tree
2020-10-01
Gereon Kremer
Allow to use the initial assignment for CAD (#5177)
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Remove too strict assertion to allow for approximate...
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Add missing includes. (#5170)
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Add strategy for nonlinear extension (#5160)
commit
|
commitdiff
|
tree
2020-09-29
Gereon Kremer
Clean up nonlinear extension (#5149)
commit
|
commitdiff
|
tree
2020-09-26
Gereon Kremer
Use inference manager for nl_solver (#5125)
commit
|
commitdiff
|
tree
2020-09-23
Gereon Kremer
Make IAND solver use inference manager. (#5126)
commit
|
commitdiff
|
tree
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
commit
|
commitdiff
|
tree
2020-09-17
Gereon Kremer
(cad-solver) Fix square-free-basis computation (#5085)
commit
|
commitdiff
|
tree
2020-09-04
Gereon Kremer
Use arith::InferenceManager for CAD lemmas (#5015)
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Added a new rule to simplify (bvugt (bvurem T x) x...
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Basic integration of arith::InferenceManager (#4999)
commit
|
commitdiff
|
tree
2020-09-03
Gereon Kremer
Make nonlinear extension (more) deterministic (#4996)
commit
|
commitdiff
|
tree
next