[proof-new] Clarifying doc (#6108)

Move ExprManager::isNAryKind to NodeManager. (#6107)

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

Improve arithmetic proofs (#6106)

The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.

cmake: Fix optimization level for debug builds. (#6097)

Further cleans up some unused variables and moves the configuration of
best to configure.sh.

(proof-new) Update ppRewrite to use skolem lemmas (#6102)

This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.

As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:

(P (witness ((x T)) (A x)))

now we return:

(P k), with skolem lemma ( (A k), k )

Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.

Fix extended equality rewrite involving replace. (#6104)

Fixes #6075.

Fix term registration and non-theory-preprocessed terms in substitutions (#6080)

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.

Add quant elim regression (#6103)

Fixes #5658.

This was fixed by recent refactoring to quantifier elimination, adding the regression to close the issue.

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

test: Fix missing std::. (#6096)

New C++ Api: Use const ref for arguments when possible. (#6092)

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.

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.

New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)

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.

New C++ Api: Clean up usage of internal kind. (#6087)

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

New C++ API: Reorder and clean up cpp file. (#6086)

Add missing include if GLPK is enabled. (#6084)

Fixes the nightly builds with GLPK.

Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

Update copyright headers to 2021. (#6081)

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

Refactor ouroborous API test to not use Expr. (#6079)

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.

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.

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.

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

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

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.

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.

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.

Remove partial UDIV/UREM operators. (#6069)

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

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.

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.

Initial implementation of an optimization solver with unit tests. (#5849)

google test: Remove obsolete Expr test fixtures. (#6060)

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.

google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)

New C++ API: Clean up usage of interal datatype classes. (#6055)

This disables the temporarily available internals of datatype classes.

Add initial bit-blaster for proof logging. (#6053)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

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.

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.

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.

Fix nightlies. (#6052)

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.

Fix nightlies. (#6048)

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.

New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)

This disables the temporarily available internals of Sort.

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.

New C++ API: Clean up usage of internal types in Op. (#6045)

This disables the temporarily available internals of Op.

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.

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

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.

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.

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.

Remove non-ASCII characters from source files. (#6039)

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

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

Remove obsolete dependency on CxxTest. (#6038)

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.

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.

Introduce quantifiers term registry (#5983)

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

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.

google test: util: Migrate floatingpoint_black. (#6021)

google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)

google test: util: Migrate bitvector_black. (#6015)

google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)

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.

Make -Werror optional but enable it for CI. (#6032)

google test: util: Migrate stats_black. (#6029)

google test: util: Migrate real_algebraic_number_black. (#6028)

google test: util: Migrate rational_white. (#6027)

google test: util: Migrate rational_black. (#6026)

google test: util: Migrate output_black. (#6025)

google test: util: Migrate integer_black. (#6023)

google test: util: Migrate datatype_black. (#6019)

google test: util: Migrate configuration_black. (#6018)

google test: util: Migrate boolean_simplification_black. (#6014)

google test: util: Migrate array_store_all_white. (#6008)

google test: util: Migrate integer_white. (#6024)

google test: theory: Migrate theory_strings_skolem_cache_black. (#6002)

google test: theory: Migrate theory_strings_word_white. (#6003)

google test: util: Migrate exception_black. (#6020)

google test: util: Migrate check_white. (#6017)

google test: util: Migrate cardinality_black. (#6016)

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.

google test: theory: Migrate type_enumerator_white. (#6007)

Some formatting and better tracing in prop engine (#6022)

Miscellaneous changes from proof-new.

google test: theory: Migrate theory_sets_type_rules_white. (#6001)

google test: theory: Migrate theory_sets_type_enumerator_white. (#6000)

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.

google test: util: Migrate binary_heap_black. (#6012)

google test: util: Migrate assert_white. (#6011)

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.

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

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.

(proof-new) Fix regular expression unfolding under substitution (#5958)

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

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.

Move slow regressions to regress1 (#5999)

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

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.

google test: Merge Node(Manager) fixtures. (#5998)