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

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
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

RSS Atom