[proofs] [alethe] Fix Alethe post-processor (#8525)

Previously the Alethe post-processor was merging subproofs, which should not be done at this stage. As a consequence some post-processed proofs were becoming open.

Start post-release for 0.0.10

Bump version to 0.0.10

Internal simplifications to constructing datatypes (#8519)

In preparation for #8511.

This makes it so that unresolved sorts are automatically inferred when constructing datatypes at the NodeManager level. This is in preparation for simplifying the API.

Changes:
(1) NodeManager is cleaned so that unresolved types are automatically inferred and are not a part of its public interface. Internal code generating datatypes is simplified as a result.
(2) Adds necessary utilities to TypeNode and cleans an unused flag
(3) The parser is cleaned to not track unresolved sorts in an ad-hoc manner.
(4) The API is patched to use the simpler interface.

Fix pypi packaging trigger again (#8512)

Further workflows are not triggered when the GITHUB_TOKEN is used. This PR creates new releases using the ACTION_USER_TOKEN instead.

[proofs] [doc] Minor changes to general proofs page, some changes to Alethe page, added DOT page (#8501)

Remove decorator from python API (#8505)

This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.

[API] Add mode argument for `Solver::blockModel()` (#8521)

This commit changes Solver::blockModel() to take a mode as an argument
instead of relying on an option.

Remove `UnknownExplanation::NO_STATUS` (#8518)

Result already supports storing a NONE result, so
UnknownExplanation::NO_STATUS seems redundant. This removes that
explanation, which was only being used in the optimization solver.

Fix javadoc custom tag warning (#8502)

Fix this warning
Note: Custom tags that could override future standard tags:  @apiNote. To avoid potential overrides, use at least one period character (.) in custom tag names.

docs: Add documentation for modes. (#8509)

Python api: Various fixes in docs. (#8480)

[API] Remove redundant version of `mkFunctionSort` (#8503)

mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.

Fix sygus-inst when combined with bounded string quantifiers (#8500)

Strings introduces bounded quantified formulas for reasoning about extended functions. We should not process these with sygus-inst.

Fixes #8497.

api: Swap arguments of declareSygusVar. (#8499)

Make it consistent with other declare*/define* functions.

api: Use std::optional for symbols in mk* functions. (#8495)

Makes all symbols in mk* functions optional.

make-release: Change instructions for pushing tag.

Start post-release for 0.0.9

Bump version to 0.0.9

Also run on created. (#8506)

The way we now create releases apparently does not trigger the release::published event. It should trigger the release::created event, though.

Add documentation for sequences (#8496)

Added documentation for sequences.

Fix bag example links (#8504)

Handled quoted symbols in indexed operators (#8491)

Fixes https://github.com/cvc5/cvc5/issues/8489.

The SMT-LIB standard says that symbols and quoted symbols are identical page 24: `This means for instance that abc and |abc| are the same symbol.`.  We did not parse quoted symbols in indexed operators, this fixes the issue.

Various fixes related to isDatatypeXXX checks. (#8473)

Sort, TypeNode: Rename functions related to datatypes. (#8472)

Disable minisat variable elimination when a parametric theory is present (#8487)

Fixes cvc5/cvc5-projects#506.

It seems there are extremely few cases where it is safe to use this option.

Remove examples that use the old API (#8486)

This removes examples that use the old API and the parser. They were not
currently being compiled and we can reintroduce them if we need
them/have a new parser API.

api: Remove warning for Sort::instantiate(). (#8475)

Do not export dt.size (#8483)

This kind is hardcoded only to work for sygus. I am not sure we want to support general constraints over it, or even if the token dt.size is the appropriate one.

Also adds a missing experimental warning that I had missed.

Fixes cvc5/cvc5-projects#504.

Fix check for whether PI is reduced (#8485)

Fixes cvc5/cvc5-projects#505.

Also fixes a counter-intuitive behavior where 0 was not considered reduced and does minor cleanup.

ci: Fix typo in update-pr job. (#8492)

Improve documentation for Statistics in C++ API (#8476)

This PR improves the documentation of the Statistics and the Stat class in the C++ API.

[proofs] Adding post-visit processing to proof node updater (#8431)

Previously in the proof node updater only structural reasoning was done at post-visit time (merging subproofs, checking free assumptions). This commit adds a virtual method to allow updating the proof node at post-visit time.

In particular this commit is important to functionality in the alethe post processing that is deactivated in master.

CC @Lachnitt

Remove support for Python 2.x (#8488)

This removes support for Python 2.x. We haven't been testing it and
there isn't a good reason to support it.

Add examples/bags.cpp (#8463)

Fix Java examples (#8484)

This fixes the Java examples. The examples were not able the find the
`cvc5::cvc5jar` target because the namespace had accidentally been
changed to `cvc5::internal::` in commit
bbcd471ed40c813c48957ced5596471cc0ccebe9. This reverts that change.

Fix lower vs upper bound issue for eager RE conflicts (#8482)

Fixes #8481.

Install necessary packages (#8479)

We use beautifulsoup to generate the version selector of the release documentation. This PR makes sure all necessary dependencies for this script are installed.

Only run update-pr for normal commits on main (#8478)

Doing a release (or generally pushing two commits at the same time) can trigger a race condition in the update-pr action that technically fails the CI workflow. This PR only runs this action for normal commits, in particular it does not run it for releases (which is the common case where we push multiple commits at once). To be sure, it also puts all update-pr jobs into a concurrency group that enforces sequential execution.

Improve documentation for OptionInfo (#8474)

This PR improves the documentation for OptionInfo and adds documentation for the DriverOptions class.

Move Java package to `io.github.cvc5` (#8469)

Previously, we were using io.github.cvc5.api to mirror the C++
namespace that the API was in. The namespace of the C++ API changed to
simply cvc5 and so this commit updates the Java package accordingly.

[proofs] [doc] Documenting arrays, bit-vectors, datatypes and quantifiers rules (#8465)

[proofs] [doc] Document equality rules (#8462)

docs: Remove api namespace. (#8455)

Fix non-termination in the strings rewriter (#8438)

Fixes #8434.

This makes our component containment utility less aggressive. This impacts (seldom used) rewrites for indexof and replace only.

api: Mark experimental kinds. (#8464)

Start post-release for 0.0.8

Bump version to 0.0.8

ci: Do not cancel jobs on main branch. (#8471)

This will prevent that jobs on the main branch get cancelled when new PRs are merged in before the previous ones finished on main.

Fix case of Boolean skolem for ground term E-matching (#8447)

Work towards fixing the second issue on cvc5/cvc5-projects#487, which now gives the same error as #8347.

ci: Update older PRs first. (#8477)

api: Remove isUninterpretedSortParameterized from header file. (#8470)

Method was removed in #8425.

Allow for multiple (equal) base model values (#8467)

This PR weakens an assertion about multiple model values in the same equivalence class. We now accept multiple base model values in the same equivalence class, as long as they compare equal. This allows to gracefully handle cases where real algebraic numbers fail to realize that they are rational.
Fixes #8414.

Exclude competition build for issue8377-resolve-indexed.smt2. (#8468)

Fixes the nightly competition builds.

Move cvc5::internal::context to cvc5::context. (#8451)

Patch cross reference in Kind.java documentation (#8458)

This PR patches cross reference links in Kind.java comments for now until a proper way is implemented that handles documentation for cpp, python and Java API.

docs: Add bags to list of theory references. (#8461)

api: Add Sort::getUninterpretedSortConstructor(). (#8459)

This further introduces TypeNode::isInstantiatedUninterpretedSort().

Fix policy for purifying arguments of exp (#8416)

This corrects the policy for when to purify exp. It ensures we purify exp whenever the kind is not a variable or constant, instead of when the kind is a transcendental function app. The latter permits problematic terms like (exp (* (exp 1.0) (exp 1.0)).

This also corrects an issue where information for ordering on variables would be skipped if we failed to produce a model value for a single variable, which was the original source of the error on #8415.

It furthermore fixes the PfRule ARITH_TRANS_EXP_APPROX_BELOW, which did not handle non-constant arguments of exp.

Fixes #8415.

Fixes for sygus-inst (#8448)

Fixes two issues:

Symmetry breaking was disabled after latest refactoring of sygus options. This meant that the terms considered by sygus-inst were often redundant.
The instantiation constant attribute is set on evaluation variables. This avoids model-unsoundness issues with sygus-inst, which are caused by using the evaluation variable (itself) in instantiations.
The latter issue was discovered by trying the second issue from cvc5/cvc5-projects#487 with --sygus-inst, where it incorrectly says "sat" after the fix from #8447.

Fixed #8456. Fixes #8457.

Fix subtype issue in cegqi arithmetic (#8440)

Fixes #8410.

Was not properly checking for cases where an Integer variable had a Real term as its solution.

TypeNode: Unify functions to instantiate parametric sorts. (#8449)

This unifies `instantiateParametricDatatype()` and
`instantiateSortConstructor()` into `instantiate()`. It further fixes
how the API calls TypeNode instantation.

[API] Move `UnknownExplanation` to `cvc5_types.h` (#8450)

This also fixes some minor issues in the `parseenums.py` script.

[proof] [doc] Document external proof rules (#8439)

Move cvc5::internal::main to cvc5::main. (#8454)

Add information for cardinality constraint to the Python API (#8444)

This PR complements #8422 by adding a tester and a getter for cardinality constraints to the python API. The corresponding test from solver_black is translated and included.

Adding some missing python API methods and tests (#8441)

This PR adds methods to the python API, as well as tests for the new methods and other tests for existing methods, translated from solver_black.cpp.

Change tuple tokens and update datatypes theory ref (#8420)

Changes tuple_ to tuple. for consistency.

Also fixes the lexer list for smt2 and updates the datatypes theory reference with missing content.

Add LFSC to internal proof checker (#8442)

Similar to ALETHE, this was forgotten. Was not causing issues since --proof-check=eager is not used by default.

Fix some documentation warnings  (#8453)

Rename master branch to main. (#8452)

Show the code for utilities in the docs. (#8387)

This PR adds the code for printing synthesis solutions to the docs. Various other changes are made to increase the consistency between the different bindings.

Signed-off-by: Abdalrhman M Mohamed <abdalrhman-mohamed@uiowa.edu>

TypeNode: Rename isSort() and getSortConstructorArity(). (#8446)

Names of these two functions were slightly confusing with respect to API
terminology. This renames isSort() to isUninterpretedSort() and
getSortConstructorArity() to getUninterpretedSortConstructorArity() for
more consistency and clarity.

Introduce internal namespace and remove api namespace. (#8443)

The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:

cvc5
  ~~ public API
  ::context
  ::internal
  ::parser
  ::main

After this PR it will be:

cvc5
  ~~ public API
  ::internal
      ::context
      ::main
  ::parser

api: Add Sort::getInstantiatedParameters(). (#8445)

This adds a function to retrieve the sort arguments an instantiated
sort has been instantiated with. It further deletes
Sort::getDatatypeParamSorts() and
Sort::getUninterpretedSortParamSorts().

bv-to-int: fix translation of bvneg  (#8437)

The translation of bvneg to integers did not match the comment documenting it, causing #8413 .
This PR fixes the issue and includes the test from #8413 as well as a simpler test.
Fixes #8413 .

Make ensureTermSort private (#8436)

This method was used to correct a limitation in the old API regarding parsing decimals. It should not be a public API method.

Add information for cardinality constraint to the API (#8422)

Python API is not implemented yet, as it requires new infrastructure for returning pairs.

Make ProofNodeManager mkScope more robust (#8435)

This make mkScope more robust in two ways:

- Literals rewritten to true can be justified by MACRO_SR_PRED_INTRO.
- Literals that are rewritten to other non-rewritable free assumptions can also be linked.

This is enough to ensure that current issues with (= t false) vs (not f) are fixed for Boolean arrays.

Add bags.rst (#8432)

Fix issue related to use of Boolean term variable for set/bag choose (#8423)

Fixes cvc5/cvc5-projects#501.

I am considering making this detail internal to SkolemManager to avoid similar issues in the future. However, there are some subtle performance implications in doing so, so this will be addressed later.

[API] Add `{is,get}RoundingModeValue()` (#8429)

It also fixes a wrong entry in s_rmodes_internal.

TypeNode: Refactor get param types handling. (#8428)

This introduces TypeNode::getInstantiatedParamTypes() and deletes
TypeNode::getParamTypes(). This is in preparation for adding
api::Sort::getInstantiatedParameters().

Fix for issue 5925: constant arrays should be nonlinear. (#8430)

Fixes #5925. The "nonlinear" optimization did not take constant arrays into account.

api: Add Sort::isInstantiated(). (#8425)

This further removes Sort::isUinterpretedSortParameterized().

Move `RoundingMode` to `cvc5_types.h` (#8427)

This moves RoundingMode to cvc5_types.h and switches to using the
auto-generated enum bindings. It also fixes the Java-bindings generator
for enums (certain parts were previously hardcoded for Kind) and
extends the unit tests for Solver::mkRoundingMode() to actually check
the value being created.

Mark more methods as experimental (#8426)

Rename get-interpol to get-interpolant. (#8424)

[API] Mark methods as experimental (#8249)

ci: Enable all language bindings for debug build. (#8419)

api: Remove left-over Sort::getUninterpretedSortName from header. (#8421)

[proofs] Alethe: Call Printer (#8408)

The alethe printer was not called on Master.

[proofs] Alethe: Add ALETHE_RULE to builtin proof checker (#8409)

Proofs would fail because the internal proof checker would return null and the alethe check is not trusted.

Fix synth result python unit test (#8418)

Mark solve-bv-as-int as expert. (#8417)

Option not yet stable.

Separating produce-interpols from the mode of interpolant generation (#8326)

In current master, --produce-interpols takes a mode, where "none" is the default mode, in which interpolant generation is not enabled.
This PR makes --produce-interpols a Boolean, and adds a interpols-mode option to determine the mode, similarly to unsat cores.

builtin: Move type rules implementation to .cpp file. (#8407)

api: Rename *SortConstructor* to *UninterpretedSortConstructor*. (#8406)

Fix spurious assertion failure (#8404)

This was wrong when doing sequences of reals and a seq.nth merges with a seq.len.

Fixes cvc5/cvc5-projects#502.

Throw logic exception for set.map (#8403)

Support parsing/rewriting, but not solving currently.