Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-09-06 | Make CEGQI term type to enum (#3256) | Andrew Reynolds | |
2019-09-05 | Model API for domain elements (#3243) | Andrew Reynolds | |
2019-09-04 | Explicitly pass current sygus solution to exclude (#3209) | Andrew Reynolds | |
2019-09-04 | Refactoring CEGQI interface (#3239) | Andrew Reynolds | |
2019-09-04 | Move getCounterexampleLiteral out of term utilities (#3238) | Andrew Reynolds | |
2019-09-04 | Fixes related to destructing null (#3231) | Andrew Reynolds | |
2019-08-30 | Fix out-of-bounds access in regexp inclusion test (#3242) | Andres Noetzli | |
If `re.*(re.allchar)` was at the end of a regular expression concatenation, the regular expression inclusion test could cause out-of-bound accesses. For `re.*(re.allchar)`, we were blindly adding the index after it to the set of indices being considered. Later in the loop, we were assuming that all the indices are smaller than the number of components in the concatenation, thus leading to out-of-bound accesses. This commit adds a check before adding the index to the set of indices. Signed-off-by: Andres Noetzli <andres.noetzli@gmail.com> | |||
2019-08-29 | Better heuristic for str.code/re.range (#3220) | Andres Noetzli | |
To make sure that our `str.code` function is injectve (except for -1 in the codomain), we send the inference that `str.code(x) == -1 v str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms. Because of the order of disjuncts, `str.code(x) != str.code(y)` was usually assigned true. This in turn lead to a difficult problem for the arithmetic engine if there were more `str.code` applications than the size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i <= 10, then the arithmetic engine had a difficult time finding a conflict. This PR improves the heuristic by setting the phase of `str.code(x) != str.code(y)` to false, so we prefer to keep the `str.code` values equal instead of trying to make them different. This change is also reflected in the models produced for inputs involving `str.code`: Previously, we were producing models with different values for the `str.code` whereas now the models are much more uniform. The PR adds two regressions, one testing `str.code` performance directly and one testing it for `str.code` terms generated by `re.range`. Signed-off-by: Andres Noetzli <anoetzli@amazon.com> | |||
2019-08-29 | Infer conflicts based on regular expression inclusion (#3234) | Andres Noetzli | |
We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)` and `R2` includes `R1` because there is no possible value for `x` that satisfies both memberships. This commit adds code to detect regular expression inclusion for a small fragment of regular expressions: string literals with single char (`re.allchar`) and multichar wildcards (`re.*(re.allchar)`). Signed-off-by: Andres Noetzli <anoetzli@amazon.com> | |||
2019-08-28 | Removing comments related to issues (#3232) | Andrew Reynolds | |
2019-08-27 | Fixes for get-abduct (#3229) | Andrew Reynolds | |
2019-08-24 | fix mismatch between "delete" and "new []" (#2795) | Piotr Trojanek | |
2019-08-23 | Infer emptiness instead of splitting when a string equality rewrites to a ↵ | Andrew Reynolds | |
constant (#3218) | |||
2019-08-23 | Fixes for sygus regressions (#3219) | Andrew Reynolds | |
2019-08-23 | Document transition inference utility (#3207) | Andrew Reynolds | |
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-23 | Fix argument in nonlinear extension. (#3216) | Andrew Reynolds | |
2019-08-23 | Minor update to term util (#3208) | Andrew Reynolds | |
2019-08-23 | Pass synthesis conjecture to sygus modules (#3212) | Andrew Reynolds | |
2019-08-22 | Local substitutions for context-depdendent simplification in strings (#3204) | 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-17 | Move quantifiers relevance module inside E-matching module (#3186) | Andrew Reynolds | |
2019-08-15 | Fix for when to apply single invocation techniques (#3193) | Andrew Reynolds | |
2019-08-14 | Update to standard implementation of getting free variables (#3175) | Andrew Reynolds | |
2019-08-14 | Call separate SMT engine for single invocation sygus (#3151) | Andrew Reynolds | |
2019-08-14 | Minor cleaning of sygus term database (#3159) | Andrew Reynolds | |
2019-08-14 | Fix issue related to higher-order purification in term database (#3157) | Andrew Reynolds | |
2019-08-13 | Track sygus variable to term relationship via attribute (#3182) | Andrew Reynolds | |
2019-08-13 | Update option to disable symbolic definitions in strings (#3180) | 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-12 | Give rewrite engine pointer to conflict-based instantiation module (#3174) | Andrew Reynolds | |
2019-08-10 | Add option to only dump unsolved queries for --sygus-query-gen (#3173) | Andrew Reynolds | |
2019-08-08 | Reorganize includes for quantifiers engine (#3169) | Andrew Reynolds | |
2019-08-05 | Remove forward declarations in quantifiers engine (#3156) | Andrew Reynolds | |
2019-08-03 | Fix printing issue related to nested quotes (#3154) | Andrew Reynolds | |
2019-08-02 | Move basic sygus enumerator to its own file (#3149) | Andrew Reynolds | |
2019-08-02 | Remove simplification specialized for sygus si solution reconstruction (#3147) | Andrew Reynolds | |
2019-08-02 | Support default sygus grammar for strings (#3148) | Andrew Reynolds | |
2019-08-02 | Throw option exception when track inst lemmas is not used (#3145) | Andrew Reynolds | |
2019-08-02 | Fix solution filtering for streaming abducts (#3143) | Andrew Reynolds | |
2019-08-01 | Fix memory leak in rewriter (debug mode). (#3141) | Mathias Preiner | |
s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit wraps s_rewriteStack in a std::unique_ptr to automatically free the memory. | |||
2019-08-01 | Move some generic utilities out of quantifiers (#3139) | Andrew Reynolds | |
2019-08-01 | Regular expression intersection modes (#3134) | Andrew Reynolds | |
2019-07-31 | Add some missing cases in evaluator (#3133) | Andrew Reynolds | |
2019-07-31 | Eager conflict detection in strings based on constant prefix/suffix (#3110) | Andrew Reynolds | |
2019-07-30 | Minor improvement for rewriter for str.replace (#3124) | Andrew Reynolds | |
2019-07-30 | Handle RE intersections modulo equality (#3120) | Andrew Reynolds | |