cvc5.git
3 years ago(proof-new) Replace witness form by original form in the internal proof calculus...
Andrew Reynolds [Wed, 10 Mar 2021 13:33:49 +0000 (07:33 -0600)]
(proof-new) Replace witness form by original form in the internal proof calculus  (#6051)

This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".

This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.

In this PR, the main changes:

The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.

3 years agotest: Fix missing std::. (#6096)
Mathias Preiner [Wed, 10 Mar 2021 00:32:40 +0000 (16:32 -0800)]
test: Fix missing std::. (#6096)

3 years agoNew C++ Api: Use const ref for arguments when possible. (#6092)
Aina Niemetz [Tue, 9 Mar 2021 23:10:40 +0000 (15:10 -0800)]
New C++ Api: Use const ref for arguments when possible. (#6092)

3 years agoMerge initialization steps in TheoryModelBuilder (#4901)
Andrew Reynolds [Tue, 9 Mar 2021 22:31:38 +0000 (16:31 -0600)]
Merge initialization steps in TheoryModelBuilder (#4901)

Currently when constructing models, we traverse the equality engine of the model 3 times during initialization. This PR merges these 3 traversals.

This refactoring is necessary to update model building for the "centralized" approach for equality reasoning, where it will be important to traverse the equality engine of the model in a careful way (to skip irrelevant terms).

The PR also makes a few minor optimizations for e.g. reducing map lookups, and adds more documentation.

3 years agoRemove logic request (#6089)
Andrew Reynolds [Tue, 9 Mar 2021 22:07:30 +0000 (16:07 -0600)]
Remove logic request (#6089)

This removes use of the logic request utility.

It generally bad practice to change the logic dynamically, e.g. during preprocessing, since it makes it so that CVC4 does not properly initialize. We now insist that logic is changed upfront in set_defaults.

This is in preparation for the smt::Env class, which will change the ownership of logic.

3 years agoNew C++ Api: Migrate stats collection for consts, vars, terms. (#6090)
Aina Niemetz [Tue, 9 Mar 2021 21:44:06 +0000 (13:44 -0800)]
New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)

3 years agoContextObj::destroy(): Guard against invalid use. (#6082)
Aina Niemetz [Tue, 9 Mar 2021 20:59:13 +0000 (12:59 -0800)]
ContextObj::destroy(): Guard against invalid use. (#6082)

We do not allow that a context object is invalid on destruction.
This guards against invalid use as described in #2607. Note that #2607
proposed to skip invalid objects on destruction. We now rather do not
allow for such a case to occur at all.

3 years agoNew C++ Api: Clean up usage of internal kind. (#6087)
Aina Niemetz [Tue, 9 Mar 2021 20:11:35 +0000 (12:11 -0800)]
New C++ Api: Clean up usage of internal kind. (#6087)

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)