Age | Commit message (Collapse) | Author |
|
This commit addresses issue #38 in cvc4-projects by introducing public API for Sygus commands. It also includes two simple examples of how to use the API.
|
|
|
|
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
|
|
Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument.
I updated the Python files, although would be helpful to double check this is correct.
Co-authored-by: makaimann <makaim@stanford.edu>
|
|
This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.
Remaining tasks:
Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.
Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.
This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
|
|
|
|
|
|
|
|
|
|
|
|
API (#3355)
* Treat uninterpreted functions as a child in Term iteration
* Remove unnecessary const_iterator constructor
* Add parameter comments to const_iterator constructor
* Use operator[] instead of storing a vector of Expr children
* Switch pos member variable from int to uint32_t
* Add comment about how UFs are treated in iteration
* Allow OpTerm to contain a single Kind, update OpTerm construction
* Update mkTerm to use only an OpTerm (and not also a Kind)
* Remove unnecessary function checkMkOpTerm
* Update mkOpTerm comments to not use _OP Kinds
* Update examples to use new mkTerm
* First pass on fixing unit test
* Override kind for Constructor and Selector Terms
* More fixes to unit tests
* Updates to parser
* Remove old assert (for Kind, OpTerm pattern which was removed)
* Remove *_OP kinds from public API
* Add hasOpTerm and getOpTerm methods to Term
* Add test for UF iteration
* Add unit test for getOpTerm
* Move OpTerm implementation above Term implemenation to match header file
Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.
* Fix mkTerm in datatypes-new.cpp example
* Use helper function for creating term from Kind to avoid nested API calls
* Rename: OpTerm->Op in API
* Update OpTerm->Op in examples/tests/parser
* Add case for APPLY_TESTER
* operator term -> operator
* Update src/api/cvc4cpp.h
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Comment comment suggestion
Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add not-null checks and implement Op from a single Kind constructor
* Undo sed mistake for OpTerm replacement
* Add 'd_' prefix to member vars
* Fix comment and remove old commented-out code
* Formatting
* Revert "Formatting"
This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.
* More fixes for sed mistakes
* Minor formatting
* Undo changes in CVC parser
* Add isIndexed and prefix with d_
* Create helper function for isIndexed to avoid calling API functions in other API functions
|
|
* Updates to the unit tests, api, and examples for datatypes
* Format
|
|
|
|
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
Adds option --ninja to configure.sh.
|
|
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.
|
|
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.
|
|
|
|
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).
|
|
|
|
Because the headers are now installed in a `cvc4` directory, the examples need to include from there as well.
|
|
|
|
s
|
|
|
|
This required fixing the OpTerm handling for mkTerm functions in the API.
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|