git.libre-soc.org Git - cvc5.git/search

2019-07-19	Andrew Reynolds	Fix case of unfolding negative membership in reg exp...	commit \| commitdiff \| tree
2019-07-18	Andrew Reynolds	Basic rewrites for tolower/toupper (#3095)	commit \| commitdiff \| tree
2019-07-17	Andrew Reynolds	Minor clean in strings. (#3093)	commit \| commitdiff \| tree
2019-07-16	Andrew Reynolds	Add support for str.tolower and str.toupper (#3092)	commit \| commitdiff \| tree
2019-07-15	Andrew Reynolds	Add string rewrite to distribute character stars over...	commit \| commitdiff \| tree
2019-07-08	Andrew Reynolds	Towards refactoring relations (#3078)	commit \| commitdiff \| tree
2019-07-06	Andrew Reynolds	Refactor strings to use an inference manager object...	commit \| commitdiff \| tree
2019-07-02	Andrew Reynolds	Use unique_ptr for UF modules (#3080)	commit \| commitdiff \| tree
2019-07-02	Alex Ozdemir	Optimize DRAT optimization: clause matching (#3074)	commit \| commitdiff \| tree
2019-07-01	Andrew Reynolds	Refactoring of relevance vector in quantifiers (#3070)	commit \| commitdiff \| tree
2019-07-01	Andrew Reynolds	Support sygus version 2 format (#3066)	commit \| commitdiff \| tree
2019-07-01	Andrew Reynolds	Split higher-order UF solver (#2890)	commit \| commitdiff \| tree
2019-07-01	Andrew Reynolds	Add higher-order elimination preprocessing pass (#2865)	commit \| commitdiff \| tree
2019-06-27	Andrew Reynolds	Variable elimination rewrite for quantified strings...	commit \| commitdiff \| tree
2019-06-24	Andrew Reynolds	Stratify unfolding of regular expressions based on...	commit \| commitdiff \| tree
2019-06-22	Andres Noetzli	Add floating-point support in the Java API (#3063)	commit \| commitdiff \| tree
2019-06-21	Andres Noetzli	Fix and simplify handling of --force-logic (#3062)	commit \| commitdiff \| tree
2019-06-21	Andres Noetzli	Use TMPDIR environment variable for temp files (#2849)	commit \| commitdiff \| tree
2019-06-18	Andres Noetzli	Strings: More aggressive skolem normalization (#2761)	commit \| commitdiff \| tree
2019-06-15	Andres Noetzli	Use Ubuntu 16.04 on Travis (#3059)	commit \| commitdiff \| tree
2019-06-14	Andres Noetzli	Add lemma for the range of values of str.indexof (...	commit \| commitdiff \| tree
2019-06-13	Andrew Reynolds	Shorten explanation for strings inference I_Norm_S...	commit \| commitdiff \| tree
2019-06-12	Andres Noetzli	Disable dumping regression for non-dumping builds ...	commit \| commitdiff \| tree
2019-06-12	Andres Noetzli	Fix 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 Reynolds	Do 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 Reynolds	Optimization for negative concatenation membership...	commit \| commitdiff \| tree
2019-06-10	Andrew Reynolds	Optimization for strings normalize disequalities (...	commit \| commitdiff \| tree
2019-06-05	Andres Noetzli	Prevent letification from shadowing variables (#3042)	commit \| commitdiff \| tree
2019-06-05	Andres Noetzli	Add support for SWIG 4 (#3041)	commit \| commitdiff \| tree
2019-06-04	Andres Noetzli	Enable proof checking for QF_LRA benchmarks (#2928)	commit \| commitdiff \| tree
2019-06-04	Andres Noetzli	Add 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 Noetzli	Enable 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 Niemetz	Update QF_BV options for SMT-COMP 2019. (#3033)	commit \| commitdiff \| tree
2019-06-01	Andrew Reynolds	Fix rewriter for regular expression consume (#3029)	commit \| commitdiff \| tree
2019-05-30	Andres Noetzli	Quote symbol when printing empty symbol name (#3025)	commit \| commitdiff \| tree
2019-05-27	Andres Noetzli	Avoid substituting Boolean term variables (#3022)	commit \| commitdiff \| tree
2019-05-18	Andres Noetzli	Support for incremental bit-blasting with CaDiCaL ...	commit \| commitdiff \| tree
2019-05-18	Andres Noetzli	Fix 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 Reynolds	Fix printing of bvurem (#2963)	commit \| commitdiff \| tree
2019-05-10	Andrew Reynolds	Disable relational triggers (#2994)	commit \| commitdiff \| tree
2019-05-09	Andrew Reynolds	Fixes for relational triggers (#2967)	commit \| commitdiff \| tree
2019-05-02	Andrew Reynolds	Simple 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 Reynolds	Remove stoi solve rewrite (#2985)	commit \| commitdiff \| tree
2019-04-30	Andrew Reynolds	Eliminate APPLY kind (#2976)	commit \| commitdiff \| tree
2019-04-29	Andrew Reynolds	Optimization for evaluation with unfolding (#2979)	commit \| commitdiff \| tree
2019-04-26	Aina Niemetz	New 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 Reynolds	Refactor normal forms in strings (#2897)	commit \| commitdiff \| tree
2019-04-22	Aina Niemetz	Add CONTRIBUTING file. (#2968)	commit \| commitdiff \| tree
2019-04-18	Andrew Reynolds	Fail 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 Reynolds	Cache explanations in the equality engine (#2937)	commit \| commitdiff \| tree
2019-04-17	Andrew Reynolds	More use of isClosure (#2959)	commit \| commitdiff \| tree
2019-04-16	Andrew Reynolds	Add interface for term enumeration (#2956)	commit \| commitdiff \| tree
2019-04-16	Andrew Reynolds	Stratify enumerative instantiation (#2954)	commit \| commitdiff \| tree
2019-04-16	Andrew Reynolds	Minor simplifications to theory quantifiers (#2953)	commit \| commitdiff \| tree
2019-04-15	Andres Noetzli	Initial version of run scripts for SMT-COMP 2019 (...	commit \| commitdiff \| tree
2019-04-12	Haniel Barbosa	Referring 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 Barbosa	fix copyright year in configuration file (#2942)	commit \| commitdiff \| tree
2019-04-05	Haniel Barbosa	prerelease -> release (#2941)	commit \| commitdiff \| tree
2019-04-05	Andrew Reynolds	Fix another corner case of datatypes+PBE (#2938)	commit \| commitdiff \| tree
2019-04-05	Haniel Barbosa	fix fp issue (#2940)	commit \| commitdiff \| tree
2019-04-05	Alex Ozdemir	SatClauseSetHashFunction (#2916)	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	adding sygus news (#2934)	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	Ignoring FP benchmarks with "unsafe" sizes unless option...	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	Update release notes and lib version (#2933)	commit \| commitdiff \| tree
2019-04-01	Andres Noetzli	FP: Fix wrong model due to partial assignment (#2910)	commit \| commitdiff \| tree
2019-04-01	Andres Noetzli	Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)	commit \| commitdiff \| tree
2019-04-01	Andrew Reynolds	Modify strategy in sets+cardinality (#2909)	commit \| commitdiff \| tree
2019-03-29	Andrew Reynolds	Apply empty splits more aggressively in sets+cardinality...	commit \| commitdiff \| tree
2019-03-29	Haniel Barbosa	removing deprecated rewriting signature / example ...	commit \| commitdiff \| tree
2019-03-29	Andrew Reynolds	Fix issues in cvc parser (#2901)	commit \| commitdiff \| tree
2019-03-28	Haniel Barbosa	fix ex_bv.plf (#2905)	commit \| commitdiff \| tree
2019-03-26	Andrew Reynolds	Fix a few warnings (#2898)	commit \| commitdiff \| tree
2019-03-26	Mathias Preiner	get-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 Noetzli	Fix memory leak when using subsolvers (#2893)	commit \| commitdiff \| tree
2019-03-23	Andres Noetzli	Strip non-matching beginning from indexof operator...	commit \| commitdiff \| tree
2019-03-22	Andrew Reynolds	Revisit strings extended function decomposition (...	commit \| commitdiff \| tree
2019-03-22	Andrew Reynolds	More fixes for PBE with datatypes (#2882)	commit \| commitdiff \| tree
2019-03-22	Haniel Barbosa	fix help information on TPTP parsing (#2884)	commit \| commitdiff \| tree
2019-03-22	Andres Noetzli	Fix 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 Reynolds	Rewrite selectors correctly applied to constructors...	commit \| commitdiff \| tree
2019-03-21	Andres Noetzli	Add more NEWS (#2859)	commit \| commitdiff \| tree
2019-03-20	Andrew Reynolds	Sygus abduction feature (#2744)	commit \| commitdiff \| tree
2019-03-19	Andrew Reynolds	Fix fairness issue with fast sygus enumerator (#2873)	commit \| commitdiff \| tree
2019-03-18	Aina Niemetz	BitVector: Allow base 10 in constructor. (#2870)	commit \| commitdiff \| tree
2019-03-16	Andres Noetzli	Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ...	commit \| commitdiff \| tree
2019-03-15	Haniel Barbosa	New beta-reduction for HOL solving (#2869)	commit \| commitdiff \| tree
2019-03-15	Haniel Barbosa	Adding capture avoiding substitution (#2867)	commit \| commitdiff \| tree
next

RSS Atom