projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
bv: Add support for --bitblast=eager. (#6516)
[cvc5.git] / src / smt / set_defaults.cpp
2021-05-19 Mathias Preinerbv: Add support for --bitblast=eager. (#6516) blob | commitdiff | raw
2021-05-17 Gereon KremerImprove integration of CAD with nl-Ext (#6542) blob | commitdiff | raw | diff to current
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) blob | commitdiff | raw | diff to current
2021-04-23 Andrew ReynoldsEnable strings exp by default for strings specific... blob | commitdiff | raw | diff to current
2021-04-22 Andrew ReynoldsMinor changes to unsat core default setting (#6425) blob | commitdiff | raw | diff to current
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) blob | commitdiff | raw | diff to current
2021-04-14 Haniel Barbosa[unsat-cores] Improving new unsat cores (#6356) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) blob | commitdiff | raw | diff to current
2021-04-05 Andrew ReynoldsEnable UF when pre-skolem nested option is enabled... blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-25 Gereon KremerAdd missing includes. (#6207) blob | commitdiff | raw | diff to current
2021-03-17 Andrew Reynolds(proof-new) Fixes to set defaults (#6163) blob | commitdiff | raw | diff to current
2021-03-16 Haniel Barbosa[proof-new] Activating proofs when dumping proofs ... blob | commitdiff | raw | diff to current
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... blob | commitdiff | raw | diff to current
2021-03-09 Andrew ReynoldsRemove logic request (#6089) blob | commitdiff | raw | diff to current
2021-03-09 Andrew Reynolds(proof-new) Minor fix and allow proof option (#6085) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) blob | commitdiff | raw | diff to current
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) blob | commitdiff | raw | diff to current
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... blob | commitdiff | raw | diff to current
2021-02-10 Andrew ReynoldsRemove track instantiations infrastructure (#5883) blob | commitdiff | raw | diff to current
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) blob | commitdiff | raw | diff to current
2021-01-29 Haniel Barbosa[proof-new] Connecting new unsat cores (#5834) blob | commitdiff | raw | diff to current
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... blob | commitdiff | raw | diff to current
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) blob | commitdiff | raw | diff to current
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713) blob | commitdiff | raw | diff to current
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647) blob | commitdiff | raw | diff to current
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672) blob | commitdiff | raw | diff to current
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... blob | commitdiff | raw | diff to current
2020-12-03 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... blob | commitdiff | raw | diff to current
2020-10-27 Gereon KremerDisable --nl-cad option by default (#5350) blob | commitdiff | raw | diff to current
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) blob | commitdiff | raw | diff to current
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... blob | commitdiff | raw | diff to current
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... blob | commitdiff | raw | diff to current
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear... blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) blob | commitdiff | raw | diff to current
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-08 Andres NoetzliMake CVC/API BV div/mod semantics match SMT-LIB (#4997) blob | commitdiff | raw | diff to current
2020-09-08 Andrew ReynoldsEliminate a custom use of TheorySep in quantifiers... blob | commitdiff | raw | diff to current
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) blob | commitdiff | raw | diff to current
2020-08-28 yoni206Incremental support for bv_to_int (#4967) blob | commitdiff | raw | diff to current
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... blob | commitdiff | raw | diff to current
2020-08-21 Andrew ReynoldsRemove BV equality slicer (#4928) blob | commitdiff | raw | diff to current
2020-07-28 Andrew ReynoldsRemove arrays lazy rintro option (#4806) blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsMake use of options in setDefaults more consistent... blob | commitdiff | raw | diff to current
2020-07-11 yoni206Changing bv_to_int options (#4721) blob | commitdiff | raw | diff to current
2020-07-08 Andrew ReynoldsAlways interleave theory combination with quantifiers... blob | commitdiff | raw | diff to current
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... blob | commitdiff | raw | diff to current
2020-06-30 Ying ShengInterpolation step 1 (#4638) blob | commitdiff | raw | diff to current
2020-06-25 Andrew ReynoldsUpdate option --nl-ext to enable/disable incremental... blob | commitdiff | raw | diff to current
2020-06-23 Mathias PreinerAdd 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 yoni206Bv to int elimination bugfix (#4435) blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-06-03 Andrew ReynoldsUse prenex normal form when using cegqi-nested-qe ... blob | commitdiff | raw | diff to current
2020-06-01 Andres NoetzliSet theoryof-mode after theory widening (#4545) blob | commitdiff | raw | diff to current
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsUse debug-check-model to enable internal debugging... blob | commitdiff | raw | diff to current
2020-05-12 Andrew ReynoldsDo not enable unconstrained simplification if arithmeti... blob | commitdiff | raw | diff to current
2020-04-22 Andrew ReynoldsAllow eager bitblasting with solve bv as int in QF_NIA... blob | commitdiff | raw | diff to current
2020-04-21 Andrew ReynoldsMake option names related to CEGQI consistent (#4316) blob | commitdiff | raw | diff to current
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsAlways assign function values in higher order (#4279) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsDisable preregistration of instantiations for cegqi... blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsDisable macros when higher-order (#4266) blob | commitdiff | raw | diff to current
2020-04-09 Andrew ReynoldsSplit ProcessAssertions module from SmtEngine (#4210) blob | commitdiff | raw | diff to current
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) blob | commitdiff | raw | diff to current
2020-04-06 Andrew ReynoldsRemove links field in all toml files (#4201) blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsMove set defaults function to its own file (#4154) blob | commitdiff | raw | diff to current