| Age | Commit message (Collapse) | Author |
|---|
|
Finally, we no longer need to link against GMP and CLN for the parser and the tests.
To actually achieve this, this PR also removes some dead code and unused includes from some parser files.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
|
|
|
|
|
|
|
|
Fixes #6298.
Enables parsing of par in the sygus parser, and adds support for default grammar construction.
Also fixes a bug related to single invocation for non-function types.
|
|
|
|
|
|
This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.
This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.
This also fixes Solver::isReal, which should return false if we are the integer type.
Fixes #6208.
|
|
|
|
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
|
|
This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.
Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.
|
|
This PR eliminates all remaining uses of SExpr outside of statistics.
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
|
|
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
|
|
This PR fixes an issue where utf8 encoded inputs are incorrectly parsed into CVC4::String. We now use std::mbtowc to first turn the char sequence from the std::string input into a std::wstring and then process this std::wstring one charactor (wchar_t) at a time.
Fixes #5673
|
|
This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.
Fixes #1479 #5769.
|
|
|
|
This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
|
|
The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.
|
|
This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.
More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.
|
|
This PR adds inference generator for basic bag rules.
|
|
|
|
|
|
Leftover from a development branch.
|
|
The smt2 parser is now 100% independent from the Expr-layer.
|
|
This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.
This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.
This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.
This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.
|
|
|
|
|
|
This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API).
|
|
This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.
This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.
This is one of the last remaining steps for migrating the parser to the new API.
The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
|
|
This is required to make the cvc parser work properly with the new version of getting models based on the symbol manager.
|
|
This further removes obsolete explicit includes of stdint.h.
|
|
This PR uses the symbol manager for handling names for unsat cores.
This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
|
|
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.
Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
|
|
This changes the default of Parser::pushScope and prepares symbol manager further for maintaining expression names.
|
|
This is in preparation for having the symbol manager manage expression names at the parser level instead of inside SmtEngine.
This adds some necessary features regarding scopes and global declarations.
This PR still does not change the behavior of the parser.
|
|
This follows a similar style to symbol_table.h/cpp. This is required since context dependent data structures are cvc4_private, and symbol manager is cvc4_public.
|
|
This is required since symbol manager will use context dependent data structures (in its cpp).
This is required since classes in src/parser/ are not allowed to include private headers.
|
|
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.
This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.
Fixes #5343, fixes #4926.
Work towards CVC4/cvc4-wishues#22.
|
|
This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.
The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.
This PR adds the basic interface for the symbol manager and passes it to the parser.
Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.
Marking "complex" since this impacts further design of the parser and the code that lives in src/main.
FYI @4tXJ7f
|
|
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
|
|
This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:
Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API
|
