Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-11-20 | Lazy evaluation via rec-funs of ITE expressions (#3482) | Haniel Barbosa | |
2019-11-15 | Fix wrong kind in sygus version 1 parser (#3463) | Andrew Reynolds | |
2019-11-10 | Fix bugs related to sygus higher-order + recursive functions (#3448) | Andrew Reynolds | |
2019-11-06 | Support for SyGuS PBE + recursive functions (#3433) | Andrew Reynolds | |
2019-11-04 | Make getSynthSolution return a Bool (#3306) | Andrew Reynolds | |
2019-11-01 | Fix non-termination in datatype type enumerator (#3369) | Andrew Reynolds | |
2019-10-23 | Fixes 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-14 | Remove benchmark (#3389) | Andrew Reynolds | |
2019-10-14 | Support UF in default sygus grammars (#3319) | Andrew Reynolds | |
2019-10-14 | Apply sygus repair constant techniques restricted to refinement lemmas (#3386) | Andrew Reynolds | |
2019-10-14 | Ensure lemmas from sygus repair const are guarded (#3385) | Andrew Reynolds | |
2019-10-08 | Limit 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-08 | Fix method for getting arithmetic function definition body (#3371) | Andrew Reynolds | |
2019-10-06 | Fix typo in regression (#3359) | Andrew Reynolds | |
2019-10-06 | Fix 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-29 | Avoid cases of empty sygus grammars (#3301) | Andrew Reynolds | |
2019-09-29 | Fail single invocation techniques when utility inference fails. (#3322) | Andrew Reynolds | |
2019-09-27 | Support smt2 language "match" term (#3258) | Andrew Reynolds | |
2019-09-27 | Fix 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-25 | Add isParameterized function to Expr (#3303) | Andrew Reynolds | |
2019-09-18 | Decouple fmf-bound and finite-model-find (#3297) | Andrew Reynolds | |
2019-09-16 | Avoid computing cardinality when constructing models (#3268) | Andrew Reynolds | |
2019-09-16 | Fix spurious meta-info in regression (#3294) | Andrew Reynolds | |
2019-09-16 | Remove 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-13 | Disallow 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-06 | Remove 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-04 | Remove 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-23 | Exclude redundant lemmas when tracking inst lemmas. (#3210) | Andrew Reynolds | |
2019-08-23 | Update dynamic splitting strategy for quantifiers (#3162) | Andrew Reynolds | |
2019-08-20 | Fixes for sygus inference on quantifier free problems (#3202) | Andrew Reynolds | |
2019-08-18 | Context-independent regular expression unfolding (#3168) | Andrew Reynolds | |
2019-08-13 | Add string rewrite involving allchar stars (#3167) | Andrew Reynolds | |
2019-08-13 | Properly implement logic info for separation logic (#3176) | Andrew Reynolds | |
2019-08-02 | Flip the polarity of the argument of get-abduct (#3153) | Andrew Reynolds | |
2019-08-02 | Support default sygus grammar for strings (#3148) | Andrew Reynolds | |
2019-08-02 | Fix solution filtering for streaming abducts (#3143) | Andrew Reynolds | |
2019-08-01 | Regular expression intersection modes (#3134) | Andrew Reynolds | |
2019-07-31 | Parsing THF and adding several regressions (#3131) | Haniel Barbosa | |
2019-07-30 | Handle RE intersections modulo equality (#3120) | Andrew Reynolds | |
2019-07-29 | Model blocker feature (#3112) | Andrew Reynolds | |
2019-07-29 | Support get-abduct smt2 command (#3122) | Andrew Reynolds | |
2019-07-24 | Fix null node when using no-strings-lazy-pp (#3114) | Andrew Reynolds | |
2019-07-19 | Fixes for sygus with datatypes (#3103) | Andrew Reynolds | |
2019-07-19 | Fix case of unfolding negative membership in reg exp concatenation (#3101) | Andrew Reynolds | |
2019-07-16 | Add 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 | |