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

Add regression. (#5994)

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

google test: theory: Migrate theory_bv_white. (#5987)

google test: theory: Migrate theory_bv_rewriter_white. (#5986)

google test: printer: Migrate smt2_printer_black. (#5970)

Enable -Werror. (#5969)

google test: theory: Migrate theory_bags_type_rules_white. (#5984)

google test: theory: Migrate theory_engine_white. (#5988)

google test: theory: Migrate theory_black. (#5985)

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.

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

google test: theory: Migrate sequences_rewriter_white. (#5975)

google test: theory: Migrate theory_bags_normal_form_white. (#5978)

google test: theory: Migrate logic_info_white. (#5973)

google test: theory: Migrate theory_bags_rewriter_white. (#5979)

google test: theory: Migrate theory_arith_white. (#5977)

google test: theory: Migrate evaluator_white. (#5972)

google test: prop: Migrate cnf_stream_white. (#5971)

Add state and inference manager to inst match generator (#5968)

In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.

Add interface to TheoryState for sort inference and facts (#5967)

This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.

This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.

Switch to C++17. (#5959)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

google test: theory: Migrate regexp_operation_black. (#5974)

google test: theory: Migrate strings_rewriter_white. (#5976)

Add proof for mult sign lemma (#5966)

This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.

[proof-new] Fix dangling pointer in SAT proof generation (#5963)

When a clause is being explained, the negation of each of its literals, other than the one it propagates, needs to be explained. This process may lead to the creation of new clauses in the SAT solver (because if a literal being explained was propagated and an explanation was not yet given, it will then be computed and added). This may lead to changes in the memory where clauses are, which may break the reference to the original clause being explained. To avoid this issue we store the literals in the reason before we start explaining their negations. We then iterate over them rather than over the clause, as before.

Add proof for monomial bounds check (#5965)

This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.

(proof-new) Add proof generator for CAD solver (#5964)

This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.

[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)

Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.