projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)
[cvc5.git] / src / prop /
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
2020-02-29 Aina NiemetzpropEngine: Reorder class declaration according to... tree | commitdiff
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) tree | commitdiff
2020-02-22 makaimannDump boolean propagations and conflicts for decision... tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-16 makaimannTrace tags for dumping the decision tree in org-mode... tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-08 Mathias Preinercmake: Disable C++ GNU extensions. (#3446) tree | commitdiff
2019-10-31 Mathias PreinerFix Unimplemented() macros missed in #3366. (#3424) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-09-07 Andrew ReynoldsRemove portfolio (#3236) tree | commitdiff
2019-08-02 Mathias PreinerUpdate CaDiCaL to version 1.0.3. (#3137) tree | commitdiff
2019-07-02 Alex OzdemirOptimize DRAT optimization: clause matching (#3074) tree | commitdiff
2019-05-18 Andres NoetzliSupport for incremental bit-blasting with CaDiCaL ... tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-05 Alex OzdemirSatClauseSetHashFunction (#2916) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-01-23 Andres NoetzliAvoid using ProofManager in non-proof CMS build (#2814) tree | commitdiff
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786) tree | commitdiff
2018-12-03 Alex OzdemirBit vector proof superclass (#2599) tree | commitdiff
2018-10-19 Mathias PreinerRemove autotools build system. (#2639) tree | commitdiff
2018-10-01 Aina NiemetzFix compiler warnings. (#2555) tree | commitdiff
2018-09-22 Mathias Preinercmake: Various CMakeLists.txt fixes/cleanup. tree | commitdiff
2018-09-22 Mathias Preinercmake: Only build libcvc4 and libcvc4parser as libraries. tree | commitdiff
2018-09-22 Mathias Preinercmake: Cleanup CMakeLists.txt files, remove SHARED. tree | commitdiff
2018-09-22 Mathias Preinercmake: Working build infrastructure. tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-13 Mathias PreinerFix #include for minisat headers in bvminisat. (#2463) tree | commitdiff
2018-08-17 Andrew ReynoldsRemove support for flipDecision (#2319) tree | commitdiff
2018-08-08 Andres NoetzliDelete functions instead of using CVC4_UNDEFINED (... tree | commitdiff
2018-08-02 Andrew Reynolds Remove references to deprecated propagate as decision... tree | commitdiff
2018-07-30 Mathias PreinerAdd support for incremental eager bit-blasting. (#1838) tree | commitdiff
2018-07-30 FabianWolffFix several spelling errors (#2231) tree | commitdiff
2018-07-13 Andres NoetzliProperly clean up assertion stack in CnfProof (#2147) tree | commitdiff
2018-06-28 Andres NoetzliFix stale reference in MiniSat when generating UC ... tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-06-13 Andres NoetzliWorkaround for incremental unsat cores (#1962) tree | commitdiff
2018-06-09 Andres NoetzliReset decisions at SAT level after solving (#2059) tree | commitdiff
2018-05-25 Andres NoetzliMiniSat: Be more careful about running proof code ... tree | commitdiff
2018-05-23 Andres NoetzliRemove ProofProxy (#1965) tree | commitdiff
next