| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.
These benchmarks were fixed by 3c98bb2.
|
|
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
|
|
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.
|
|
We currently were ignoring the option --sygus-expr-miner-timeout=N. This corrects the issue.
|
|
This PR adds InferenceIds that were previously missing from the corresponding toString() method.
|
|
Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.
|
|
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.
|
|
Fixes #5150.
|
|
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 #5101.
|
|
Fixes #4400.
|
|
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.
|
|
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
|
|
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.
|
|
|
|
Fixes #5942.
This benchmark was fixed by recent changes to ppRewrite.
|
|
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.
|
|
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.
|
|
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
|
