summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-09-13Disallow let in sygus grammars, check for free variables in sygus ↵Andrew Reynolds
constructors (#3259)
2019-09-13Move higher-order matching predicate (#3280)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-09-12Update to standard implementation of contains term (#3270)Andrew Reynolds
2019-09-12 Fix default grammar construction for arrays when no free variables are ↵Andrew Reynolds
present (#3225)
2019-09-12Encapsulate synth engine (#3271)Andrew Reynolds
2019-09-11Refactoring finite bounds in Quantifiers Engine (#3261)Andrew Reynolds
2019-09-11Fix not to output all warnings (#2778)Ken Matsui
Fix syntax error when --language-bindings is java Replace __attribute__((__unused__)) with CVC4_UNUSED macro Signed-off-by: matken11235 <26405363+matken11235@users.noreply.github.com>
2019-09-11Fix type assertion in getSynthSolutions (#3252)Andrew Reynolds
2019-09-11Infrastructure for instantiation rewriter (#3262)Andrew Reynolds
2019-09-11Fix constructor type printing (#3246)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-06Remove portfolio (#3236)Andrew Reynolds
2019-09-06Remove parsing/printing of meta-info command. (#3260)Mathias Preiner
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-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-04Towards incremental SyGuS in SMT engine (#3195)Andrew Reynolds
2019-09-04More details in substitution function documentation (#3244)yoni206
2019-09-04Move getCounterexampleLiteral out of term utilities (#3238)Andrew Reynolds
2019-09-04Fix DAGification for printer. (#3233)Mathias Preiner
2019-09-04 Fixes related to destructing null (#3231)Andrew Reynolds
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-08-30Fix 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-30Undo unintential change to FindCxxTest (#3240)Andrew Reynolds
2019-08-29Better 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-29Infer 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-28Removing comments related to issues (#3232)Andrew Reynolds
2019-08-27Fixes for get-abduct (#3229)Andrew Reynolds
2019-08-26Make contrib/get-* more robust. (#3198)Mathias Preiner
We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.
2019-08-26Remove unnecessary code from Cvc.g (#3213)Andrew Reynolds
2019-08-24fix misuse of iterator with a different container (#3214)Piotr Trojanek
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 ↵Andrew Reynolds
constant (#3218)
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-19New C++ API: Add checks for Solver::checkValid and ↵Aina Niemetz
Solver::checkValidAssuming. (#3197)
2019-08-18Context-independent regular expression unfolding (#3168)Andrew Reynolds
2019-08-17 Cleaning make bound var in smt2 parser (#3192)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback