Age | Commit message (Collapse) | Author |
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
|
|
This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
|
|
Make collect_tags.py more robust for non-ASCII characters.
|
|
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.
|
|
Fixes warnings with CVC4_FALLTHROUGH and -Werror for debug/production with gcc/clang. Clang detects that a CVC4_FALLTHROUGH after an Assert(false); is unreachable and issues a warning, while gcc issues a warning about an implicit fall-through if CVC4_FALLTHROUGH is not present.
|
|
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
|
|
|
|
|
|
|
|
We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.
|
|
|
|
Miscellaneous changes from proof-new.
|
|
|
|
|
|
This fixes some issues that break the nightly ASAN builds with clang.
|
|
|
|
|
|
This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
|
|
This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
|
|
The justification heuristic stores a "copy" of assertions as TNode. As witnessed by #5938, these TNodes may invalid.
This PR changes this to store Nodes instead.
Fixes #5938.
|
|
This case was previously unhandled and exercised by a recently added regression.
|
|
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
|
|
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
|
|
Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
|
|
|
|
This PR adds the test case from #5187 as a regression.
Fixes #5187.
|
|
|