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

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

2019-10-14	Andrew Reynolds	Support UF in default sygus grammars (#3319)	blob \| commitdiff \| raw
2019-10-14	Andrew Reynolds	Apply sygus repair constant techniques restricted to...	blob \| commitdiff \| raw \| diff to current
2019-10-14	Andrew Reynolds	Ensure lemmas from sygus repair const are guarded ...	blob \| commitdiff \| raw \| diff to current
2019-10-13	Andrew Reynolds	Eliminate negative constant coefficients in div/mod...	blob \| commitdiff \| raw \| diff to current
2019-10-11	Andrew Reynolds	Check that logic is set when synth-fun command is encou...	blob \| commitdiff \| raw \| diff to current
2019-10-09	Andres Noetzli	Avoid printing success for `--force-logic` (#3363)	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andrew Reynolds	Limit cases of sygus inference based on type (#3370)	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andrew Reynolds	Fix method for getting arithmetic function definition...	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andres Noetzli	[CVC Parser] Add support for regular expressions (...	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andres Noetzli	Disallow --proof and --incremental (#3332)	blob \| commitdiff \| raw \| diff to current
2019-10-08	Ying Sheng	Make ackermannization generally applicable rather than...	blob \| commitdiff \| raw \| diff to current
2019-10-06	Andrew Reynolds	Fix str to int reduction (#3358)	blob \| commitdiff \| raw \| diff to current
2019-10-03	yoni206	Disable proofs for unsupported logics (#3327)	blob \| commitdiff \| raw \| diff to current
2019-10-01	Andrew Reynolds	Trivial solve method for single invocation sygus (...	blob \| commitdiff \| raw \| diff to current
2019-09-30	Andrew Reynolds	Avoid cases of empty sygus grammars (#3301)	blob \| commitdiff \| raw \| diff to current
2019-09-29	Andrew Reynolds	Fail single invocation techniques when utility inferenc...	blob \| commitdiff \| raw \| diff to current
2019-09-27	Andrew Reynolds	Fix case of disjunctive conclusion in strings (#3254)	blob \| commitdiff \| raw \| diff to current
2019-09-27	Andrew Reynolds	CVC print support for recoverable failure (#3323)	blob \| commitdiff \| raw \| diff to current
2019-09-25	Andrew Reynolds	Fix off by one error in strings flat form explanation...	blob \| commitdiff \| raw \| diff to current
2019-09-25	Andrew Reynolds	Add isParameterized function to Expr (#3303)	blob \| commitdiff \| raw \| diff to current
2019-09-25	Andrew Reynolds	Return choice functions for approximate values in get...	blob \| commitdiff \| raw \| diff to current
2019-09-19	Andrew Reynolds	Support context-(in)dependent decision strategies....	blob \| commitdiff \| raw \| diff to current
2019-09-17	Andrew Reynolds	Avoid computing cardinality when constructing models...	blob \| commitdiff \| raw \| diff to current
2019-09-16	Andrew Reynolds	Fix HO model construction for functions having Boolean...	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Fix default grammar construction for arrays when no...	blob \| commitdiff \| raw \| diff to current
2019-09-11	Andrew Reynolds	Fix constructor type printing (#3246)	blob \| commitdiff \| raw \| diff to current
2019-09-06	Mathias Preiner	Remove SMT1 parser. (#3228)	blob \| commitdiff \| raw \| diff to current
2019-09-04	Mathias Preiner	Remove duplicate regression tests. (#3227)	blob \| commitdiff \| raw \| diff to current
2019-08-30	Andres Noetzli	Better heuristic for str.code/re.range (#3220)	blob \| commitdiff \| raw \| diff to current
2019-08-30	Andres Noetzli	Infer conflicts based on regular expression inclusion...	blob \| commitdiff \| raw \| diff to current
2019-08-23	Andrew Reynolds	Infer emptiness instead of splitting when a string...	blob \| commitdiff \| raw \| diff to current
2019-08-23	Andrew Reynolds	Exclude redundant lemmas when tracking inst lemmas...	blob \| commitdiff \| raw \| diff to current
2019-08-23	Andrew Reynolds	Update dynamic splitting strategy for quantifiers ...	blob \| commitdiff \| raw \| diff to current
2019-08-22	Andrew Reynolds	Local substitutions for context-depdendent simplificat...	blob \| commitdiff \| raw \| diff to current
2019-08-20	Andrew Reynolds	Fixes for sygus inference on quantifier free problems...	blob \| commitdiff \| raw \| diff to current
2019-08-18	Andrew Reynolds	Context-independent regular expression unfolding (...	blob \| commitdiff \| raw \| diff to current
2019-08-14	Andrew Reynolds	Update to standard implementation of getting free...	blob \| commitdiff \| raw \| diff to current
2019-08-13	Andrew Reynolds	Add string rewrite involving allchar stars (#3167)	blob \| commitdiff \| raw \| diff to current
2019-08-08	Mathias Preiner	Fix issues with Ninja build system and add configure...	blob \| commitdiff \| raw \| diff to current
2019-08-06	Andrew Reynolds	Properly parse qualified identifiers (#3111)	blob \| commitdiff \| raw \| diff to current
2019-08-02	Mathias Preiner	Update CaDiCaL to version 1.0.3. (#3137)	blob \| commitdiff \| raw \| diff to current
2019-08-02	Andrew Reynolds	Remove simplification specialized for sygus si solution...	blob \| commitdiff \| raw \| diff to current
2019-08-02	Andrew Reynolds	Support default sygus grammar for strings (#3148)	blob \| commitdiff \| raw \| diff to current
2019-08-02	Andrew Reynolds	Fix solution filtering for streaming abducts (#3143)	blob \| commitdiff \| raw \| diff to current
2019-08-02	Andrew Reynolds	Enable sygus logic when produce-abducts is true (#3144)	blob \| commitdiff \| raw \| diff to current
2019-08-01	Andrew Reynolds	Regular expression intersection modes (#3134)	blob \| commitdiff \| raw \| diff to current
2019-07-31	Haniel Barbosa	Parsing THF and adding several regressions (#3131)	blob \| commitdiff \| raw \| diff to current
2019-07-30	Andrew Reynolds	Minor improvement for rewriter for str.replace (#3124)	blob \| commitdiff \| raw \| diff to current
2019-07-30	Andrew Reynolds	Handle RE intersections modulo equality (#3120)	blob \| commitdiff \| raw \| diff to current
2019-07-29	Andrew Reynolds	Model blocker feature (#3112)	blob \| commitdiff \| raw \| diff to current
2019-07-29	Andrew Reynolds	Support get-abduct smt2 command (#3122)	blob \| commitdiff \| raw \| diff to current
2019-07-24	Andrew Reynolds	Fix null node when using no-strings-lazy-pp (#3114)	blob \| commitdiff \| raw \| diff to current
2019-07-23	Andrew Reynolds	Fix sygus datatype parsing in sygus v1 format (#3113)	blob \| commitdiff \| raw \| diff to current
2019-07-19	Andrew Reynolds	Fixes for sygus with datatypes (#3103)	blob \| commitdiff \| raw \| diff to current
2019-07-19	Andrew Reynolds	Fix case of unfolding negative membership in reg exp...	blob \| commitdiff \| raw \| diff to current
2019-07-18	Andrew Reynolds	Basic rewrites for tolower/toupper (#3095)	blob \| commitdiff \| raw \| diff to current
2019-07-16	Andrew Reynolds	Add support for str.tolower and str.toupper (#3092)	blob \| commitdiff \| raw \| diff to current
2019-07-15	Andrew Reynolds	Add string rewrite to distribute character stars over...	blob \| commitdiff \| raw \| diff to current
2019-06-27	Andrew Reynolds	Variable elimination rewrite for quantified strings...	blob \| commitdiff \| raw \| diff to current
2019-06-24	Andrew Reynolds	Stratify unfolding of regular expressions based on...	blob \| commitdiff \| raw \| diff to current
2019-06-21	Andres Noetzli	Fix and simplify handling of --force-logic (#3062)	blob \| commitdiff \| raw \| diff to current
2019-06-10	Andrew Reynolds	Optimization for negative concatenation membership...	blob \| commitdiff \| raw \| diff to current
2019-06-05	Andres Noetzli	Prevent letification from shadowing variables (#3042)	blob \| commitdiff \| raw \| diff to current
2019-06-04	Andres Noetzli	Add check that result matches benchmark status (#3028)	blob \| commitdiff \| raw \| diff to current
2019-06-01	Andrew Reynolds	Fix rewriter for regular expression consume (#3029)	blob \| commitdiff \| raw \| diff to current
2019-05-30	Andres Noetzli	Quote symbol when printing empty symbol name (#3025)	blob \| commitdiff \| raw \| diff to current
2019-05-27	Andres Noetzli	Avoid substituting Boolean term variables (#3022)	blob \| commitdiff \| raw \| diff to current
2019-05-21	Martin	Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)	blob \| commitdiff \| raw \| diff to current
2019-05-17	Martin	Add the problematic input from issue 2183 as a regressi...	blob \| commitdiff \| raw \| diff to current
2019-05-15	Andres Noetzli	Fix model of Boolean vars with eager bit-blaster (...	blob \| commitdiff \| raw \| diff to current
2019-05-15	Andrew Reynolds	Fix printing of bvurem (#2963)	blob \| commitdiff \| raw \| diff to current
2019-05-09	Andrew Reynolds	Fixes for relational triggers (#2967)	blob \| commitdiff \| raw \| diff to current
2019-05-06	Andres Noetzli	Add support for re.all (#2980)	blob \| commitdiff \| raw \| diff to current
2019-05-01	Andrew Reynolds	Use total versions of div/mod in re-elim-agg (#2986)	blob \| commitdiff \| raw \| diff to current
2019-04-30	Andres Noetzli	Fix concat-find regexp elimination (#2983)	blob \| commitdiff \| raw \| diff to current
2019-04-30	Andrew Reynolds	Remove stoi solve rewrite (#2985)	blob \| commitdiff \| raw \| diff to current
2019-04-30	Andrew Reynolds	Eliminate APPLY kind (#2976)	blob \| commitdiff \| raw \| diff to current
2019-04-17	Andrew Reynolds	Fix extended function decomposition (#2960)	blob \| commitdiff \| raw \| diff to current
2019-04-16	Andres Noetzli	Make bv{add,mul,and,or,xor,xnor} left-associative ...	blob \| commitdiff \| raw \| diff to current
2019-04-16	Andrew Reynolds	Stratify enumerative instantiation (#2954)	blob \| commitdiff \| raw \| diff to current
2019-04-11	Andrew Reynolds	Eliminate Boolean ITE within terms, fixes 2947 (#2949)	blob \| commitdiff \| raw \| diff to current
2019-04-05	Andrew Reynolds	Fix another corner case of datatypes+PBE (#2938)	blob \| commitdiff \| raw \| diff to current
2019-04-03	Andrew Reynolds	Fix combination of datatypes + strings in PBE (#2930)	blob \| commitdiff \| raw \| diff to current
2019-04-01	Andres Noetzli	FP: Fix wrong model due to partial assignment (#2910)	blob \| commitdiff \| raw \| diff to current
2019-04-01	Andres Noetzli	Move slow string regression to regress3 (#2913)	blob \| commitdiff \| raw \| diff to current
2019-03-29	Andrew Reynolds	Apply empty splits more aggressively in sets+cardinalit...	blob \| commitdiff \| raw \| diff to current
2019-03-22	Andrew Reynolds	More fixes for PBE with datatypes (#2882)	blob \| commitdiff \| raw \| diff to current
2019-03-21	Andrew Reynolds	Rewrite selectors correctly applied to constructors...	blob \| commitdiff \| raw \| diff to current
2019-03-20	Andrew Reynolds	Sygus abduction feature (#2744)	blob \| commitdiff \| raw \| diff to current
2019-03-19	Andrew Reynolds	Fix fairness issue with fast sygus enumerator (#2873)	blob \| commitdiff \| raw \| diff to current
2019-03-15	Haniel Barbosa	New beta-reduction for HOL solving (#2869)	blob \| commitdiff \| raw \| diff to current
2019-03-14	Andrew Reynolds	Use zero slope tangent planes for transcendental functi...	blob \| commitdiff \| raw \| diff to current
2019-03-14	Andrew Reynolds	Implement proper semantics for TPTP predicate is_rat...	blob \| commitdiff \| raw \| diff to current
2019-03-12	Andrew Reynolds	Move tuple/record update elimination from ppRewrite...	blob \| commitdiff \| raw \| diff to current
2019-01-22	Andrew Reynolds	Fix tuple and record CVC printing (#2818)	blob \| commitdiff \| raw \| diff to current
2019-01-22	Andrew Reynolds	Fix parsing of overloaded parametric datatype selector...	blob \| commitdiff \| raw \| diff to current
2019-01-17	Andres Noetzli	Add option to print BV constants in binary (#2805)	blob \| commitdiff \| raw \| diff to current
2019-01-16	Andrew Reynolds	Fix constant contains ITOS rewrite (#2799)	blob \| commitdiff \| raw \| diff to current
2019-01-15	Andrew Reynolds	Fix unsound double abs rewrite rule for FP (#2792)	blob \| commitdiff \| raw \| diff to current
2019-01-09	Andrew Reynolds	Do not rewrite 1-constructor sygus testers to true...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom