projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Initial setup for docs of python API (#6445)
[cvc5.git] / src / prop /
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) tree | commitdiff
2021-04-26 Haniel BarbosaFix assertions in SAT solver (#6443) tree | commitdiff
2021-04-24 Mathias PreinerAdd assumption-based unsat cores. (#6427) tree | commitdiff
2021-04-23 Gereon KremerMake sure a ReferenceStat is set to values of the corre... tree | commitdiff
2021-04-22 Andrew Reynolds Reorganizing use of skolem definition manager in prop... tree | commitdiff
2021-04-22 Haniel BarbosaReconciling proofs and unsat cores (#6405) tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-15 Mathias PreinerBuild support library from base and context. (#6368) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-14 Haniel Barbosa[unsat-cores] Improving new unsat cores (#6356) tree | commitdiff
2021-04-14 Haniel Barbosa[proof-new] Fix explanation of literals in SAT proof... tree | commitdiff
2021-04-12 Gereon KremerRefactor resource manager (#6322) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-12 Andrew ReynoldsConsolidate interface to prop engine (#6189) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-09 Haniel Barbosa[proof-new] Optimizing sat proof (#6324) tree | commitdiff
2021-04-07 Haniel Barbosa[proof-new] Fixing SMT post-processor's handling of... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187) tree | commitdiff
2021-03-16 Mathias Preinercmake: Generate cvc4_export.h and set visibility to... tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-12 Andres NoetzliSchedule preregistration lemmas to be satisfied after... tree | commitdiff
2021-03-12 Gereon KremerAdd missing includes for statistics (#6124) tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099) tree | commitdiff
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-26 Haniel BarbosaSome formatting and better tracing in prop engine ... tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix dangling pointer in SAT proof generatio... tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix handling of removable clauses in proof... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
2021-02-12 Andrew ReynoldsSimplify and fix decision engine's handling of skolem... tree | commitdiff
2021-02-11 Haniel Barbosa[proof-new] Adding a proof-producing ensure literal... tree | commitdiff
2021-02-04 Haniel Barbosa[proof-new] Catch trivial cycles in SAT proof generatio... tree | commitdiff
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) tree | commitdiff
2021-02-02 Andrew ReynoldsCleanup some includes (#5847) tree | commitdiff
2021-01-28 Andrew ReynoldsSimplify lemma interface (#5819) tree | commitdiff
2021-01-28 Andrew ReynoldsAlways theory-preprocess lemmas (#5817) tree | commitdiff
2021-01-24 Andrew ReynoldsAdd interface for getting preprocessed term (#5798) tree | commitdiff
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) tree | commitdiff
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory... tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708) tree | commitdiff
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy... tree | commitdiff
2020-12-17 Haniel Barbosa[proof-new] Only use old proof code for unsat cores... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing... tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667) tree | commitdiff
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine... tree | commitdiff
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... tree | commitdiff
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own... tree | commitdiff
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) tree | commitdiff
2020-11-09 Gereon KremerProperly clear interrupt for solve() as well. (#5403) tree | commitdiff
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro... tree | commitdiff
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262) tree | commitdiff
2020-10-14 Haniel Barbosausing NOT_NOT_ELIM rather than macros to do double... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Removing spurious forward declaration in... tree | commitdiff
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... tree | commitdiff
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-12 Andrew Reynolds(proof-new) Update TheoryEngine lemma and conflict... tree | commitdiff
2020-09-02 Andres NoetzliFix CryptoMiniSat build, regression (#5006) tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-09-01 FabianWolffFix spelling errors (#4977) tree | commitdiff
2020-08-15 Andrew ReynoldsAdd finishInit method to PropEngine (#4895) tree | commitdiff
2020-07-30 Andres NoetzliPython API: Add support for sequences (#4757) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-05-22 Aina NiemetzCaDiCaL: Clean up initialization on creation. (#4516) tree | commitdiff
2020-05-22 Aina NiemetzCryptominisat: Clean up initialization on creation... tree | commitdiff
2020-05-22 Aina NiemetzAdd support for SAT solver Kissat. (#4514) tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-03-31 Andrew ReynoldsRemove replay and use-theory options and idl (#4186) tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-10 Aina NiemetzFix issue with reset-assertions. (#3988) tree | commitdiff
2020-03-09 Andres NoetzliMake registration of unit clauses more robust (#3965) tree | commitdiff
2020-03-05 Aina NiemetzMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Aina NiemetzRevert "Move ownership of DecisionEngine into PropEngin... tree | commitdiff
2020-03-05 Andrew ReynoldsMove ownership of DecisionEngine into PropEngine. ... tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
next