projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Shorten explanation for strings inference I_Norm_S (#3051)
2019-06-13 Andrew Reynolds Shorten explanation for strings inference I_Norm_S...
commit | commitdiff | tree
2019-06-12 Andres NoetzliDisable dumping regression for non-dumping builds ...
commit | commitdiff | tree
2019-06-12 Andres NoetzliFix compilation issue for Java bindings + CLN (#3045)
 commit | commitdiff | tree
2019-06-11 Andrew Reynolds Minor cleaning of conflict-based instantiation (#2966)
 commit | commitdiff | tree
2019-06-11 Andrew ReynoldsDo not require sygus constructors to be flattened ...
commit | commitdiff | tree
2019-06-11 Andrew Reynolds Fix spurious assertion in get-value (#3052)
 commit | commitdiff | tree
2019-06-10 Andrew ReynoldsOptimization for negative concatenation membership...
commit | commitdiff | tree
2019-06-10 Andrew ReynoldsOptimization for strings normalize disequalities (...
commit | commitdiff | tree
2019-06-05 Andres NoetzliPrevent letification from shadowing variables (#3042)
 commit | commitdiff | tree
2019-06-05 Andres NoetzliAdd support for SWIG 4 (#3041)
 commit | commitdiff | tree
2019-06-04 Andres NoetzliEnable proof checking for QF_LRA benchmarks (#2928)
 commit | commitdiff | tree
2019-06-04 Andres NoetzliAdd check that result matches benchmark status (#3028)
 commit | commitdiff | tree
2019-06-03 Andres Noetzli[SMT-COMP] No unconstrained simp for QF_LIA UC (#3039)
 commit | commitdiff | tree
2019-06-03 Andres Noetzli[SMT-COMP] Increase sequential portfolio times (#3038)
 commit | commitdiff | tree
2019-06-03 Andres Noetzli[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV ...
commit | commitdiff | tree
2019-06-03 Andres NoetzliEnable SymFPU assertions in production (#3036)
 commit | commitdiff | tree
2019-06-03 Andres Noetzli[SMT-COMP 2019] Update run script for unsat cores ...
commit | commitdiff | tree
2019-06-01 Aina NiemetzUpdate QF_BV options for SMT-COMP 2019. (#3033)
 commit | commitdiff | tree
2019-06-01 Andrew ReynoldsFix rewriter for regular expression consume (#3029)
 commit | commitdiff | tree
2019-05-30 Andres NoetzliQuote symbol when printing empty symbol name (#3025)
 commit | commitdiff | tree
2019-05-27 Andres NoetzliAvoid substituting Boolean term variables (#3022)
 commit | commitdiff | tree
2019-05-18 Andres NoetzliSupport for incremental bit-blasting with CaDiCaL ...
commit | commitdiff | tree
2019-05-18 Andres NoetzliFix BV ITE rewrite (#3004)
 commit | commitdiff | tree
2019-05-15 Aina Niemetz BV: Do not enable abstraction when eager bit-blasting...
commit | commitdiff | tree
2019-05-15 Andrew ReynoldsFix printing of bvurem (#2963)
 commit | commitdiff | tree
2019-05-10 Andrew ReynoldsDisable relational triggers (#2994)
 commit | commitdiff | tree
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 ...
https://github.com/CVC4/LFSC/pull/14).
 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
next