projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Eliminate Output macro in favor of simple Env functions (#7223)
[cvc5.git] / src / prop /
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194) tree | commitdiff
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) tree | commitdiff
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process... tree | commitdiff
2021-08-19 Haniel Barbosa[unsat cores] [proofs] Revert test about when to explai... tree | commitdiff
2021-08-18 Andrew ReynoldsMake TheoryProxy use Env, simplify initialization of... tree | commitdiff
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) tree | commitdiff
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) tree | commitdiff
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... tree | commitdiff
2021-07-09 Andrew ReynoldsImplement stop-only for new justification heuristic... tree | commitdiff
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... tree | commitdiff
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) tree | commitdiff
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761) tree | commitdiff
2021-06-18 Mathias PreinerMake CnfStream::toCNF iterative (#6757) tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) tree | commitdiff
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) tree | commitdiff
2021-05-27 Andrew ReynoldsEnable new justification heuristic by default (#6613) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-20 Gereon KremerProperly initialize. (#6586) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-19 Mathias PreinerCorrectly handle negated assertions for assumption... tree | commitdiff
2021-05-17 Andres NoetzliInclude cinttypes instead of inttypes.h (#6548) tree | commitdiff
2021-05-14 Mathias Preinerbv: Assert input facts on user-level 0. (#6515) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-05 Andrew ReynoldsMove current decision engine to decision engine old... tree | commitdiff
2021-05-04 Andrew ReynoldsMove env into smt solver, theory engine, prop engine... tree | commitdiff
2021-05-04 Haniel BarbosaDo not use proof CNF stream with assumptions-based... tree | commitdiff
2021-04-28 Gereon KremerMake sure reference stats are reset properly (#6457) tree | commitdiff
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
next