| Age | Commit message (Collapse) | Author |
|---|
|
Towards parser migration.
Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers.
This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.
|
|
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.
It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.
This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
|
|
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.
This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.
This is work towards parser migration.
|
|
The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.
The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.
This is work towards the SyGuS API.
|
|
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.
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
|
|
This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes:
Indexed ops are carried in ParseOp via api::Op not Expr,
getKindForFunction is limited to "APPLY" kinds from the new API,
The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity.
TPTP should use DIVISION not DIVISION_TOTAL.
This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.
|
|
Removing dependency of kinds corresponding to expressions.
|
|
Towards parser migration.
(Partially) updates the central function used for synth-fun in sygus v2 to the new API.
It also removes an optimization for "pure operators" from the v2 parser that is incompatible with the new API.
|
|
Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing.
|
|
This moves a fix for vacuous sygus types out of the parser and into the Expr-level datatype.
This is a temporary fix so that further progress can be made on parser migration (and to declutter the parser).
This will be refactored when an API for SyGuS is established (CVC4/cvc4-projects#38).
|
|
Towards v1 -> v2 sygus conversion.
This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
|
|
Fixes #3408 .
Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h
|
|
Towards parser migration.
This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API.
This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.
|
|
|
|
Towards parser migration, will make the diff of the eventual conversion a bit smaller.
|
|
Towards parser/API migration.
|
|
|
|
With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.
|
|
This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
The next steps will be to address the more invasive changes required to support the standard.
|
|
|
|
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
|
|
|
|
|
|
|
|
|
|
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).
Also improves support in a few places for tolower/toupper.
|
|
Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value.
This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
This commit enables compiler warnings for implicit fallthroughs in
switch statements that are not explicitly marked as such. The commit
introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate
that a fallthrough is intentional. The commit fixes existing warnings
and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't
be triggered easily because we rewrite `abs` to an `ite` while expanding
definitions).
To have the new macro also available in the parser, the commit changes
`src/base/check.h` to be visible to the parser (it includes
`cvc4_private_library.h` now instead of `cvc4_private.h`).
|
|
|
|
Fixes #3353. #3062 introduced a flag that tracks whether we have seen a
`(set-logic ...)` command to improve the handling of `--force-logic`.
However, the flag was not set to `false` when `(reset)` was called. This
commit fixes the issue.
|
|
|
|
|
|
|
|
Fixes #2517.
This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.
This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.
I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993
|
|
CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.
The issue was likely introduced with #3062.
|
|
|
|
This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.
|
|
This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.
|
|
|
