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

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
2019-03-15	Andrew Reynolds	Fix non-variable function head elimination in UF. ...	commit \| commitdiff \| tree
2019-03-14	Andrew Reynolds	Fix function term set for theory strings compute care...	commit \| commitdiff \| tree
2019-03-14	Aina Niemetz	Improve INSTALL instructions. (#2866)	commit \| commitdiff \| tree
2019-03-14	Andrew Reynolds	Use zero slope tangent planes for transcendental functions...	commit \| commitdiff \| tree
2019-03-14	Andrew Reynolds	Properly 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 Reynolds	Implement 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 Reynolds	Generalize sygus-rr-verify for fast enumerator (#2829)	commit \| commitdiff \| tree
2019-03-13	Andres Noetzli	Add statistics for proof gen./checking time, size ...	commit \| commitdiff \| tree
2019-03-13	Andrew Reynolds	Remove spurious data member. (#2857)	commit \| commitdiff \| tree
2019-03-13	Mathias Preiner	Fix public headers for make install. (#2856)	commit \| commitdiff \| tree
2019-03-12	Andrew Reynolds	Add 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 Ozdemir	ErProof class with LFSC output (#2812)	commit \| commitdiff \| tree
2019-02-27	Andres Noetzli	Use string stream for proofs instead of tmp files ...	commit \| commitdiff \| tree
2019-02-26	Andres Noetzli	ClangFormat: Disable DerivePointerAlignment (#2842)	commit \| commitdiff \| tree
2019-02-13	Aina Niemetz	New C++ API: Remove redundant declareFun function....	commit \| commitdiff \| tree
2019-02-13	Andres Noetzli	Rewrite simple regexp pattern to str.contains (#2827)	commit \| commitdiff \| tree
2019-02-11	Aina Niemetz	New C++ API: Unit tests for declare* functions. (#2831)	commit \| commitdiff \| tree
2019-02-04	Andres Noetzli	Add rewrite for contains + const strings replace (...	commit \| commitdiff \| tree
2019-02-02	Andres Noetzli	Fix corner case in stripConstantEndpoints (#2824)	commit \| commitdiff \| tree
2019-01-29	Aina Niemetz	New C++ API: Fix checks for mkTerm. (#2820)	commit \| commitdiff \| tree
2019-01-29	Andres Noetzli	Strings: Remove redundant replace rewrite (#2822)	commit \| commitdiff \| tree
2019-01-24	Alex Ozdemir	Extended DRAT signature to operational DRAT (#2815)	commit \| commitdiff \| tree
2019-01-23	Andres Noetzli	Avoid using ProofManager in non-proof CMS build (#2814)	commit \| commitdiff \| tree
2019-01-23	Andres Noetzli	Strings: 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 Niemetz	New README (markdown). (#2797)	commit \| commitdiff \| tree
2019-01-19	Andres Noetzli	Fix missing-override warning (#2811)	commit \| commitdiff \| tree
2019-01-18	Andres Noetzli	Fix ABC build (#2808)	commit \| commitdiff \| tree
2019-01-17	Andres Noetzli	Add option to print BV constants in binary (#2805)	commit \| commitdiff \| tree
2019-01-16	Alex Ozdemir	Bugfix: LFSC clause equality (#2801)	commit \| commitdiff \| tree
2019-01-16	Alex Ozdemir	Extended Resolution Signature (#2788)	commit \| commitdiff \| tree
2019-01-16	Andres Noetzli	CMake: Fix search for static libraries (#2798)	commit \| commitdiff \| tree
2019-01-15	Andres Noetzli	Strings: 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 Ozdemir	ClausalBitvectorProof (#2786)	commit \| commitdiff \| tree
2019-01-13	Alex Ozdemir	LFSC LRAT Output (#2787)	commit \| commitdiff \| tree
2019-01-12	Alex Ozdemir	LratInstruction inheritance (#2784)	commit \| commitdiff \| tree
2019-01-11	Alex Ozdemir	Fixed linking against drat2er, and use drat2er (#2785)	commit \| commitdiff \| tree
2019-01-11	Aina Niemetz	New C++ API: Add unit tests for setInfo, setLogic,...	commit \| commitdiff \| tree
2019-01-10	Aina Niemetz	New C++ API: Get rid of mkConst functions (simplify...	commit \| commitdiff \| tree
2019-01-09	Andrew Reynolds	Do not rewrite 1-constructor sygus testers to true...	commit \| commitdiff \| tree
2019-01-09	Alex Ozdemir	Clause proof printing (#2779)	commit \| commitdiff \| tree
2019-01-09	Alex Ozdemir	LFSC drat output (#2776)	commit \| commitdiff \| tree
2019-01-07	Aina Niemetz	New 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-04	Alex Ozdemir	[LRAT] A C++ data structure for LRAT. (#2737)	commit \| commitdiff \| tree
2019-01-04	Aina Niemetz	New C++ API: Add missing catch blocks for std::invalid_argum...	commit \| commitdiff \| tree
2019-01-03	Alex Ozdemir	[LRA proof] Recording & Printing LRA Proofs (#2758)	commit \| commitdiff \| tree
2019-01-03	Aina Niemetz	New C++ API: Add tests for mk-functions in solver object...	commit \| commitdiff \| tree
2018-12-19	Andrew Reynolds	Fix issues with REWRITE_DONE in floating point rewriter...	commit \| commitdiff \| tree
2018-12-18	Aina Niemetz	Remove noop. (#2763)	commit \| commitdiff \| tree
2018-12-17	Aina Niemetz	New C++ API: Add tests for term object. (#2755)	commit \| commitdiff \| tree
2018-12-17	Alex Ozdemir	DRAT Signature (#2757)	commit \| commitdiff \| tree
2018-12-15	Alex Ozdemir	[LRA Proof] Storage for LRA proofs (#2747)	commit \| commitdiff \| tree
2018-12-14	Aina Niemetz	New C++ API: Add tests for opterm object. (#2756)	commit \| commitdiff \| tree
2018-12-13	Aina Niemetz	New C++ API: Add tests for sort functions of solver...	commit \| commitdiff \| tree
2018-12-13	Andrew Reynolds	Remove spurious map (#2750)	commit \| commitdiff \| tree
next

RSS Atom