[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.

More minor cleaning of options (#8401)

Removes a few more unnecessary options and moves the location of one.

Fixes for API kind documentation (#8397)

Also renames str.tolower -> str.to_lower, str.toupper -> str.to_upper.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>

Add API unit tests for options (#8339)

This PR adds some unit tests that cover some remaining cases of getOptionInfo() and getDriverOptions().
It also adds some fixes to the java bindings of these methods.

api: Unify mkOp variants. (#8369)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

api: More comprehensive documentation of INTERNAL_KIND. (#8400)

[Parser] Fix resolution of indexed symbols (#8383)

Fixes #8377. Commit 3a97480ffab492f8272ad9c7c192d04b43eeea60 changed how
we handle indexed symbols. In particular, it added the option to resolve
them later when the arguments are known. However, the condition for when
to do this resolution was incorrect: It was applied to _all_ known
indexed symbols and not only the ones that can't immediately be resolved
to a kind. This commit fixes the condition.

api: Remove Sort::isParametricDatatype(). (#8405)

Previously, Sort::isParametricDatatype() returned true for both
instantiated and non-instantiated parametric datatypes.

This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated.

Co-authored-by: ajreynol <andrew.j.reynolds@gmail.com>

[proofs] [sat] Have SAT solver communicate whether it has optimized the assertion level of a clause (#8399)

This way both the SAT proof manager and the Proof Cnf Stream can properly track
proofs for clauses added at assertion levels below their original user level.

This commit, besides some minor tweaks, adds the hooks in the places where
a clause can be created with an optimized level and we need to track:

when the explanation of a propagation is requested
when a clause/lemma is added
when a lemma is added (from the backlog of lemmas added when Minisat was busy)
For clauses derived via resolution, this information is computed directly in the SAT proof manager.

This commit also reverts a change from #7790 where whether to optimize clauses was computed only once for the SAT solver. This cannot be the case because between different check-sat calls the state can change.

Finally, this commit enables proofs for several regressions that were previously incompatible with proofs. Since now proofs are compatible with optimizing the level of clauses during incremental solving, this commit should lead to performance improvements.

Fixes cvc5/cvc5-projects#314

api: Rename kind NULL_EXPR to NULL_TERM. (#8402)

Generate `enum` bindings for Python and Java (#8393)

This commit generalizes the generation of bindings for enums to include
enums in cvc5_types.h. The commit only generates the bindings, but
does not use them yet (e.g., do add an argument to
Solver::blockModels()). The generated Java bindings already respect
the C++ namespace whereas the Python bindings require a minor
restructuring to make the namespaces work (i.e., instead of cvc5kinds,
we should have cvc5.api.kinds).

Update checkSynth and checkSynthNext to return SynthResult (#8382)

Also extends to non-trivial unit test of SynthResult.

Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.

Change output of abduction/interpolation for failed inputs (#8396)

Changes from "none" to "fail" to be consistent with SyGuS standard. Note that this means that we don't know if an abduct/interpolant exists.

[proofs] Alethe: Bug Fix in Cong Rule (#8391)

cvc5 suffered a segfault in the CONG rule because the refl step, e.g. (= v0 v0), was added without the cl connector, e.g. (cl (= v0 v0))

api: Remove  blocks in kinds header. (#8398)

[proofs] [cnf] Utilities to notify and track proofs of optimized SAT clauses in the ProofCnfStream (#8388)

Adds functionality for the TheoryProxy and ProofCnfStream modules to be notified of clauses that were asserted in lower levels than the current one. These clauses have their proofs tracked in the ProofCnfStream via an OptimizedClausesManager object.

Since the SAT solver may optimize the assertion level of propagation
explanations and of added clauses, we need to be able to maintain proofs across
context-popping. Not doing this can lead to open proofs. To do this the Proof
cnf stream uses an OptClausesManager to re-add proofs of facts inserted at
optimized levels.

Future PRs will change the SAT solver to use these notifications.

Fixes related to set defaults for sygus/proofs (#8395)

This ensures we always report that SyGuS is incompatible with proofs. As a result, we require disabling sygus in 2 contexts where it should have been disabled before.

Fix Python API tests (#8392)

Note that we are currently not running API tests on the CI due to the
changes in 23dd064.

api: Refactor kinds documentation. (#8384)

Properly guard commands in the SyGuS API (#8390)

This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.

For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.

This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.

It also adds a unit test for checkSynth.

Recategorize options (#8386)

Fixes for theory reference for datatypes (#8380)

Document proof rules for coverings solver (#8376)

This PR converts the documentation for the proof rules for the coverings solver.

Minor updates for quantifiers options (#8385)

[proofs] [sat] Handle resolution proofs for optimized clauses in incremental (#8389)

The SAT solver may associate, to the result of a resolution, a lower assertion
level than the current one. To be able to produce proofs to such clauses, we
extend the SAT proof manager to track which resolution results were
optimized. Then, when the SAT solver pops, the manager is notified and stores
the proofs for these optimized clauses, so that they can be reinserted when the
user context is popped. The latter is handled by the SAT proof manager's
OptClauseManager attribute.

Document arithmetic proof rules (#8373)

This PR converts the documentation for the arithmetic proof rules, excluding those for transcendentals and coverings.

Standardize more instances of skolems (#8351)

This is work towards limiting our usage of witness terms for skolems.

It standardizes witnessing of disequalities for sets, bags, and arrays in the appropriate way that uses mkSkolemFunction(...) instead of mkSkolem(...).

[sat] Add option to disable Minisat simplifications (#7992)

Useful to better control behavior, specially in terms of how the solver performs
when these simplifications (mainly variable and clause elimination) are
disabled, e.g. with incremental and/or proofs.

Also renames the previously confusing "--minisat--elimination" option, which
only refers to variable elimination, a subset of the Minisat simplifications.

Moreover deletes an old comment which no longer applies.

Fix a couple of parse error messages for sygus (#8381)

[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)

Previously when producing sat proofs for unsat cores (no theory proofs) theory lemmas were becoming open leafs in the final proof, breaking the invariant that only inputs should be so. This commit guards against this by justifying these lemmas with a THEORY_LEMMA step.

Fixes cvc5/cvc5-projects#468

Clean options (#8309)

Deletes many unnecessary options, cleans some documentation, consolidates several options.

Add API unit tests for statistics (#8341)

This PR adds some unit tests that cover getStatistics() and the api::Stat class.

Add SynthResult to the API (#8370)

Does not modify the code to return a SynthResult yet, just adds the class.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>

Add `getOptionInfo()` and `getOptionNames()` to python API (#8342)

These extended options operations were still missing from the python API and are added with this PR. To simplify the integration (and also provide a reasonably pythonic interface) we return a dictionary from getOptionInfo() instead of exposing a std::variant-like interface.
The PR also includes the corresponding unit tests.

Document proof rules for transcendentals (#8375)

This PR converts the documentation for the proof rules for the transcendental reasoning in the arithmetic solver.

Make IDOF_MAX rewrite only apply when all children are constant (#8363)

Fixes #8346.

Only update latest tag if commit changed. (#8379)

Previously the latest tag was always updated when a new binary was added to a release (i.e. 3 updates per commit). This commit ensures that we only update the tag if the commit sha changed.

Add internal synth result class (#8352)

This is in preparation for refactoring the return values of several API methods.

Run gen-versioninfo unconditionally (#8368)

This fixes an issue where the output of `--show-config` would not be updated properly in certain cases (e.g., when files were modified but cmake is not run). We now run the `gen-versioninfo` target unconditionally, always updating the `versioninfo.cpp` where the version data for `--show-config` is stored.

Store latest builds in a special release (#8337)

This PR refactors our current github ci action that takes care of storing binaries for releases. It now stores binaries both in the current release (if we are in a release build) or attaches them to a special latest tag. For any regular build on the master branch, it moves the latest tag to the current commit, weeds out the current assets attached to that latest release and adds the current binary. This makes sure we always have the equivalent of our current nightly builds in one place.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

Remove dependency on build (#8367)

We automatically update PRs that can be merged automatically in the CI on master. This PR makes it so that this update is done immediately, not only after the CI has run successfully for master.
As we only merge to master if CI works, CI failures on master should only be glitches or issues with the CI itself.
This allows to merge stuff to master twice as fast when using the auto-merge feature.

update SET_COMPREHENSION documentation (#8372)

Initial documentation on LFSC (#8365)

Fix cvc5-projects issue 497 (#8331)

Fixes cvc5/cvc5-projects#497

Fix non-termination issue in sygus enumerator (#8340)

This ensures that the sygus enumerator does not get stuck in rare cases.

In particular this is important when doing PBE and one of the enumerators (among return/condition enumeration) is out of values. This ensures we break when we fail to increment an enumerator for a type that is required to validate a child enumerator.

Change null terminator for regular expression intersection (#8362)

Refactor proof rule documentation (#8303)

This PR starts to refactor the proof rule comments so that they generate proper sphinx documentation.
It sets up doxygen to include the proof_rule.h, includes some useful configuration for mathjax and provides proper documentation for all core rules and Boolean rules.

Updates for the theory reference for separation logic (#8366)

Make uncovered-api-functions.py exit with 1 if something is not covered (#8360)

This simplifies the integration of this script in CI or buildbot jobs. The idea is to automatically check that the whole API is covered by unit tests, and that the language bindings do the same.

[proofs] Alethe: fixing formatting and adding missing comment (#7779)

update sets-and-relations.rst (#8364)

Add a timeout option for verification of synthesized terms. (#8359)

This PR adds an option to timeout on the verification check for the terms enumerated by the Sygus solver.

[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind  (#8334)

This commit removes the `FLOATINGPOINT_TO_FP_GENERIC` kind, which was
only used in the parser and immediately rewritten by the floating-point
arithmetic solver. It extends the `ParseOp` class to handle indexed
operators of which we do not know the kind (`to_fp` in this case) by
storing the name and the indices. The name is then resolved later when
we have parsed the arguments.

Fixes for witness terms appearing in CEGQI instantiations (#8350)

Fixes #8344.

We now have cases where witness terms e.g. `(witness x : String. len(x) = N)` appear in model values.  These terms require special care in CEGQI.

There are 2 fixes in this PR:
(1) we update our policy on what a legal term is,
(2) we erase annotations from witness terms appearing in instantiations, which is required for ensuring that proofs are consistent.  Otherwise, the skolemization lemma for a witness term does not introduce the same skolem.

Refactor result class (#8313)

This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.

Simplifies the usage of this class throughout the code.

It also changes the API Result method isSatUnknown to isUnknown.

api: Unify mkTerm variants. (#8357)

[API] Support `Op::operator[]` in Java and Python (#8356)

This commit adds support for `Op::operator[]` in Java and Python and
updates all unit tests to be consistent.

Remove `Op::getIndices()` (#8355)

This commit removes `Op::getIndices()`. As discussed offline, the
semantics of that method were confusing and the use cases are covered by
`Op::getNumIndices()` and `Op::operator[]()` (which mirror
`Term::getNumChildren()` and `Term::operator[]()`).

Future changes are going to update the Python and Java bindings to
support `Op::operator[]()`.

Fix return value for candidate rewrite database (#8354)

Currently causes sygus reconstruction to return spurious solutions, due to being justified by candidate rewrites.

Refactor documentation (#8288)

This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command.

Fix LFSC conversion for seq unit (#8353)

Fix names of unit tests (#8338)

We are generally converging to tests names that are identical to their file name relative to the test directory, making running a particular subset of tests via ctest -R reasonably easy. This PR makes sure that the tests in unit/api/cpp also adhere to this schema.

Fix learned literals for top-level AND (#8336)

This is important for a deep restart strategy where substitutions may be consolidated by the preprocessor to a single AND.

Add `getStatistics()` to python API (#8343)

This PR adds Solver.getStatistics() to the python API. To make the usage a bit more pythonic, we do not expose the iterator interface of api::Statistics but instead offer .get() which returns the whole range as a dictionary. The ::get() method to obtain a single statistic value is instead implemented via __getitem__().
The PR also includes the corresponding unit tests.