summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-08-17Move quantifiers relevance module inside E-matching module (#3186)Andrew Reynolds
2019-08-17Mark 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-15cmake: Use ExactVersion instead of SameMinorVersion. (#3191)Mathias Preiner
2019-08-14Remove option --continued-execution. (#3189)Mathias Preiner
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-14cmake: Export CVC4 library interface. (#3179)Mathias Preiner
2019-08-14Enable Clang-Format for Java (#3064)Andres Noetzli
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-13SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)Aina Niemetz
2019-08-13New C++ API: Add checks and tests for Solver::simplify. (#3170)Aina Niemetz
2019-08-13New C++ API: Fix test names of solver_black unit test. (#3170)Aina Niemetz
2019-08-13New 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-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-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-13Introduce smt2 parsing utility ParseOp and refactor (#3165)Andrew Reynolds
2019-08-12Clean 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-11New C++ API: Add documentation/guidelines for API guards. (#3178)Aina Niemetz
2019-08-11New 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-10Simplify how defined functions are tracked during parsing (#3177)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-08Add subdirectories to contrib for competition scripts (#3164)Andrew Reynolds
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
Adds option --ninja to configure.sh.
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
2019-08-07New C++ API: Introduce macros for try-catch blocks in Solver. (#3121)Aina Niemetz
2019-08-06New C++ API: Fix branch prediction in CHECK macros. (#3161)Aina Niemetz
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-08-06Scripts for CASC-27 (#3163)Haniel Barbosa
2019-08-05Fix drat signature wrt side condition return types. (#3160)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-08-04Fix 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-03Fix printing issue related to nested quotes (#3154)Andrew Reynolds
2019-08-03Collapse @ chains in SMT2 printer (#3140)Haniel Barbosa
2019-08-02Update 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-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-02Add 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-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 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-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback