| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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)
|
|
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.
|
|
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
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).
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
|
|
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
|
|
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.
|
|
This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.
It also adds proof support for datatypes purification.
|
|
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.
|
|
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.
|
|
|
|
|
|
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).
|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
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.
|
|
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
|
|
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.
|
|
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 #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
|
