New C++ Api: Comprehensive guards for member functions of Datatype classes. (#6141)

[proof-new] Adding a dot printer for proof nodes (#6144)

Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).

Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>

New C++ Api: Move checks to separate file. (#6138)

New C++ API: Rename TRY CATCH macros. (#6135)

Schedule preregistration lemmas to be satisfied after user assertions (#6134)

Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>

cmake: Remove install rules for old API headers. (#6120)

(proof-new) Miscellaneous sync to master (#6129)

Towards having proofs working on master.

[proof-new] Fix arity check when building equality engine proofs  (#6133)

Broken in dc679ed.

Add missing includes for statistics (#6124)

Simplify instantiation match generator interface (#6121)

Add more unit tests for api::Sort. (#6122)

ci: Replace debug builds with assertion enabled production builds. (#6098)

This will help reduce the CI times and ccache sizes.

Make linear arithmetic use its inference manager (#5934)

This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.

arith proof rules shuffle & add ARITH_SUM_UB (#6118)

Preparation for making ARITH_SCALE_SUM_UB a macro.

Adds a proof rule for summing upper bounds: ARITH_SUM_UB.
Moves ARITH_MULT_* rules from the non-linear extension to the main
arithmetic checker, since they will be needed for all of arith now.
Aligns the ARITH_SCALE_SUM_UB documentation with its checker.

Introduce inference ids for quantifier instantiation (#6119)

This makes quantifiers use standard inference ids.

This eliminates the need to track ad-hoc statistics, per instantiation type.

This makes minor modifications to a few interfaces in quantifiers to enable this.

First refactoring of statistics classes (#6105)

This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.

Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.

Delete Expr layer. (#6117)

Improvements and refactoring for enumeratative strategy (#6030)

Refactoring out the code from  `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.

Signed-off-by: mikolas <mikolas.janota@gmail.com>

(proof-new) Clean up uses of witness with skolem lemmas (#6109)

This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.

It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.

Direct lemmas and inference ids for sygus extension (#5960)

This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.

Fix compile warnings when compiling with GLPK. (#6115)

Fixes -Wshadow and -Wsuggest-override wranings.

Remove obsolete test/api/statistics.cpp. (#6116)

This test shouldn't be an API test and is not portable to the new API
right now statistics are not retrievable via the API. When we add
methods for retrieving statistics to the new API, we'll need thorough
unit tests this, which makes this test obsolete.

Clean up ownership of Datatypes in NodeManager. (#6113)

This is in preparation for deleting the Expr layer.
This further fixes incorrect handling of ownership for the datatypes
owned by the NodeManager.

Refactor Node::getOperator() to fix compiler warning. (#6110)

Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)

Ensures that all checks are performed in production builds with enabled assertions.

Add GitHub action to automatically update approved PRs. (#6114)

Use Assert instead of assert. (#6095)

This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.

New C++ Api: Add missing argument checks in Solver functions. (#6094)

This adds missing checks to guard that Term and Sort arguments are
associated with the solver object that is called.

Add Env class (#6093)

This class contains all globally available utilities for internal code.

Improved handing of 'lib64' vs. 'lib' for glpk-cut-log and antlr-3.4 (#6091)

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

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