projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Improve arithmetic proofs (#6106)
[cvc5.git] / src / proof /
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-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... 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-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) 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-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-03 Andres NoetzliRemove SWIG bindings (#4683) tree | commitdiff
2020-06-19 Haniel BarbosaGeneralize atom collection in old proof code (#4626) tree | commitdiff
2020-06-18 Andres NoetzliImprove memory management in Java bindings (#4629) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... tree | commitdiff
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) tree | commitdiff
2020-03-16 Alex OzdemirRemove AlwaysAssert(false) for hole. tree | commitdiff
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes tree | commitdiff
2020-03-11 Andres NoetzliSet assertion in `CnfStream::ensureLiteral()` (#3927) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826) tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-12 Andres NoetzliRename Java package to edu.stanford.CVC4 (#3752) tree | commitdiff
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740) tree | commitdiff
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732) tree | commitdiff
2020-02-07 Alex OzdemirPropagate expected types through UF arguments (#3717) tree | commitdiff
2020-02-07 Alex OzdemirAdd `ArithProof::{printInteger,getLfscFunction}` (... tree | commitdiff
2020-02-01 Alex OzdemirHandle `expectedType` in TheoryProofEngine (#3691) tree | commitdiff
2020-01-30 Alex OzdemirexpectedType in proof-printing code (#3665) tree | commitdiff
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... tree | commitdiff
2019-11-19 Alex OzdemirAdd a few comments to ProofManager (#3477) tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-07-22 Andres NoetzliAvoid move constructor of std::fstream for GCC < 5... tree | commitdiff
2019-07-02 Alex OzdemirOptimize DRAT optimization: clause matching (#3074) tree | commitdiff
2019-06-21 Andres NoetzliUse TMPDIR environment variable for temp files (#2849) tree | commitdiff
2019-06-13 Haniel BarbosaFix warning (#3053) tree | commitdiff
2019-06-05 Alex OzdemirDRAT-Optimization (#2971) tree | commitdiff
2019-05-16 Andres NoetzliFix iterators in Java API (#3000) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-18 Andrew Reynolds Less aggressive caching in equality engine when proofs... tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) tree | commitdiff
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... tree | commitdiff
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812) tree | commitdiff
2019-01-18 Alex OzdemirExtract DIMACS Printing (#2800) tree | commitdiff
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786) tree | commitdiff
2019-01-13 Alex OzdemirLFSC LRAT Output (#2787) tree | commitdiff
2019-01-12 Alex OzdemirLratInstruction inheritance (#2784) tree | commitdiff
2019-01-11 Alex OzdemirFixed linking against drat2er, and use drat2er (#2785) tree | commitdiff
2019-01-09 Alex OzdemirClause proof printing (#2779) tree | commitdiff
2019-01-09 Alex OzdemirLFSC drat output (#2776) tree | commitdiff
2019-01-06 Alex Ozdemir[DRAT] DRAT data structure (#2767) tree | commitdiff
2019-01-04 Alex Ozdemir[LRAT] A C++ data structure for LRAT. (#2737) tree | commitdiff
2019-01-03 Alex Ozdemir[LRA proof] Recording & Printing LRA Proofs (#2758) tree | commitdiff
2018-12-17 Aina NiemetzNew C++ API: Add tests for term object. (#2755) tree | commitdiff
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747) tree | commitdiff
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733) tree | commitdiff
2018-12-06 Andres NoetzliFix use-after-free due to destruction order (#2739) tree | commitdiff
2018-12-03 Alex OzdemirBit vector proof superclass (#2599) tree | commitdiff
2018-11-20 Alex OzdemirChange lemma proof step storage & iterators (#2712) tree | commitdiff
2018-09-25 yoni206carefully printing trusted assertions in proofs (#2505) tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-08-27 Andres NoetzliResolution proof: separate printing from proof (#1964) tree | commitdiff
2018-08-17 Andrew ReynoldsRemove support for flipDecision (#2319) tree | commitdiff
2018-07-13 Andres NoetzliProperly clean up assertion stack in CnfProof (#2147) tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-05-23 Andres NoetzliRemove ProofProxy (#1965) tree | commitdiff
2018-05-03 Andres NoetzliFix warnings in proof code (#1850) tree | commitdiff
2018-04-25 yoni206Refactor array-proofs and uf-proofs (#1655) tree | commitdiff
2018-04-02 Mathias PreinerReorganize bitblaster code. (#1695) tree | commitdiff
2018-03-07 Mathias PreinerMake statistics output consistent. (#1647) tree | commitdiff
2018-03-05 Mathias PreinerEnable -Wsuggest-override by default. (#1643) tree | commitdiff
2018-02-10 Aina NiemetzMove BitVector specific funs from bv::utils to util... tree | commitdiff
2018-02-09 Tim KingReplacing an incorrect reference to an injected class... tree | commitdiff
2017-11-16 Tim KingInitializes BitVectorProof::d_isAssumptionConflict... tree | commitdiff
2017-11-15 Tim KingAdding garbage collection for Proof objects. (#1294) tree | commitdiff
2017-10-26 Tim KingRemoving throw specifiers from OutputChannel and subcla... tree | commitdiff
2017-10-25 Tim KingSwitching EqProof to use shared_ptr everywhere. (... tree | commitdiff
2017-10-11 Tim KingCleaning up ProofArray class. (#1208) tree | commitdiff
2017-10-11 Andrew ReynoldsMove unsat core names to smt engine (#1192) tree | commitdiff
2017-09-19 Andres NoetzliFix issue #1074, improve non-fatal error handling ... tree | commitdiff
2017-08-24 Andrew ReynoldsMerge pull request #191 from timothy-king/cleanup-regexp tree | commitdiff
2017-08-21 Mathias PreinerChange Bugzilla urls to Github issues. tree | commitdiff
2017-08-09 Andres NoetzliFix compiler warning in sat_proof_implementation tree | commitdiff
2017-07-21 Tim KingMerge branch 'master' into cleanup-regexp tree | commitdiff
2017-07-21 Tim KingMoving from the gnu extensions for hash maps to the... tree | commitdiff
2017-07-07 Mathias PreinerUpdate copyright headers. tree | commitdiff
2017-06-30 Andres NötzliFix use-after-free with unsat cores/proofs (#174) tree | commitdiff
2017-06-21 Andrew ReynoldsMerge pull request #175 from CVC4/fix_uninit tree | commitdiff
2017-06-16 Clark BarrettMerge pull request #170 from CVC4/fix_2_6_parser3 tree | commitdiff
2017-06-16 Andres NötzliFix segfault by making unit conflict CDMaybe tree | commitdiff
2017-05-31 guykatzzA more informative error message when a theory is not... tree | commitdiff
next