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

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
2018-12-13	Aina Niemetz	Fix compiler warnings. (#2748)	commit \| commitdiff \| tree
2018-12-12	Andres Noetzli	API: Add simple empty/sigma regexp unit tests (#2746)	commit \| commitdiff \| tree
2018-12-12	Alex Ozdemir	[LRA proof] More complete LRA example proofs. (#2722)	commit \| commitdiff \| tree
2018-12-12	Alex Ozdemir	[LRAT] signature robust against duplicate literals...	commit \| commitdiff \| tree
2018-12-11	Andrew Reynolds	Remove alternate versions of mbqi (#2742)	commit \| commitdiff \| tree
2018-12-11	Alex Ozdemir	LRAT signature (#2731)	commit \| commitdiff \| tree
2018-12-07	Alex Ozdemir	Arith Constraint Proof Loggin (#2732)	commit \| commitdiff \| tree
2018-12-07	Alex Ozdemir	Enable BV proofs when using an eager bitblaster (#2733)	commit \| commitdiff \| tree
2018-12-06	Andrew Reynolds	Take into account minimality and types for cached...	commit \| commitdiff \| tree
2018-12-04	Andrew Reynolds	Apply extended rewriting on PBE static symmetry breaking...	commit \| commitdiff \| tree
2018-12-03	Alex Ozdemir	Bit vector proof superclass (#2599)	commit \| commitdiff \| tree
2018-12-02	Andrew Reynolds	Optimizations for PBE strings (#2728)	commit \| commitdiff \| tree
2018-11-29	Andrew Reynolds	Infrastructure for sygus side conditions (#2729)	commit \| commitdiff \| tree
2018-11-29	Andrew Reynolds	Combine sygus stream with PBE (#2726)	commit \| commitdiff \| tree
2018-11-28	Andrew Reynolds	Improve interface for sygus grammar cons (#2727)	commit \| commitdiff \| tree
2018-11-28	Andrew Reynolds	Information gain heuristic for PBE (#2719)	commit \| commitdiff \| tree
2018-11-28	Andrew Reynolds	Optimize re-elim for re.allchar components (#2725)	commit \| commitdiff \| tree
2018-11-28	Andres Noetzli	Improve skolem caching by normalizing skolem args ...	commit \| commitdiff \| tree
2018-11-28	Andrew Reynolds	Generalize sygus stream solution filtering to logical...	commit \| commitdiff \| tree
2018-11-28	Andrew Reynolds	Improve cegqi engine trace. (#2714)	commit \| commitdiff \| tree
2018-11-27	Andrew Reynolds	Lazy model construction in TheoryEngine (#2633)	commit \| commitdiff \| tree
2018-11-27	Alex Ozdemir	LRA proof signature fixes and a first proof for linear...	commit \| commitdiff \| tree
2018-11-22	Andres Noetzli	Move ss-combine rewrite to extended rewriter (#2703)	commit \| commitdiff \| tree
2018-11-22	Andres Noetzli	Add rewrite for (str.substr s x y) --> "" (#2695)	commit \| commitdiff \| tree
2018-11-21	Andrew Reynolds	Cache evaluations for PBE (#2699)	commit \| commitdiff \| tree
2018-11-21	Andrew Reynolds	Support string replace all (#2704)	commit \| commitdiff \| tree
2018-11-21	Andrew Reynolds	Fix type enumerator for FP (#2717)	commit \| commitdiff \| tree
2018-11-20	Andrew Reynolds	Clausify context-dependent simplifications in ext...	commit \| commitdiff \| tree
2018-11-19	Andrew Reynolds	Fix E-matching for case where candidate generator is...	commit \| commitdiff \| tree
2018-11-15	Andrew Reynolds	Expand definitions prior to model core computation...	commit \| commitdiff \| tree
next

RSS Atom