projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2019-03-18 Aina NiemetzBitVector: Allow base 10 in constructor. (#2870) commit | commitdiff | tree
2019-03-16 Andres NoetzliLimit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ... commit | commitdiff | tree
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) commit | commitdiff | tree
2019-03-15 Haniel BarbosaNew beta-reduction for HOL solving (#2869) commit | commitdiff | tree
2019-03-15 Haniel BarbosaAdding capture avoiding substitution (#2867) commit | commitdiff | tree
2019-03-15 Andrew ReynoldsFix non-variable function head elimination in UF. ... commit | commitdiff | tree
2019-03-14 Andrew ReynoldsFix function term set for theory strings compute care... commit | commitdiff | tree
2019-03-14 Aina NiemetzImprove INSTALL instructions. (#2866) commit | commitdiff | tree
2019-03-14 Andrew ReynoldsUse zero slope tangent planes for transcendental functi... commit | commitdiff | tree
2019-03-14 Andrew ReynoldsProperly handle lambdas in relevant domain (#2853) commit | commitdiff | tree
2019-03-14 Andrew Reynolds Add getFreeVariables method to node algorithm (#2852) commit | commitdiff | tree
2019-03-14 Mathias PreinerDisable DCO signing for organization members. commit | commitdiff | tree
2019-03-14 Andrew ReynoldsImplement proper semantics for TPTP predicate is_rat... commit | commitdiff | tree
2019-03-14 Andrew Reynolds Fix substitution step in ho matching (#2825) commit | commitdiff | tree
2019-03-14 Andrew ReynoldsGeneralize sygus-rr-verify for fast enumerator (#2829) commit | commitdiff | tree
2019-03-14 makaimanncheck for null assumption in query and replace with... commit | commitdiff | tree
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... commit | commitdiff | tree
2019-03-13 Andrew ReynoldsRemove spurious data member. (#2857) commit | commitdiff | tree
2019-03-13 Mathias PreinerFix public headers for make install. (#2856) commit | commitdiff | tree
2019-03-12 Andrew ReynoldsAdd option --sygus-rr-synth-rec for considering all... commit | commitdiff | tree
2019-03-12 Andrew Reynolds Move tuple/record update elimination from ppRewrite... commit | commitdiff | tree
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812) commit | commitdiff | tree
2019-02-27 Andres NoetzliUse string stream for proofs instead of tmp files ... commit | commitdiff | tree
2019-02-26 Andres NoetzliClangFormat: Disable DerivePointerAlignment (#2842) commit | commitdiff | tree
2019-02-13 Aina NiemetzNew C++ API: Remove redundant declareFun function.... commit | commitdiff | tree
2019-02-13 Andres NoetzliRewrite simple regexp pattern to str.contains (#2827) commit | commitdiff | tree
2019-02-13 Aina NiemetzNew C++ API: Remove redundant mkTerm function. (#2836) commit | commitdiff | tree
2019-02-12 Andres NoetzliDelete temporary proof files when aborting CVC4 (#2834) commit | commitdiff | tree
2019-02-11 Aina NiemetzNew C++ API: Unit tests for declare* functions. (#2831) commit | commitdiff | tree
2019-02-05 Andres NoetzliMake stripConstantEndpoints() less aggressive (#2830) commit | commitdiff | tree
2019-02-04 Andres NoetzliAdd rewrite for contains + const strings replace (... commit | commitdiff | tree
2019-02-02 Andres NoetzliFix corner case in stripConstantEndpoints (#2824) commit | commitdiff | tree
2019-01-29 Andres NoetzliFix warning due to catching polymorphic exceptions... commit | commitdiff | tree
2019-01-29 Aina NiemetzNew C++ API: Fix checks for mkTerm. (#2820) commit | commitdiff | tree
2019-01-29 Andres NoetzliStrings: Remove redundant replace rewrite (#2822) commit | commitdiff | tree
2019-01-24 Alex OzdemirExtended DRAT signature to operational DRAT (#2815) commit | commitdiff | tree
2019-01-23 Andres NoetzliAvoid using ProofManager in non-proof CMS build (#2814) commit | commitdiff | tree
2019-01-23 Andres NoetzliStrings: Strengthen multiset reasoning (#2817) commit | commitdiff | tree
2019-01-22 Andrew Reynolds Fix tuple and record CVC printing (#2818) commit | commitdiff | tree
2019-01-22 Andrew Reynolds Fix parsing of overloaded parametric datatype selector... commit | commitdiff | tree
2019-01-22 Aina NiemetzNew README (markdown). (#2797) commit | commitdiff | tree
2019-01-19 Andres NoetzliFix missing-override warning (#2811) commit | commitdiff | tree
2019-01-18 Alex OzdemirExtract DIMACS Printing (#2800) commit | commitdiff | tree
2019-01-18 Andres NoetzliStrings: Introduce checkEntailContains() (#2809) commit | commitdiff | tree
2019-01-18 Andres Noetzli Fix ABC build (#2808) commit | commitdiff | tree
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805) commit | commitdiff | tree
2019-01-16 Andres NoetzliUpdate NEWS file (#2804) commit | commitdiff | tree
2019-01-16 Alex OzdemirBugfix: LFSC clause equality (#2801) commit | commitdiff | tree
2019-01-16 Alex OzdemirExtended Resolution Signature (#2788) commit | commitdiff | tree
2019-01-16 Andrew ReynoldsFix constant contains ITOS rewrite (#2799) commit | commitdiff | tree
2019-01-16 Andres NoetzliCMake: Fix search for static libraries (#2798) commit | commitdiff | tree
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794) commit | commitdiff | tree
2019-01-15 Andrew Reynolds Fix unsound double abs rewrite rule for FP (#2792) commit | commitdiff | tree
2019-01-15 Andrew Reynolds Only check disequal terms with sygus-rr-verify (#2793) commit | commitdiff | tree
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786) commit | commitdiff | tree
2019-01-13 Alex OzdemirLFSC LRAT Output (#2787) commit | commitdiff | tree
2019-01-12 Alex OzdemirLratInstruction inheritance (#2784) commit | commitdiff | tree
2019-01-11 Alex OzdemirFixed linking against drat2er, and use drat2er (#2785) commit | commitdiff | tree
2019-01-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,... commit | commitdiff | tree
2019-01-10 Aina NiemetzNew C++ API: Get rid of mkConst functions (simplify... commit | commitdiff | tree
2019-01-09 Andrew ReynoldsDo not rewrite 1-constructor sygus testers to true... commit | commitdiff | tree
2019-01-09 Alex Ozdemir[BV Proofs] Option for proof format (#2777) commit | commitdiff | tree
2019-01-09 Alex OzdemirClause proof printing (#2779) commit | commitdiff | tree
2019-01-09 Alex OzdemirLFSC drat output (#2776) commit | commitdiff | tree
2019-01-07 Aina NiemetzNew C++ API: Add missing getType() calls to kick off... commit | commitdiff | tree
2019-01-06 Alex Ozdemir[DRAT] DRAT data structure (#2767) commit | commitdiff | tree
2019-01-05 Mathias Preinercmake: Disable unit tests for static builds. (#2775) commit | commitdiff | tree
2019-01-04 Andres NoetzliC++ API: Fix OOB read in unit test (#2774) commit | commitdiff | tree
2019-01-04 Alex Ozdemir[LRAT] A C++ data structure for LRAT. (#2737) commit | commitdiff | tree
2019-01-04 Aina NiemetzNew C++ API: Add missing catch blocks for std::invalid_... commit | commitdiff | tree
2019-01-03 Andres NoetzliAPI/Smt2 parser: refactor termAtomic (#2674) commit | commitdiff | tree
2019-01-03 Andres NoetzliC++ API: Reintroduce zero-value mkBitVector method... commit | commitdiff | tree
2019-01-03 Alex Ozdemir[LRA proof] Recording & Printing LRA Proofs (#2758) commit | commitdiff | tree
2019-01-03 Aina NiemetzNew C++ API: Add tests for mk-functions in solver objec... commit | commitdiff | tree
2018-12-20 Aina NiemetzClean up BV kinds and type rules. (#2766) commit | commitdiff | tree
2018-12-20 Aina NiemetzAdd missing type rules for parameterized operator kinds... commit | commitdiff | tree
2018-12-19 Andrew ReynoldsFix issues with REWRITE_DONE in floating point rewriter... commit | commitdiff | tree
2018-12-18 Aina NiemetzRemove noop. (#2763) commit | commitdiff | tree
2018-12-17 Alex Ozdemir Configured for linking against drat2er (#2754) commit | commitdiff | tree
2018-12-17 Aina NiemetzNew C++ API: Add tests for term object. (#2755) commit | commitdiff | tree
2018-12-17 Alex OzdemirDRAT Signature (#2757) commit | commitdiff | tree
2018-12-15 Andres NoetzliRevert "Move ss-combine rewrite to extended rewriter... commit | commitdiff | tree
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747) commit | commitdiff | tree
2018-12-14 Aina NiemetzFixed typos. commit | commitdiff | tree
2018-12-14 Aina NiemetzNew C++ API: Add tests for opterm object. (#2756) commit | commitdiff | tree
2018-12-14 Andrew Reynolds Fix extended rewriter for binary associative operators... commit | commitdiff | tree
2018-12-14 Andrew ReynoldsMake single invocation and invariant pre/post condition... commit | commitdiff | tree
2018-12-13 Aina NiemetzNew C++ API: Add tests for sort functions of solver... commit | commitdiff | tree
2018-12-13 Andrew ReynoldsRemove spurious map (#2750) commit | commitdiff | tree
2018-12-13 Aina NiemetzFix compiler warnings. (#2748) commit | commitdiff | tree
2018-12-12 Andres NoetzliAPI: Add simple empty/sigma regexp unit tests (#2746) commit | commitdiff | tree
2018-12-12 Alex Ozdemir[LRA proof] More complete LRA example proofs. (#2722) commit | commitdiff | tree
2018-12-12 Alex Ozdemir[LRAT] signature robust against duplicate literals... commit | commitdiff | tree
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) commit | commitdiff | tree
2018-12-11 Alex OzdemirLRAT signature (#2731) commit | commitdiff | tree
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) commit | commitdiff | tree
2018-12-07 Andres NoetzliStrings: Make EXTF_d inference more conservative (... commit | commitdiff | tree
2018-12-07 Alex OzdemirArith Constraint Proof Loggin (#2732) commit | commitdiff | tree
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733) commit | commitdiff | tree
2018-12-06 Andres NoetzliFix use-after-free due to destruction order (#2739) commit | commitdiff | tree
next