projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fixes for relational triggers (#2967)
2019-05-09 Andrew ReynoldsFixes for relational triggers (#2967)
 commit | commitdiff | tree
2019-05-02 Andrew ReynoldsSimple optimizations to core strings theory. (#2988)
 commit | commitdiff | tree
2019-05-01 Andrew Reynolds Use total versions of div/mod in re-elim-agg (#2986)
 commit | commitdiff | tree
2019-04-30 Andrew ReynoldsRemove stoi solve rewrite (#2985)
 commit | commitdiff | tree
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976)
 commit | commitdiff | tree
2019-04-29 Andrew ReynoldsOptimization for evaluation with unfolding (#2979)
 commit | commitdiff | tree
2019-04-26 Aina NiemetzNew C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar...
commit | commitdiff | tree
2019-04-23 Alex Ozdemir[BV] An option for SAT proof optimization (#2915)
 commit | commitdiff | tree
2019-04-23 Andrew ReynoldsRefactor normal forms in strings (#2897)
 commit | commitdiff | tree
2019-04-22 Aina NiemetzAdd CONTRIBUTING file. (#2968)
 commit | commitdiff | tree
2019-04-18 Andrew ReynoldsFail fast strategy for propagating instances (#2939)
 commit | commitdiff | tree
2019-04-18 Andrew Reynolds Less aggressive caching in equality engine when proofs...
commit | commitdiff | tree
2019-04-17 Andrew ReynoldsCache explanations in the equality engine (#2937)
 commit | commitdiff | tree
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959)
 commit | commitdiff | tree
2019-04-16 Andrew ReynoldsAdd interface for term enumeration (#2956)
 commit | commitdiff | tree
2019-04-16 Andrew ReynoldsStratify enumerative instantiation (#2954)
 commit | commitdiff | tree
2019-04-16 Andrew ReynoldsMinor simplifications to theory quantifiers (#2953)
 commit | commitdiff | tree
2019-04-15 Andres NoetzliInitial version of run scripts for SMT-COMP 2019 (...
commit | commitdiff | tree
2019-04-12 Haniel BarbosaReferring to prerelease 1.8 (#2943)
 commit | commitdiff | tree
2019-04-11 Andrew Reynolds Eliminate Boolean ITE within terms, fixes 2947 (#2949)
 commit | commitdiff | tree
2019-04-08 Haniel Barbosafix copyright year in configuration file (#2942)
 commit | commitdiff | tree
2019-04-05 Haniel Barbosaprerelease -> release (#2941)
 commit | commitdiff | tree
2019-04-05 Andrew ReynoldsFix another corner case of datatypes+PBE (#2938)
 commit | commitdiff | tree
2019-04-05 Haniel Barbosafix fp issue (#2940)
 commit | commitdiff | tree
2019-04-05 Alex OzdemirSatClauseSetHashFunction (#2916)
 commit | commitdiff | tree
2019-04-04 Haniel Barbosaadding sygus news (#2934)
 commit | commitdiff | tree
2019-04-04 Haniel BarbosaIgnoring FP benchmarks with "unsafe" sizes unless option...
commit | commitdiff | tree
2019-04-04 Haniel BarbosaUpdate release notes and lib version (#2933)
 commit | commitdiff | tree
2019-04-01 Andres NoetzliFP: Fix wrong model due to partial assignment (#2910)
 commit | commitdiff | tree
2019-04-01 Andres NoetzliFix RewriteITEBv to ensure rewrite to fixpoint (#2878)
 commit | commitdiff | tree
2019-04-01 Andrew ReynoldsModify strategy in sets+cardinality (#2909)
 commit | commitdiff | tree
2019-03-29 Andrew ReynoldsApply empty splits more aggressively in sets+cardinality...
commit | commitdiff | tree
2019-03-29 Haniel Barbosaremoving deprecated rewriting signature / example ...
commit | commitdiff | tree
2019-03-29 Andrew ReynoldsFix issues in cvc parser (#2901)
 commit | commitdiff | tree
2019-03-28 Haniel Barbosafix ex_bv.plf (#2905)
 commit | commitdiff | tree
2019-03-26 Andrew ReynoldsFix a few warnings (#2898)
 commit | commitdiff | tree
2019-03-26 Mathias Preinerget-authors: Exclude common source code patterns. ...
commit | commitdiff | tree
2019-03-24 Andrew Reynolds Split regular expression solver (#2891)
 commit | commitdiff | tree
2019-03-23 Andres NoetzliFix memory leak when using subsolvers (#2893)
 commit | commitdiff | tree
2019-03-23 Andres NoetzliStrip non-matching beginning from indexof operator...
commit | commitdiff | tree
2019-03-22 Andrew ReynoldsRevisit strings extended function decomposition (...
commit | commitdiff | tree
2019-03-22 Andrew ReynoldsMore fixes for PBE with datatypes (#2882)
 commit | commitdiff | tree
2019-03-22 Haniel Barbosafix help information on TPTP parsing (#2884)
 commit | commitdiff | tree
2019-03-22 Andres NoetzliFix stripConstantEndpoints in strings rewriter (#2883)
 commit | commitdiff | tree
2019-03-21 Andrew Reynolds Fix bad comparison in RE solver's addMembership (...
commit | commitdiff | tree
2019-03-21 Andrew ReynoldsRewrite selectors correctly applied to constructors...
commit | commitdiff | tree
2019-03-21 Andres NoetzliAdd more NEWS (#2859)
 commit | commitdiff | tree
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744)
 commit | commitdiff | tree
2019-03-19 Andrew ReynoldsFix fairness issue with fast sygus enumerator (#2873)
 commit | commitdiff | tree
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-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 functions...
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 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-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-11 Aina NiemetzNew C++ API: Unit tests for declare* functions. (#2831)
 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 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 selectors...
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 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 Alex OzdemirBugfix: LFSC clause equality (#2801)
 commit | commitdiff | tree
2019-01-16 Alex OzdemirExtended Resolution Signature (#2788)
 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 OzdemirClause proof printing (#2779)
 commit | commitdiff | tree
next