| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2019-08-01 | Use python realpath instead of relying on shell realpath (#3117) | makaimann | |
| * Use a custom implementation instead of relying on realpath, because it doesn't exist on Mac * Use local variables and move portable_realpath to its own file * Replace portable_realpath with python realpath * Consistent command substitution Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com> * Substitute pwd directly | |||
| 2019-08-01 | Fix memory leak in rewriter (debug mode). (#3141) | Mathias Preiner | |
| s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit wraps s_rewriteStack in a std::unique_ptr to automatically free the memory. | |||
| 2019-08-01 | Move some generic utilities out of quantifiers (#3139) | Andrew Reynolds | |
| 2019-08-01 | Regular expression intersection modes (#3134) | Andrew Reynolds | |
| 2019-07-31 | Parsing THF and adding several regressions (#3131) | Haniel Barbosa | |
| 2019-07-31 | adding bv_gauss unit test to build files (#3135) | yoni206 | |
| 2019-07-31 | Add some missing cases in evaluator (#3133) | Andrew Reynolds | |
| 2019-07-31 | Eager conflict detection in strings based on constant prefix/suffix (#3110) | Andrew Reynolds | |
| 2019-07-30 | Track solver execution mode (#3132) | Andrew Reynolds | |
| 2019-07-30 | Code to activate hoelim preprocessing pass (#3129) | Haniel Barbosa | |
| 2019-07-30 | Minor improvement for rewriter for str.replace (#3124) | Andrew Reynolds | |
| 2019-07-30 | Handle RE intersections modulo equality (#3120) | Andrew Reynolds | |
| 2019-07-30 | Remove hard coded option for TPTP regressions in run_regression (#3128) | Haniel Barbosa | |
| 2019-07-29 | Model blocker feature (#3112) | Andrew Reynolds | |
| 2019-07-29 | Support get-abduct smt2 command (#3122) | Andrew Reynolds | |
| 2019-07-29 | Fix match trie for polymorphic operators (#3125) | Andrew Reynolds | |
| 2019-07-29 | Refactoring of bit-vector elimination rules (#3105) | yoni206 | |
| This commit makes the following minor refactors to src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h: - Including options/bv_options.h: this is needed because this header file is being used. - Marking all functions as inline: details in a discussion inside the PR. | |||
| 2019-07-27 | Minor improvement to term canonizer (#3123) | Andrew Reynolds | |
| 2019-07-25 | Input user grammar in sygus abduct (#3119) | Andrew Reynolds | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback