summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2021-02-26google test: theory: Migrate type_enumerator_white. (#6007)Aina Niemetz
2021-02-26Some formatting and better tracing in prop engine (#6022)Haniel Barbosa
Miscellaneous changes from proof-new.
2021-02-26google test: theory: Migrate theory_sets_type_rules_white. (#6001)Aina Niemetz
2021-02-26google test: theory: Migrate theory_sets_type_enumerator_white. (#6000)Aina Niemetz
2021-02-26Fix -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-26google test: util: Migrate binary_heap_black. (#6012)Aina Niemetz
2021-02-26google test: util: Migrate assert_white. (#6011)Aina Niemetz
2021-02-26Minor 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-26Optionally 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-25Store 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-26Move (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-25Move slow regressions to regress1 (#5999)Andrew Reynolds
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
2021-02-25Datatypes 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-25google test: Merge Node(Manager) fixtures. (#5998)Aina Niemetz
2021-02-25Add regression. (#5994)Gereon Kremer
This PR adds the test case from #5187 as a regression. Fixes #5187.
2021-02-25google test: theory: Migrate theory_bv_white. (#5987)Aina Niemetz
2021-02-25google test: theory: Migrate theory_bv_rewriter_white. (#5986)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback