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

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

2020-03-11	Andres Noetzli	Set assertion in `CnfStream::ensureLiteral()` (#3927)	blob \| commitdiff \| raw
2020-03-11	Andrew Reynolds	Fix real to int for parameterized kinds (#4016)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Fix sort inference for top-level Boolean variables...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Aina Niemetz	Fix issue with reset-assertions. (#3988)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Fix assertion failure in sort inference for Boolean...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Do not set values for non-linear mult terms in collectM...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Fix real as int for incremental (#3979)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Do not traverse quantifiers in nl ext purify (#3982)	blob \| commitdiff \| raw \| diff to current
2020-03-10	makaimann	Enhancement: make the bool-to-bv pass more robust and...	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Ensure standard miniscoping is applied before aggressiv...	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andrew Reynolds	Fix type issue in arith rewrite equality (#3972)	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andres Noetzli	Make registration of unit clauses more robust (#3965)	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andrew Reynolds	Rewrite again full for DIV rewrite (#3945)	blob \| commitdiff \| raw \| diff to current
2020-03-08	Ying Sheng	Explicit end marker for models printed in the CVC langu...	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andrew Reynolds	Support default sygus grammar construction for sets...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andrew Reynolds	Fix issues with real to int (#3918)	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andres Noetzli	Add support for str.from_code (#3829)	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andrew Reynolds	Fix assertion related to assignability in the model...	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andrew Reynolds	Replace conditional rewrite pass in quantifiers with...	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Fix large models for strings (#3835)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Add support for is_digit and regular expression differe...	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Disable regression that times out on debug (#3833)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Use side effect utility for non-linear lemmas (#3780)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Basic support for regular expression complement (#3437)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Use default consts when not using any const during...	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Fix node arity issue in reduction of int2bv (#3777)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Support for witnessing choice in models (#3781)	blob \| commitdiff \| raw \| diff to current
2020-02-25	yoni206	bv_to_int preprocessing pass	blob \| commitdiff \| raw \| diff to current
2020-02-24	Andres Noetzli	Make lambda rewriter more robust (#3806)	blob \| commitdiff \| raw \| diff to current
2020-02-22	Alex Ozdemir	Switch to th_lira.plf (#3741)	blob \| commitdiff \| raw \| diff to current
2020-02-21	Andrew Reynolds	Simple changes towards unicode string standard (#3791)	blob \| commitdiff \| raw \| diff to current
2020-02-19	Andrew Reynolds	Delay enumerative instantiation if theory engine does...	blob \| commitdiff \| raw \| diff to current
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod...	blob \| commitdiff \| raw \| diff to current
2020-02-16	Andrew Reynolds	Disable regression (#3761)	blob \| commitdiff \| raw \| diff to current
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	blob \| commitdiff \| raw \| diff to current
2020-02-12	Andrew Reynolds	Ensure ext rewrites for associative ops dont throw...	blob \| commitdiff \| raw \| diff to current
2020-02-11	Andrew Reynolds	Fix term simplification based on entailment in quantifi...	blob \| commitdiff \| raw \| diff to current
2020-02-08	Andres Noetzli	Make "unknown" non-critical for unsat cores check ...	blob \| commitdiff \| raw \| diff to current
2020-02-07	mudathirmahgoub	Univeset Cardinality constraints for infinite types...	blob \| commitdiff \| raw \| diff to current
2020-02-07	Andrew Reynolds	Refactor check-model handling in SmtEngine (#3723)	blob \| commitdiff \| raw \| diff to current
2020-02-07	Andrew Reynolds	Fix exact sqrt (#3721)	blob \| commitdiff \| raw \| diff to current
2020-02-04	Alex Ozdemir	Regression tests for arithmetic proofs. (#3701)	blob \| commitdiff \| raw \| diff to current
2020-02-03	mudathirmahgoub	Fix cardinality of uninterpreted types when univset...	blob \| commitdiff \| raw \| diff to current
2020-02-03	Andrew Reynolds	Split on model values when repaired model from non...	blob \| commitdiff \| raw \| diff to current
2020-02-03	Andrew Reynolds	Fix invariant template inference for trivially infeasib...	blob \| commitdiff \| raw \| diff to current
2020-02-03	Andrew Reynolds	Fix corner case of empty domains in bounded fmf (#3690)	blob \| commitdiff \| raw \| diff to current
2020-02-03	Andrew Reynolds	Example inference utility (#3670)	blob \| commitdiff \| raw \| diff to current
2020-01-31	Andrew Reynolds	Refactor relevance vectors for asserted quantifiers...	blob \| commitdiff \| raw \| diff to current
2020-01-31	Andres Noetzli	Fix arithmetic rewriter for exponential (#3688)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Fix rep set increment for empty domains (#3682)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Make eq chain an aggressive rewrite in extended rewrite...	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Eliminate spurious postprocessing step for single invoc...	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Ensure literals in FMF decision strategies are in the...	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Weaken assertion for models with approximations (#3667)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Do not debug check model for models with approximations...	blob \| commitdiff \| raw \| diff to current
2020-01-29	Andrew Reynolds	Fix isLeq function in String utility (#3659)	blob \| commitdiff \| raw \| diff to current
2020-01-28	Andrew Reynolds	Do not insist on bound values being constant in arithme...	blob \| commitdiff \| raw \| diff to current
2020-01-28	Andrew Reynolds	Avoid PLUS with one child for bv2nat elimination (...	blob \| commitdiff \| raw \| diff to current
2020-01-23	Andrew Reynolds	Fix trivial solve method for single invocation (#3650)	blob \| commitdiff \| raw \| diff to current
2020-01-22	Andrew Reynolds	Fix subtyping for instantiations where internal represe...	blob \| commitdiff \| raw \| diff to current
2020-01-22	Andrew Reynolds	Fix single invocation partition for non-function non...	blob \| commitdiff \| raw \| diff to current
2020-01-22	Andrew Reynolds	Fix check for subtypes in sygus PBE (#3640)	blob \| commitdiff \| raw \| diff to current
2020-01-22	Andrew Reynolds	Fix parameteric sorts involving Booleans in sygus defau...	blob \| commitdiff \| raw \| diff to current
2020-01-14	Andrew Reynolds	Generalize example-based sym breaking to conjectures...	blob \| commitdiff \| raw \| diff to current
2020-01-10	Andrew Reynolds	Fix side condition check in sygus core connective ...	blob \| commitdiff \| raw \| diff to current
2020-01-10	Andres Noetzli	Fix printing of models of uninterpreted sorts (#3597)	blob \| commitdiff \| raw \| diff to current
2020-01-10	Andrew Reynolds	Track trivial cases in transition inference (#3598)	blob \| commitdiff \| raw \| diff to current
2020-01-08	Andrew Reynolds	Fix backtracking issue in sygus fast enumerator (#3593)	blob \| commitdiff \| raw \| diff to current
2020-01-08	mudathirmahgoub	Universe set cardinality for finite types with finite...	blob \| commitdiff \| raw \| diff to current
2020-01-07	Andrew Reynolds	Update any-constant and normalization policies for...	blob \| commitdiff \| raw \| diff to current
2020-01-04	Andrew Reynolds	Fix finiteness check for bounded fmf (#3589)	blob \| commitdiff \| raw \| diff to current
2019-12-31	Alex Ozdemir	[proof] ITE translation fix (#3484)	blob \| commitdiff \| raw \| diff to current
2019-12-23	Andrew Reynolds	Initial support for string reverse (#3581)	blob \| commitdiff \| raw \| diff to current
2019-12-18	Andrew Reynolds	Increment Taylor degree for tangent and secant plane...	blob \| commitdiff \| raw \| diff to current
2019-12-18	Andres Noetzli	Avoid calling rewriter from type checker (#3548)	blob \| commitdiff \| raw \| diff to current
2019-12-17	Andrew Reynolds	Fix spurious parse error for rational real array consta...	blob \| commitdiff \| raw \| diff to current
2019-12-16	Ying Sheng	Support ackermannization on uninterpreted sorts in...	blob \| commitdiff \| raw \| diff to current
2019-12-13	Andrew Reynolds	Add support for set comprehension (#3312)	blob \| commitdiff \| raw \| diff to current
2019-12-12	Andrew Reynolds	Make CEGIS sampling robust to non-vanilla CEGIS (#3559)	blob \| commitdiff \| raw \| diff to current
2019-12-12	Haniel Barbosa	Fix Unif+PI algorithm with symbolic unfolding (#3558)	blob \| commitdiff \| raw \| diff to current
2019-12-12	Andrew Reynolds	Fixes for regressions (#3557)	blob \| commitdiff \| raw \| diff to current
2019-12-12	Andrew Reynolds	Fix CEGIS refinement for recursive functions evaluation...	blob \| commitdiff \| raw \| diff to current
2019-12-11	Andrew Reynolds	Do not substitute beneath arithmetic terms in the non...	blob \| commitdiff \| raw \| diff to current
2019-12-09	Andrew Reynolds	Fix case of uninterpreted constant instantiation in...	blob \| commitdiff \| raw \| diff to current
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	blob \| commitdiff \| raw \| diff to current
2019-12-05	Andrew Reynolds	Make nonlinear solver intercept model assignments from...	blob \| commitdiff \| raw \| diff to current
2019-12-05	Andres Noetzli	Bi-directional unrolling of R* regular expressions...	blob \| commitdiff \| raw \| diff to current
2019-12-05	Andrew Reynolds	Fix the subtyping relation for functions (#3494)	blob \| commitdiff \| raw \| diff to current
2019-12-04	Andrew Reynolds	New grammar construction modes for SyGuS (#3486)	blob \| commitdiff \| raw \| diff to current
2019-12-04	Andrew Reynolds	Fix single invocation solution construction for multipl...	blob \| commitdiff \| raw \| diff to current
2019-12-02	Andres Noetzli	[SMT2 Printer] Quote symbols starting with digit (...	blob \| commitdiff \| raw \| diff to current
2019-12-02	Andrew Reynolds	Update ownership policy for dynamic quantifiers splitt...	blob \| commitdiff \| raw \| diff to current
2019-12-02	Andrew Reynolds	Fix case of higher-order + sygus inference (#3509)	blob \| commitdiff \| raw \| diff to current
2019-12-02	Andrew Reynolds	Ensure quantifiers options are set with --no-strings...	blob \| commitdiff \| raw \| diff to current
2019-11-30	Andrew Reynolds	Fix fast SyGuS enumeration for interpreted constants...	blob \| commitdiff \| raw \| diff to current
2019-11-27	Andrew Reynolds	Fix sygus inference for choice functions introduced...	blob \| commitdiff \| raw \| diff to current
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	blob \| commitdiff \| raw \| diff to current
2019-11-27	Andrew Reynolds	Fix indexof range lemma (#3499)	blob \| commitdiff \| raw \| diff to current
2019-11-25	Andrew Reynolds	Better front-end type checking for SyGuS (#3496)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom