summaryrefslogtreecommitdiff
path: root/src/api/cvc4cpp.cpp
AgeCommit message (Collapse)Author
2019-03-18New C++: Remove redundant mkBoundVar function.Aina Niemetz
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
s
2019-02-13New C++ API: Remove redundant declareFun function. (#2837)Aina Niemetz
2019-02-12New C++ API: Remove redundant mkTerm function. (#2836)Aina Niemetz
2019-02-11New C++ API: Unit tests for declare* functions. (#2831)Aina Niemetz
2019-01-29New C++ API: Fix checks for mkTerm. (#2820)Aina Niemetz
This required fixing the OpTerm handling for mkTerm functions in the API.
2019-01-11New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)Aina Niemetz
2019-01-10New C++ API: Get rid of mkConst functions (simplify API). (#2783)Aina Niemetz
2019-01-07New C++ API: Add missing getType() calls to kick off type checking. (#2773)Aina Niemetz
2019-01-03New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)Aina Niemetz
2019-01-03API/Smt2 parser: refactor termAtomic (#2674)Andres Noetzli
2019-01-03C++ 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-02New C++ API: Add tests for mk-functions in solver object. (#2764)Aina Niemetz
2018-12-17New C++ API: Add tests for term object. (#2755)Aina Niemetz
2018-12-14New C++ API: Add tests for opterm object. (#2756)Aina Niemetz
2018-12-13New C++ API: Add tests for sort functions of solver object. (#2752)Aina Niemetz
2018-11-05API: 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-08Fix compiler warnings. (#2601)Aina Niemetz
2018-10-04New 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-18New C++ API: Introduce new macro and exception for API checks. (#2486)Aina Niemetz
2018-09-14Refactor 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-12New C++ API: Try to fix (false positive) Coverity warnings. (#2454)Aina Niemetz
2018-08-23New 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-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-01New C++ API: Fixed ownership of options object. (#2243)Aina Niemetz
2018-07-26New C++ API: Third batch of commands (SMT-LIB). (#2212)Aina Niemetz
2018-07-26New 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-23New C++ API: Implementation of Solver class: OpTerm handling. (#2164)Aina Niemetz
2018-07-23New C++ API: declare-datatype. (#2166)Aina Niemetz
2018-07-13New C++ API: Minor reorder. (#2163)Aina Niemetz
2018-07-13New C++ API: Implementation of datatype classes. (#2142)Aina Niemetz
2018-07-13New C++ API: Implementation of Solver class: Consts handling. (#2145)Aina Niemetz
2018-07-06New C++ API: Implementation of Solver class: Term handling. (#2144)Aina Niemetz
2018-07-06New C++ API: Implementation of Solver class: Sort handling. (#2143)Aina Niemetz
2018-07-04New C++ API: Implementation of datatype declaration classes. (#2136)Aina Niemetz
2018-07-04New C++ API: Implementation of OpTerm. (#2132)Aina Niemetz
2018-07-03New C++ API: Implementation of Term. (#2131)Aina Niemetz
2018-07-03New C++ API: Implementation of Kind maps. (#2130)Aina Niemetz
2018-07-02New C++ API: Implementation of Sort. (#2122)Aina Niemetz
2018-06-28New C++ API: Implementation of Result. (#2112)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback