Fix/Improve static and shared builds with CLN or Poly (#7306)

We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.

Miscellaneous fixes from proof-new (#7313)

Includes a few fixes for strings and datatypes theory lemma proofs.

Fast exit for string extended equality rewriter (#7312)

In benchmarks with many string equalities between variables and constants, a significant portion of the run time is spent on extended equality rewriting. This adds a fast exit when the equality is between variable/constants only.

Replace doubles by rationals in C++ quickstart (#7317)

This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.

Eliminate more circular dependencies on solver engine (#7311)

This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.

Change behaviour of Term::getRealValue() (#7316)

This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).

Change semantics of dumpUnsatCoresFull (#7314)

This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.

Refactor skolem definitions notifications for the decision engine (#7310)

These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.

This is in preparation for virtual clause deletion.

Enable static builds in CI (#7281)

This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.

Remove timestamped javadoc comments (#7304)

This PR also removes the javadoc timestamps from index.html, which for some reason does not honor the -notimestamp option.

Eliminate more hard coded uses of user context (#7309)

This is in preparation to make the "lemma context" configurable.

Avoid calling `quoteSymbol` multiple times. (#7307)

Calling `quoteSymbol(...)` twice on an empty string `""` returns `"|__|"`.

First round of refactoring on NlModel (#7255)

This PR performs a first refactoring on the NlModel class. It improves model value computation, comparison and stores the model substitutions in a map (instead of two vectors).

Reformulate (#7305)

Finish refactoring on option handlers (#7295)

This PR finishes refactoring on the option handlers.

Add sygus examples to documentation (#7303)

For some reason, we didn't have any SMT-LIB (or rather SyGuS) example files for the SyGuS examples yet.
This PR adds these missing examples.

Various improvements to documentation (#7283)

This PR adds a couple of improvements to our documentation setup
- add an explicit dependency on the extension so that sphinx rebuilds pages appropriately when an extension is modified
- sphinx now emits warnings for examples that are not implemented in all languages (smt2, cpp, java and python)
- add -v to make the sphinx output more log-file friendly
- avoid a warning when the java bindings (and thus java docs) are not build
- replace file(WRITE by configure_file to avoid rather common erroneous rebuilds of python docs
- fix a reference to a label in the python docs
- suppress timestamps in javadoc output to avoid docs-ci being triggered for every PR
- improve placeholder message when java bindings are disabled

Refactor internally generated bounded quantified formulas (#7291)

This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them.  It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself.  This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.

Move isFiniteType from theory engine to Env (#7287)

In preparation for breaking more dependencies on TheoryEngine.

Make decision engine use env (#7300)

No longer build docs by default. Use make docs. (#7296)

This PR changes our policy when to build the documentation. Beforehand, make docs was included in make and make all.
Now, you need to run make docs explicitly.

Eliminating static calls to rewriter in quantifiers (#7301)

Eliminating static calls to rewriter from strings (#7302)

Update java examples using the new Java API (#7225)

This PRs updates java examples using the new Java API, by converting C++ examples to Java.
Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API.
All examples are not included in the build which would be added in a future PR.

Update theory preprocessor to use Env (#7288)

In preparation for making the "lemma context" configurable.

Fix ascription check for return types on ordinary functions (#7290)

Fixes #7274.

Make preregistration safe for uninterpreted constants (#7292)

Work towards addressing #6908.

Remove (apparently obsolete) checks in cms config (#7294)

This removes checks from the CryptoMiniSat config for the existence of a couple of static libraries. Apparently, these are not necessary any more.

Clean options handlers (#7201)

Some cleanup on the option handlers, starting with handlers for base and main options.

Fix some python docstrings which lead to sphinx warnings (#7293)

This PR fixes some docstrings that are not properly indented for sphinx.

Add the LFSC printer (#7158)

This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR.

Further PRs will connect this printer as a possible output format for cvc5.

Add the print benchmark utility (#7196)

This utility is capable of printing a vector of Node as a valid (SMT-LIB) benchmark with no prior bookkeeping. It also optionally allows for taking a vector Node corresponding to define-fun.

It will be used to replace the old internal benchmark dumping infrastructure which was error prone.

Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)

This updates the datatypes rewriter to use the evaluator from Env instead of creating local copies of Evaluator. This makes all uses of the Evaluator dependent on the proper options (e.g. which will be based later on the cardinality of the alphabet for strings).

This moves one utility method (sygusToBuiltinEval) to the datatypes rewriter, as it uses an Evaluator that will be dependent on options.

Notice that this is another instance where it is important for us to make the cache for the rewriter local. The same issue occurs for other places where rewriting is dependent on options. This issue will be revisited when the option for strings alphabet cardinality is added.

Rename SmtEngine to SolverEngine. (#7282)

Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)

This is in preparation for renaming SmtEngine to SolverEngine.

Integrate javadoc documentation  (#7278)

This PR adds the cmake setup to generate javadoc documentation for the java API and integrates it into the sphinx documentation. Right now, we simply link to the javadoc. This PR also modifies a bunch of javadoc comments to use proper javadoc syntax.

configure: Fix --static flag. (#7280)

bv: Refactor ppRewrite and move to TheoryBV. (#7271)

This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules.

Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse.

Refactor our static builds (#7251)

This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).

Properly cache assertions in static learning preprocessing pass. (#7242)

The cache is user-context dependent and guarantees that ppStaticLearn is only called once per assertion in a given context - if assertions are popped from the context and added again ppStaticLearn is called again on that assertion. Further, the preprocessing pass now also handles the splitting of top-level AND terms. Before that each theory was responsible for splitting and caching. Refactoring the corresponding ppStaticLearn theory methods will be part of future PRs.

Marking do-not-merge until cluster runs finished.

Finish the Java Api (#6396)

This commit finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.

Make theory engine modules use Env (#7277)

This updates several core modules of TheoryEngine to use Env and eliminates some getters from TheoryEngine.

Simplify the syntax and representation of the separation logic empty heap constraint (#7268)

Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.

This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.

Remove usage of static options in arithmetic theory (#7221)

This PR removes the usage of static accesses to options from the arithmetic theory, mostly by making more classes inherit from EnvObj.

Print `str.is_digit` and `int.pow2` correctly. (#7276)

[Printer] Only quote `set-info` value if necessary (#7262)

PR #7240 changed the printing of set-info to always include quote the
value. This commit changes the policy to only quote a symbol if
necessary using existing an existing helper method. Otherwise,
(set-info :status sat) is for example printed as (set-info :status |sat|), which is a bit unusual and may break certain scripts.

[API] Update comments w.r.t. SymFPU, fix typos (#7263)

Previously, SymFPU was an optional dependency but it is now required.
The comments in the API were not updated to reflect that. This commit
fixes the comments.

Remove support for extended `(check-sat <term>)` command. (#7270)

This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.

Properly restrict PBE symmetry breaking for abduction queries (#7269)

This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.

It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.

Update the syntax for tuples in smt2 (#7265)

This changes mkTuple -> tuple and tupSel -> tuple_select.

This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.

Add the strings array solver (#7232)

This adds the arrays subsolver utility. It does not yet connect it down to the core array solver, or up to TheoryStrings.

It adds implementation of its lemma schemas for processing nth/update over concat.

Update `--lang=help` (#7260)

Support for the CVC language was removed in #7219 but the help message
for languages was not updated. This removes the mention of CVC from the
help message.

Add Statistics and Stat to the Java API (#7243)

This adds Statistics and Stat to the Java API

remove stuff (#7258)

This PR removes the BUILD_LIB_ONLY cmake option, and the associated --lib-only configure script option.
If you only want the library, just run make cvc5 instead of make.

contrib: Fix check for get-script-header.sh. (#7259)

PR #7219 removed CVC language support and therefore also the file src/parser/cvc/Cvc.g. This commit fixes the check (and the nightlies).

Add Sort.java to the java API (#6382)

This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.

Remove linking against RT (#7257)

This PR removes long obsolete cmake code that is only required when using a pre-2013 glibc.

Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)

There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.

Generalize string enumerator for fixed length sequences (#7234)

This adds a utility to get enumerators for fixed length constants of a given sequence type.

This will be used to construct fixed length gaps in array models.

Eliminate Output macro in favor of simple Env functions (#7223)

This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.

[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)

Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.

[proofs] Alethe: Translate THEORY_REWRITE (#7236)

Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Add Alethe Files to be Compiled  (#7241)

Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled.
During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.

Refactor check interface of nonlinear extension (#7235)

This PR does a first step for refactoring the main check interface of the nonlinear extension. It does not change anything yet, but merely moves code around.

More uses of EnvObj (#7230)

[proofs] Alethe: Translate SCOPE rule (#7224)

Implementation of the translation of SCOPE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Use `|` to print quoted strings in `set-info` command. (#7240)

This PR is a step towards enabling raw-benchmark for cvc5 regressions. cvc5 fails to reparse 57 regressions (in regress0) printed be raw-benchmark because they contain multi-line strings in set-info that we don't print between vertical bars right now. This PR fixes that bug and removes 2 commands (derived from set-info commands) that are not used by the parsers anymore.

Implement alpha equivalence proofs (#7066)

This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.

It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.

Make cegqi subsolvers EnvObj (#7205)

Makes a few places do multiplication for Rational directly instead of invoking the rewriter.

Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

Towards standard usage of evaluator (#7189)

This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.

Construction of Evaluator utilities is now discouraged.

The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.

This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.

Fix solver_black unit test (#7233)

In file `test/unit/api/solver_black.cpp` line 1499,
`for (const std::pair<Term, Term>& t : dmap)` is not the correct way of iterating through the element pairs,
it should be `for (const std::pair<const Term, Term>& t : dmap)` as the keys are immutable.
This triggers a warning on LLVM clang 12.0.1 (not AppleClang) on macOS.

Add extensionality option for strings disequalities (#7229)

Towards the strings array solver.

Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.

arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)

This does not yet clean up the usage of Rewriter::rewrite in the arrays
type enumerator yet. Will be cleaned up in a follow-up PR.

arrays: Move type enumerator implementation to .cpp. (#7216)

This further cleans up the class declaration in the header to comply
with code style guidelines.

Eliminate arithmetic proof macros (#7226)

This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.

Minimal fixing version for tuple update parsing (#7228)

This takes the essential changes from #7218 so that the current ANTLR issues are avoided.

[Proofs] Alethe: Translate ASSUME rule (#7213)

Implementation of the translation of ASSUME rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)

Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

README: Fix link to INSTALL.rst. (#7222)

Fix handling of conversions between FP and reals (#7149)

Fixes #7056. Currently, we introduce a UF for conversions between FP
numbers and reals. This is done as part of `ppRewrite()`. The problem is
that terms sent to `ppRewrite()` are not fully preprocessed yet and the
FP theory solver was storing terms that were not fully preprocessed in a
map for later lookup. For the issue at hand, the conversion term
contained an `ite`, which was later removed. As a result, the theory
solver did not consider the term to be relevant when refining
abstractions. This commit changes the handling of conversion functions
to instead adding purification lemmas for conversion terms when they are
registered. The purification lemmas are needed, because otherwise, we
can't retrieve the model values for the term without the rewriter
interferring.

Start python API Solver documentation (#7064)

[proofs] Alethe: adds a node converter

Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.

Add the LFSC proof post-processor (#7134)

Includes the necessary conversions to LFSC for the core rules of the internal calculus.

TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)

Optionally enable interprocedural optimization (#7209)

This commit adds support for enabling interprocedural optimization. The
option is enabled by default for --best builds and cuts down our
executable size from about 33M to 20M.

Add anchors to cmdline options (#7210)

This PR adds anchors to the auto-generates command line option documentation. This allows to link to specific options from other parts of the documentation.

Fix printer for datatype udpater (#7208)

Refactor tag suggestion mechanism (#7199)

This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead.

Use a single `NodeManager` per thread (#7204)

This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.

One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.

[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)

Added proof postprocessor class to alethe_proof_processor header file.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)

Added final callback class to alethe_proof_processor header file.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Replace write access to options by a local variable (#7207)

This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.

Minor cleanup related to EnvObj (#7206)

This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.

Fix relevant domain for parametric operators (#7198)

Fixes #6531.

This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.

It does some cleanup on relevant domain in the process.

[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)

Added alethe_proof_processor header file and introduced callback class.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Minor changes to E-matching utilities (#7062)

remove options that are no longer used (#7197)

This PR removes a handful of options that are no longer used anywhere.

[proof] Added printer for proof rule names (#7185)

Implementation file for Alethe proof rules.

[proof] Alethe proof rules (#7180)

Adds header for Alethe proof rules

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>