Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-03-18 | New C++: Remove redundant mkBoundVar function. | 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-02-12 | New C++ API: Remove redundant mkTerm function. (#2836) | Aina Niemetz | |
2019-02-11 | New C++ API: Unit tests for declare* functions. (#2831) | 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-11 | New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782) | Aina Niemetz | |
2019-01-10 | New C++ API: Get rid of mkConst functions (simplify API). (#2783) | Aina Niemetz | |
2019-01-07 | New C++ API: Add missing getType() calls to kick off type checking. (#2773) | Aina Niemetz | |
2019-01-03 | New C++ API: Add missing catch blocks for std::invalid_argument. (#2772) | Aina Niemetz | |
2019-01-03 | API/Smt2 parser: refactor termAtomic (#2674) | Andres Noetzli | |
2019-01-03 | C++ API: Reintroduce zero-value mkBitVector method (#2770) | Andres Noetzli | |
PR #2764 removed `Solver::mkBitVector(uint32_t)` (returns a bit-vector of a given size with value zero), which made the build fail when SymFPU was enabled because solver_black used it for SymFPU-enabled builds. This commit simply adds a zero default argument to `mkBitVector(uint32_t, uint64_t)` to allow users to create zero-valued bit-vectors without explicitly specifying the value again. Additionally, the commit replaces the use of the `CVC4_USE_SYMFPU` macro by a call to `Configuration::isBuiltWithSymFPU()`, making sure that we can catch compile-time errors regardless of configuration. Finally, `Solver::mkConst(Kind, uint32_t, uint32_t, Term)` now checks whether CVC4 has been compiled with SymFPU when creating a `CONST_FLOATINGPOINT` and throws an exception otherwise (solver_black has been updated correspondingly). | |||
2019-01-02 | New C++ API: Add tests for mk-functions in solver object. (#2764) | Aina Niemetz | |
2018-12-17 | New C++ API: Add tests for term object. (#2755) | Aina Niemetz | |
2018-12-14 | New C++ API: Add tests for opterm object. (#2756) | Aina Niemetz | |
2018-12-13 | New C++ API: Add tests for sort functions of solver object. (#2752) | Aina Niemetz | |
2018-11-05 | API: Fix assignment operators (#2680) | Andres Noetzli | |
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have an issue. The operators dereference their `shared_ptr` member and assign the corresponding member of the other object. This is problematic because if we have for example two `Term`s pointing to the same `Expr`, then the assignment changes both `Term`s even though we only assign to one, which is not what we want (see the unit test in this commit for a concrete example of the desired behavior). To fix the issue, the assignment operator should just copy the pointer of the other object. This happens to be the behavior of the default assignment operator, so this commit simply removes the overloaded assignment operators. Testing: I did `make check` with an ASAN build and no errors other than the one fixed in #2607 were reported. | |||
2018-10-08 | Fix compiler warnings. (#2601) | Aina Niemetz | |
2018-10-04 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
2018-09-23 | New C++ API: Add checks for Terms/OpTerms. (#2455) | Aina Niemetz | |
2018-09-18 | New C++ API: Introduce new macro and exception for API checks. (#2486) | Aina Niemetz | |
2018-09-14 | Refactor how assertions are added to decision engine (#2396) | Andres Noetzli | |
Before refactoring the preprocessing passes, we were using three arguments to add assertions to the decision engine. Now all that information lives in the AssertionPipeline. This commit moves the AssertionPipeline to its own file and changes the `addAssertions()` methods related to the decision engine to take an AssertionPipeline as an arguement instead of three separate ones. Additionally, the TheoryEngine now uses an AssertionPipeline for lemmas. | |||
2018-09-12 | New C++ API: Try to fix (false positive) Coverity warnings. (#2454) | Aina Niemetz | |
2018-08-23 | New C++ API: Add checks for kind arguments. (#2369) | Aina Niemetz | |
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp. | |||
2018-08-09 | Fix char overflow issues in regular expression solver (#2275) | Andrew Reynolds | |
2018-08-08 | Plug solver API object into parser. (#2240) | Aina Niemetz | |
2018-08-01 | New C++ API: Fixed ownership of options object. (#2243) | Aina Niemetz | |
2018-07-26 | New C++ API: Third batch of commands (SMT-LIB). (#2212) | Aina Niemetz | |
2018-07-26 | New C++ API: Second batch of commands (SMT-LIB). (#2201) | Aina Niemetz | |
2018-07-24 | New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199) | Aina Niemetz | |
2018-07-23 | New C++ API: Implementation of Solver class: OpTerm handling. (#2164) | Aina Niemetz | |
2018-07-23 | New C++ API: declare-datatype. (#2166) | Aina Niemetz | |
2018-07-13 | New C++ API: Minor reorder. (#2163) | Aina Niemetz | |
2018-07-13 | New C++ API: Implementation of datatype classes. (#2142) | Aina Niemetz | |
2018-07-13 | New C++ API: Implementation of Solver class: Consts handling. (#2145) | Aina Niemetz | |
2018-07-06 | New C++ API: Implementation of Solver class: Term handling. (#2144) | Aina Niemetz | |
2018-07-06 | New C++ API: Implementation of Solver class: Sort handling. (#2143) | Aina Niemetz | |
2018-07-04 | New C++ API: Implementation of datatype declaration classes. (#2136) | Aina Niemetz | |
2018-07-04 | New C++ API: Implementation of OpTerm. (#2132) | Aina Niemetz | |
2018-07-03 | New C++ API: Implementation of Term. (#2131) | Aina Niemetz | |
2018-07-03 | New C++ API: Implementation of Kind maps. (#2130) | Aina Niemetz | |
2018-07-02 | New C++ API: Implementation of Sort. (#2122) | Aina Niemetz | |
2018-06-28 | New C++ API: Implementation of Result. (#2112) | Aina Niemetz | |