Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)

This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.

It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.

As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:

Make sure a ReferenceStat is set to values of the correct type (#6430)

This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.

Enable strings exp by default for strings specific logics (#6424)

One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.

BV: Add proof logging for bit-blasting.  (#6373)

Move implementation of UF rewriter to cpp (#6393)

Make trust substitution map generate proofs lazily (#6379)

This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.

This makes the proof generation in trust substitution map lazy.

Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.

Minor improvements to substitutions (#6380)

In preparation for using this class as part of our proof checker.

This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.

Minor changes to unsat core default setting (#6425)

cmake: Do not require --auto-download for already downloaded dependencies. (#6417)

This will look for already downloaded dependencies in the build
directory and therefore will not require --auto-download if the
dependencies were already downloaded in a previous build.

Update INSTALL.md (#6412)

This PR updates our build and installation instructions in INSTALL.md after we have changed how we handle dependencies.
Thanks @polgreen / #6391.

Add API documentation for statistics (#6364)

This PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.

Remove unused stuff from options setup (#6422)

This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.

 Reorganizing use of skolem definition manager in prop engine (#6415)

Towards setting up the proper callbacks into the new justification heuristic.

Moves ownership of skolem definition manager from TheoryProxy to PropEngine.

api docs: Rename doxygen output directory. (#6426)

api docs: Remove file reintroduced in past merge. (#6426)

Fix models for sygus-inference, bv2int, real2int (#6421)

In each case, previously we were generating a define-fun, what we needed was to do a model substitution.

This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.

Reconciling proofs and unsat cores (#6405)

This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:

the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.

Allow in-place construction of `CDList` items (#6409)

This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.

Move expand definition from Theory to TheoryRewriter (#6408)

This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.

The next step will be to add Rewriter::expandDefinition.

Arithmetic: Move implementation of type rules to cpp. (#6419)

UF: Move implementation of type rules to cpp. (#6403)

Add explicit dependencies for base lib (#6410)

This PR adds missing cmake dependencies for the base library. This makes sure that Debug_tags.h and Trace_tags.h are already present when we start compiling.

Pass GMP to libpoly (#6411)

This PR makes sure that our build of libpoly works on systems without GMP: by passing the paths to GMP we use ourselves to libpoly, we make sure libpoly always has a suitable version of GMP.
Also, we make libpoly somewhat faster to build by disabling tests.

Datatypes: Move implementation of type rules to cpp. (#6418)

Goodbye CVC4, hello cvc5! (#6371)

This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.

cmake: Add optional module name argument for check_python_module helper. (#6406)

Addtionally adds checks for required documentation modules.

Sets: Move implementation of type rules to cpp. (#6401)

Arrays: Move implementation of type rules to cpp. (#6407)

Add unit test for abduction (#6400)

Add basic utilities for new implementation of justification heuristic (#6333)

This sets up the core utilities for the new implementation of justification heuristic

Add getNumIndices to Op (#6386)

Add getNumIndices to Op

Split FP expand definitions to own module (#6392)

This moves the code for expanding definitions in floating point to its own module, which lives in the rewriter.

This is work towards moving Theory::expandDefinitions to Rewriter::expandDefinitions.

The code was only moved, not modified in this PR.

BV: Move implementation of type rules from header to .cpp. (#6360)

Sep: Move implementation of type rules to cpp. (#6402)

Quantifiers: Move implementation of type rules to cpp. (#6404)

Add InferenceId as resources (#6339)

This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.

Add instantiation pool feature to the API (#6358)

This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.

Split C++ API docs from general docs (#6365)

Remove support for CVC3 language. (#6369)

Basic setup for examples in documentation (#6383)

Add guards to disable clang-format around placeholders in templates. (#6375)

Fix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)

ANTLR3_COMMAND was using a fixed path instead of relying on the
ANTLR3_JAR variable. If the ANTLR3 JAR was found on the system (for
example due to an existing deps folder at the root of the CVC4
folder), then the command would fail because the JAR was not at the
expected location. This commit changes the command to use the variable
and prints the location of the JAR file to make debugging easier.

Properly link Poly against GMP (#6398)

This PR fixes a linker issue with libpoly and static builds where Poly and GMP would be linked against in the wrong order.

python API sorts: adding functions and tests (#6361)

This PR does the following:

1. removes old python sort API test
2. creates a new python sort API test, obtained by translating the (entire) cpp unit test https://github.com/CVC4/CVC4/blob/master/test/unit/api/sort_black.cpp
3. adds support for bags and datatype selectors/testers domain/codomain in the python API.

Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)

This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.

This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.

In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.

This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.

Remove linking against gmp and cln in tests and parser (#6376)

Finally, we no longer need to link against GMP and CLN for the parser and the tests.
To actually achieve this, this PR also removes some dead code and unused includes from some parser files.

Fix dependencies for stats options (#6378)

A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.

Fix ONCE for post-rewrite (#6372)

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.