Eliminate a level of nesting of traversals in theory preprocessing (#7345)

This simplifies the theory preprocessor so that it does not rely on the term formula removal to do a nested traversal. Instead, it only relies on its "runCurrent" method.

Notice that this PR essentially replaces TheoryPreprocessor's theoryPreprocess method with TermFormulaRemoval's runInternal method, while adding the required call to rewriteWithProof and preprocessWithProof as post-rewrites. This is far simpler than the previous method, which invoked nested traversals using TermFormulaRemoval::run.

There are two things that will be improved in follow up PRs:

The initial full rewrite step in the theory preprocessor can be merged into the main traversal of theory preprocess (I believe this is why we are slower on nec benchmark than we were previously),
We should eliminate the traversal methods from TermFormulaRemoval altogether, as they are now subsumed by the theory preprocessors main traversal. This will require refactoring how "early ITE removal" works, as this is the only user now of TermFormulaRemoval::run.
Note we should probably performance test this change.

This incidentally fixes #6973, as the previous theory preprocessing code was to blame for that issue.

Remove `Chat()` in favor of new `verbose()` (#7586)

This PR completely removes the first of several logging macros. Instead of Chat(), we now use verbose(2).

Move functions and lambdas from builtin to uf (#7570)

This is in preparation for adding better native support for handling lambdas in the higher-order extension of the UF theory.

We require that LAMBDA and function types belong to theory UF so that the theory solver is properly notified.

This also splits the utility methods for computing whether a function is "constant" to its own file.

This PR is code move only.

[FP] Do not assert that model has shared term (#7585)

Fixes #7569. Currently, the FP solver asserts that
m->hasTerm(sharedTerm) is always true for the real term in the
conversion from real to floating-point value. This is not necessarily
the case because the arithmetic solver computes values for the variables
in the shared terms but not necessarily for the terms themselves. This
commit removes the assertion and instead relies on the fact that a later
assertion checks that m->getValue(sharedTerm).isConst(), which is the
property that we are actually interested in.

Fix some issues with the java api (#7583)

This PR fixes two issues with the java api:
- the JNI_HEADERS variable was set to a non-existent file, which caused the generate-jni-headers target to always rebuilt.
- the directory structure was unnecessarily nested (probably because we use CMAKE_CURRENT_BINARY_DIR instead of CMAKE_BINARY_DIR).

Alethe: Translate CNF rules (#7532)

Implementation of the translation of various CNF rules into the Alethe calculus.

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

Minor changes to circuit propagator (#7584)

Previously in a given part of the code a proof would be retrieved only so that it'd be printed. This commit guards that part of the code with whether the trace is on and gives more information in what is printed.

Also changes the style of a call.

Remove many static calls to rewrite (#7580)

This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.

It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).

Remove quadratic solving in NlModel (#7542)

This PR removes obsolete code from NlModel concerned with solving quadratic equations. This code is only used on nonlinear real problems where the cad solver is not used.

Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)

This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.

Remove a bunch of debugging/logging code from the linear solver (#7576)

This PR removes old debugging code from the linear solver.
The removed code was either redundant, already in comments, or manually disabled by a constant false.

Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)

Fixes #5341.

Improve defaults for sygus default grammars (#7553)

We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.

Replace the old dump infrastructure (#7572)

This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.

This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.

This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.

The other dumping tags are deleted for now, and will be reimplemented as needed.

Start refactoring of `-o` and `-v` (#7449)

This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.

Refactor cmake to build either static or shared (#7534)

This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static.

 Fix links in README.md (#7568)

This PR fixes links to releases and nightly builds. Fixes #7016.

Enable CDCAC solver for selected quantified logics (#7571)

This PR enables the CDCAC solver for quantified logics with reals, but no integers. Also, it disables SyGuS if no integers are used. The regression is a benchmark that is only solved with this new configuration.

Add support for special tag collectors (#7562)

This PR makes the collection of trace and debug tags more flexible by allowing for "special tag collectors". They can be used to inject tags that are not used as constant strings, but only assembled dynamically at runtime.
One example is the set of assertions::pre-X and assertions::post-X tags. They are currently handled by Dump, and will be migrated to Trace.

Minor cleanup in SolverEngine::setInfo() (#7566)

This does a bit of cleanup by properly calling the option handler instead of trying to manually replicating it. This is way more robust in the face of modifications to the option handlers.

Make `Theory::get()` private (#7518)

Now that theories have been refactored to use common interfaces, they
should not access Theory::get() anymore because facts are consumed by
Theory::check().

api: Rename some separation logic functions for consistency. (#7564)

This renames Solver::getSeparationHeap to Solver::getValueSepHeap,
Solver::getSeparationNilTerm to Solver::getSepNil and
Solver::declareSeparationHeap to Solver::declareSepHeap.

@mudathirmahgoub @alex-ozdemir @yoni206

Add unit test to cover previous failure with second solver instance. (#7565)

Fixes #5893.

Enable CI for Junit tests (#7436)

This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.

Fix debug trace for miplib (#7563)

A debug trace on miplib referred to a possibly out of bounds child.

Refactor skolem construction (#7561)

This makes all methods for constructing skolems local to SkolemManager.

It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.

This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.

Formalize more string skolems (#7554)

This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.

Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.

Fix preregistration for floating point theory (#7558)

Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.

Fixes cvc5/cvc5-projects#329.

bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)

When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates.

Fixes the nightly failure.

Move `fmf.card` printing code. (#7559)

The code for printing fmf.card does not run in its current location. This PR moves the code to a different switch statement to ensure that it runs.

Add printing methods for some commands. (#7557)

This PR is a step towards enabling -o raw-benchmark. It adds printing methods for some of the new commands and fixes some other miscellaneous issues.

Improve syntax for fmf cardinality constraints (#7556)

This is an experimental extension of smt2.

Add LFSC signature for quantifiers (#7540)

Also includes a fix for the Boolean signature. After the strings PR and this one, the initial LFSC signature is complete.

Fix setDefaults() for proofs with bitblast-internal. (#7552)

bv: Remove remaining Rewriter::rewrite calls. (#7545)

Make quant elimination robust to presence of other quantified formulas (#7551)

Fixes #4813

Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)

There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter.

Weaken assertion in CEGQI (#7548)

The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.

Fixes #7537.

Add explicit option enum value __MAX_VALUE (#7547)

This PR fixes a subtle issue with the dict ordering changing across different python versions.
To store the flags of -o, we store a bitset with the index being the enum value cast to size_t. To specify the bitset size, we simply used the last enum value (in the toml file). This, however, assumes that the order within dictionaries is stable: toml simply puts all modes in a python dict.
This PR avoids this issue by introducing an explicit __MAX_VALUE enum value. Note that this also avoids the need to update the bitset definition when new output tags are added.

bv: Remove layered solver. (#7455)

This commit removes the old bit-vector solver code.

api: Fix documentation for kind IAND. (#7536)

Fix a couple of issues with uploading docs for releases (#7543)

This PR fixes multiple issues with uploading docs for releases: the regular upload moved the generated docs, so the release upload would not find the docs; the check whether we have a release was incorrect; we probably want $NAME instead of docs-$NAME here.

Clean up CLN includes (#7544)

This PR pushes a couple of includes for the CLN integers from the header into the source files.

Add fuzzing target for murxla (#7490)

This PR aims to make it easier for cvc5 developers to fuzz the current cvc5 working copy with murxla.
It adds a new external project Murxla-EP that builds murxla, linking (only) against cvc5. It depends (indirectly) on the make install target, which is called with a custom install prefix for this purpose.
As the murxla repository is not public yet, automatically downloading it does not work, but instead we need the user to clone it manually for now.
The user should simply execute make fuzz-murxla and follow the instructions.

Fix upwards closure for relations (#7515)

This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms).

It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join.

It disables a regression that times out after these fixes, and does further cleanup.

Replace more static options accesses (#7531)

This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.

Refactor DidYouMean (#7535)

This refactors the `DidYouMean` class, which is used to make helpful suggestions for misspelled tags and options. It uses `std::vector` instead of `std::set`, moves it from `options` to `util` (so that we can keep using it in both libcvc5 and the driver) and generally modernizes the code a bit. Also, it replaces the stand-alone and never executed test by a regular unit test.

api: Add guard against querying value from term with free vars. (#7529)

Fix soundess issue for bags with negative multiplicity (#7539)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
One error was with the rewrite rule (bag.count x (bag x c) = c which did not account for cases when c is negative.
This conflicts with fact that all multiplicities are non-negative.
Another error was that the difference_remove inference rule didn't consider the negative case for (count e B)

(= (count e (difference_remove A B)) (ite (=  (count e B) 0) (count e A) 0))) ; not enough
(= (count e (difference_remove A B)) (ite (<= (count e B) 0) (count e A) 0))) ; the right rule

Remove  assertSkeleton for bag elements during model building   (#7538)

This PR fixes a bug found by cvc5 fuzzy sygus.

Fix proof of nl lemma for a corner case (#7530)

This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.

Start post-release for 0.0.3

Bump version to 0.0.3

Remove options::X__numValues (#7419)

This PR removes yet another special purpose options detail that is only used in a single place: X__numValues currently holds the number of modes for an option, that is the number of elements of the respective enums. It is solely used to obtain the size of the std::bitset used to store the flags passed to the -o option. However, it can easily be replaced using the last mode.

This PR also improves a bit on options-related documentation.

Minor cleanup of proof messages (#7494)

Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.

Fix model construction for higher order involving irrelevant function terms (#7526)

This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.

Add PfRule ARITH_POLY_NORM (#7501)

This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.

Improvements for LFSC proof conversion (#7524)

Includes miscellaneous improvements and fixes to the LFSC proof conversion from proof-new in preparation for CI on master.

Remove static access to options in decision folder (#7527)

This PR replaces static accesses to options (options::foo()) by using the options object provided via the environment.

Fix proof for xor in circuit propagator (#7525)

This PR fixes another double negation issue in the circuit propagator.
Fixes cvc5/cvc5-projects#332.

Combine `--static` and `--static-binary` (#7520)

This PR combines the two configure flags --static and --static-binary into a single --static. Consequently, the two corresponding cmake variables are combined as well. The two variables have been implying each other for some time now and were only used to build not-completely-static binaries for MacOS, which is now done automatically anyway.

[proofs] Fix assertion in EqProof conversion  (#7522)

Also improves a few traces.

Fixes cvc5/cvc5-projects#330

Add support for checking if a `-Wno` flag exists before using it (#7514)

This PR resolves that issue by checking that a -W<error-class> flag exists before trying to use the -Wno-<error-class> flag.

Add a `define-fun` command for each `:named` term. (#7308)

This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.

Properly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)

Fixes one of the issues raised in cvc5/cvc5-projects#331, the other involves missing skolem definitions for str.replace_all_re @4tXJ7f .

This properly guards cases of proof reconstruction for STRINGS_EXTF_EQ_REW where an intermediate step in the proof checker inferring something stronger than what it is asked to prove. In particular, substitution+rewriting is more powerful than congruence+rewriting:
s=x => (str.<= t s) ----> (= r "") since (str.<= t "") ----> (= r "")
but additionally:
(str.<= t s) * { s -> x } ----> true, which is possible if s occurs as a subterm of t.

The proof reconstruction for STRINGS_EXTF_EQ_REW is not precise as there are several other aspects that are not covered. After this PR, we properly guard and fail to reconstruct if the above issue arises, so the assertion failure will not throw.

LFSC signature for linear arithmetic (#7445)

LFSC signature for CNF (#7444)

LFSC signature for Booleans (#7443)

LFSC signature for equality (#7442)

Fix `(set-info <sexpr>)` parsing and printing bugs. (#7427)

Given
```smt2
(set-info :source (0 1 True False x ""))
```
`cvc5` currently prints the command below with `-o raw-benchmark`
```smt2
(set-info : |(0 1 True False x )|)
```
This PR ensures that `cvc5` correctly prints the command by
- Parsing and storing keywords eagerly before parsing their values.
- Removing pre-processing steps done to symbols and string literals.

Remove separate cpp docs for UnknownExplanation (#7516)

This removes the separate documentation for the `UnknownExplanation` enum, as it is already included in the documentation of the `Result` class.

Build shared and static in CI (#7472)

This PR changes our strategy to deal with shared vs. static builds in CI jobs.
All jobs now build cvc5 both shared and static by default. The builds happen in different build directories (build-shared and build-static), and we configure ccache such that these two build directories share a common cache.

Add missing API checks to getValue (#7475)

Fixes cvc5/cvc5-projects#307.

Add comments for arith type rules. (#7488)

Add comments for the arithmetic type rules.

Fixes cvc5/cvc5-projects#273.

Add documentation on output tags (#7499)

This PR adds documentation on how users can use -o. After some offline discussion, we decided it makes sense to generate them automatically in mkoptions.py and also include example outputs.

[Regression Script] Fix use of undefined variables (#7510)

Fixes #7504.

Fix patching for poly on windows (#7513)

This PR is another step to fix our windows nightlies.
It moves the patch steps for libpoly in a separate script. Apparently, it is impossible to properly escape this stuff to work on all platforms and all cmake versions.

Require ITE branches to be first class types (#7508)

Fixes cvc5/cvc5-projects#316.

Fix care graph computation for higher-order (#7474)

Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph.

Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.

Fix model unsoundness for relation join  (#7511)

This fixes a model unsoundness issue in the theory solver for relations.

Python api documentation for sorts (#7440)

This PR adds documentation for the Sort python API.

Avoid non-terminating check with assumptions in strings rewriter (#7503)

These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.

Instead, these rewrites are now moved to the extended rewriter.

Deterministic variables for RE elim (#7489)

Fixes #6766.

Fix mac compile errors in sort.cpp (#7507)

This fixes compile errors in Mac for the java api  where `jlong` means `long long`.

Make --version exit (#7506)

This PR adds the missing handler declaration for the --version option.
Fixes #7505.

Fix libpoly build on windows (#7502)

This PR should finally resolve the current issues with libpoly and windows cross compilation.

[proofs] Fix singleton check in MACRO_RES post-processing (#7498)

Previously the check for whether the original conclusion of the MACRO_RESOULTION step was a singleton was incomplete. Now the test is made the proper way.

Depends on #7497.

Fixes cvc5/cvc5-projects#318

[proofs] Modularize check for whether a clause is singleton (#7497)

Essentially moves the code for this check from the Alethe post-processor. A further PR will include a new use of this method.

[proofs] Reset local var in SatProofManager since incremental exists (#7500)

Fixes cvc5/cvc5-projects#317

Disable automatic symmetry in proofs of theory explanations (#7493)

This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form.

This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories.

Fixes cvc5/cvc5-projects#311.

[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)

Fixes cvc5/cvc5-projects#319

Add regressions for fixed issues (#7495)

Fixes #4656. Fixes #5234. These do not occur on master.

Disable sygus-inst when incremental (#7485)

Fixes #7385.

Option --sygus-inst relies on the quantifier-free sygus extension of datatypes, which does not support incremental mode. Updating it to support incremental is a long term project.

Until this is complete, --sygus-inst should not be run in incremental mode.

[proofs] Alethe: Translate Block of clause pattern rule (#7406)

Implementation of the translation of a number of rules that follow the clause pattern into the Alethe calculus.

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

[proofs] Alethe: Translate AND_INTRO rule (#7405)

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

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

[proofs] Alethe: Translate AND_ELIM rule  (#7404)

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

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

[proofs] Alethe: Translate CONTRA rule (#7403)

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

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

Upload docs for tags to docs-releases (#7415)

This automatically uploads the generated docs to a new repository docs-releases (which should eventually become docs). In contrast to docs-ci, we only store docs for releases there.

Fix frequent rebuild of options target (#7450)

The mkoptions.py script only updates its output files if their content would actually change. This avoid a full rebuild on every run, and makes sure that only parts that actually change are rebuild.
Unfortunately this interacts badly with how cmake/make/... do inter-target dependency tracking.
This PR adds a stamp file options.stamp that is always updated by mkoptions.py and used by cmake as main output.

Fix Configuration::isStaticBuild (#7456)

This PR fixes a minor issue in Configuration::isStaticBuild() which would always return true. Note that CVC5_STATIC_BUILD is always defined via #cmakedefine01 in cvc5config.h.