| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
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.
|
