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.

[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)

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

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

[proofs] Alethe: Translate MODUS_PONENS rule (#7401)

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

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

Add new method for enumerating unsat queries with SyGuS (#7459)

This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).

The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.

It does some minor refactoring of ExprMinerManager to support the new module.

[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)

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

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

Fix spurious checks to closed proofs (#7484)

This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver.

This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.

Java and python unit tests for mkCardinalityConstraint (#7486)

Adds leftover missing unit tests for new API call for mkCardinalityConstraint from eeb78c8.

Fix more missing uses of CDProof::isSame (#7491)

Fixes cvc5/cvc5-projects#306.

Fix support for global declarations (#7480)

Previously, we asserted global declarations as substitutions/formulas just before check-sat. This is not ideal since the current set of assertions can be preprocessed without having knowledge of definitions of defined functions. Moreover, this could lead to model unsoundness if it were the case that a defined symbol was solved during preprocessing.

Fixes #7479. In that example, y was solved for true and then we failed to overwrite y with its definition (> x 0), hence dropping the definition. Now, y is defined as (> x 0) before we preprocess.

Remove HOL/fmf bound messages in set defaults (#7487)

This block is misleading after the last commit.

Add inference for count map (#7264)

Reenable proofs on some regressions (#7483)

[proofs] Alethe: Translate SPLIT rule  (#7399)

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

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

[Regression Script] Support older Python versions (#7482)

This removes two uses of f-strings, which are not supported by Python
<3.6.

Delete redundant file option_Info.cpp (#7477)

Add new eager conflict detection in strings for integer equivalence classes (#7453)

Required to address Zelkova bottlenecks.

This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds.

The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts.

It also changes EqcInfo to store (str.len x) instead of x for length terms.

Remove spurious assertoin (#7458)

Fixes #7439. That benchmark is now "unknown".

Add requires libpoly to regression (#7467)

Required to avoid timeout in non-libpoly builds.

FYI @dddejan .

Refactor java package name from cvc5 to io.github.cvc5.api (#7340)

This PR refactors java package name from cvc5 to io.github.cvc5.api.
It also refactor the names of cpp and java files.

Remove options::X__name (#7414)

This PR removes the static strings options::module::X__name that hold the primary long option name. We used them to figure out which option an handler function was called on for certain handler functions. This was always a weird way, and the past refactorings have eliminated all these cases.
This also removes the need to the two arguments option and flag to all option handlers.

Remove stale pointer to proof node manager from skolemize utility (#7471)

Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).

[proof] Fixing CHAIN_RESOLUTION checker (#7465)

Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain.

Fixes cvc5/cvc5-projects#310

Fix out-of-sync pruning in CDCAC proofs (#7470)

This PR resolves a subtle issue with CDCAC proofs.
The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals.
This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered.

Fixes cvc5/cvc5-projects#313.

Fix another double negation proof issue (#7468)

This PR fixes another subtle proof issue in the circuit propagator concerning negated ites.
Fixes cvc5/cvc5-projects#309.

Remove `--uf-ho` option (#7463)

This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder.

It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.

Fix symmetry issue in theory engine conflicts (#7469)

Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.

Add more abduction regressions (#7461)

Fixes #5848.

This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.

Also introduces subfolder regress/regress1/abduction.

[proofs] Alethe: Translate FACTORING rule (#7398)

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

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

[proofs] Alethe: Translate CHAIN_RESOLUTION rule (#7397)

Implementation of the translation of RESOLUTION and CHAIN_RESOLUTION rules into the Alethe calculus.

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

Make CAD proofs user context dependent (#7466)

Given that arithmetic lemmas can survive the current (sat) context by being buffered in the inference manager, their proofs need to do as well. This PR changes the CAD proofs to be user context dependent.

Fixes cvc5/cvc5-projects#315.

Refactor theory inference manager constructor (#7457)

Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead.

Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV.

Making `IntBlaster` inherit from `EnvObj` (#7431)

This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications.

Do not use global proxy variable attribute for strings (#7460)

Fixes #6180.

Fix memory management of `ErrorInformation` (#7388)

Fixes
https://scan6.coverity.com/reports.htm#v37053/p11644/fileInstanceId=125548448&defectInstanceId=32441274&mergedDefectId=1453884.

Add missing methods to Solver.java (#7299)

A life of solver object was simple before summer. Then it got complicated with getDifficulty, optional proofs getProof, more assumptions addSygusAssume, and finally different options to choose from OptionInfo.
This PR attempts to prepare solver objects for this new life.

Make expression mining use configurable options and logic (#7426)

Required for doing options-specific internal fuzzing using SyGuS.

docs: Use light gray for background on the right. (#7438)

Also fix case of negated ite (#7454)

This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.