projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
[proof-new] Adding a proof-producing ensure literal method (#5889)
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
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-28
Gereon Kremer
Add new arithmetic BoundInference class (#5148)
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-17
Gereon Kremer
Use new inference manager in transcendental solver...
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
2020-09-02
Gereon Kremer
Remove #line directives from generated files. (#5005)
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Use std::unique_ptr instead of std::shared_ptr for...
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Add ArithLemma and arith::InferenceManager (#4960)
commit
|
commitdiff
|
tree
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically different...
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
(cad-solver) Fixed excluding lemma generation. (#4958)
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
Make iand lemmas use proper Inference types. (#4956)
commit
|
commitdiff
|
tree
2020-08-24
Gereon Kremer
Fix memory issue in AntlrInput::parseError (#4873)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
(cad solver) Add a partial check method. (#4904)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Fix SmtEngine::reset() (#4917)
commit
|
commitdiff
|
tree
2020-08-16
Gereon Kremer
(cad solver) Use the current model as initial assignment...
commit
|
commitdiff
|
tree
2020-08-14
Gereon Kremer
Inspect roots to avoid certain resultants (Algorithm...
commit
|
commitdiff
|
tree
2020-08-12
Gereon Kremer
Add naive support for integer variables. (#4835)
commit
|
commitdiff
|
tree
2020-08-12
Gereon Kremer
Fix infinite loop in arith_ite_simp (#4805)
commit
|
commitdiff
|
tree
2020-08-05
Gereon Kremer
Improve error message for unsupported exponents (#4852)
commit
|
commitdiff
|
tree
2020-08-05
Gereon Kremer
Add dummy returns if libpoly is unavailable. (#4845)
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Properly initialize d_fullyInited. (#4840)
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Cad implementation (#4774)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Adds the interface for the CAD-based arithmetic solver...
commit
|
commitdiff
|
tree
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
commit
|
commitdiff
|
tree
2020-07-17
Gereon Kremer
Integration of libpoly (#4679)
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Resource manager cleanup (#4732)
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Remove cumulative time limits and cpu time limits ...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Fixes memory leak when an exception goes through runCvc4...
commit
|
commitdiff
|
tree
2020-07-15
Gereon Kremer
Add missing header (Fixes #4743) (#4749)
commit
|
commitdiff
|
tree
2020-07-13
Gereon Kremer
Implement --tlimit for windows (#4716)
commit
|
commitdiff
|
tree
2020-07-10
Gereon Kremer
Add deps/install/lib to RPATH and warn user when using...
commit
|
commitdiff
|
tree
2020-07-08
Gereon Kremer
Re-implement handling of --tlimit (#4655)
commit
|
commitdiff
|
tree