projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
README: Remove project leaders, history.
[cvc5.git] / src /
2019-04-23 Alex Ozdemir[BV] An option for SAT proof optimization (#2915) tree | commitdiff
2019-04-23 Andrew ReynoldsRefactor normal forms in strings (#2897) tree | commitdiff
2019-04-18 Andrew ReynoldsFail fast strategy for propagating instances (#2939) tree | commitdiff
2019-04-18 Andrew Reynolds Less aggressive caching in equality engine when proofs... tree | commitdiff
2019-04-17 Andrew ReynoldsCache explanations in the equality engine (#2937) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
2019-04-17 Andrew ReynoldsFix extended function decomposition (#2960) tree | commitdiff
2019-04-16 Andrew ReynoldsAdd interface for term enumeration (#2956) tree | commitdiff
2019-04-16 Andres NoetzliMake bv{add,mul,and,or,xor,xnor} left-associative ... tree | commitdiff
2019-04-16 Andrew ReynoldsStratify enumerative instantiation (#2954) tree | commitdiff
2019-04-16 Andrew ReynoldsMinor simplifications to theory quantifiers (#2953) tree | commitdiff
2019-04-16 makaimannCheck for rt library in configuration -- support for... tree | commitdiff
2019-04-11 Andrew Reynolds Eliminate Boolean ITE within terms, fixes 2947 (#2949) tree | commitdiff
2019-04-08 Haniel Barbosafix copyright year in configuration file (#2942) tree | commitdiff
2019-04-05 Andrew ReynoldsFix another corner case of datatypes+PBE (#2938) tree | commitdiff
2019-04-05 Haniel Barbosafix fp issue (#2940) tree | commitdiff
2019-04-05 Alex OzdemirSatClauseSetHashFunction (#2916) tree | commitdiff
2019-04-04 Haniel BarbosaIgnoring FP benchmarks with "unsafe" sizes unless optio... tree | commitdiff
2019-04-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-04-03 Andrew ReynoldsFix combination of datatypes + strings in PBE (#2930) tree | commitdiff
2019-04-01 Andres NoetzliFP: Fix wrong model due to partial assignment (#2910) tree | commitdiff
2019-04-01 Andres NoetzliFix RewriteITEBv to ensure rewrite to fixpoint (#2878) tree | commitdiff
2019-04-01 Andrew ReynoldsModify strategy in sets+cardinality (#2909) tree | commitdiff
2019-03-29 Andrew ReynoldsApply empty splits more aggressively in sets+cardinalit... tree | commitdiff
2019-03-29 Andres NoetzliFix freeing nodes with maxed refcounts (#2903) tree | commitdiff
2019-03-29 Andrew ReynoldsFix issues in cvc parser (#2901) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-26 Andres NoetzliFix warnings about wrong line numbers (#2899) tree | commitdiff
2019-03-26 Andrew ReynoldsFix a few warnings (#2898) tree | commitdiff
2019-03-24 Andrew Reynolds Split regular expression solver (#2891) tree | commitdiff
2019-03-24 Aina NiemetzNew C++ API: Fix include. (#2896) tree | commitdiff
2019-03-24 Aina NiemetzBV: Fix typerules for rotate operators. (#2895) tree | commitdiff
2019-03-23 Andres NoetzliFix memory leak when using subsolvers (#2893) tree | commitdiff
2019-03-23 Andres NoetzliStrip non-matching beginning from indexof operator... tree | commitdiff
2019-03-22 Andrew ReynoldsRevisit strings extended function decomposition (... tree | commitdiff
2019-03-22 Andrew ReynoldsFix instantiation stat for fmf (#2889) tree | commitdiff
2019-03-22 Andrew ReynoldsMore fixes for PBE with datatypes (#2882) tree | commitdiff
2019-03-22 Haniel Barbosafix help information on TPTP parsing (#2884) tree | commitdiff
2019-03-22 Andres NoetzliFix stripConstantEndpoints in strings rewriter (#2883) tree | commitdiff
2019-03-22 makaimannUse empty vector instead of false in query with null... tree | commitdiff
2019-03-21 Andrew Reynolds Fix bad comparison in RE solver's addMembership (... tree | commitdiff
2019-03-21 Andrew ReynoldsRewrite selectors correctly applied to constructors... tree | commitdiff
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) tree | commitdiff
2019-03-19 Andrew ReynoldsMake declare-datatype(s) a standard, non-extended comma... tree | commitdiff
2019-03-19 Andrew ReynoldsFix fairness issue with fast sygus enumerator (#2873) tree | commitdiff
2019-03-19 Aina NiemetzNew C++: Remove redundant mkBoundVar function. tree | commitdiff
2019-03-19 Aina NiemetzNew C++: Remove redundant mkVar function. tree | commitdiff
2019-03-18 Aina NiemetzBitVector: Allow base 10 in constructor. (#2870) tree | commitdiff
2019-03-16 Andres NoetzliLimit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ... tree | commitdiff
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) tree | commitdiff
2019-03-15 Haniel BarbosaNew beta-reduction for HOL solving (#2869) tree | commitdiff
2019-03-15 Haniel BarbosaAdding capture avoiding substitution (#2867) tree | commitdiff
2019-03-15 Andrew ReynoldsFix non-variable function head elimination in UF. ... tree | commitdiff
2019-03-14 Andrew ReynoldsFix function term set for theory strings compute care... tree | commitdiff
2019-03-14 Andrew ReynoldsUse zero slope tangent planes for transcendental functi... tree | commitdiff
2019-03-14 Andrew ReynoldsProperly handle lambdas in relevant domain (#2853) tree | commitdiff
2019-03-14 Andrew Reynolds Add getFreeVariables method to node algorithm (#2852) tree | commitdiff
2019-03-14 Andrew ReynoldsImplement proper semantics for TPTP predicate is_rat... tree | commitdiff
2019-03-14 Andrew Reynolds Fix substitution step in ho matching (#2825) tree | commitdiff
2019-03-14 Andrew ReynoldsGeneralize sygus-rr-verify for fast enumerator (#2829) tree | commitdiff
2019-03-14 makaimanncheck for null assumption in query and replace with... tree | commitdiff
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... tree | commitdiff
2019-03-13 Andrew ReynoldsRemove spurious data member. (#2857) tree | commitdiff
2019-03-13 Mathias PreinerFix public headers for make install. (#2856) tree | commitdiff
2019-03-12 Andrew ReynoldsAdd option --sygus-rr-synth-rec for considering all... tree | commitdiff
2019-03-12 Andrew Reynolds Move tuple/record update elimination from ppRewrite... tree | commitdiff
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812) tree | commitdiff
2019-02-27 Andres NoetzliUse string stream for proofs instead of tmp files ... tree | commitdiff
2019-02-13 Aina NiemetzNew C++ API: Remove redundant declareFun function.... tree | commitdiff
2019-02-13 Andres NoetzliRewrite simple regexp pattern to str.contains (#2827) tree | commitdiff
2019-02-13 Aina NiemetzNew C++ API: Remove redundant mkTerm function. (#2836) tree | commitdiff
2019-02-12 Andres NoetzliDelete temporary proof files when aborting CVC4 (#2834) tree | commitdiff
2019-02-11 Aina NiemetzNew C++ API: Unit tests for declare* functions. (#2831) tree | commitdiff
2019-02-05 Andres NoetzliMake stripConstantEndpoints() less aggressive (#2830) tree | commitdiff
2019-02-04 Andres NoetzliAdd rewrite for contains + const strings replace (... tree | commitdiff
2019-02-02 Andres NoetzliFix corner case in stripConstantEndpoints (#2824) tree | commitdiff
2019-01-29 Aina NiemetzNew C++ API: Fix checks for mkTerm. (#2820) tree | commitdiff
2019-01-29 Andres NoetzliStrings: Remove redundant replace rewrite (#2822) tree | commitdiff
2019-01-23 Andres NoetzliAvoid using ProofManager in non-proof CMS build (#2814) tree | commitdiff
2019-01-23 Andres NoetzliStrings: Strengthen multiset reasoning (#2817) tree | commitdiff
2019-01-22 Andrew Reynolds Fix tuple and record CVC printing (#2818) tree | commitdiff
2019-01-22 Andrew Reynolds Fix parsing of overloaded parametric datatype selector... tree | commitdiff
2019-01-19 Andres NoetzliFix missing-override warning (#2811) tree | commitdiff
2019-01-18 Alex OzdemirExtract DIMACS Printing (#2800) tree | commitdiff
2019-01-18 Andres NoetzliStrings: Introduce checkEntailContains() (#2809) tree | commitdiff
2019-01-18 Andres Noetzli Fix ABC build (#2808) tree | commitdiff
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805) tree | commitdiff
2019-01-16 Andrew ReynoldsFix constant contains ITOS rewrite (#2799) tree | commitdiff
2019-01-15 Andres NoetzliStrings: Add option to change loop process mode (#2794) tree | commitdiff
2019-01-15 Andrew Reynolds Fix unsound double abs rewrite rule for FP (#2792) tree | commitdiff
2019-01-15 Andrew Reynolds Only check disequal terms with sygus-rr-verify (#2793) 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-11 Aina NiemetzNew C++ API: Add unit tests for setInfo, setLogic,... tree | commitdiff
2019-01-10 Aina NiemetzNew C++ API: Get rid of mkConst functions (simplify... tree | commitdiff
2019-01-09 Andrew ReynoldsDo not rewrite 1-constructor sygus testers to true... tree | commitdiff
2019-01-09 Alex Ozdemir[BV Proofs] Option for proof format (#2777) tree | commitdiff
2019-01-09 Alex OzdemirClause proof printing (#2779) tree | commitdiff
next