git.libre-soc.org Git - cvc5.git/history - src/smt/set

[cvc5.git] / src / smt / set_defaults.cpp

2020-12-16	Andrew Reynolds	Simplify preprocessing (#5647)	blob \| commitdiff \| raw
2020-12-15	Andrew Reynolds	Remove bv divide by zero option (#5672)	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	Fix issue with free variables introduced by quantifier...	blob \| commitdiff \| raw \| diff to current
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-11-19	Andrew Reynolds	Enable new implementation of CEGQI based on nested...	blob \| commitdiff \| raw \| diff to current
2020-10-27	Gereon Kremer	Disable --nl-cad option by default (#5350)	blob \| commitdiff \| raw \| diff to current
2020-10-27	Gereon Kremer	Enable --nl-cad by default (#5345)	blob \| commitdiff \| raw \| diff to current
2020-10-22	Gereon Kremer	Use theoryof-mode=type for QF_NRA (#5326)	blob \| commitdiff \| raw \| diff to current
2020-10-12	Andrew Reynolds	Ensure uninterpreted sort owner is UF if uf-ho or finit...	blob \| commitdiff \| raw \| diff to current
2020-10-05	Andrew Reynolds	Make sygus more robust to unknown responses in solution...	blob \| commitdiff \| raw \| diff to current
2020-10-02	Gereon Kremer	Allow for theory combination of strings with nonlinear...	blob \| commitdiff \| raw \| diff to current
2020-09-23	Andrew Reynolds	Disable cegqi-bv when using sygus (#5124)	blob \| commitdiff \| raw \| diff to current
2020-09-23	Andrew Reynolds	Allow E-matching by default when strings are enabled...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Add simple BV solver (#5065)	blob \| commitdiff \| raw \| diff to current
2020-09-22	mudathirmahgoub	Add skeleton for theory of bags (multisets) (#5100)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-08	Andres Noetzli	Make CVC/API BV div/mod semantics match SMT-LIB (#4997)	blob \| commitdiff \| raw \| diff to current
2020-09-08	Andrew Reynolds	Eliminate a custom use of TheorySep in quantifiers...	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-08-28	yoni206	Incremental support for bv_to_int (#4967)	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Connect the relevance manager to TheoryEngine and use...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove BV equality slicer (#4928)	blob \| commitdiff \| raw \| diff to current
2020-07-28	Andrew Reynolds	Remove arrays lazy rintro option (#4806)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andrew Reynolds	Make use of options in setDefaults more consistent...	blob \| commitdiff \| raw \| diff to current
2020-07-11	yoni206	Changing bv_to_int options (#4721)	blob \| commitdiff \| raw \| diff to current
2020-07-08	Andrew Reynolds	Always interleave theory combination with quantifiers...	blob \| commitdiff \| raw \| diff to current
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	blob \| commitdiff \| raw \| diff to current
2020-06-30	Ying Sheng	Interpolation step 1 (#4638)	blob \| commitdiff \| raw \| diff to current
2020-06-25	Andrew Reynolds	Update option --nl-ext to enable/disable incremental...	blob \| commitdiff \| raw \| diff to current
2020-06-23	Mathias Preiner	Add support for eqrange predicate (#4562)	blob \| commitdiff \| raw \| diff to current
2020-06-22	Andrew Reynolds	(proof-new) Add proof-new to options file (#4641)	blob \| commitdiff \| raw \| diff to current
2020-06-19	yoni206	Bv to int elimination bugfix (#4435)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-03	Andrew Reynolds	Use prenex normal form when using cegqi-nested-qe ...	blob \| commitdiff \| raw \| diff to current
2020-06-01	Andres Noetzli	Set theoryof-mode after theory widening (#4545)	blob \| commitdiff \| raw \| diff to current
2020-05-23	Andrew Reynolds	Refactor operator elimination in arithmetic (#4519)	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Use debug-check-model to enable internal debugging...	blob \| commitdiff \| raw \| diff to current
2020-05-12	Andrew Reynolds	Do not enable unconstrained simplification if arithmeti...	blob \| commitdiff \| raw \| diff to current
2020-04-22	Andrew Reynolds	Allow eager bitblasting with solve bv as int in QF_NIA...	blob \| commitdiff \| raw \| diff to current
2020-04-21	Andrew Reynolds	Make option names related to CEGQI consistent (#4316)	blob \| commitdiff \| raw \| diff to current
2020-04-17	Mathias Preiner	SyGuS instantiation quantifiers module (#3910)	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Always assign function values in higher order (#4279)	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Disable preregistration of instantiations for cegqi...	blob \| commitdiff \| raw \| diff to current
2020-04-14	Andrew Reynolds	Disable macros when higher-order (#4266)	blob \| commitdiff \| raw \| diff to current
2020-04-09	Andrew Reynolds	Split ProcessAssertions module from SmtEngine (#4210)	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-06	Andrew Reynolds	Remove links field in all toml files (#4201)	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andrew Reynolds	Move set defaults function to its own file (#4154)	blob \| commitdiff \| raw \| diff to current

RSS Atom