More documentation for idiomatic python API (#7798)

Arithmetic, bit-vectors, arrays.

Get getRealOrIntegerValueSign to the API (#7832)

Implement model construction for the array extension of sequences (#7815)

The array solver is still not usable, the only remaining changes from seqArray are to connect the array solver to the strings theory solver via the strategy + the regressions.

api: Rename DatatypeSelector::getRangeSort() to getCodomainSort(). (#7831)

api: Add Solver::mkUnresolvedSort(). (#7817)

This adds a function to create unresolved sorts for mutually recursive
datatpes. This function creates an uninterpreted sort if the arity of
the unresolved sort is 0, and a sort constructor sort otherwise.

Eliminate more uses of CONST_RATIONAL (#7816)

Disable unsat cores for quaternion_ds1_symm_0428.fof.smt2. (#7830)

Avoids timeout for nightly ASAN builds.

Eliminate most static calls to rewrite in quantifiers (#7823)

Fix get-model when sort constructors are present (#7828)

Fixes a spurious error on kind benchmarks.

Note that we don't properly handle instantiated sort constructors currently, which I believe need to be handled as declared sorts when calling getModel.

[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf Stream (#7826)

These will be necessary for upcoming changes to the SAT proof manager and Proof Cnf Stream to handle incremental proofs when optimizing the level of SAT clauses.

api: Add Sort::hasSymbol() and Sort::getSymbol(). (#7825)

Minor fix for print benchmark. (#7821)

Also adds benchmark that triggered this issue.

bv-to-int: use pow2 operator (#7812)

Currently, the int-blaster translates shifts using an ite whose size is the bit-width.
This PR adds an option to use the internal pow2 operator instead.

int-to-bv: fail if one of the arguments has type real (#7810)

This PR generates a failure in int-to-bv in case a real argument is detected as a child of an arithmetic operation.
fixes cvc5/cvc5-projects#348 .

Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com

Add regression bags-of-bags-subtypes.smt2 (#7814)

Explicitly disallow `mkConst(Rational)` (#7818)

The Rational payload can be associated with two kinds (CONST_INTEGER
and CONST_RATIONAL), so we should never call
NodeManager::mkConst(Rational), but instead use
NodeManager::mkConstInt() and NodeManager::mkConstReal(). Currently,
calling NodeManager::mkConst(Rational) silently creates an integer
constant, which is dangerous. This commit makes it a compile-time error
instead.

Ensure match terms are exhaustive in its type rule (#7807)

Fixes cvc5/cvc5-projects#382.

Makes it so that we always fully type check match terms before they are rewritten, which guards potential unsoundness.

api: Fix smt-lib code blocks and math in C++ docs. (#7795)

Add trace to see inferences in final proof (#7813)

Adds -t im-pf to see which inferences occur in the final proof. Must be used with proofs and --proof-annotate.

Eliminate static calls to rewrite in strings (#7803)

Fix cvc5-projects issue 358 (#7804)

This PR fixes issue cvc5/cvc5-projects#358 which is caused by unregistered terms in the equality engine of bags

Add a random Sygus enumerator. (#7782)

This PR adds a Sygus enumerator that generates random terms from a grammar. The size of the terms generated by the enumerator approximates a geometric distribution and can be configured with an option.

Make some undocumented options regular/expert (#7805)

We have some options that are currently "undocumented" for no good reason.
This PR makes them regular or expert options.

Fix issues with tracing builds (#7809)

This PR fixes two issues that were revealed when analyzing decreased performance on trace-enabled builds.
hasIntegerModel() turns out to be a rather expensive method and should thus not be called in a Trace output.
Furthermore, the implementation of Rational::isIntegral() was generally bad because it used getDenominator() (which returns a copy of the denominator as an Integer) instead of directly checking the underlying denominator with equality for zero.

Add switches to toggle eager and inclusion solvers (#7784)

Connecting the core array solver in strings (#7800)

This PR takes most of the remaining changes from the seqArray branch apart from the extension to model construction.

Notably it connects the core array solver to the array solver in strings.

Minor fix for sygus unsat query generator (#7811)

Throw exception for getting value of non-well-founded datatype (#7806)

Fixes cvc5/cvc5-projects#383

Eliminate use of rewrite, CONST_RATIONAL in ArithMSum (#7808)

api: Add note to Solver::mkDatatypeSorts. (#7799)

Distinguishing more uses of CONST_RATIONAL (#7802)

Towards eliminating subtyping Int/Real.

A more efficient implementation for bag.card operator (#7797)

This PR provides a fold like implementation for bag.card operator that does not depends on higher order logic, although it still requires finite model finding.

Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

Fixes and additions for API for parametric datatypes (#7760)

Update Relations.java (#7796)

Improve nonlinear solver (#7787)

This PR does two things:

we remove splitting on shared values
we add variable elimination for the cad-based solver, exploiting equalities present in the input.

Integrate new int-blaster (#7781)

This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.

Tests are updated and added, as well as other minor changes.

Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345
cvc5/cvc5-projects#344
cvc5/cvc5-projects#343

@mpreiner FYI

Fix cvc5-projects issues  #358 and #375 (#7743)

api: Use 'note' constructs for API documentation. (#7794)

This uses '@note' for notes in the C++ API documentation, '.. note::'
for Python, and '@apiNote' for Java.

Reorganize declareDatatype unit tests. (#7767)

Refactor and fixes related to getSpecializedConstructorTerm (#7774)

Fixes cvc5/cvc5-projects#381.

Array-inspired Sequence Solver - Adding the ArrayCoreSolver class and options (#7723)

This pull request adding the ArrayCoreSolver class and the options to turn on the array-inspired sequence solver.

Eliminate more static rewrites (#7786)

This PR eliminates almost all remaining static rewrites from the arithmetic theory.

Some cleanup around trace and debug (#7792)

Some minor cleanup in our output routines. While ScopedDebug and ScopedTrace are never used at all (and don't seem to make much sense considering how we use Debug and Trace), IndentedScope may be useful in some more places.

Mute `define-fun` command generated for named terms. (#7788)

Kind 2 uses print-success option to track cvc5's status after each command. When I added implicit define-fun commands for each named term (needed for raw-benchmark), cvc5 started printing spurious ; success messages. This change ended up crashing Kind 2's driver for cvc5. This PR fixes this issue by muting the results of those implicit define-fun commands.

Allow for wildcards in `-t` (#7791)

This PR extends -t to allow for wildcards: -t nl-ext-*. Internally, these wildcards are replaced by .* and fed into std::regex.

[proofs] Make LazyCDProofChain extend CDProof (#7726)

This commit makes LazyCDProofChain behave more similarly to LazyCDProof, in that it is an object that not only builds a proof to a fact based on lazy steps but also on regular steps that may already have for it.

The motivation for this commit is the upcoming handling of context-dependent proofs in incremental mode, which benefits from a more uniform behavior between CDProof, LazyCDProof and LazyCDProofChain (with the latter two both extending CDProof).

[proofs] Add option to prune inputs from final proof (#7789)

This is useful for example to remove inputs corresponding to definition of symbols, which may be unexpected for some users, like when using named to wrap assertions and generate unsat cores.

Consider polarity in relevance manager (#7768)

This ensures we only consider things relevant if their polarity is compatible with current asserted value.

As a consequence, this makes our computation of get-difficulty more accurate, as well as making Valuation::isRelevant more precise (e.g. for non-linear).

Notice that this fixes a bug in PolarityTermContext as well.

Fix sine symmetry proof (#7783)

This PR fixes an issue in proofs for sine symmetry arising from the proof checker no longer using the rewriter.

Remove a few static access to options in proof code (#7780)

Do not make SyGuS subsolver in unsat state after solving (#7759)

This makes subsolvers answer "unknown" instead of "unsat" when solving SyGuS inputs, by setting unknown when a SyGuS input is solved instead of asserting the negation of the input. Knowing whether the call was successful is simply obtained by calling getSynthSolutions.

This will allow for multiple solutions for the same conjecture.

api: Add note to Sort::getTesterCodomainSort(). (#7776)

test: Remove CDList memory limit test. (#7777)

This test is of little usefulness and has issues with different platforms (mac) and architectures (arm64).

Return bool for lemmaTheoryInference (#7773)

Remove rewrites from iand and pow2 solvers (#7775)

This PR removes some more static calls to the rewriter from the iand and pow2 solvers.

Eliminate rewriter from transcendental solver (#7772)

This PR eliminates all static calls to the rewriter from the transcendental solver. We now either use the rewriter from the Env object or the theory evaluator. For this to work, the evaluator is extended to support division. In some places, the rewriting was removed altogether.

Static options acceses again (#7771)

This PR removes some more static accesses to options from strings and solver engine.

Make several regressions faster (#7769)

This makes several slow regressions faster, mostly by changing options. It changes a strings regression to be faster by making it smaller.

This should avoid timeouts on https://cvc5-buildbot.stanford.edu/.

Fix type rule for datatype updater for parametric sorts (#7762)

Fixes cvc5/cvc5-projects#379.
Fixes cvc5/cvc5-projects#378.

Turn kinds in python API into a proper Enum (#7686)

This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
  (including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
  (Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
  the documentation for kinds from the cpp api to the other apis)

api: Improve documentation for getDatatypeParamSorts(). (#7763)

api: Fix Sort::getDatatypeArity() for non-parametric datatypes. (#7766)

Fixes cvc5/cvc5-projects#380

FP: Remove static call to Rewriter. (#7765)

Improve options tests (#7761)

This PR adds unit tests for a few more corners of the options code.

Remove more static accesses to options (#7764)

This PR removes a bunch of the remaining places where options are accessed statically.

Simpler versioning if release flag is set (#7758)

Following some discussion, this PR introduces a simpler versioning scheme if the CVC5_IS_RELEASE flag is set.
In our regular versioning scheme, the first commit after release x.y.z has the version x.y.(z+1)-dev.1.abcdef0. Some users however may want to apply some patches, and still have cvc5 show the release version.
With this PR, the version printed (if any commits are present since the tag) is x.y.z-modified if the CVC5_IS_RELEASE flag is still true. We always set it to false immediately after the tagged commit, so it does not change the versions printed by mainline cvc5.

Add proof annotation option (#7750)

Adds --proof-annotate which enables a useful stat in which we count the number of times a lemma with a given inference id appears in a final proof.

This can be used to determine which lemma schemas are the most useful for showing a problem unsat.

Fix some java documentation links (#7757)

[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (#7753)

Translation of the ARITH_TRICHOTOMY rule into the Alethe calculus.

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

[proofs] Alethe: Fix Bug in Finalize (#7746)

Assumptions in Alethe are printed as (or F1 ... Fn) but should be treated as if they are printed as (cl (or F1 ... Fn)). Thus, if in the post visit it is checked whether an additional or step is needed this has to be treated as a special case.

Allow sygus in incremental mode (#7756)

This allows the basic use of SyGuS in incremental mode, where constraints can be pushed/popped.

It does not yet support getting multiple solutions for the same set of constraints, which will require more significant changes.

Make data structures in relevance manager SAT-context dependent (#7733)

This PR significantly improves the quality of values in get-difficulty. It fixes several bugs related to get-difficulty, including over-pruning values in ProofManager, and not tracking explanations for certain literals. It also improves performance by tracking justifications in relevance manager in a SAT-context dependent manner.

This is to support difficulty measurements based on lemmas sent at STANDARD effort.

It also adds 2 simple regressions.

A further PR will further improve the quality by being more careful about the relationships between literals and the assertions that entail that they are relevant.

Eliminate more static calls to Rewriter::rewrite (#7755)

Towards support for incremental sygus (#7736)

This makes several key changes to smt::SygusSolver in preparation for incremental mode.

The key idea is to use a subsolver that:

may take multiple check-sat commands for an encoded synthesis conjecture
does not push/pop
is reconstructed when the SyGuS conjecture becomes stale.
This is motivated by 2 use cases of incremental SyGuS:

Where constraints are push/pop, in which case we should start from scratch, since the SyGuS solver uses symmetry breaking techniques that become unsound when new constraints are added.
Where multiple solutions are needed for the same set of constraints, in which the state of the subsolver should be preserved.
This functionality is still guarded by an exception.

A follow up PR will make several further changes to allow for the above use cases.

Eliminate more static calls to Rewriter::rewrite (#7740)

Add bitwise option to IntBlaster (#7721)

This is part of a series of PRs by @yoni206  to add full int-blasting support to the master branch of `cvc5`. This adds support for the bitwise encoding to `IntBlaster`. Future PRs would unify the `bv2int` and `IntBlaster` helper functions.

Fix 32bit issue in sep_log_api test (#7752)

This uses the proper `t.getInt64Value()` getter instead of `std::stoll(t.toString())`, fixing an issue on 32bit platforms.

Add documentation for QuickStart.java (#7730)

Improve java documentation: add QuickStart and a java API overview.

Disable option regression for competition build (#7751)

This disables a regression that checks the didyoumean output for an invalid output on competition builds. On competition builds, we simply print "unknown" instead of shown any exceptions.

Use unique_ptr instead of raw pointers (#7749)

This PR fixes a memory leak when invalid values are supplied to the stream options err, in or out. Whenever opening the stream would fail, we throw an exception and the created (though not properly opened) stream is leaked.
We now properly wrap the streams in unqiue_ptrs directly on creation.

Add regressions for fixed projects issues (#7739)

Fixes cvc5/cvc5-projects#164.
Fixes cvc5/cvc5-projects#172.
Fixes cvc5/cvc5-projects#175.
Fixes cvc5/cvc5-projects#178.
Fixes cvc5/cvc5-projects#181.
Fixes cvc5/cvc5-projects#183.
Fixes cvc5/cvc5-projects#185.

More robust fix for 32bit issues. (#7735)

This PR implements a more robust fix for the 32bit issues with GMP. Relying on mpz_sizeinbase proves to be very tricky for the corner cases. This PR instead does a simple comparison against the min and max values of the respective types.

[proofs] Alethe: Implementation of Process Function (#7745)

Add call to updater and finalizer to process function of the AlethePostProcessor.

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

api: Fix docs for TUPLE_PROJECT. (#7741)

Faster hasing for `cvc5::String` (#7742)

Previously, our hashing algorithm for cvc5::String would create an
std::string representation of the string and then call
std::hash<std::string> on the result. Creating the temporary
std::string is quite expensive and can be avoided by computing the
hash directly on the elements of the vector of characters in
cvc5::String.

This change improves our solving time on an industrial benchmark from
about 59s to 55s.

Fix a few broken links (#7734)

This PR fixes a few broken links in our documentation.

Check constructor is used in APPLY_CONSTRUCTOR (#7737)

Fixes cvc5/cvc5-projects#373.

Proper error for using constructor in multiple datatypes (#7738)

Now gives error cannot use a constructor for multiple datatypes.

Fixes cvc5/cvc5-projects#372.

Add explicit 64bit getters for Integer class (#7728)

This PR addresses a few issues on our 32bit builds. Most importantly, it adds int64_t Integer::getSigned64() and uint64_t Integer::getUnsigned64().

Remove void as possible option type (#7731)

This PR removes the possibility to have void options. While there are (very) few options that may legitimately be considered void (they do not actually hold a value, but merely trigger a handler or predicate), the type being void introduces a number of special cases in the options setup. Their only real benefit was to avoid having data members that would never be used.
As it turns out, though, the same can be achieved by not specifying a name, which already supported as well.

Check docs for broken links before uploading (#7729)

We currently have a few broken links in our documentation. This PR make our CI check for broken links before uploading it. Note that it will not fail any job, so we still need to check the output occasionally for now.

Fixes for sygus-rr-synth-input (#7716)

Includes aborting when no non-constant subterms exist, a spurious assertion failure, and bad variable names.

Fixes cvc5/cvc5-projects#351

Fixes cvc5/cvc5-projects#353

[proofs] Fix a trace in SAT proof manager (#7732)

add bag.fold operator (#7718)

Add unit tests for api::Solver::setOption() (#7708)

This PR adds a generic unit test for api::Solver::setOption(). It iterates over all options and calls setOption() with somewhat cleverly chosen values according to getOptionInfo().
While building this, it occurred to me that calling std::exit() in an option handler is weird (for example for version) and we should do this in the driver instead. This PR also refactors this issue, moving all calls to std::exit() from the option handlers into the driver.

api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)

[proofs] Add method to CDProof to obtain number of proof nodes (#7725)

Useful for example to easily see by how much a proof grew after some reconstruction expansion.

[proofs] Alethe: Add finalize function to insert missing OR steps (#7724)

A post visit that adds an OR step is needed in case a premise is printed as a singleton (cl (or F1 ... Fn)) but used as a clause (cl F1 ... Fn).

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

Improvements for get-difficulty (#7720)

This makes 2 improvements for get-difficulty:
(1) Ensures that we recompute relevance info for lemmas sent at STANDARD effort.
(2) An open proof error was reported by Certora using --produce-difficulty.
This makes get-difficulty more robust by ensuring that lemmas are not marked as having a difficulty. It also minimizes the cases where we mark lemmas as having a difficulty internally.