Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-03-03 | Remove 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-03 | Add 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-02 | Remove non-ASCII characters from source files. (#6039) | Mathias Preiner | |
Make collect_tags.py more robust for non-ASCII characters. | |||
2021-03-02 | Improve 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-02 | Remove obsolete dependency on CxxTest. (#6038) | Aina Niemetz | |
2021-03-02 | Add 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-02 | Fix 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-02 | Introduce quantifiers term registry (#5983) | Andrew Reynolds | |
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules. | |||
2021-03-02 | Clean 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-02 | google test: util: Migrate floatingpoint_black. (#6021) | Aina Niemetz | |
2021-03-01 | google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate bitvector_black. (#6015) | Aina Niemetz | |
2021-03-01 | google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989) | Aina Niemetz | |
2021-03-01 | Refactor 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-01 | Make -Werror optional but enable it for CI. (#6032) | Mathias Preiner | |
2021-03-01 | google test: util: Migrate stats_black. (#6029) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate real_algebraic_number_black. (#6028) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate rational_white. (#6027) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate rational_black. (#6026) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate output_black. (#6025) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate integer_black. (#6023) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate datatype_black. (#6019) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate configuration_black. (#6018) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate boolean_simplification_black. (#6014) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate array_store_all_white. (#6008) | Aina Niemetz | |
2021-03-01 | google test: util: Migrate integer_white. (#6024) | Aina Niemetz | |
2021-03-01 | google test: theory: Migrate theory_strings_skolem_cache_black. (#6002) | Aina Niemetz | |
2021-03-01 | google test: theory: Migrate theory_strings_word_white. (#6003) | Aina Niemetz | |
2021-02-27 | google test: util: Migrate exception_black. (#6020) | Aina Niemetz | |
2021-02-27 | google test: util: Migrate check_white. (#6017) | Aina Niemetz | |
2021-02-27 | google test: util: Migrate cardinality_black. (#6016) | Aina Niemetz | |
2021-02-27 | google 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. | |||
2021-02-26 | google test: theory: Migrate type_enumerator_white. (#6007) | Aina Niemetz | |
2021-02-26 | Some formatting and better tracing in prop engine (#6022) | Haniel Barbosa | |
Miscellaneous changes from proof-new. | |||
2021-02-26 | google test: theory: Migrate theory_sets_type_rules_white. (#6001) | Aina Niemetz | |
2021-02-26 | google test: theory: Migrate theory_sets_type_enumerator_white. (#6000) | Aina Niemetz | |
2021-02-26 | Fix -Werror issues with clang and use clang for debug-cln build. (#6004) | Mathias Preiner | |
This fixes some issues that break the nightly ASAN builds with clang. | |||
2021-02-26 | google test: util: Migrate binary_heap_black. (#6012) | Aina Niemetz | |
2021-02-26 | google test: util: Migrate assert_white. (#6011) | Aina Niemetz | |
2021-02-26 | Minor improvement and fix to smt2 printer (#6009) | Andrew Reynolds | |
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. | |||
2021-02-26 | Optionally permit creation of non-flat function types (#6010) | Andrew Reynolds | |
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)). | |||
2021-02-25 | Store Node instead of TNode (#5993) | Gereon Kremer | |
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. | |||
2021-02-25 | (proof-new) Fix regular expression unfolding under substitution (#5958) | Andrew Reynolds | |
This case was previously unhandled and exercised by a recently added regression. | |||
2021-02-26 | Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992) | Gereon Kremer | |
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. | |||
2021-02-25 | Move slow regressions to regress1 (#5999) | Andrew Reynolds | |
Moves regressions taking >4 seconds (summing all configs) in debug to regress1. | |||
2021-02-25 | Datatypes lemmas: share only external types (#5997) | yoni206 | |
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. | |||
2021-02-25 | google test: Merge Node(Manager) fixtures. (#5998) | Aina Niemetz | |
2021-02-25 | Add regression. (#5994) | Gereon Kremer | |
This PR adds the test case from #5187 as a regression. Fixes #5187. | |||
2021-02-25 | google test: theory: Migrate theory_bv_white. (#5987) | Aina Niemetz | |
2021-02-25 | google test: theory: Migrate theory_bv_rewriter_white. (#5986) | Aina Niemetz | |