bags: Rename kinds with a more consistent naming scheme (#7611)

[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during double SYMM elimination (#7630)

This fixes the potential for cyclic proofs in CDProof when P and (SYMM P) are added as proofs to a CDProof with automatic managing of symmetry.

This manifested as non-termination on the seqArray branch with proofs enabled, instead, if this were to occur, we should throw an error, which is easy to catch.

Fix redundant definitions of `NodeValue::getConst` (#7636)

If multiple kinds have the same payload, cvc5 is currently generating
multiple copies of NodeValue::getConst() with the same template
argument, which results in a redefinition of the same function. This
commit modifies the mkmetakind script to avoid emitting redundant
definitions of NodeValue::getConst().

Add some basic rewrites for regular expression intersection (#7629)

Adds some basic rewrites for re.inter and re.union involving children of the form (str.to_re c) for constants c.

This is towards addressing bottlenecks for Zelkova benchmarks.

Remove `ConstantMap<Rational>` (#7635)

This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.

Various minor docs improvements (#7626)

This PR does a number of minor improvements to the docs.

Add an API method to get the raw name of a term. (#7618)

Generalize front-end checks to check for shadowed variables (#7634)

When using the API, we currently check for free variables in assertions and in terms passed to get-value.

We also require checking for variable shadowing.

This generalizes the utility method so that both free variables and shadowed variables are checked and reported to the user.

Add lazy approach for handling lambdas in the HO extension (#7625)

This adds a new option --uf-lazy-ll for not applying lambda lifting eagerly. This is motivated by HO operators in theory of bags, e.g. bag.map, which cannot answer "sat" for simple problems where lambdas are mapped to bags, due to the introduction of quantified formulas for eliminating lambdas.

It moves lambda lifting from term formula removal to a utility module within TheoryUF. If lazy lambda lifting is enabled, this module does not introduce quantified formulas for lambdas eagerly.

It adds 2 lemma schemas for reasoning about quantifier-free constraints with lambdas natively in TheoryUF. It extends the model construction in the HoExtension to assign lambdas in the case that an equivalence class contains a variable that is defined by a lambda.

Fixes for update/nth over constant sequences (#7631)

This includes fixes related to how we process seq.update / seq.nth applied to sequence constants.

api: Add Solver::mkRegexpAll(). (#7614)

[proofs] Alethe: Translate of Arithmetic rules (#7613)

Implementation of the translation of MACRO_ARITH_SCALE_SUM_UB, INT_TIGHT_UB and INT_TIGHT_LB into the Alethe calculus.

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

[proofs] Alethe: Translate INSTANTIATE rule  (#7607)

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

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

docs: Also create javadoc for generated Kind.java (#7624)

Fix soundness issue of missing premises for count bag lemmas (#7615)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
The error is related to a previous fix which did not include the required antecedent in the two lemmas:

(=>  (= e x)
        (=
              (bag.count e (bag x c))
             (ite (>= c 1) c 0)))

and

(=>  (distinct x e))  (= (bag.count e (bag x c)) 0))

java: Fix building cvc5.jar for cmake 3.16. (#7623)

Fixes #7579.

Fix parsing array constants (#7617)

This generalizes a fix for parsing array constants.

Fixes #7596.

sets: Rename set.intersection to set.inter. (#7622)

This further renames kind SET_INTERSECTION to SET_INTER.

Reorganize test/unit/api directory. (#7612)

This moves .cpp files to directory test/unit/api/cpp and python files in
test/python/unit/api to test/unit/api/python.

[proofs] Alethe: Translate Further Equality rules (#7606)

Implementation of the translation of FALSE_INTRO, FALSE_ELIM, TRUE_INTRO and TRUE_ELIM rules into the Alethe calculus.

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

[proofs] Alethe: Translate Equality rules (#7605)

Implementation of the translation of SYMM, TRANS and CONG rules into the Alethe calculus.

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

Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)

Required for lazy lambdas in HO.

Also properly guards the case when the preprocessing pass is a no-op.

Minor optimizations for term database (#7600)

A few minor optimizations for term database.

Also collects private/public blocks in quantifiers engine.

Clean up ctest configuration and CI test configuration. (#7620)

Previously, on CI, unit tests and api tests were run twice since we use
a ctest exclude rule based on labels (-LE) which includes unit and api
tests, but then run them separately again. This cleans up the CI test
configuration.

Further, unit gtest unit tests were added with gtest_add_tests, which
adds every test of a unit test binary as a single test target to ctest.
In theory, this may speed up testing (because more parallelism) but in
practice it slows it down due to the start up overhead. It also clutters
CI output. This cleans up the gtest configuration to add the gtest unit
tests per test binary rather then per test of a test binary.

[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)

Previously the trivial cycle check only covered the case in which the currently-being-expanded assumption `A` had as its stored proof node `pf` an assumption proof justifying itself. However, it can be the case that `pf` is not an assumption proof, but a proof that nevertheless has `A` as one of its free assumptions. This commit generalizes the trivial cycle check to account for this.

[proofs] Alethe: Translate REORDERING rule (#7533)

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

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

sets: Update theory reference and smt2 examples. (#7602)

Preparation for non-constant lambda models (#7604)

This makes our core model construction amenable to (non-constant) lambdas as assignments to function equivalence classes for higher-order.

We currently only generate almost constant functions for values of functions. After this PR, we allow explicitly provided lambdas as representatives provided by a theory, which will be used by the higher-order extension.

It also makes some improvements to debug check models regarding checking when representatives are equal to their model values.

Make secant points user context dependent (#7567)

This PR fixes an issue where the secant points associated with certain transcendental lemmas were not properly cleared when leaving a user context.
Closes #4694.

Remove redundant rules for generating Java and Python kinds. (#7616)

This PR addresses an issue where the Ninja build generator errors when either Java or Python bindings are enabled. As shown in the error message below, the error occurs because the build.ninja file generated by CMake contains multiple rules for generating OUTPUT and BYPRODUCTS files.

Add LFSC signature for strings (#7523)

This includes the currently supported rules and cases, although it is highly incomplete.

regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)

This renames kinds REGEXP_EMPTY to REGEXP_NONE and REGEXP_SIGMA to
REGEXP_ALLCHAR to match their SMT-LIB representation (re.none,
re.allchar). It further renames api::Solver::mkRegexpEmpty() to
mkRegexpNone and api::Solver::mkRegexpSigma to mkRegexpAllchar.

Remove `CVC5Message` (#7610)

This PR removes the few remaining usages of the CVC5Message() and gets rid of the whole thing.

Remove antlr_tracing.h (#7608)

This PR removes the long obsolete antlr_tracing.h. The file contains an ugly hack to make lexer tracing work for ANTLR 3.2. It has been obsolete since ANTLR 3.3 (April 2011). Note that the code is only enabled with -DCVC5_TRACE_ANTLR, a flag that is never used.

Remove more static option accesses (#7582)

This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.

Remove command-verbosity option (#7581)

This PR removes the command-verbosity option. It is implemented as a weird special case, and nobody seems to use it anyway.

cmake: Use fastcov for generating coverage reports. (#7594)

fastcov is a parallelized gcov wrapper.

Improve rendering of expert options. (#7589)

The way expert-only options have been rendered in the documentation emphasized those options, which is exactly what should not be done. This PR changes the rendering to make those options slightly opaque instead.

expand bag.choose operator (#7481)

This PR expands bag.choose operator as a preprocessing step.
It also refactors the implementation of choose operator for sets

Add lambda lift utility (#7601)

Towards a lazy approach for handling lambdas in the higher-order extension.

sets: Rename kinds with a more consistent naming scheme. (#7595)

This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.

Evaluate cast-to-real operator (#7599)

Fixes cvc5/cvc5-projects#341.

[proofs] Adding NoSubtype node converter to Alethe (#7587)

Initial version. It'll be improved on demand according to new cases that may lead to issues.

[proofs] Method to convert node representation of Alethe rule (#7598)

Integrate java unit tests into ctest (#7593)

This PR properly integrates the java api unit tests into ctest.

Print `unsupported` for unrecognized flags. (#7384)

Fixes #7374.

better traces in node converter (#7590)

Do not use extended rewrites on recursive function definitions (#7549)

Leads to potential non-idempotent behavior in the rewriter.

The issue cannot be replicated on master, but this safe guards this case anyways.

Fixes #5278.

Only run regress0 for static build (#7592)

It is surprisingly tricky to call ctest properly with multiple -LE arguments (and I actually doubt that the CI version of ctest adheres to its documentation). This PR avoid calling make check (which sets -LE regress[3-4] as a default) and calls ctest directly.

Remove `Notice()` in favor of new `verbose()` (#7588)

This PR removes the remaining usages of the Notice() macros and uses verbose() instead.

Disable regress2 test. (#7591)

Fix exclusion criteria for codatatype model values (#7546)

This fixes codatatype model value construction.

Model construction for codatatypes is non-standard since it requires analyzing whether (possibly recursively defined) terms are alpha equivalent to others during model construction. This is currently handled as a special case within the theory model builder. (This should eventually be moved somewhere more appropriate via a new callback to theory).

This fixes the criteria which was too permissive about which values can be used in models. We now exclude values that match the skeleton of representative codatatype terms. Previously we additionally required that the terms were bisimilar.

Fixes #4851.

[proofs] Fix open sat proof (#7509)

Improves how LazyCDProofChain handles cycles, which fixes a particular case triggered by the added regression. Also makes LazyCDProofChain::getProofFor more robust in that when it can't connect the requested fact it yields an assumption proof node.

Fixes cvc5/cvc5-projects#324

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.