Add basic regular expression type enumerator (#7416)

The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.

It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.

Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)

Fixes a proof checking failure during post-processing.

Fixes a rare case where the RHS of equality resolve step requires a symmetry step.

Support sequences of fixed finite cardinality (#7371)

The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).

Fix issue related to sanity checking integer models (#7363)

We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat".

This also changes an assertion to warning, to allow the regression to pass.

Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks).

As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252.

Remove setDefaults methods (#7413)

This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it.

Add regression for fixed issue (#7395)

Fixes #6653.

The third benchmark on that issue is no longer an issue, this adds it as a regression, which is the last open benchmark on the referenced issue.

Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)

Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module.

Update SMT-COMP script (#7389)

PR #6848 disabled relevancy order by default, but for QF_NIA, it helps
us solve significantly more benchmarks (17525 vs. 16889 with a 20 minute
timeout using the updated SMT-COMP script). This also updates the
options for `QF_AUFBV` and `QF_ALIA` to use `--decision=stoponly`,
following the name change of the option.

Python api documentation: Op, Grammar, Result, Enums (#7095)

This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.

Add more regressions for fixed issues (#7382)

Fixes #6535, Fixes #6475, Fixes #5660, Fixes #6607, Fixes #6638, Fixes #6642, Fixes #6775.

Have docs_upload properly upload tags. (#7352)

This PR improves our docs-ci mechanism to properly upload documentation for tags.

Fix bad cast in the python API (#7359)

Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366)

This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check.

This fixes one of the two issues related to proofs for #6973.

Add regressions for fixed issues (#7369)

Fixes #4393. Fixes #3966.

These issues do not occur on current master.

Fix (get-info :authors) (#7373)

This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped.
We now simply print the cvc5 authors.
It also fixes isValidGetInfoFlag() which was missing filename.

Fixes #7362.

Improve ManagedStreams (#7367)

This PR addresses #7361, but also a more general issue about regular-output-channel being able to hold stderr and diagnostic-output-channel being able to hold stdout.
It therefore changes how non-owned streams are stored: beforehand, an explicit stream would always be owned by the ManagedStream (through a std::shared_ptr) and a nullptr implicitly stood for stdout, stderr or stdin. Now we explicitly hold a pointer to a non-owned stream for these special values.

Fixes #7361.

Add regression for fixed issue (#7365)

Fixes #6845.

This issue does not occur in current master.

Improve parser for tuple select (#7364)

Split entailment check from term database (#7342)

Towards addressing some bottlenecks on Facebook benchmarks.

Also test older cmake versions (#7347)

This PR generally improves the new CI job to test different cmake versions. It extends the tested versions back to 3.8 and also sets the minimum required version (cmake_minimum_required) to the version that is tested. This allows to check compatibility with changing cmake policies.
It also modifies the run-tests action to get the regression options from explicit inputs instead of the build matrix. As the cmake job had no build matrix, it used to build regress3-4 as well.

Fix quantifiers variable elimination for parametric datatypes (#7358)

Fixes #7353.

Fix GLPK linking (#7357)

While #7341 added cmake-3.9 compatible linking for GLPK, it did not actually remove the line that triggers the error on older cmake versions. This commit does.

Add core LFSC signatures (#7289)

These files define how terms and sorts are represented. It also adds basic utilities used throughout.

Eliminate uses of rewrite from datatypes theory (#7354)

Also simplifies slightly how rewritten forms of operators in sygus grammars are obtained.

Make (proof) equality engine use Env (#7336)

Simplify refinement in sygus solver (#7343)

This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.

Eliminate calls to currentResourceManager (#7350)

The remaining calls to smt::currentResourceManager are in the bitblasters, which should probably update to Env. FYI @mpreiner .

cmake: Fix git info if build directory is outside of source tree. (#7351)

Clean up occurrences of SmtEngine in comments. (#7349)

Get rid of unused member d_smtStats in ExpandDefs. (#7346)

This further renames d_smtStats to d_slvStats in ProcessAssertions.

Rename SmtEngineState to SolverEngineState. (#7344)

Fix glpk, add antlr.so (#7341)

This PR makes the cmake integration of GLPK compatible with cmake 3.9.
Also, it adds a missing BUILD_BYPRODUCT for antlr.

Provide a non-traversal interface to term formula removal (#7328)

Towards making theory preprocessing a single pass.

Minor cleaning of instantiation utilities (#7334)

Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.

This is work towards a major refactoring of conflict-based instantiation / entailment checks.

Simplify skolemization in sygus solver (#7331)

The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.

fix deprecation of std::iterator (#7332)

When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;

difference_type         Iter::difference_type
value_type         Iter::value_type
pointer                 Iter::pointer
reference         Iter::reference
iterator_category Iter::iterator_category

```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.

This pull request performs the fix, and the program is semantically equivalent before and after the fix.

References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator

Start post-release for 0.0.2

Bump version to 0.0.2

Fix release action.

Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)

Start post-release for 0.0.1

Bump version to 0.0.1

Antlr: runtime -> libraries (#7338)

For static builds, there was a mixup of variable naming in FindANTLR3 (RUNTIME vs LIBRARIES).

Rename SmtScope to SolverEngineScope. (#7284)

Revert #7257 (#7337)

This PR reverts #7257 and restores compatibility with ancient glibc versions.

Add CI workflow to test different cmake versions (#7254)

This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.

Connect the LFSC printer (#7323)

This adds the option --proof-format=lfsc.

It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.

Add cardinality constraint utilities (#7286)

This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.

This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.

Restore compatibility with cmake 3.9 (#7329)

This goes back to the new cmake setup and makes it compatible again with cmake 3.9.
It mostly means we can not link object libraries and also not link other libraries to object libraries.

I've tested these changes within docker on `ubuntu:18-04` with a manually installed `cmake-3.9.6`.

Remove static accesses to options where EnvObj is used (#7330)

This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().

Make skolem definition manager robust to function skolems (#7327)

This led to a model soundness issue in a development branch that reorganizes theory preprocessing.

This ensures that skolem definition manager looks for skolems that appear in operators.

This is important for inputs like:
(declare-fun h (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= h (ite A f g)))
(assert (= (h 0) ...)))

Add argument to distinguish lemmas and input assertions (#7326)

Work towards virtual clause deletion, where lemmas will be SAT-context dependent.

This adds an argument to the decision engine so it can distinguish lemmas from input assertions.

A few more miscellaneous uses of EnvObj (#7325)

Ignore zip files for docs upload diff (#7322)

This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.

Attach the static binaries to a release (#7324)

This adds another step to our CI pipeline that uploads the binary build by some of the jobs to a release.

Move preprocessor to smt solver (#7321)

This breaks the circular dependency of preprocessing pass context of solver engine.

It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.

It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).

Add a binary / SMT-LIB quickstart (#7315)

This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.

Finish the LFSC printer (#7285)

This adds the remaining implementation of the LFSC printer.

It also corrects a bug introduced during merging the last PR.

The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added.

Use skolem lemma in prop layer interfaces (#7320)

Add new versioning scheme (#7253)

This introduces a new versioning mechanism that allows for better automation.

Make the cardinality of the alphabet of strings configurable (#7298)

This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.

Add missing functions in Term.java (#7297)

This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.

Fix/Improve static and shared builds with CLN or Poly (#7306)

We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.

Miscellaneous fixes from proof-new (#7313)

Includes a few fixes for strings and datatypes theory lemma proofs.

Fast exit for string extended equality rewriter (#7312)

In benchmarks with many string equalities between variables and constants, a significant portion of the run time is spent on extended equality rewriting. This adds a fast exit when the equality is between variable/constants only.

Replace doubles by rationals in C++ quickstart (#7317)

This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.

Eliminate more circular dependencies on solver engine (#7311)

This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.

Change behaviour of Term::getRealValue() (#7316)

This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).

Change semantics of dumpUnsatCoresFull (#7314)

This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.

Refactor skolem definitions notifications for the decision engine (#7310)

These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.

This is in preparation for virtual clause deletion.

Enable static builds in CI (#7281)

This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.

Remove timestamped javadoc comments (#7304)

This PR also removes the javadoc timestamps from index.html, which for some reason does not honor the -notimestamp option.

Eliminate more hard coded uses of user context (#7309)

This is in preparation to make the "lemma context" configurable.

Avoid calling `quoteSymbol` multiple times. (#7307)

Calling `quoteSymbol(...)` twice on an empty string `""` returns `"|__|"`.

First round of refactoring on NlModel (#7255)

This PR performs a first refactoring on the NlModel class. It improves model value computation, comparison and stores the model substitutions in a map (instead of two vectors).

Reformulate (#7305)

Finish refactoring on option handlers (#7295)

This PR finishes refactoring on the option handlers.

Add sygus examples to documentation (#7303)

For some reason, we didn't have any SMT-LIB (or rather SyGuS) example files for the SyGuS examples yet.
This PR adds these missing examples.

Various improvements to documentation (#7283)

This PR adds a couple of improvements to our documentation setup
- add an explicit dependency on the extension so that sphinx rebuilds pages appropriately when an extension is modified
- sphinx now emits warnings for examples that are not implemented in all languages (smt2, cpp, java and python)
- add -v to make the sphinx output more log-file friendly
- avoid a warning when the java bindings (and thus java docs) are not build
- replace file(WRITE by configure_file to avoid rather common erroneous rebuilds of python docs
- fix a reference to a label in the python docs
- suppress timestamps in javadoc output to avoid docs-ci being triggered for every PR
- improve placeholder message when java bindings are disabled

Refactor internally generated bounded quantified formulas (#7291)

This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them.  It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself.  This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.

Move isFiniteType from theory engine to Env (#7287)

In preparation for breaking more dependencies on TheoryEngine.

Make decision engine use env (#7300)

No longer build docs by default. Use make docs. (#7296)

This PR changes our policy when to build the documentation. Beforehand, make docs was included in make and make all.
Now, you need to run make docs explicitly.

Eliminating static calls to rewriter in quantifiers (#7301)

Eliminating static calls to rewriter from strings (#7302)

Update java examples using the new Java API (#7225)

This PRs updates java examples using the new Java API, by converting C++ examples to Java.
Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API.
All examples are not included in the build which would be added in a future PR.

Update theory preprocessor to use Env (#7288)

In preparation for making the "lemma context" configurable.

Fix ascription check for return types on ordinary functions (#7290)

Fixes #7274.

Make preregistration safe for uninterpreted constants (#7292)

Work towards addressing #6908.

Remove (apparently obsolete) checks in cms config (#7294)

This removes checks from the CryptoMiniSat config for the existence of a couple of static libraries. Apparently, these are not necessary any more.

Clean options handlers (#7201)

Some cleanup on the option handlers, starting with handlers for base and main options.

Fix some python docstrings which lead to sphinx warnings (#7293)

This PR fixes some docstrings that are not properly indented for sphinx.

Add the LFSC printer (#7158)

This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR.

Further PRs will connect this printer as a possible output format for cvc5.

Add the print benchmark utility (#7196)

This utility is capable of printing a vector of Node as a valid (SMT-LIB) benchmark with no prior bookkeeping. It also optionally allows for taking a vector Node corresponding to define-fun.

It will be used to replace the old internal benchmark dumping infrastructure which was error prone.

Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)

This updates the datatypes rewriter to use the evaluator from Env instead of creating local copies of Evaluator. This makes all uses of the Evaluator dependent on the proper options (e.g. which will be based later on the cardinality of the alphabet for strings).

This moves one utility method (sygusToBuiltinEval) to the datatypes rewriter, as it uses an Evaluator that will be dependent on options.

Notice that this is another instance where it is important for us to make the cache for the rewriter local. The same issue occurs for other places where rewriting is dependent on options. This issue will be revisited when the option for strings alphabet cardinality is added.

Rename SmtEngine to SolverEngine. (#7282)

Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)

This is in preparation for renaming SmtEngine to SolverEngine.

Integrate javadoc documentation  (#7278)

This PR adds the cmake setup to generate javadoc documentation for the java API and integrates it into the sphinx documentation. Right now, we simply link to the javadoc. This PR also modifies a bunch of javadoc comments to use proper javadoc syntax.

configure: Fix --static flag. (#7280)

bv: Refactor ppRewrite and move to TheoryBV. (#7271)

This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules.

Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse.