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.

Add trans secant proofs. (#5957)

This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.

Explanation of failure for instantiate, use in enumerative instantiation (#5951)

This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly.

This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout.

This is in preparation for further improvements to enumerative instantiation.

google test: preprocessing: Migrate pass_bv_gauss_white. (#5935)

Eliminate raw use of output channel and valuation in quantifiers (#5933)

This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.

Move quantifiers attributes to quantifiers registry (#5929)

This moves the utility class beneath quantifiers registry.

(proof-new) Change proof-new option to proof (#5955)

Also moves several proof-specific options to proof_options.

(proof-new) Add proofs for exponential functions (#5956)

This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.

Require length-in-conclusion form for strings inferences (#5953)

Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.

It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.

Fixes #5940.

Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.

(proof-new) Option to automatically add SYMM steps during proof node update. (#5939)

Required for work on external proof conversions.

[proof-new] Optionally print conclusion in the AST proof (#5954)

Adds an option to optionally print conclusion in the AST proof.

google test: preprocessing: Migrate pass_foreign_theory_rewrite_white. (#5936)

Add the LazyTreeProofGenerator. (#5948)

This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.