Age | Commit message (Collapse) | Author | |
---|---|---|---|
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. | |||
2019-08-07 | New C++ API: Add checks and tests for push/pop. (#3121) | Aina Niemetz | |
2019-08-07 | New C++ API: Introduce macros for try-catch blocks in Solver. (#3121) | Aina Niemetz | |
2019-08-06 | New C++ API: Fix branch prediction in CHECK macros. (#3161) | Aina Niemetz | |
2019-08-06 | Properly parse qualified identifiers (#3111) | Andrew Reynolds | |
2019-08-06 | Scripts for CASC-27 (#3163) | Haniel Barbosa | |
2019-08-05 | Fix drat signature wrt side condition return types. (#3160) | Andrew Reynolds | |
2019-08-05 | Remove forward declarations in quantifiers engine (#3156) | Andrew Reynolds | |
2019-08-04 | Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155) | Mathias Preiner | |
The regression script did not extract the expected status from incremental SMT-LIB v2 benchmarks correctly if status was given via (set-info :status ...). The script used re.search for finding the status, which only searches for the first occurrence instead of finding all (set-info :status ...). This commit fixes the issue by using re.findall instead. | |||
2019-08-03 | Fix printing issue related to nested quotes (#3154) | Andrew Reynolds | |
2019-08-03 | Collapse @ chains in SMT2 printer (#3140) | Haniel Barbosa | |
2019-08-02 | Update CaDiCaL to version 1.0.3. (#3137) | Mathias Preiner | |
* Removes incremental API check (#3011) * Fixes toSatValueLit to use the new semantics of CaDiCaL's val() Fixes #3011 | |||
2019-08-02 | Flip the polarity of the argument of get-abduct (#3153) | Andrew Reynolds | |
2019-08-02 | Add better Python detection for contrib scripts. (#3150) | Mathias Preiner | |
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 BVGauss unit tests. (#3142) | Mathias Preiner | |
pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the anonymous namespace, which resulted in ODR (one definition rule) violations reported by ASAN. This commit exposes the functionality required in the unit tests as private static members of the BVGauss class. Since this is a white unit test, we can access private members in the tests. | |||
2019-08-01 | Enable sygus logic when produce-abducts is true (#3144) | Andrew Reynolds | |