summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-03-05google test: Remove obsolete Expr test fixtures. (#6060)Aina Niemetz
2021-03-05Reimplement time limit mechanism for windows (#6049)Gereon Kremer
As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this. Fixes #5034.
2021-03-05google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)Aina Niemetz
2021-03-04New C++ API: Clean up usage of interal datatype classes. (#6055)Aina Niemetz
This disables the temporarily available internals of datatype classes.
2021-03-04Add initial bit-blaster for proof logging. (#6053)Aina Niemetz
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
2021-03-04New C++ Api: Clean up usage of internal types in Term. (#6054)Aina Niemetz
This disables the temporarily available internals of Term. Note: getExpr() is still available and will be disabled when the API is fully converted to Nodes.
2021-03-04Add proper define for libpoly usage (#6050)Gereon Kremer
When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.
2021-03-04Add cmake scripts for iwyu targets. (#6042)Gereon Kremer
This PR adds some utility targets that simplify the usage of iwyu (include-what-you-use) on our code base.
2021-03-04Fix nightlies. (#6052)Aina Niemetz
2021-03-04Ignore isInConflict when adding conflicts (#5995)Gereon Kremer
Right now, the inference manager infrastructure drops conflicts (and literal propagations) if the solver already is in a conflict. This PR removes this behavior. The current setup in linear arithmetic requires adding conflicts, even when already in conflict, and experiments showed a small but beneficial effect of this change.
2021-03-04Fix nightlies. (#6048)Aina Niemetz
2021-03-04context_black: Clean up classes. (#6046)Aina Niemetz
This cleans up the MyContext* classes defined for the tests according to the code style guidelines. It further converts non-fixed width integer types to fixed-width types. This was missed in #5587.
2021-03-04New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)Aina Niemetz
This disables the temporarily available internals of Sort.
2021-03-04New C++ API: Clean up usage of internal Result. (#6043)Aina Niemetz
This disables the temporarily available internals of Result. It further changes the interface for getUnknownExplanation, which now returns an enum value instead of a string.
2021-03-03New C++ API: Clean up usage of internal types in Op. (#6045)Aina Niemetz
This disables the temporarily available internals of Op.
2021-03-03Remove obsolete gcc check. (#6041)Gereon Kremer
This PR removes a cmake check for gcc 4.5.1. As this version is more than a decade old and would not work anyway, as it does not fully support C++11, not to mention C++17.
2021-03-03(proof-new) Simplifications to arithmetic operator elimination and ↵Andrew Reynolds
preprocessing (#6040) Due to refactoring in theory preprocessor, which does fixed point preprocessing on created lemmas, several things can be simplified in arithmetic operator elimination. This is required for further simplification to witness forms in the internal proof calculus.
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
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.
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
This PR adds tuple projection operator to the theory of data types. It Also adds helper functions for selecting elements from a tuple.
2021-03-02Remove non-ASCII characters from source files. (#6039)Mathias Preiner
Make collect_tags.py more robust for non-ASCII characters.
2021-03-02Improve handling of utf8 encoded inputs (#5694)Gereon Kremer
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
2021-03-02Remove obsolete dependency on CxxTest. (#6038)Aina Niemetz
2021-03-02Add aarch64 (ARM64) cross-compile support. (#6033)Mathias Preiner
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.
2021-03-02Fix nightly errors. (#6034)Mathias Preiner
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.
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
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.
2021-03-02google test: util: Migrate floatingpoint_black. (#6021)Aina Niemetz
2021-03-01google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)Aina Niemetz
2021-03-01google test: util: Migrate bitvector_black. (#6015)Aina Niemetz
2021-03-01google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)Aina Niemetz
2021-03-01Refactor collection of debug and trace tags (#5996)Gereon Kremer
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.
2021-03-01Make -Werror optional but enable it for CI. (#6032)Mathias Preiner
2021-03-01google test: util: Migrate stats_black. (#6029)Aina Niemetz
2021-03-01google test: util: Migrate real_algebraic_number_black. (#6028)Aina Niemetz
2021-03-01google test: util: Migrate rational_white. (#6027)Aina Niemetz
2021-03-01google test: util: Migrate rational_black. (#6026)Aina Niemetz
2021-03-01google test: util: Migrate output_black. (#6025)Aina Niemetz
2021-03-01google test: util: Migrate integer_black. (#6023)Aina Niemetz
2021-03-01google test: util: Migrate datatype_black. (#6019)Aina Niemetz
2021-03-01google test: util: Migrate configuration_black. (#6018)Aina Niemetz
2021-03-01google test: util: Migrate boolean_simplification_black. (#6014)Aina Niemetz
2021-03-01google test: util: Migrate array_store_all_white. (#6008)Aina Niemetz
2021-03-01google test: util: Migrate integer_white. (#6024)Aina Niemetz
2021-03-01google test: theory: Migrate theory_strings_skolem_cache_black. (#6002)Aina Niemetz
2021-03-01google test: theory: Migrate theory_strings_word_white. (#6003)Aina Niemetz
2021-02-27google test: util: Migrate exception_black. (#6020)Aina Niemetz
2021-02-27google test: util: Migrate check_white. (#6017)Aina Niemetz
2021-02-27google test: util: Migrate cardinality_black. (#6016)Aina Niemetz
2021-02-27google test: theory: Migrate theory_white. (#6006)Aina Niemetz
This moves test utils for theory tests to test_smt.h and consolidates two implementations of dummy theories into one.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback