cvc5.git
3 years ago(proof-new) Minor fix and allow proof option (#6085)
Andrew Reynolds [Tue, 9 Mar 2021 19:02:14 +0000 (13:02 -0600)]
(proof-new) Minor fix and allow proof option (#6085)

This is in preparation for enabling CI / proofs on master.

This does not throw an option exception when proofs are enabled, it also makes a fix that was missing on master and needed for regressions to pass on master.

This is partially taken from #5980.

3 years agoNew C++ API: Reorder and clean up cpp file. (#6086)
Aina Niemetz [Tue, 9 Mar 2021 18:00:47 +0000 (10:00 -0800)]
New C++ API: Reorder and clean up cpp file. (#6086)

3 years agoAdd missing include if GLPK is enabled. (#6084)
Gereon Kremer [Tue, 9 Mar 2021 14:05:22 +0000 (15:05 +0100)]
Add missing include if GLPK is enabled. (#6084)

Fixes the nightly builds with GLPK.

3 years agoSome more cleanup of includes (#6083)
Gereon Kremer [Tue, 9 Mar 2021 12:48:43 +0000 (13:48 +0100)]
Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

3 years agoUpdate copyright headers to 2021. (#6081)
Aina Niemetz [Tue, 9 Mar 2021 07:27:03 +0000 (23:27 -0800)]
Update copyright headers to 2021. (#6081)

3 years agoNew C++ API: Migrate to Node layer. (#6070)
Aina Niemetz [Tue, 9 Mar 2021 00:59:35 +0000 (16:59 -0800)]
New C++ API: Migrate to Node layer. (#6070)

The following items will be added / adressed in subsequent PRs:

* migrate statistics tracking for variables and bound variables

* migrate adding of listeners when variables and bound variables
  are created

* consistent and clean NodeManagerScope handling
  (out of scope for this PR)

* clean up all interfaces to use const references when possible

3 years agoRefactor ouroborous API test to not use Expr. (#6079)
Aina Niemetz [Mon, 8 Mar 2021 22:48:36 +0000 (14:48 -0800)]
Refactor ouroborous API test to not use Expr. (#6079)

3 years agocontrib: Do not use HOST env variable for cross-compilation host target. (#6078)
Mathias Preiner [Mon, 8 Mar 2021 20:24:41 +0000 (12:24 -0800)]
contrib: Do not use HOST env variable for cross-compilation host target. (#6078)

On some systems HOST is set by default to the host name. This commit adds a --host option for the get-antlr-3.4 and get-gmp-dev scripts. It further simplifies the machine type check in get-antlr-3.4 and updates the GMP version to 6.2.1.

3 years agoFix handling of negation of Boolean bound variables in FMF (#6066)
Andrew Reynolds [Mon, 8 Mar 2021 20:11:24 +0000 (14:11 -0600)]
Fix handling of negation of Boolean bound variables in FMF (#6066)

Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.

3 years agoBuild api tests in build/bin/test/api. (#6076)
Aina Niemetz [Mon, 8 Mar 2021 19:10:14 +0000 (11:10 -0800)]
Build api tests in build/bin/test/api. (#6076)

Previously, api tests where built in build/test/api instead of in the
bin directory for the tests.

3 years ago(proof-new) Separating optimizations for strings skolem caching (#6064)
Andrew Reynolds [Mon, 8 Mar 2021 17:32:43 +0000 (11:32 -0600)]
(proof-new) Separating optimizations for strings skolem caching (#6064)

This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.

These errors were caught by the LFSC proof checker.

3 years ago(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)
Andrew Reynolds [Mon, 8 Mar 2021 17:06:45 +0000 (11:06 -0600)]
(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)

Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms.

Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms.

This PR changes arithmetic in preparation for this change.

Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94.

Note that the indentation of code in operator_elim.cpp changed.

3 years agoSimplify theory preprocessing (#6058)
Andrew Reynolds [Mon, 8 Mar 2021 16:50:39 +0000 (10:50 -0600)]
Simplify theory preprocessing (#6058)

Theory preprocessing now theory-preprocesses lemmas until fixed point. This eliminates the old code for rewriting them only, which is no longer necessary as theory-preprocessing subsumes rewriting.

3 years agoFix justification heuristic again (#6074)
Gereon Kremer [Mon, 8 Mar 2021 14:46:30 +0000 (15:46 +0100)]
Fix justification heuristic again (#6074)

This PR replaces all TNode types in datatypes by Node within justification heuristic.
Fixes #6073.
Unfortunately, the example from #6073 times out now, thus there is no new regression.

3 years agoDo not process conjunctions as facts in strings (#6065)
Andrew Reynolds [Mon, 8 Mar 2021 09:40:05 +0000 (03:40 -0600)]
Do not process conjunctions as facts in strings (#6065)

This changes things so we process inferences with AND conclusions as lemmas always.

This fixes #6056, that benchmark times out.

3 years agoRemove partial UDIV/UREM operators. (#6069)
Mathias Preiner [Sat, 6 Mar 2021 03:28:19 +0000 (19:28 -0800)]
Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

3 years agoRemove SMT-LIB 2.5 and 2.0 support. (#6068)
Mathias Preiner [Sat, 6 Mar 2021 00:17:15 +0000 (16:17 -0800)]
Remove SMT-LIB 2.5 and 2.0 support. (#6068)

This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.

3 years agoSet logic in interpolation unit test. (#6067)
yoni206 [Fri, 5 Mar 2021 20:09:41 +0000 (12:09 -0800)]
Set logic in interpolation unit test. (#6067)

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.

3 years agoInitial implementation of an optimization solver with unit tests. (#5849)
mcjuneho [Fri, 5 Mar 2021 19:51:23 +0000 (11:51 -0800)]
Initial implementation of an optimization solver with unit tests. (#5849)

3 years agogoogle test: Remove obsolete Expr test fixtures. (#6060)
Aina Niemetz [Fri, 5 Mar 2021 14:09:06 +0000 (06:09 -0800)]
google test: Remove obsolete Expr test fixtures. (#6060)

3 years agoReimplement time limit mechanism for windows (#6049)
Gereon Kremer [Fri, 5 Mar 2021 11:37:50 +0000 (12:37 +0100)]
Reimplement time limit mechanism for windows (#6049)

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.

3 years agogoogle test: Remove dependency on ExprManager in type_cardinality_black. (#6061)
Aina Niemetz [Fri, 5 Mar 2021 07:21:08 +0000 (23:21 -0800)]
google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)

3 years agoNew C++ API: Clean up usage of interal datatype classes. (#6055)
Aina Niemetz [Thu, 4 Mar 2021 23:29:00 +0000 (15:29 -0800)]
New C++ API: Clean up usage of interal datatype classes. (#6055)

This disables the temporarily available internals of datatype classes.

3 years agoAdd initial bit-blaster for proof logging. (#6053)
Aina Niemetz [Thu, 4 Mar 2021 22:07:16 +0000 (14:07 -0800)]
Add initial bit-blaster for proof logging. (#6053)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
3 years agoNew C++ Api: Clean up usage of internal types in Term. (#6054)
Aina Niemetz [Thu, 4 Mar 2021 20:07:13 +0000 (12:07 -0800)]
New C++ Api: Clean up usage of internal types in Term. (#6054)

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.

3 years agoAdd proper define for libpoly usage (#6050)
Gereon Kremer [Thu, 4 Mar 2021 19:36:02 +0000 (20:36 +0100)]
Add proper define for libpoly usage (#6050)

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.

3 years agoAdd cmake scripts for iwyu targets. (#6042)
Gereon Kremer [Thu, 4 Mar 2021 19:03:24 +0000 (20:03 +0100)]
Add cmake scripts for iwyu targets. (#6042)

This PR adds some utility targets that simplify the usage of iwyu (include-what-you-use) on our code base.

3 years agoFix nightlies. (#6052)
Aina Niemetz [Thu, 4 Mar 2021 18:49:28 +0000 (10:49 -0800)]
Fix nightlies. (#6052)

3 years agoIgnore isInConflict when adding conflicts (#5995)
Gereon Kremer [Thu, 4 Mar 2021 14:24:21 +0000 (15:24 +0100)]
Ignore isInConflict when adding conflicts (#5995)

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.

3 years agoFix nightlies. (#6048)
Aina Niemetz [Thu, 4 Mar 2021 03:06:53 +0000 (19:06 -0800)]
Fix nightlies. (#6048)

3 years agocontext_black: Clean up classes. (#6046)
Aina Niemetz [Thu, 4 Mar 2021 02:24:00 +0000 (18:24 -0800)]
context_black: Clean up classes. (#6046)

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.

3 years agoNew C++ API: Clean up usage of internal Type/TypeNodes. (#6044)
Aina Niemetz [Thu, 4 Mar 2021 01:58:33 +0000 (17:58 -0800)]
New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)

This disables the temporarily available internals of Sort.

3 years agoNew C++ API: Clean up usage of internal Result. (#6043)
Aina Niemetz [Thu, 4 Mar 2021 01:36:57 +0000 (17:36 -0800)]
New C++ API: Clean up usage of internal Result. (#6043)

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.

3 years agoNew C++ API: Clean up usage of internal types in Op. (#6045)
Aina Niemetz [Thu, 4 Mar 2021 01:17:17 +0000 (17:17 -0800)]
New C++ API: Clean up usage of internal types in Op. (#6045)

This disables the temporarily available internals of Op.

3 years agoRemove obsolete gcc check. (#6041)
Gereon Kremer [Wed, 3 Mar 2021 17:59:43 +0000 (18:59 +0100)]
Remove obsolete gcc check. (#6041)

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.

3 years ago(proof-new) Simplifications to arithmetic operator elimination and preprocessing...
Andrew Reynolds [Wed, 3 Mar 2021 17:25:02 +0000 (11:25 -0600)]
(proof-new) Simplifications to arithmetic operator elimination and 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.

3 years agoMore cleanup of includes to reduce compilation times (#6037)
Gereon Kremer [Wed, 3 Mar 2021 16:50:45 +0000 (17:50 +0100)]
More cleanup of includes to reduce compilation times (#6037)

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.

3 years agoRemove uses of SExpr class. (#6035)
Abdalrhman Mohamed [Wed, 3 Mar 2021 10:28:45 +0000 (04:28 -0600)]
Remove uses of SExpr class. (#6035)

This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.

3 years agoAdd tuple projection operator (#5904)
mudathirmahgoub [Wed, 3 Mar 2021 08:16:32 +0000 (02:16 -0600)]
Add tuple projection operator (#5904)

This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.

3 years agoRemove non-ASCII characters from source files. (#6039)
Mathias Preiner [Tue, 2 Mar 2021 23:22:03 +0000 (15:22 -0800)]
Remove non-ASCII characters from source files. (#6039)

Make collect_tags.py more robust for non-ASCII characters.

3 years agoImprove handling of utf8 encoded inputs (#5694)
Gereon Kremer [Tue, 2 Mar 2021 22:49:29 +0000 (23:49 +0100)]
Improve handling of utf8 encoded inputs (#5694)

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

3 years agoRemove obsolete dependency on CxxTest. (#6038)
Aina Niemetz [Tue, 2 Mar 2021 22:06:38 +0000 (14:06 -0800)]
Remove obsolete dependency on CxxTest. (#6038)

3 years agoAdd aarch64 (ARM64) cross-compile support. (#6033)
Mathias Preiner [Tue, 2 Mar 2021 08:26:29 +0000 (00:26 -0800)]
Add aarch64 (ARM64) cross-compile support. (#6033)

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.

3 years agoFix nightly errors. (#6034)
Mathias Preiner [Tue, 2 Mar 2021 04:18:24 +0000 (20:18 -0800)]
Fix nightly errors. (#6034)

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.

3 years agoIntroduce quantifiers term registry (#5983)
Andrew Reynolds [Tue, 2 Mar 2021 03:37:03 +0000 (21:37 -0600)]
Introduce quantifiers term registry (#5983)

This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.

3 years agoClean up includes to reduce compile times (#6031)
Gereon Kremer [Tue, 2 Mar 2021 00:58:20 +0000 (01:58 +0100)]
Clean up includes to reduce compile times (#6031)

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.

3 years agogoogle test: util: Migrate floatingpoint_black. (#6021)
Aina Niemetz [Tue, 2 Mar 2021 00:07:25 +0000 (16:07 -0800)]
google test: util: Migrate floatingpoint_black. (#6021)

3 years agogoogle test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)
Aina Niemetz [Mon, 1 Mar 2021 23:32:16 +0000 (15:32 -0800)]
google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)

3 years agogoogle test: util: Migrate bitvector_black. (#6015)
Aina Niemetz [Mon, 1 Mar 2021 22:46:53 +0000 (14:46 -0800)]
google test: util: Migrate bitvector_black. (#6015)

3 years agogoogle test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)
Aina Niemetz [Mon, 1 Mar 2021 22:00:51 +0000 (14:00 -0800)]
google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)

3 years agoRefactor collection of debug and trace tags (#5996)
Gereon Kremer [Mon, 1 Mar 2021 21:17:54 +0000 (22:17 +0100)]
Refactor collection of debug and trace tags (#5996)

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.

3 years agoMake -Werror optional but enable it for CI. (#6032)
Mathias Preiner [Mon, 1 Mar 2021 18:36:58 +0000 (10:36 -0800)]
Make -Werror optional but enable it for CI. (#6032)

3 years agogoogle test: util: Migrate stats_black. (#6029)
Aina Niemetz [Mon, 1 Mar 2021 16:40:11 +0000 (08:40 -0800)]
google test: util: Migrate stats_black. (#6029)

3 years agogoogle test: util: Migrate real_algebraic_number_black. (#6028)
Aina Niemetz [Mon, 1 Mar 2021 16:04:01 +0000 (08:04 -0800)]
google test: util: Migrate real_algebraic_number_black. (#6028)

3 years agogoogle test: util: Migrate rational_white. (#6027)
Aina Niemetz [Mon, 1 Mar 2021 15:39:26 +0000 (07:39 -0800)]
google test: util: Migrate rational_white. (#6027)

3 years agogoogle test: util: Migrate rational_black. (#6026)
Aina Niemetz [Mon, 1 Mar 2021 15:08:33 +0000 (07:08 -0800)]
google test: util: Migrate rational_black. (#6026)

3 years agogoogle test: util: Migrate output_black. (#6025)
Aina Niemetz [Mon, 1 Mar 2021 14:46:01 +0000 (06:46 -0800)]
google test: util: Migrate output_black. (#6025)

3 years agogoogle test: util: Migrate integer_black. (#6023)
Aina Niemetz [Mon, 1 Mar 2021 14:02:54 +0000 (06:02 -0800)]
google test: util: Migrate integer_black. (#6023)

3 years agogoogle test: util: Migrate datatype_black. (#6019)
Aina Niemetz [Mon, 1 Mar 2021 13:42:33 +0000 (05:42 -0800)]
google test: util: Migrate datatype_black. (#6019)

3 years agogoogle test: util: Migrate configuration_black. (#6018)
Aina Niemetz [Mon, 1 Mar 2021 13:07:19 +0000 (05:07 -0800)]
google test: util: Migrate configuration_black. (#6018)

3 years agogoogle test: util: Migrate boolean_simplification_black. (#6014)
Aina Niemetz [Mon, 1 Mar 2021 12:44:11 +0000 (04:44 -0800)]
google test: util: Migrate boolean_simplification_black. (#6014)

3 years agogoogle test: util: Migrate array_store_all_white. (#6008)
Aina Niemetz [Mon, 1 Mar 2021 12:22:48 +0000 (04:22 -0800)]
google test: util: Migrate array_store_all_white. (#6008)

3 years agogoogle test: util: Migrate integer_white. (#6024)
Aina Niemetz [Mon, 1 Mar 2021 11:55:20 +0000 (03:55 -0800)]
google test: util: Migrate integer_white. (#6024)

3 years agogoogle test: theory: Migrate theory_strings_skolem_cache_black. (#6002)
Aina Niemetz [Mon, 1 Mar 2021 09:31:23 +0000 (01:31 -0800)]
google test: theory: Migrate theory_strings_skolem_cache_black. (#6002)

3 years agogoogle test: theory: Migrate theory_strings_word_white. (#6003)
Aina Niemetz [Mon, 1 Mar 2021 09:00:46 +0000 (01:00 -0800)]
google test: theory: Migrate theory_strings_word_white. (#6003)

3 years agogoogle test: util: Migrate exception_black. (#6020)
Aina Niemetz [Sat, 27 Feb 2021 03:51:25 +0000 (19:51 -0800)]
google test: util: Migrate exception_black. (#6020)

3 years agogoogle test: util: Migrate check_white. (#6017)
Aina Niemetz [Sat, 27 Feb 2021 02:54:23 +0000 (18:54 -0800)]
google test: util: Migrate check_white. (#6017)

3 years agogoogle test: util: Migrate cardinality_black. (#6016)
Aina Niemetz [Sat, 27 Feb 2021 00:30:39 +0000 (16:30 -0800)]
google test: util: Migrate cardinality_black. (#6016)

3 years agogoogle test: theory: Migrate theory_white. (#6006)
Aina Niemetz [Sat, 27 Feb 2021 00:04:58 +0000 (16:04 -0800)]
google test: theory: Migrate theory_white. (#6006)

This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.

3 years agogoogle test: theory: Migrate type_enumerator_white. (#6007)
Aina Niemetz [Fri, 26 Feb 2021 23:16:57 +0000 (15:16 -0800)]
google test: theory: Migrate type_enumerator_white. (#6007)

3 years agoSome formatting and better tracing in prop engine (#6022)
Haniel Barbosa [Fri, 26 Feb 2021 22:52:15 +0000 (19:52 -0300)]
Some formatting and better tracing in prop engine (#6022)

Miscellaneous changes from proof-new.

3 years agogoogle test: theory: Migrate theory_sets_type_rules_white. (#6001)
Aina Niemetz [Fri, 26 Feb 2021 22:11:49 +0000 (14:11 -0800)]
google test: theory: Migrate theory_sets_type_rules_white. (#6001)

3 years agogoogle test: theory: Migrate theory_sets_type_enumerator_white. (#6000)
Aina Niemetz [Fri, 26 Feb 2021 21:28:22 +0000 (13:28 -0800)]
google test: theory: Migrate theory_sets_type_enumerator_white. (#6000)

3 years agoFix -Werror issues with clang and use clang for debug-cln build. (#6004)
Mathias Preiner [Fri, 26 Feb 2021 20:48:33 +0000 (12:48 -0800)]
Fix -Werror issues with clang and use clang for debug-cln build. (#6004)

This fixes some issues that break the nightly ASAN builds with clang.

3 years agogoogle test: util: Migrate binary_heap_black. (#6012)
Aina Niemetz [Fri, 26 Feb 2021 19:59:38 +0000 (11:59 -0800)]
google test: util: Migrate binary_heap_black. (#6012)

3 years agogoogle test: util: Migrate assert_white. (#6011)
Aina Niemetz [Fri, 26 Feb 2021 19:25:05 +0000 (11:25 -0800)]
google test: util: Migrate assert_white. (#6011)

3 years agoMinor improvement and fix to smt2 printer (#6009)
Andrew Reynolds [Fri, 26 Feb 2021 18:47:05 +0000 (12:47 -0600)]
Minor improvement and fix to smt2 printer (#6009)

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.

3 years agoOptionally permit creation of non-flat function types (#6010)
Andrew Reynolds [Fri, 26 Feb 2021 17:44:23 +0000 (11:44 -0600)]
Optionally permit creation of non-flat function types (#6010)

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)).

3 years agoStore Node instead of TNode (#5993)
Gereon Kremer [Fri, 26 Feb 2021 05:02:43 +0000 (06:02 +0100)]
Store Node instead of TNode (#5993)

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.

3 years ago(proof-new) Fix regular expression unfolding under substitution (#5958)
Andrew Reynolds [Fri, 26 Feb 2021 03:41:27 +0000 (21:41 -0600)]
(proof-new) Fix regular expression unfolding under substitution (#5958)

This case was previously unhandled and exercised by a recently added regression.

3 years agoMove (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)
Gereon Kremer [Thu, 25 Feb 2021 23:46:17 +0000 (00:46 +0100)]
Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)

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.

3 years agoMove slow regressions to regress1 (#5999)
Andrew Reynolds [Thu, 25 Feb 2021 22:40:24 +0000 (16:40 -0600)]
Move slow regressions to regress1 (#5999)

Moves regressions taking >4 seconds (summing all configs) in debug to regress1.

3 years agoDatatypes lemmas: share only external types (#5997)
yoni206 [Thu, 25 Feb 2021 20:36:05 +0000 (12:36 -0800)]
Datatypes lemmas: share only external types (#5997)

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.

3 years agogoogle test: Merge Node(Manager) fixtures. (#5998)
Aina Niemetz [Thu, 25 Feb 2021 19:44:48 +0000 (11:44 -0800)]
google test: Merge Node(Manager) fixtures. (#5998)

3 years agoAdd regression. (#5994)
Gereon Kremer [Thu, 25 Feb 2021 13:34:40 +0000 (14:34 +0100)]
Add regression. (#5994)

This PR adds the test case from #5187 as a regression.
Fixes #5187.

3 years agogoogle test: theory: Migrate theory_bv_white. (#5987)
Aina Niemetz [Thu, 25 Feb 2021 13:07:17 +0000 (05:07 -0800)]
google test: theory: Migrate theory_bv_white. (#5987)

3 years agogoogle test: theory: Migrate theory_bv_rewriter_white. (#5986)
Aina Niemetz [Thu, 25 Feb 2021 12:27:15 +0000 (04:27 -0800)]
google test: theory: Migrate theory_bv_rewriter_white. (#5986)

3 years agogoogle test: printer: Migrate smt2_printer_black. (#5970)
Aina Niemetz [Thu, 25 Feb 2021 11:43:56 +0000 (03:43 -0800)]
google test: printer: Migrate smt2_printer_black. (#5970)

3 years agoEnable -Werror. (#5969)
Mathias Preiner [Thu, 25 Feb 2021 00:26:44 +0000 (16:26 -0800)]
Enable -Werror. (#5969)

3 years agogoogle test: theory: Migrate theory_bags_type_rules_white. (#5984)
Aina Niemetz [Wed, 24 Feb 2021 22:35:22 +0000 (14:35 -0800)]
google test: theory: Migrate theory_bags_type_rules_white. (#5984)

3 years agogoogle test: theory: Migrate theory_engine_white. (#5988)
Aina Niemetz [Wed, 24 Feb 2021 20:25:10 +0000 (12:25 -0800)]
google test: theory: Migrate theory_engine_white. (#5988)

3 years agogoogle test: theory: Migrate theory_black. (#5985)
Aina Niemetz [Wed, 24 Feb 2021 18:24:14 +0000 (10:24 -0800)]
google test: theory: Migrate theory_black. (#5985)

3 years agoEnsure static-learning adds rewritten assertions. (#5982)
Gereon Kremer [Wed, 24 Feb 2021 15:41:49 +0000 (16:41 +0100)]
Ensure static-learning adds rewritten assertions. (#5982)

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.

3 years ago(proof-new) Add proofs for CAD solver (#5981)
Gereon Kremer [Wed, 24 Feb 2021 15:04:59 +0000 (16:04 +0100)]
(proof-new) Add proofs for CAD solver (#5981)

This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.

3 years agogoogle test: theory: Migrate sequences_rewriter_white. (#5975)
Aina Niemetz [Wed, 24 Feb 2021 12:22:21 +0000 (04:22 -0800)]
google test: theory: Migrate sequences_rewriter_white. (#5975)

3 years agogoogle test: theory: Migrate theory_bags_normal_form_white. (#5978)
Aina Niemetz [Wed, 24 Feb 2021 11:17:42 +0000 (03:17 -0800)]
google test: theory: Migrate theory_bags_normal_form_white. (#5978)

3 years agogoogle test: theory: Migrate logic_info_white. (#5973)
Aina Niemetz [Wed, 24 Feb 2021 10:39:00 +0000 (02:39 -0800)]
google test: theory: Migrate logic_info_white. (#5973)

3 years agogoogle test: theory: Migrate theory_bags_rewriter_white. (#5979)
Aina Niemetz [Wed, 24 Feb 2021 09:13:09 +0000 (01:13 -0800)]
google test: theory: Migrate theory_bags_rewriter_white. (#5979)

3 years agogoogle test: theory: Migrate theory_arith_white. (#5977)
Aina Niemetz [Wed, 24 Feb 2021 08:53:23 +0000 (00:53 -0800)]
google test: theory: Migrate theory_arith_white. (#5977)

3 years agogoogle test: theory: Migrate evaluator_white. (#5972)
Aina Niemetz [Wed, 24 Feb 2021 08:17:55 +0000 (00:17 -0800)]
google test: theory: Migrate evaluator_white. (#5972)