git.libre-soc.org Git - cvc5.git/history - test/regress/CMakeLists.txt

[cvc5.git] / test / regress / CMakeLists.txt

2021-12-21	Andrew Reynolds	Support get-abduct-next (#7850)	blob \| commitdiff \| raw
2021-12-20	Andrew Reynolds	Allow SyGuS subsolver to be reused in incremental mode...	blob \| commitdiff \| raw \| diff to current
2021-12-17	Andres Noetzli	Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)	blob \| commitdiff \| raw \| diff to current
2021-12-16	Andrew Reynolds	Fix get-model when sort constructors are present (...	blob \| commitdiff \| raw \| diff to current
2021-12-16	Andrew Reynolds	Minor fix for print benchmark. (#7821)	blob \| commitdiff \| raw \| diff to current
2021-12-16	yoni206	int-to-bv: fail if one of the arguments has type real...	blob \| commitdiff \| raw \| diff to current
2021-12-16	mudathirmahgoub	Add regression bags-of-bags-subtypes.smt2 (#7814)	blob \| commitdiff \| raw \| diff to current
2021-12-14	mudathirmahgoub	Fix cvc5-projects issue 358 (#7804)	blob \| commitdiff \| raw \| diff to current
2021-12-14	Abdalrhman Mohamed	Add a random Sygus enumerator. (#7782)	blob \| commitdiff \| raw \| diff to current
2021-12-13	mudathirmahgoub	A more efficient implementation for bag.card operator...	blob \| commitdiff \| raw \| diff to current
2021-12-13	yoni206	Integrate new int-blaster (#7781)	blob \| commitdiff \| raw \| diff to current
2021-12-13	mudathirmahgoub	Fix cvc5-projects issues #358 and #375 (#7743)	blob \| commitdiff \| raw \| diff to current
2021-12-10	Abdalrhman Mohamed	Mute `define-fun` command generated for named terms...	blob \| commitdiff \| raw \| diff to current
2021-12-09	Andrew Reynolds	Consider polarity in relevance manager (#7768)	blob \| commitdiff \| raw \| diff to current
2021-12-08	Andrew Reynolds	Make several regressions faster (#7769)	blob \| commitdiff \| raw \| diff to current
2021-12-08	Andrew Reynolds	Fix type rule for datatype updater for parametric sorts...	blob \| commitdiff \| raw \| diff to current
2021-12-07	Andrew Reynolds	Allow sygus in incremental mode (#7756)	blob \| commitdiff \| raw \| diff to current
2021-12-07	Andrew Reynolds	Make data structures in relevance manager SAT-context...	blob \| commitdiff \| raw \| diff to current
2021-12-06	Andrew Reynolds	Add regressions for fixed projects issues (#7739)	blob \| commitdiff \| raw \| diff to current
2021-12-02	mudathirmahgoub	add bag.fold operator (#7718)	blob \| commitdiff \| raw \| diff to current
2021-12-02	Gereon Kremer	Add unit tests for api::Solver::setOption() (#7708)	blob \| commitdiff \| raw \| diff to current
2021-12-01	Andrew Reynolds	Remove spurious assertion in parser (#7713)	blob \| commitdiff \| raw \| diff to current
2021-11-30	Andrew Reynolds	Add rewrite for is_int pi (#7711)	blob \| commitdiff \| raw \| diff to current
2021-11-30	Andrew Reynolds	Proper check for first-class types in datatype subfield...	blob \| commitdiff \| raw \| diff to current
2021-11-24	Andrew Reynolds	Fix potential for cycles in trust substitutions (#7687)	blob \| commitdiff \| raw \| diff to current
2021-11-23	mudathirmahgoub	Add rewrite rule for bag.card operator using bag.map...	blob \| commitdiff \| raw \| diff to current
2021-11-22	Andrew Reynolds	Fix const RE test for internal regexp rv kind (#7678)	blob \| commitdiff \| raw \| diff to current
2021-11-17	Andres Noetzli	Fix binding of quoted symbols in `define-fun` (#7655)	blob \| commitdiff \| raw \| diff to current
2021-11-16	Haniel Barbosa	[proofs] Make sure --proof-check=... is no-op when...	blob \| commitdiff \| raw \| diff to current
2021-11-13	Andres Noetzli	Skip `str.code` inferences for sequence eqcs (#7644)	blob \| commitdiff \| raw \| diff to current
2021-11-11	Andrew Reynolds	Add lazy approach for handling lambdas in the HO extens...	blob \| commitdiff \| raw \| diff to current
2021-11-10	mudathirmahgoub	Fix soundness issue of missing premises for count bag...	blob \| commitdiff \| raw \| diff to current
2021-11-10	Andrew Reynolds	Fix parsing array constants (#7617)	blob \| commitdiff \| raw \| diff to current
2021-11-09	Andrew Reynolds	Only eliminate lambdas in higher-order elimination...	blob \| commitdiff \| raw \| diff to current
2021-11-08	mudathirmahgoub	expand bag.choose operator (#7481)	blob \| commitdiff \| raw \| diff to current
2021-11-06	Andrew Reynolds	Do not use extended rewrites on recursive function...	blob \| commitdiff \| raw \| diff to current
2021-11-06	Mathias Preiner	Disable regress2 test. (#7591)	blob \| commitdiff \| raw \| diff to current
2021-11-05	Andrew Reynolds	Fix exclusion criteria for codatatype model values...	blob \| commitdiff \| raw \| diff to current
2021-11-05	Haniel Barbosa	[proofs] Fix open sat proof (#7509)	blob \| commitdiff \| raw \| diff to current
2021-11-05	Andrew Reynolds	Eliminate a level of nesting of traversals in theory...	blob \| commitdiff \| raw \| diff to current
2021-11-05	Andres Noetzli	[FP] Do not assert that model has shared term (#7585)	blob \| commitdiff \| raw \| diff to current
2021-11-04	Andrew Reynolds	Add -o sygus-grammar to print auto-generated SyGuS...	blob \| commitdiff \| raw \| diff to current
2021-11-04	Andrew Reynolds	Improve defaults for sygus default grammars (#7553)	blob \| commitdiff \| raw \| diff to current
2021-11-04	Andrew Reynolds	Replace the old dump infrastructure (#7572)	blob \| commitdiff \| raw \| diff to current
2021-11-04	Gereon Kremer	Enable CDCAC solver for selected quantified logics...	blob \| commitdiff \| raw \| diff to current
2021-11-03	Andrew Reynolds	Formalize more string skolems (#7554)	blob \| commitdiff \| raw \| diff to current
2021-11-03	Andrew Reynolds	Fix preregistration for floating point theory (#7558)	blob \| commitdiff \| raw \| diff to current
2021-11-02	Andrew Reynolds	Make quant elimination robust to presence of other...	blob \| commitdiff \| raw \| diff to current
2021-11-01	Andrew Reynolds	Weaken assertion in CEGQI (#7548)	blob \| commitdiff \| raw \| diff to current
2021-11-01	Mathias Preiner	bv: Remove layered solver. (#7455)	blob \| commitdiff \| raw \| diff to current
2021-11-01	Andrew Reynolds	Fix upwards closure for relations (#7515)	blob \| commitdiff \| raw \| diff to current
2021-10-31	mudathirmahgoub	Fix soundess issue for bags with negative multiplicity...	blob \| commitdiff \| raw \| diff to current
2021-10-31	mudathirmahgoub	Remove assertSkeleton for bag elements during model...	blob \| commitdiff \| raw \| diff to current
2021-10-29	Gereon Kremer	Fix proof of nl lemma for a corner case (#7530)	blob \| commitdiff \| raw \| diff to current
2021-10-29	Andrew Reynolds	Fix model construction for higher order involving irrel...	blob \| commitdiff \| raw \| diff to current
2021-10-28	Gereon Kremer	Fix proof for xor in circuit propagator (#7525)	blob \| commitdiff \| raw \| diff to current
2021-10-28	Haniel Barbosa	[proofs] Fix assertion in EqProof conversion (#7522)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andrew Reynolds	Add missing API checks to getValue (#7475)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andres Noetzli	Require ITE branches to be first class types (#7508)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andrew Reynolds	Fix care graph computation for higher-order (#7474)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andrew Reynolds	Fix model unsoundness for relation join (#7511)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andrew Reynolds	Avoid non-terminating check with assumptions in strings...	blob \| commitdiff \| raw \| diff to current
2021-10-27	Andrew Reynolds	Deterministic variables for RE elim (#7489)	blob \| commitdiff \| raw \| diff to current
2021-10-27	Gereon Kremer	Make --version exit (#7506)	blob \| commitdiff \| raw \| diff to current
2021-10-26	Haniel Barbosa	[proofs] Fix singleton check in MACRO_RES post-processi...	blob \| commitdiff \| raw \| diff to current
2021-10-26	Haniel Barbosa	[proofs] Reset local var in SatProofManager since incre...	blob \| commitdiff \| raw \| diff to current
2021-10-26	Andrew Reynolds	Disable automatic symmetry in proofs of theory explanat...	blob \| commitdiff \| raw \| diff to current
2021-10-26	Haniel Barbosa	[proofs] Fix and simplify CHAIN_RESOLUTION checker...	blob \| commitdiff \| raw \| diff to current
2021-10-26	Andrew Reynolds	Add regressions for fixed issues (#7495)	blob \| commitdiff \| raw \| diff to current
2021-10-26	Andrew Reynolds	Disable sygus-inst when incremental (#7485)	blob \| commitdiff \| raw \| diff to current
2021-10-25	Andrew Reynolds	Add new method for enumerating unsat queries with SyGuS...	blob \| commitdiff \| raw \| diff to current
2021-10-25	Andrew Reynolds	Fix support for global declarations (#7480)	blob \| commitdiff \| raw \| diff to current
2021-10-25	mudathirmahgoub	Add inference for count map (#7264)	blob \| commitdiff \| raw \| diff to current
2021-10-24	Andrew Reynolds	Add new eager conflict detection in strings for integer...	blob \| commitdiff \| raw \| diff to current
2021-10-22	Haniel Barbosa	[proof] Fixing CHAIN_RESOLUTION checker (#7465)	blob \| commitdiff \| raw \| diff to current
2021-10-22	Gereon Kremer	Fix another double negation proof issue (#7468)	blob \| commitdiff \| raw \| diff to current
2021-10-22	Andrew Reynolds	Add more abduction regressions (#7461)	blob \| commitdiff \| raw \| diff to current
2021-10-22	Andrew Reynolds	Do not use global proxy variable attribute for strings...	blob \| commitdiff \| raw \| diff to current
2021-10-21	Gereon Kremer	Also fix case of negated ite (#7454)	blob \| commitdiff \| raw \| diff to current
2021-10-21	Gereon Kremer	Fix symmetric proof issue for ITE in circuit propagator...	blob \| commitdiff \| raw \| diff to current
2021-10-21	Haniel Barbosa	[proofs] Fix open proof in SAT solver due to cycles...	blob \| commitdiff \| raw \| diff to current
2021-10-21	Gereon Kremer	Add regression (#7447)	blob \| commitdiff \| raw \| diff to current
2021-10-21	Gereon Kremer	Fix incorrect proof from ITE in circuit propagator...	blob \| commitdiff \| raw \| diff to current
2021-10-21	Andres Noetzli	Enable and fix dump test (#7387)	blob \| commitdiff \| raw \| diff to current
2021-10-21	Gereon Kremer	Fix (#7437)	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Enable some previously failing regressions (#7434)	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Add regressions for fixed issues (#7421)	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Make SyGuS solver robust to non-closed enumerable sorts...	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Reimplement support for relational triggers (#7063)	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Do not make assumption about model for Boolean variable...	blob \| commitdiff \| raw \| diff to current
2021-10-20	Andrew Reynolds	Correctly parse uninterpreted constant values in get...	blob \| commitdiff \| raw \| diff to current
2021-10-19	Andrew Reynolds	Fix expected conclusion for EQ_RESOLVE when expanding...	blob \| commitdiff \| raw \| diff to current
2021-10-19	Andrew Reynolds	Support sequences of fixed finite cardinality (#7371)	blob \| commitdiff \| raw \| diff to current
2021-10-19	Andrew Reynolds	Fix issue related to sanity checking integer models...	blob \| commitdiff \| raw \| diff to current
2021-10-18	Andrew Reynolds	Add regression for fixed issue (#7395)	blob \| commitdiff \| raw \| diff to current
2021-10-18	Abdalrhman Mohamed	Move check for experimental arrays features to `theory_...	blob \| commitdiff \| raw \| diff to current
2021-10-15	Andrew Reynolds	Add more regressions for fixed issues (#7382)	blob \| commitdiff \| raw \| diff to current
2021-10-15	Andrew Reynolds	Fix issues related to proofs of lemmas with duplicate...	blob \| commitdiff \| raw \| diff to current
2021-10-14	Andrew Reynolds	Add regressions for fixed issues (#7369)	blob \| commitdiff \| raw \| diff to current
2021-10-14	Gereon Kremer	Improve ManagedStreams (#7367)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom