Eliminate remaining calls to callExtendedRewrite (#7839)

Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)

Fixes https://github.com/cvc5/cvc5-projects/issues/371.
Fixes https://github.com/cvc5/cvc5-projects/issues/339.
Fixes https://github.com/cvc5/cvc5-projects/issues/333.

Variants of the tests in the above issues are added to this PR. In them, we expect to get an exception because the constant is too big.

Disable unit tests without poly (#7844)

This PR disables the new unit tests from #7829 when poly is not available.

Connect sequences array solver to strategy in theory of strings (#7847)

Also corrects an issue with model construction, where SEQ_NTH should be assignable in addition to SEQ_NTH_TOTAL.

seqArray branch (which has regressions) can be merged to master after this PR.

Eliminating some uses of const rational in arithmetic (#7846)

Note that there are several nested dependencies in arithmetic for constructing constants Constant::mkConstant ---> mkRationalNode ---> mkConst(CONST_RATIONAL, r)

This starts to disambiguate these calls.

Updates to LFSC signatures (#7840)

Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions.

Allow SyGuS subsolver to be reused in incremental mode (#7785)

This allows SyGuS subsolvers to be called multiple times to produce solutions for a given set of SyGuS constraints using a new command check-synth-next.

By default, the SyGuS subsolver will generate a new solution for each successive check-synth.

This simplifies the internal SyGuS solver in several ways for this purpose. It also ensures that solutions are cached; current master may recompute solutions in the same state more than once if asked, which is no longer the case.

This completes our support for incremental SyGuS.

[Sequences/Array Solver] Minor refactoring (#7843)

This commit performs a minor refactoring of our array core solver. It
adds more comments and avoids sending the
STRINGS_ARRAY_NTH_TERM_FROM_UPDATE lemma more than once in a given
user context.

[proofs] Fix helper LFSC script (#7845)

api: java: Support default arity for Solver::mkUnresolvedSort(). (#7842)

[Strings] Minor fixes/improvements (#7837)

This is a quick follow-up for PR #7815. My comments didn't make it in
before the PR was merged, so this commit fixes some of the minor issues
I found.

Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver class and options (#7820)

This commit fixes several issues in the ArrayCoreSolver class and the options:
1. Add range checking for an update rule.
2. Assign different inference ids to different rules.
3. small syntax optimizations.

Simplify contrib/get-lfsc-checker and use cvc5 repo for LFSC signatures (#7835)

Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)

Fixes https://github.com/cvc5/cvc5-projects/issues/390. This commit
fixes two issues with the rewrite: (1) the rewrite should only apply if
the update is of size 1 and (2) the `str.rev(...)` should be removed
inside the `str.update(...)`.

Minor refactoring of API for eliminating arithmetic subtypes (#7833)

Fix tracker in SubstitutionMap (#7829)

This PR fixes a subtle issue in #7787 where the rhs (instead of the lhs) of the applied substitution was inserted into the tracker.
Fixes cvc5/cvc5-projects#388

Remove Rewriter::rewrite from bags type enumerator (#7827)

Refactoring initialization of proofs (#7834)

Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.

Add relations.cpp, relations.py examples (#7801)

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.