Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-06-21 | Add floating-point support in the Java API (#3063) | Andres Noetzli | |
This commit adds support for the theory of floating-point numbers in the Java API. Previously, floating-point related classes were missing in the JAR. The commit also provides an example that showcases how to work with the theory of floating-point numbers through the API. | |||
2019-05-15 | Fix iterators in Java API (#3000) | Andres Noetzli | |
Fixes #2989. SWIG 3 seems to have an issue properly resolving `T::const_iterator::value_type` if that type itself is a `typedef`. This is for example the case in the `UnsatCore` class, which `typedef`s `const_iterator` to `std::vector<Expr>::const_iterator`. As a workaround, this commit changes the `JavaIteratorAdapter` class to take two template parameters, one of which is the `value_type`. The commit also adds a compile-time assertion that `T::const_iterator::value_type` can be converted to `value_type` to avoid nasty surprises. A nice side-effect of this solution is that explicit `typemap`s are not necessary anymore, so they are removed. Additionally, the commit adds a `toString()` method for the Java API of `UnsatCore` and adds examples that show and test the iteration over the unsat core and the statistics. Iterating over `Statistics` now returns instances of `Statistic` instead of `Object[]`, which is a bit cleaner and requires less glue code. | |||
2019-04-30 | Fix use of APPLY kind in examples (#2984) | Andres Noetzli | |
2019-04-25 | New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977) | Aina Niemetz | |
This cleans up naming of API functions to create first-order constants and variables. mkVar -> mkConst mkBoundVar -> mkVar declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed. Note that we want to avoid redundancy in order to reduce code duplication and maintenance overhead (we do not allow nested API calls, since this is problematic when tracing API calls). | |||
2019-04-03 | Update copyright headers. | Aina Niemetz | |
2019-04-01 | Update includes to use cvc4 top-level directory in examples (#2877) | makaimann | |
Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well. | |||
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2019-03-18 | New C++: Remove redundant mkVar function. | Aina Niemetz | |
s | |||
2019-02-13 | New C++ API: Remove redundant declareFun function. (#2837) | Aina Niemetz | |
2019-01-29 | New C++ API: Fix checks for mkTerm. (#2820) | Aina Niemetz | |
This required fixing the OpTerm handling for mkTerm functions in the API. | |||
2019-01-02 | New C++ API: Add tests for mk-functions in solver object. (#2764) | Aina Niemetz | |
2018-11-14 | cmake: Require boost 1.50.0 for examples. (#2710) | Mathias Preiner | |
2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
2018-10-08 | Cmake: Fix ctest call for example/translator. (#2600) | Aina Niemetz | |
example/translator expects an input file to translate but none was provided in the ctest call. This caused the ctest call to hang and wait for input on stdin in some configurations (in particular in the nightlies). | |||
2018-10-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
2018-10-03 | Fix mem leak in sha1_collision example. (#2588) | Aina Niemetz | |
2018-10-03 | Fix mem leak in sets_translate example. (#2589) | Aina Niemetz | |
2018-09-25 | cmake: New INSTALL.md for build and testing instructions. (#2536) | Aina Niemetz | |
2018-09-25 | examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534) | Aina Niemetz | |
2018-09-22 | cmake: Add more documentation, some fixes and cleanup. | Mathias Preiner | |
2018-09-22 | cmake: Refactor cvc4_add_unit_test macro to support test names with '/'. | Aina Niemetz | |
Required for consistent naming of tests, unit test names now also use the test naming scheme <category>/<subdir>/<test name>, e.g., unit/theory/theory_bv_white. | |||
2018-09-22 | cmake: Add target runexamples. | Aina Niemetz | |
2018-09-22 | cmake: Guard examples that require Boost. | Mathias Preiner | |
2018-09-22 | cmake: examples: Configure output directory per target. | Aina Niemetz | |
2018-09-22 | cmake: Added java examples | Aina Niemetz | |
2018-09-22 | cmake: Added target examples (currently .cpp examples only) | Aina Niemetz | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-09-12 | Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461) | Aina Niemetz | |
2018-09-04 | Remove CVC3 compatibility layer (#2418) | Andres Noetzli | |
2018-08-08 | Plug solver API object into parser. (#2240) | Aina Niemetz | |
2018-07-26 | New C++ API: Enable examples. (#2222) | Aina Niemetz | |
2018-07-23 | New C++ API: declare-datatype. (#2166) | Aina Niemetz | |
2018-07-03 | Fix datatypes example: nil constructor was missing. (#2135) | Aina Niemetz | |
2018-06-27 | Header for new C++ API. (#1697) | Aina Niemetz | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-05-21 | Fix compiler warning in hashsmt example (#1927) | Andres Noetzli | |
Previously, we were using delete for an array allocated on the heap, which caused a warning. @dddejan fixed this and other issues in PR #1909 but after @ajreynol fixed the other issues in a separate PR and to not waste @dddejan's time, I am submitting this fix separately (note: the fix is slightly different in that it changes the array to a vector, making a delete[] unnecessary). | |||
2018-04-05 | Make Python bindings example compatible w/ Python3 (#1751) | Andres Noetzli | |
2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
2018-03-21 | Add bit-vector extract example. (#1681) | Aina Niemetz | |
2018-03-20 | Add parameterized datatypes example. (#1676) | Aina Niemetz | |
2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
2018-03-05 | Add support for check-sat-assuming. (#1637) | Aina Niemetz | |
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). | |||
2017-09-27 | Add quantifiers API example, fixes #879 (#1146) | Andrew Reynolds | |
2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King | |
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. | |||
2017-07-16 | Moving to static_assert now that c++11 is available. | Tim King | |
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
2017-01-11 | Proposed fix for bug 702. Checks to make sure the Expr's operator is not of ↵ | makaimann | |
kind BUILTIN before passing to prefixPrintGetValue() | |||
2016-04-20 | update from the master | PaulMeng | |
2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ↵ | Tim King | |
Breaking an edge between the sat solver and command.h. |