| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-12 | Add more unit tests for api::Sort. (#6122) | Aina Niemetz | |
| 2021-03-11 | Make linear arithmetic use its inference manager (#5934) | Gereon Kremer | |
| This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas. | |||
| 2021-03-11 | First refactoring of statistics classes (#6105) | Gereon Kremer | |
| This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes. It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation. Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete. | |||
| 2021-03-11 | Delete Expr layer. (#6117) | Aina Niemetz | |
| 2021-03-11 | Remove obsolete test/api/statistics.cpp. (#6116) | Aina Niemetz | |
| This test shouldn't be an API test and is not portable to the new API right now statistics are not retrievable via the API. When we add methods for retrieving statistics to the new API, we'll need thorough unit tests this, which makes this test obsolete. | |||
| 2021-03-11 | Refactor Node::getOperator() to fix compiler warning. (#6110) | Aina Niemetz | |
| 2021-03-10 | Use Assert instead of assert. (#6095) | Mathias Preiner | |
| This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions. | |||
| 2021-03-10 | Move ExprManager::isNAryKind to NodeManager. (#6107) | Aina Niemetz | |
| This also renames metakind::getLowerBoundForKind and metakind::getUpperBoundForKind for consistency. Note that the NodeManager class needs to be reordered to comply to our style guidelines. This PR does not reorder but introduces a public block at the top (where the rest of the public interface of the class should go eventually). | |||
| 2021-03-10 | cmake: Fix optimization level for debug builds. (#6097) | Mathias Preiner | |
| Further cleans up some unused variables and moves the configuration of best to configure.sh. | |||
| 2021-03-10 | Fix extended equality rewrite involving replace. (#6104) | Andrew Reynolds | |
| Fixes #6075. | |||
| 2021-03-10 | Fix term registration and non-theory-preprocessed terms in substitutions (#6080) | Andrew Reynolds | |
| This fixes two issues for preprocessing: (1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to. (2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing. To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing. These two fixes are required to fix #6071. Note: we should performance test this on SMT-LIB. | |||
| 2021-03-10 | Add quant elim regression (#6103) | Andrew Reynolds | |
| Fixes #5658. This was fixed by recent refactoring to quantifier elimination, adding the regression to close the issue. | |||
| 2021-03-10 | test: Fix missing std::. (#6096) | Mathias Preiner | |
| 2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz | |
| 2021-03-08 | Refactor ouroborous API test to not use Expr. (#6079) | Aina Niemetz | |
| 2021-03-08 | Fix handling of negation of Boolean bound variables in FMF (#6066) | Andrew Reynolds | |
| Fixes #5922. We were not correctly handling when a Boolean bound variable was negated. | |||
| 2021-03-08 | Build api tests in build/bin/test/api. (#6076) | Aina Niemetz | |
| Previously, api tests where built in build/test/api instead of in the bin directory for the tests. | |||
| 2021-03-05 | Remove partial UDIV/UREM operators. (#6069) | Mathias Preiner | |
| This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total. | |||
| 2021-03-06 | Remove SMT-LIB 2.5 and 2.0 support. (#6068) | Mathias Preiner | |
| This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6. | |||
| 2021-03-05 | Set logic in interpolation unit test. (#6067) | yoni206 | |
| The logic QF_LIA was not set in the api interpolation test. Setting it brings the solving time from ~37s to ~2s. Also, a comment is fixed. | |||
| 2021-03-05 | Initial implementation of an optimization solver with unit tests. (#5849) | mcjuneho | |
| 2021-03-05 | google test: Remove obsolete Expr test fixtures. (#6060) | Aina Niemetz | |
| 2021-03-05 | google test: Remove dependency on ExprManager in type_cardinality_black. (#6061) | Aina Niemetz | |
| 2021-03-04 | Fix nightlies. (#6052) | Aina Niemetz | |
| 2021-03-04 | Fix nightlies. (#6048) | Aina Niemetz | |
| 2021-03-04 | context_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-04 | New 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-03 | New C++ API: Clean up usage of internal types in Op. (#6045) | Aina Niemetz | |
| This disables the temporarily available internals of Op. | |||
| 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 | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback