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)

Delete hashsmt example. (#6263)

This example does not serve the purpose of documenting how to use the
new API. It uses Command, which is not available via the API, and it's
not worth the effort to migrate it.

Refactor CLN dependency & Cleanup (#6251)

This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system.
Also, it does a bit of cleanup.

Rename namespace CVC5 to cvc5. (#6258)

kinds: Remove non-existent properties. (#6253)

 Add debug traces to theory inference manager (#6250)

Fix non-linear for unknown case (#6252)

As a result of this issue, currently we are incorrectly trying to repair a model when one is not guaranteed to exist, leading to a spurious assertion failure.

Fixes #6228. The benchmarks on that issue now answer "unknown" without an assertion failure.

Make ResetCommand go through APISolver (#6172)

This PR changes ResetCommand to not call SmtEngine::reset but instead reconstruct the api::Solver object. This makes SmtEngine::reset obsolete and removes it, and moves the original options from SmtEngine to api::Solver.
The motivation for this change is twofold:

The ResetCommand should not use SmtEngine directly, but only through the API (i.e. Solver).
As soon as the statistics data lives within the registry, we need to re-register statistics after resetting the SmtEngine. We can now do this within the api::Solver constructor.

Rename namespace CVC4 to CVC5. (#6249)

Refactor GMP and Poly dependencies (#6245)

Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.

Refactor dependencies for external SAT solvers (#6215)

This PR refactors how we obtain, build and use the external SAT solvers used by CVC4: CaDiCaL, CryptoMiniSat and Kissat.
All three contrib scripts are removed and instead an external project is integrated into the cmake find scripts.

Refactor SymFPU dependency (#6218)

This PR refactors the contrib script to download SymFPU to a cmake external project.

Bags: Move implementation of type rules from header to .cpp file. (#6247)

Fix years in COPYING. (#6248)

Eliminate dependencies on quantifiers engine in internal quantifiers code (#6240)

This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned.

Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.

Add missing inference ids (#6242)

Towards having complete stats on inference ids for each lemma, fact, and conflict.

FP: Move implementation of type rules from header to .cpp file. (#6241)

Fix compilation of Python bindings for named build directories (#6244)

In current master, the following fails whenever <name> contains a /:

./configure.sh --python-bindings --name=<name>

The reason is that src/api/python/genkinds.py adds a directory to the python path while relying on the fact that the build directory is located directly under the main repo directory, which is not the case if <name> contains a /.
This PR fixes this by having cmake determine the right directory to add to the python path.

Fix printing for double patterns (#6235)

Make SEXPR simply typed (#6160)

Currently, SEXPR applications are given a parametric type SEXPR_TYPE applied to the types of its arguments. This means that SEXPR that are type checked consume roughly double the memory. This issue arises in practice when printing proofs in the internal calculus.

There is no need to have SEXPR_TYPE as a parametric type, this PR makes SEXPR simply typed.

Also moves some implementation of TypeNode methods to type_node.cpp.

Implement simple tracking of instantiation lemmas (#6077)

We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.

This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.

Fixes #5899.

Refactoring quantifier annotation kinds, add kinds in preparation for pool-based instantiation (#6234)

This is in preparation for a new pool-based instantiation technique.

Eliminate use of rational from tptp parser (#6239)

Give a better error when sygus grammar rules contain free variables. (#6199)

Fix total time statistic (#6233)

Since one of the last changes to the total time collection in the driver, this collection fails when the solver terminates unexpectedly (either by a signal or an exception). This PR fixes this issue and does some cleanup along the way.

Miscellaneous elimination of dependencies on quantifiers engine  (#6238)

This should be the last PR before quantifiers engine will not be passed to quantifiers modules.

Add external project to install gtest (#6229)

This PR enables us to build gtest ourselves if it is not already installed.

Eliminate the use of quantifiers engine in sygus solver (#6232)

Fix configuration printing. (#6236)

Eliminate use of quantifiers engine in enumerative instantiation (#6217)

This also makes minor updates to how term tuple enumerators are constructed.

Move decision manager into theory inference manager (#6231)

This makes it so that the decision manager is accessible from TheoryInferenceManager.

This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.

Modular bv2int part 1 (#6212)

This PR introduces the header file for a more modular bv-to-int module, that will be called from the preprocessing pass bv-to-int, and possibly from the bit-vector solver after preprocessing.

The header file is basically a copy of the bv_to_int.h header file from preprocessing, with some adjustments to increase modularity.

In addition to the header file we also introduce an empty unit test that #includes the header, in order to identify compilation errors. The unit test will be populated in subsequent PRs, that will also include implementations.

FloatingPointLiteral: Constructor for special consts. (#6220)

This replaces static helpers for creating special consts with
constructors. This is in preparation for a FP literal implementation
using MPFR. In the next step, I'll introduce a FloatingPointLiteral base
class, from which the specialization FloatingPointSymFPULiteral is
derived. The MPFR implementation will also be derived from the base class.
This is in order to make unit tests that compare between the two
possible. Further, in the worst case, MPFR will have to use SymFPU for
unsupported cases (to be determined).

When building ANTLR via CMake, do not require javac #6224 (#6225)

As title; attempts to correct #6224.

Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com

Refactor ANTLR3 dependency (#6202)

This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.

Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.

Use color output to print configuration. (#6219)

FloatingPointLiteral: Make constructors that shouldn't be used outside of FloatingPoint(Literal) private. (#6211)