| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
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 benchmarks 2 and 3 from #5848.
|
|
|
|
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.
|
|
This utility will be used to track pools for pool-based instantiation.
|
|
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.
|
|
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.
|
|
Only regenerate files if dependencies changed. This avoids unnecessary
rebuilds of the Cython code.
|
|
|
|
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
|
|
|
|
Fixes #4370.
|
|
|
|
Fixes #4179.
|
|
|
|
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}.
|
|
|
|
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.
|
|
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.
|
|
Fixes #4328.
|
|
Fixes #6260.
Signed-off-by: Nicolaas <nweidema@usc.edu>
|
|
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.
|
|
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.
|
|
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
|
|
Fixes the first benchmark from #6203.
|
|
CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.
|
|
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.*.
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
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.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
|
