summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-09-11Refactoring finite bounds in Quantifiers Engine (#3261)Andrew Reynolds
2019-09-11Fix type assertion in getSynthSolutions (#3252)Andrew Reynolds
2019-09-11Infrastructure for instantiation rewriter (#3262)Andrew Reynolds
2019-09-10Fix issue related to enum in cegqi (#3267)Andrew Reynolds
2019-09-09Fix issue in cegqi related to enum (#3265)Andrew Reynolds
2019-09-06Make CEGQI term type to enum (#3256)Andrew Reynolds
2019-09-05 Model API for domain elements (#3243)Andrew Reynolds
2019-09-04Explicitly pass current sygus solution to exclude (#3209)Andrew Reynolds
2019-09-04Refactoring CEGQI interface (#3239)Andrew Reynolds
2019-09-04Move getCounterexampleLiteral out of term utilities (#3238)Andrew Reynolds
2019-09-04 Fixes related to destructing null (#3231)Andrew Reynolds
2019-08-30Fix out-of-bounds access in regexp inclusion test (#3242)Andres Noetzli
2019-08-29Better heuristic for str.code/re.range (#3220)Andres Noetzli
2019-08-29Infer conflicts based on regular expression inclusion (#3234)Andres Noetzli
2019-08-28Removing comments related to issues (#3232)Andrew Reynolds
2019-08-27Fixes for get-abduct (#3229)Andrew Reynolds
2019-08-24fix mismatch between "delete" and "new []" (#2795)Piotr Trojanek
2019-08-23 Infer emptiness instead of splitting when a string equality rewrites to a co...Andrew Reynolds
2019-08-23 Fixes for sygus regressions (#3219)Andrew Reynolds
2019-08-23Document transition inference utility (#3207)Andrew Reynolds
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-23Fix argument in nonlinear extension. (#3216)Andrew Reynolds
2019-08-23Minor 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-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-18Context-independent regular expression unfolding (#3168)Andrew Reynolds
2019-08-17Move 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-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-14Minor cleaning of sygus term database (#3159)Andrew Reynolds
2019-08-14Fix 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-13Update option to disable symbolic definitions in strings (#3180)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-12 Give rewrite engine pointer to conflict-based instantiation module (#3174)Andrew Reynolds
2019-08-10Add option to only dump unsolved queries for --sygus-query-gen (#3173)Andrew Reynolds
2019-08-08Reorganize includes for quantifiers engine (#3169)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-08-03Fix 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-02Remove simplification specialized for sygus si solution reconstruction (#3147)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-08-02Throw option exception when track inst lemmas is not used (#3145)Andrew Reynolds
2019-08-02Fix solution filtering for streaming abducts (#3143)Andrew Reynolds
2019-08-01Fix memory leak in rewriter (debug mode). (#3141)Mathias Preiner
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback