Refactor cmake: auto-download and default-on dependencies (#6355)

This PR changes a few things in how dependencies are handled during configuration:

- --x-dir are removed for most dependencies, use the generic --dep-path instead
- the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves
- external projects check this option and send an error if it is OFF
- some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU)

This will essentially fail every call to ./configure.sh until the user specifies --auto-download.

Replace SExpr class by simpler conversion routines (#6363)

This PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:

- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer

cmake: Build object libraries for base and context. (#6374)

cmake complains that the static base and context libraries are not
exported as install targets. Since we do not want to install these
libraries we'll build object libraries instead.

preprocessing context: Add wrapper for model substitutions. (#6370)

Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.

Fixes #5473.

Build support library from base and context. (#6368)

This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.

Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.

Avoid options listener for resource manager. (#6366)

This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.

Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

Fix printing of stats when aborted. (#6362)

This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup.

add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>()
improve kindToString() to avoid std::stringstream
fix newlines between statistics in printSafe()
make printing of histograms consistent
make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa)

Reenable regression for minimizing instantiations (#6367)

Fix type rule for relations join image (#6349)

The join image type rule restricted that an argument was a constant. This is a logic restriction that should not be a part of the type checker.

This is required for not throwing type checking exceptions during proof conversion to LFSC.

Improve documentation for FP rounding mode, add bibliography (#6343)

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

Improve documentation of API kinds (#6341)

This PR improves the documentation of the api::Kind enum. Note that the docs for many of the enum values should still be improved. This PR merely makes sure that everything that is already there is actually output (/* vs /**) and properly rendered (missing spacing between lists, some formulas, etc).

Improve documentation for API exceptions (#6340)

Refactor / reimplement statistics (#6162)

This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.

Rename public and private headers in src/include. (#6352)

[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.

Add internal API methods for pool-based instantiation (#6350)

Add interface for getting relevant assertions (#5131)

This adds an interface to TheoryEngine for getting the current set of relevant assertions if it is available.

An interface to this can further be added to the API in a future PR.

Merge equivalent sub-obligations instead of discarding them. (#6353)

This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.

Warn about infeasible SyGuS conjectures (#6345)

[proof-new] Fix explanation of literals in SAT proof manager (#6346)

Prevents exponential behavior in SAT proof generation by not reexplaining previously explained literals. Also fix a potential issue in not previously overwriting rederived resolution chains during solving.

[proof-new] Miscellaneous improvements to dot printer (#6342)

Fix libpoly build and use new release (#6354)

This PR fixes the libpoly build: it naively removed the test/ folder from the source directory to save on cache size.
It also uses the recently published 0.1.9 release of libpoly.
Fixes #4706.

Add pool instantiation strategy (#6308)

Adds an instantiation strategy based on user-provided pool annotations.

The next PR will connect this to quantifiers engine.

Refactor quantifiers macros (#6348)

This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.

This is work towards adding proofs for macros.

ci: Use CVC5_REGRESSION_ARGS. (#6347)

Formalize more skolems (#6307)

This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.

It also adds proof support for datatypes purification.

API docs: Add custom target to build for GH pages. (#6335)

Avoid using substitute's input cache after the method call. (#6328)

As it traverses a node, Node::substitute populates its input cache with TNodes that are not preserved by the SygusReconstruct module and maybe destroyed after the method call. This PR fixes a bug where those unsafe TNodes are referenced throughout the module by passing the method a temporary copy of the cache instead.

Fix sexpr bug with AST output language. (#6329)

When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.

Bags: Move more implementation of type rule from header to .cpp. (#6336)

Strings: Move implementation of type rules from header to .cpp file. (#6334)

Fix computation of whether a type is finite (#6312)

This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.

Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).

Refactor resource manager (#6322)

This PR does another round of refactoring of the resource manager and related code.

- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager

Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.

Only require GMP 6.1 (#6332)

The recent refactoring of the dependencies raised the required GMP version to 6.2 for no particular reason. This PR reverts this change to only require GMP 6.1 again.

Refactor and update copyright headers. (#6316)

Consolidate interface to prop engine (#6189)

This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.

As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.

I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.

Fix GitHub Actions macOS build (#6331)

The build is currently failing because it tries to download an older
version of the ccache package. This commit makes sure that Homebrew is
up-to-date before trying to install packages.

Rename CVC4_ macros to CVC5_. (#6327)

Rename CVC4__ header guards to CVC5__. (#6326)

New C++ Api: Initial layout of Api documentation. (#6325)

[proof-new] Optimizing sat proof (#6324)

For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.

Add identifiers for extended function reductions (#6314)

This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures.

This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class.

Add regressions for issue 6214 (#6305)

Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.

These benchmarks were fixed by 3c98bb2.

Learn equalities involving Boolean variables (#6323)

Previously, the circuit propagator was not learning literals of the form (= x t) where x is Boolean, since this term was not treated as a theory literal.
This commit changes that, which improves performance significantly, since it
allows the elimination of Boolean variables, which, in turn, can make the
justification heuristic much more effective.

Signed-off-by: Andres Noetzli noetzli@amazon.com

Avoid spurious runs in run_regression.py (#6318)

The options --check-synth-sol and --check-abducts are independent from the rest of the solver. Hence, it is not necessary to run with/without them enabled in our regressions.

This saves roughly 30-40 seconds on regression regress0-2.

Use expr miner timeout (#6321)

We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue.

Add missing InferenceIds to toString (#6320)

This PR adds InferenceIds that were previously missing from the corresponding toString() method.

Fix run_regression for cvc expected outputs (#6317)

Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.

Use newer version of update-pr-branch action. (#6315)

The CI action we use to update PRs that are ready to merge has been updated and now only considers the last review of every reviewer. It now allows to automatically update (and then merge) PRs where a reviewer first requested changes, and then accepted the PR. See adRise/update-pr-branch#11 for more details.
This PR bumps the version to the most recent one.

Use exceptions when constructing malformed datatypes (#6303)

Fixes #5150.

Add identifiers for sources of incompleteness (#6311)

This PR classifies all internal kinds of incompleteness as identifiers.

It makes it so TheoryEngine records an identifier when its incomplete flag is set.

The next step will be to possibly communicate this value to the user.

Add benchmark for issue 5101 (#6301)

Fixes #5101.

Add benchmark for issue 4400 (#6288)

Fixes #4400.

Initial support for parametric datatypes in sygus (#6304)

Fixes #6298.

Enables parsing of par in the sygus parser, and adds support for default grammar construction.

Also fixes a bug related to single invocation for non-function types.

Remove old API header. (#6309)

Add cardinality class definition (#6302)

This is work towards correcting our computation of whether a type is finite. Currently, arrays/functions with uninterpreted sorts as element/range types are always considered infinite. This is incorrect if finite model finding is enabled, since the interpretation of the uninterpreted sort can be one. This leads to errors during model building due to exhausted values (#4260, #6100).

This PR adds a new concept of a cardinality class, which is required for properly categorizing types with/without finite model finding.

A followup PR will replace TypeNode::isFinite with TypeNode::getCardinalityClass. Calls to TypeNode::isFinite will be replaced by calls to TheoryState::isTypeFinite, which will properly take cardinality classes into account.

Add benchmark for 6270 (#6283)

[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)

Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.

This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.

Add benchmark for issue 4420 (#6286)

Adds a benchmark that was previous sensitive to assertion order, fixes #4420.

Set incomplete if not applying ho extensionality (#6281)

If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.

Fixes #4318.

Fixes for abducts (#6279)

Fixes benchmarks 2 and 3 from #5848.

New C++ Api: Rename and move checks.h. (#6306)

(proof-new) Proper implementation of proof node cloning (#6285)

Previously, we were traversing proof node as a tree, now we use a dag traversal.

This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.

Add term pools utility (#6243)

This utility will be used to track pools for pool-based instantiation.

New C++ Api: Initial setup of Api documentation. (#6295)

This configures the initial setup for generating Api documentation with
Sphinx via Breathe and Doxygen. All fixes in the documentation of the
cvc5.h header are for the purpose of eliminating warnings. This PR does
not check for completeness of the documentation, and does not yet tweak
the documentation to be nice, beautiful and consistent, which is
postponed to future PRs.

Configure with `--docs`, and then make. This will generate a `docs`
directory in the build directory. The Sphinx documentation can be found
at `build/docs/sphinx/index.html`. Doxygen documentation is only
generated as xml under `build/docs/doxygen`.

This PR further proposes a new style for copyright headers. If this
style is approved, I will submit a PR to update the update_copyright.pl
script.

Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)

This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.

This PR also eliminates some unused code in TheoryArithPrivate.

Followup PRs will start formalizing/eliminating calls to mkDummySkolem.

cmake: Do not always regenerate cvc4kinds.{pxi,pxd}. (#6300)

Only regenerate files if dependencies changed. This avoids unnecessary
rebuilds of the Cython code.

cmake: Add helper to check if a given Python module is installed. (#6299)

Add benchmark for issue 5942 (#6296)

Fixes #5942.

This benchmark was fixed by recent changes to ppRewrite.

Remove template argument from `NodeBuilder` (#6290)

Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.

CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s

Signed-off-by: Andres Noetzli noetzli@amazon.com

Fix tptp parser for negative rational (#6297)

Fix issue with lemma during equality engine iterator in sets (#6289)

Fixes #4370.

genkinds: Do not use relative paths to find src directory. (#6293)

Remove stdPrintAscii option (#6280)

Fixes #4179.

New C++ Api: Rename and move headers. (#6292)

parsekinds: Remove DEFAULT_HEADER. (#6294)

DEFAULT_HEADER in src/api/parsekinds.py is essentially unused since both genkinds.py scripts pass the kinds header to the script. The current value of DEFAULT_HEADER does not work for the scripts since the working directory for genkinds.py is in src/api/{java,python}.

Add documentation for theory_bags_type_rules.h (#6268)

Fix spurious antecedant for symbolic regular expressions (#6284)

Fixes #6271.

This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.

Add benchmark for issue 4412 (#6287)

[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)

Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.

This is in preparation for the new unsat cores based on proofs.

Enable UF when pre-skolem nested option is enabled (#6282)

Fixes #4328.

python: Fix type casting in mkBitVector (#6261)

Fixes #6260.

Signed-off-by: Nicolaas <nweidema@usc.edu>

Fix subtyping for sets care graph (#6278)

We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.

Fixes #5705.

Add interface for skolem functions in SkolemManager (#6256)

This PR introduces the notion of a "skolem function" to SkolemManager, which is implemented as a simple cache of canonical skolem functions/variables.

This is a prerequisite for two things:
(1) Making progress on the LFSC proof conversion, which currently is cumbersome for skolems corresponding to regular expression unfolding.
(2) Cleaning up singletons. Having the ability make canonical skolem functions in skolem manager will enable Theory::expandDefinitions to move to TheoryRewriter::expandDefinitions. This will then enable removal of calls to SmtEngine::expandDefinitions.

This PR also makes arithmetic make use of this functionality already.

The next steps will be to clean up all raw uses of NodeManager::mkSkolem, especially for other theories that manually track allocated skolem functions.

A proposal for python api unit tests (#6255)

This PR introduces two unit tests for the python api, translated directly from the unit tests for the cpp api.
The goal is to get feedback in order to reach some kind of a pattern/style for python API tests.
Also, i'd be happy to hear if there is any specific cpp api unit test I should translate for this initial attempt (e.g., a test that is more representative or might raise difficulties). For now i just picked the first two solver tests.

Optimizer for BitVectors (#6213)

Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.

Disable substring component contains in strip endpoints (#6266)

Fixes the first benchmark from #6203.

Add cache for new dependencies folder. (#6265)

This PR adds caching of the new dependencies folder build/deps/ for the CI jobs and renames the old deps folder to "auxiliary told".
Note that we need to cache the entirety of build/deps/ (instead of just the install folder for the old one), otherwise cmake will try to rebuild them. Some of the external projects remove unnecessary files in their build to reduce their footprint in the cache.

cmake: Do not link against main object library. (#6269)

CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.

New statistics registry (#6210)

This PR adds the next part of the new statistics setup: the registry.
The new statistics registry owns the actual data and only issues proxy objects that can be used to modify the internally stored data.
Once we replace the old statistics setup, the files should be renamed from statistics_reg.* to statistics_registry.*.

Minor refactoring (#6273)

This PR does some minor refactorings in preparation for the new statistics: some renamings, removal of now obsolete code and usage of references instead of pointers.

Cleaning up friend relationships for commands (#6254)

Fix case where RE unfolding generates a trivially true lemma (#6267)

An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.

An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).

This PR ensures we are robust to these cases.

This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.

FindCaDiCaL: Avoid redirect to file (#6272)

This PR avoids output redirection by replacing sed + redirect with copy + in-place sed.
Using output redirects can cause problems if the cmake output itself is redirected as well.
This should fix the current nightly failure.

Add utility classes for new statistics (#6178)

This PR introduces two new sets of classes used for the new statistics setup.
The first set are the statistic values that hold the actual data and will live in the new statistics registry itself.
The second set are proxy objects: they only hold a pointer to the value classes and implement all the modifiers.

The code is not used yet, but replaces the code in the stats_* files in a subsequent PR.

Simplify caching of regular expression unfolding (#6262)

This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.

This fixes the second benchmark from #6203.

This PR also improves our traces for checking models in strings.

FP: Factor out symfpu traits. (#6246)

This is in preparation for a MPFR floating-point literal implementation.
We will need to have both literal kinds return a symFPU unpacked float
via `getSymUF()` in order to be able to plug it into the fp_converter.
For this, it makes sense to have the traits implemented and to be
included separately, so that they can also be included in the MPFR
implementation.

Fix type rule for to_real (#6257)

This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.

This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.

This also fixes Solver::isReal, which should return false if we are the integer type.

Fixes #6208.

Add regression for issue 6191 (#6264)