Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-26 | Make 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-26 | Remove unnecessary code from Cvc.g (#3213) | Andrew Reynolds | |
2019-08-24 | fix misuse of iterator with a different container (#3214) | Piotr Trojanek | |
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-19 | New C++ API: Add checks for Solver::checkValid and ↵ | Aina Niemetz | |
Solver::checkValidAssuming. (#3197) | |||
2019-08-18 | Context-independent regular expression unfolding (#3168) | Andrew Reynolds | |
2019-08-17 | Cleaning make bound var in smt2 parser (#3192) | Andrew Reynolds | |
2019-08-17 | Move quantifiers relevance module inside E-matching module (#3186) | Andrew Reynolds | |
2019-08-17 | Mark symbols introduced by named attributes as defined. (#3190) | Andrew Reynolds | |
2019-08-15 | Fix for when to apply single invocation techniques (#3193) | Andrew Reynolds | |
2019-08-15 | cmake: Use ExactVersion instead of SameMinorVersion. (#3191) | Mathias Preiner | |
2019-08-14 | Remove option --continued-execution. (#3189) | Mathias Preiner | |
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 | cmake: Export CVC4 library interface. (#3179) | Mathias Preiner | |
2019-08-14 | Enable Clang-Format for Java (#3064) | Andres Noetzli | |
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 | SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183) | Aina Niemetz | |
2019-08-13 | New C++ API: Add checks and tests for Solver::simplify. (#3170) | Aina Niemetz | |
2019-08-13 | New C++ API: Fix test names of solver_black unit test. (#3170) | Aina Niemetz | |
2019-08-13 | New C++ API: Reorganize Solver code (move only). (#3170) | Aina Niemetz | |
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-13 | Implement check abduct feature (#3152) | Andrew Reynolds | |
2019-08-13 | Introduce smt2 parsing utility ParseOp and refactor (#3165) | Andrew Reynolds | |
2019-08-12 | Clean smt2 parsing of named attributes (#3172) | Andrew Reynolds | |
2019-08-12 | Give rewrite engine pointer to conflict-based instantiation module (#3174) | Andrew Reynolds | |
2019-08-11 | New C++ API: Add documentation/guidelines for API guards. (#3178) | Aina Niemetz | |
2019-08-11 | New C++ API: Add templated getIndices method for OpTerm (#3073) | makaimann | |
* Implement templated getIndices method for OpTerm * Add getIndices unit tests * Update src/api/cvc4cpp.cpp Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Update src/api/cvc4cpp.cpp Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Add comment about DIVISIBLE_OP * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Add exception checks to other unit tests (instead of having its own function) * Fix unit test names in opterm_black.h * Add description to docstring for getIndices * Formatting * Clang format older commits * Use '-' in docstring list to match other docstrings * Support creating DIVISIBLE_OP with a string (for arbitrary precision integers) * Move mkOpTerm(DIVISIBLE_OP, <str>) test to solver_black.h * Fix pointer access * Replace switch statement with if statement * Guard string input for CVC4::Integer in mkOpTerm for consistency on GMP/CLN back-end | |||
2019-08-10 | Simplify how defined functions are tracked during parsing (#3177) | 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-08 | Add subdirectories to contrib for competition scripts (#3164) | Andrew Reynolds | |
2019-08-08 | Fix issues with Ninja build system and add configure option. (#3166) | Mathias Preiner | |
Adds option --ninja to configure.sh. |