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.

Add the first example for z3pycompat (#7722)

This PR adds the first example for the z3py compat API.

Enable Java examples (#7702)

Alethe: Add function that adds final steps to proof (#7710)

There are some cases when the result has to be transformed, e.g. when it was printed as (cl false) which is correct everywhere except in the last step. This function then transforms the result into (cl).

Should be merged after PR #7675.

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

Translating API tests to Python — part 2 (#7651)

This PR translates the remaining cpp API tests to python.

Use new token for docs-release (#7709)

This PR uses the new CVC5_DOCS_RELEASE_TOKEN to make uploads to docs-release actually work.

Remove spurious assertion in parser (#7713)

When global declarations are true, we do not push/pop the context of the symbol manager. This removes a spurious assertion that checked whether a pop in this case was greater than the actual context level of the symbol manager.

Fixes cvc5/cvc5-projects#370.

Define sort undeclared (#7714)

Fixes cvc5/cvc5-projects#369.

Now gives:

(error "Parse Error: proj-369.smt2:3.22: Symbol 'Bool' previously declared as a type

  (define-sort _s0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
                    ^
")

Translating more cpp API unit tests to python (#7669)

This translates the majority of the tests from https://github.com/cvc5/cvc5/blob/master/test/unit/api/cpp/solver_black.cpp that were not translated yet, to python.
Additionally, some minor renames and `yapf` formatting is done the the existing tests.

Always run update-pr (#7719)

This removes the event condition on the `update-pr` ci job. Right now, it is not run although it should.

Extend docs example extension (#7717)

This PR extends the custom sphinx extension for examples. It now allows for simple patterns in the file names and matches the file types using arbitrary regular expressions instead of just looking at the file extensions. This is necessary to integrate examples from the z3pycompat API: the examples live at a nontrivial place (in the build folder), which we inject via the file name patterns; we will have two separate examples which both end in .py but can be distinguished via the pattern used in the beginning.

Change CVC4 urls to cvc5. (#7706)

This commit will change the URLs to the new cvc5 nightly builds and coverage
information.

Add rewrite for is_int pi (#7711)

Fixes cvc5/cvc5-projects#365.
Fixes cvc5/cvc5-projects#356.

Scaffold the idiomatic API's documentation (#7715)

Scaffolding the documentation, and fleshing it out for the Boolean functions and terms.

Generalize eager length bound conflicts for regular expression memberships (#7633)

This generalizes eager length bound conflicts to take into account regular expression memberships.

For example:

If `(str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar))` is asserted, then we know `(str.len x) >= 3`.

If e.g. equivalence class of `x` is merged with `(str.substr y 0 2)`, we get the conflict

`(and (str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar)) (= x (str.substr y 0 2))`

since `(str.len (str.substr y 0 2)) <= 2`.

This also does some minor refactoring to eager prefix conflicts to make it more analogous to our implementation of length conflicts.

Proper check for first-class types in datatype subfields (#7712)

Fixes two issues with our check for datatype subfields (isFunctionLike -> isFirstClass): functions should be allowed, RegLan should not.

Fixes cvc5/cvc5-projects#368. That issue now throws an error:

(error "Parse Error: proj-368.smt2:3.39: cannot use fields in datatypes that are not first class types

  (declare-datatype x ((_x (x8 RegLan))))
                                         ^
")
This adds a regression showing we allow functions as subfields.

Alethe: Further Printer Implementation (#7675)

Adds implementation of PrintInternal a function to print a proof node after the first step has been printed.

Should be merged after PR #7674.

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

[proofs] Alethe: Implementation of Printer (#7674)

Adds an implementation file of the Alethe printer with function stubs to be filled in in further PRs.

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

Remove now unused dumping infrastructure (#7703)

This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.

[proofs] Alethe: Printer Specification (#7673)

Header of the Alethe printer

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

Fix minor issues (#7704)

This fixes a few minor coverity issues.

Start post-release for 0.0.4

Bump version to 0.0.4

Bug in printing parameter list in define_fun_to_string (#7700)

Signed-off-by: Sujit Muduli <smuduli@cse.iitk.ac.in>

Consolidate CI jobs (#7697)

This PR integrates the cancel and update-pr jobs into the main CI jobs. This not only looks nicer in the actions menu (less jobs) but also improves which jobs we cancel: this now also allows to cancel jobs in forks by getting rid of the magic workflow number.

Guard regression tests that require libpoly to pass. (#7698)

Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.

api: Refactor mkTerm for kinds with arity = 0. (#7699)

This refactors mkTerm to allow creation of terms of kinds with arity = 0
via Op and/or empty children vector.

examples: Update python api datatypes example. (#7692)

The C++ datatypes example was extended in #7689. This updates the Python
API datatypes example accordingly.

Always enable API black box unit tests (#7696)

Currently, when assertions are disabled, we do not enable any unit
tests. However, we have decided that it would be beneficial to do black
box unit testing of the API even when building cvc5 without assertions,
because the API is user facing. This commit makes the following changes:

- Always enables API black box unit tests
- Adds a test to check whether a buggy version of Clang is being used,
  which prevents the use of `-fno-access-control` for white box tests
- Fixes a spooky variable name in a Python unit test

cmake: Add option --[no]-static-binary. (#7695)

Allows to disable linking against static system libraries explicitly.

Fix ANTLR3 config for i386 and aarch64 builds. (#7694)

This fixes the i386 and aarch64 nightly builds.

examples: Update Java datatypes example with recent extensions. (#7693)

The C++ datatypes example was extended in #7689. This updates the Java
API datatypes example accordingly.

Remove dependency of `TypeNode` on `Node` (#7690)

This is further work towards breaking cyclic dependencies in the `expr`
folder.

Fix potential for cycles in trust substitutions (#7687)

This ensures we use only the prefix of substitutions for the *first* time a formula is proven in a substitution map.

This avoids the possibility for cycles in proof generators during non-clausal simplification, where we may reprove a formula F later at a point where later substitutions depend on F.

examples: Extend DT api example with APPLY_TESTER and APPLY_UPDATER application. (#7689)

Minor fixes (#7691)

api: Fix creation of nary term kinds via Op. (#7688)

Fixes cvc5/cvc5-projects#367.

Make difficulty manager only consider lemmas at full effort (#7685)

Fixes cvc5/cvc5-projects#350

Enable model-based reduction technique for strings (#7680)

This changes our default strategy for deferring (some) reductions until after the model is constructed. It introduces the option `--strings-mbr` (model-based reduction) which is enabled by default.

When using model-based reductions, only *negatIve* contains and negative memberships are deferred for reduction/unfolding until LAST_CALL effort, where a candidate model is available. These steps are performed only if the constraints are not already satisfied in the model.  The intuition is that negative contains/membership are the *most* expensive constraints to process and are moreover the *least* likely to be false in the model.

It makes a few fixes to the extended/RE solvers:
- 2 kinds of inferences in `checkExtfEval` should not be performed for substitutions based on models
- The regular expression solver should not use inclusion tests to justify reduction of memberships when the basis for the reduction is an unfolded membership, due to the reasoning being potentially cyclic.  This led to a bogus model on a regression when the new strategy was enabled.

It also does minor refactoring of those solvers that was required for implementing the new policy.

This branch is +446-1 on SMT-LIB, with all gains coming on "sat" benchmarks, mostly from pyex.  It also solves 2 previously unsolved challenge Amazon benchmarks quickly.

Add kinds to python docs (#7672)

This PR adds the kinds to the documentation for the regular python docs.

Push output language inside the printing code (#7683)

This PR pushes the explicit specification of the output language further inside the printing methods.
The general way to specify the output language is to attach it to the output stream. The changes simplify the interface, while we still allow printing in another output language via using a scope (as used in the lfsc and tptp printers).

Add rewrite rule for bag.card operator using bag.map and lambda (#7643)

Add rewrite rule for bag.card operator using bag.map and lambda

Python API documentation: terms (#7659)

This PR adds documentation for the Terms class in the python API.
Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de