Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-03-03 | More 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-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 obsolete dependency on CxxTest. (#6038) | Aina Niemetz | |
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 | 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 | 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 | 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 | 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 | |
2021-02-25 | google test: printer: Migrate smt2_printer_black. (#5970) | Aina Niemetz | |
2021-02-24 | Enable -Werror. (#5969) | Mathias Preiner | |
2021-02-24 | google test: theory: Migrate theory_bags_type_rules_white. (#5984) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate theory_engine_white. (#5988) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate theory_black. (#5985) | Aina Niemetz | |
2021-02-24 | Ensure static-learning adds rewritten assertions. (#5982) | Gereon Kremer | |
The static-learning preprocessing sometimes added non-rewritten assertions, despite being used in a part of the preprocessor that assumes all assertions to be rewritten. This may then break other passes further down, in the case of #5729 the non-clausal simplification which explicitly asserts that assertions are rewritten. This PR rewrites the respective assertion properly in the static-learning pass. Fixes #5729. | |||
2021-02-24 | google test: theory: Migrate sequences_rewriter_white. (#5975) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate theory_bags_normal_form_white. (#5978) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate logic_info_white. (#5973) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate theory_bags_rewriter_white. (#5979) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate theory_arith_white. (#5977) | Aina Niemetz | |
2021-02-24 | google test: theory: Migrate evaluator_white. (#5972) | Aina Niemetz | |