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

2022-03-09	Andrew Reynolds	Add REGEXP_ALL kind to API (#8264)	commit \| commitdiff \| tree
2022-03-09	Andrew Reynolds	Add regression for fixed issue 6700 (#8265)	commit \| commitdiff \| tree
2022-03-09	Andrew Reynolds	Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)	commit \| commitdiff \| tree
2022-03-08	Andrew Reynolds	Do not expand APPLY_SELECTOR (#8174)	commit \| commitdiff \| tree
2022-03-08	Andrew Reynolds	Guard another case of non-termination in quantifiers...	commit \| commitdiff \| tree
2022-03-08	Andrew Reynolds	Fixes and additions to LFSC signature (#8205)	commit \| commitdiff \| tree
2022-03-08	Andrew Reynolds	Eliminate shadowing in the quantifiers rewriter (#8244)	commit \| commitdiff \| tree
2022-03-08	Andrew Reynolds	Add unit for fixed project issue (#8253)	commit \| commitdiff \| tree
2022-03-07	Andrew Reynolds	Proper error message for non-first-class sets (#8245)	commit \| commitdiff \| tree
2022-03-05	Andrew Reynolds	Unit tests for fixed projects issues (#8229)	commit \| commitdiff \| tree
2022-03-05	Andrew Reynolds	Make seq.unit robust wrt subtyping (#8209)	commit \| commitdiff \| tree
2022-03-05	Andrew Reynolds	Enable NL tangent planes by default (#8233)	commit \| commitdiff \| tree
2022-03-04	Andrew Reynolds	Fix rewrite rule synthesis for 0-ary operators (#8221)	commit \| commitdiff \| tree
2022-03-04	Andrew Reynolds	Logic exception when using solution filtering for non...	commit \| commitdiff \| tree
2022-03-04	Andrew Reynolds	Add regressions for fixed projects issues (#8228)	commit \| commitdiff \| tree
2022-03-04	Andrew Reynolds	Add support for get learned literals in the API (#8099)	commit \| commitdiff \| tree
2022-03-03	Andrew Reynolds	Fix datatype declaration printing in LFSC printer ...	commit \| commitdiff \| tree
2022-03-03	Andrew Reynolds	Generalize LFSC string signature to sequences (#8220)	commit \| commitdiff \| tree
2022-03-03	Andrew Reynolds	Throw logic exception if a transcendental function...	commit \| commitdiff \| tree
2022-03-03	Andrew Reynolds	Add regression for fixed issue (#8213)	commit \| commitdiff \| tree
2022-03-03	Andrew Reynolds	Improve error for higher-order logic (#8207)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Fix issue with dropping non-reduced sine terms (#8211)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Fix models involving cardinality of sets of finite...	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Always purify universe from set minus (#8201)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Eliminate CDHashMap::insertAtContextLevelZero (#8173)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Fix incorrect assertion in prop engine proofs (#8204)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Clean usage of options in regressions (#8190)	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Improve error message when not using strings-exp (...	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Add utility to access how to print floating point ...	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Make blockModelValues robust to non-closed enumerable...	commit \| commitdiff \| tree
2022-03-02	Andrew Reynolds	Add regressions for fixed issues (#8202)	commit \| commitdiff \| tree
2022-03-01	Andrew Reynolds	Fix issue involving dropped purification lemmas for...	commit \| commitdiff \| tree
2022-03-01	Andrew Reynolds	Do not use sygus evaluation functions in sygus-inst...	commit \| commitdiff \| tree
2022-03-01	Andrew Reynolds	Disable regression (#8191)	commit \| commitdiff \| tree
2022-03-01	Andrew Reynolds	Fix lambda lifting + proofs (#8152)	commit \| commitdiff \| tree
2022-02-28	Andrew Reynolds	Fix special casing for PI in model value (#8189)	commit \| commitdiff \| tree
2022-02-28	Andrew Reynolds	Preserve model values for exact sine points (#8188)	commit \| commitdiff \| tree
2022-02-28	Andrew Reynolds	Track names for witness terms in model (#8184)	commit \| commitdiff \| tree
2022-02-28	Andrew Reynolds	Add two reduction schemas for sin terms (#8171)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Consider PI to be a model value (#8176)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Syntax fixes for LFSC signature (#8172)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Fix non-termination in quantifiers rewriter (#8165)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Simplify and fix how purified terms are managed in...	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Fix dropped bounds on PI (#8164)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Remove approximations infrastructure from model (#8166)	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Remove spurious assertion involving constants for arguments...	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Make quantifiers terminate if it detects a (duplicate...	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Add regression for fixed transcendental regression...	commit \| commitdiff \| tree
2022-02-25	Andrew Reynolds	Consolidate extended rewrite preprocessing modes (...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Ensure variables are constrained in model when equal...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make model builder robust to multiple value-like terms...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make sine solver sound with respect to region boundaries...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Check for free variables in several SolverEngine calls...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make uninterpreted sort owner non-static (#8144)	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Add regression for some fixed array issues (#8145)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Allow elimination of unevaluated terms by default ...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Further relax what is considered a value in the model...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Do not insist that entries for UF are constant in FMF...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Eliminate match from LFSC proofs (#8090)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Option exception when incompatible with proofs (#8064)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Properly sanatize user names in LFSC (#8080)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Fix issue in datatypes care graph computation involving...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Support some cases of isConst for regular expressions...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Remove refineConflicts option (#8129)	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Change inference scheme in transcendentals to rewrite...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Relax what is generated in the model from NL (#8113)	commit \| commitdiff \| tree
2022-02-21	Andrew Reynolds	Fixes and additions for LFSC signatures (#8120)	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Add unit test for fixed issue with get-difficulty ...	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Throw option exceptions when combining input conversion...	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Add well formed term check to solver engine (#8056)	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Make spurious assertion into warning (#8051)	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Introduce skolem function to make transcendental function...	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Missing ids for arith conflicts (#8108)	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Remove some irrelevant node kinds from the model (...	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	[proofs] Consolidate multiple substitutions to single...	commit \| commitdiff \| tree
2022-02-16	Andrew Reynolds	[proofs] Make cache (optionally) persistent in lazy...	commit \| commitdiff \| tree
2022-02-16	Andrew Reynolds	Only consider relevant terms in the array-inspired...	commit \| commitdiff \| tree
2022-02-11	Andrew Reynolds	Ensure proofs are fully disabled when incompatible...	commit \| commitdiff \| tree
2022-02-11	Andrew Reynolds	Fix for lambda-to-array constant conversion for unused...	commit \| commitdiff \| tree
2022-02-10	Andrew Reynolds	Add assertion to require inference ids (#8091)	commit \| commitdiff \| tree
2022-02-10	Andrew Reynolds	Use witness terms to represent values for large strings...	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Simplify formalism of introduced arithmetic skolems...	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Distinguish proof mode from unsat core mode (#8062)	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Fix LFSC node conversion for non-shared selectors ...	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Always produce assertions (#8041)	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Make witness form visited ref counted (#8081)	commit \| commitdiff \| tree
2022-02-07	Andrew Reynolds	Generalize LFSC concat unify for splitting constants...	commit \| commitdiff \| tree
2022-02-07	Andrew Reynolds	Fix unsoundness in IAND solver (#8053)	commit \| commitdiff \| tree
2022-02-07	Andrew Reynolds	Fix indexof_re reduction (#8065)	commit \| commitdiff \| tree
2022-02-05	Andrew Reynolds	Fix another rewrite involving iand (#8054)	commit \| commitdiff \| tree
2022-02-04	Andrew Reynolds	Standardizing notifications for setting options in...	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Simplify handling of disequalities in strings (#8047)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Eliminate even more static uses of rewrite (#8044)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Test proof granularity theory-rewrite by default (...	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Eliminate more static uses of rewrite (#8040)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Add miscellaneous missing theory definitions for LFSC...	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix rewrite for eliminating constant factors of PI...	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix invalid rewrite involving iand (#8026)	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix printing of re.loop as an operator in LFSC (#8029)	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Make LFSC side condition for concat unify robust to...	commit \| commitdiff \| tree
next

RSS Atom