summaryrefslogtreecommitdiff
path: root/test/regress/regress1
AgeCommit message (Collapse)Author
2019-11-20Lazy evaluation via rec-funs of ITE expressions (#3482)Haniel Barbosa
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-10-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
This commit fixes numerous issues involving the combination of SyGuS and regular expressions. Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
2019-10-14Remove benchmark (#3389)Andrew Reynolds
2019-10-14Support UF in default sygus grammars (#3319)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-14Ensure lemmas from sygus repair const are guarded (#3385)Andrew Reynolds
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar. It also fixes an issue where skolem variables were not being treated as functions-to-synthesize. Fixes #3250 and fixes #3356.
2019-10-08Fix method for getting arithmetic function definition body (#3371)Andrew Reynolds
2019-10-06Fix typo in regression (#3359)Andrew Reynolds
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string. This fixes #3357.
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
Fixes #3272. This was caused by not explaining the last equal component in a flat form inference. For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error. Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`. #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-16Avoid computing cardinality when constructing models (#3268)Andrew Reynolds
2019-09-16Fix spurious meta-info in regression (#3294)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16 Fix HO model construction for functions having Boolean arguments (#3158)Andrew Reynolds
2019-09-13Disallow let in sygus grammars, check for free variables in sygus ↵Andrew Reynolds
constructors (#3259)
2019-09-12 Fix default grammar construction for arrays when no free variables are ↵Andrew Reynolds
present (#3225)
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-08-23 Infer emptiness instead of splitting when a string equality rewrites to a ↵Andrew Reynolds
constant (#3218)
2019-08-23Exclude redundant lemmas when tracking inst lemmas. (#3210)Andrew Reynolds
2019-08-23Update dynamic splitting strategy for quantifiers (#3162)Andrew Reynolds
2019-08-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-18Context-independent regular expression unfolding (#3168)Andrew Reynolds
2019-08-13Add string rewrite involving allchar stars (#3167)Andrew Reynolds
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-08-02Fix solution filtering for streaming abducts (#3143)Andrew Reynolds
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-30 Handle RE intersections modulo equality (#3120)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-24 Fix null node when using no-strings-lazy-pp (#3114)Andrew Reynolds
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-07-19Fix case of unfolding negative membership in reg exp concatenation (#3101)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)Andrew Reynolds
2019-07-15 Add string rewrite to distribute character stars over concatenation (#3091)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback