| Age | Commit message (Collapse) | Author |
|---|
|
Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should.
In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes. The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.
|
|
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
|
|
This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.
This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
|
|
This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).
Fixes #4850.
|
|
mkScope (#5012)
This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.
A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
|
|
Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
|
|
|
|
This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass.
Many parts are wrapped by helper functions and so the main loop becomes smaller.
remark: selecting "Hide whitespace changes" cuts the diff by ~50%.
|
|
Fixes #4973.
|
|
Previously, in case we encountered a term we cannot translate to integers (e.g. a bit-vector array), we would fail.
This PR improves that behavior by keeping the original term, and potentially wrapping it BV_TO_NAT and INT_TO_BV operators.
A test which includes a bit-vector array is included, which was not supported before.
In addition, the treatment of uninterpreted functions is refactored and documented better.
|
|
Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.
|
|
This includes some changes to proof node updater that are not currently on master.
This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.
It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.
|
|
Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).
|
|
This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.
|
|
Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.
|
|
This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:
(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.
|
|
Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies.
This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas.
Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative.
A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.
|
|
Fixes #5032
|
|
This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.
|
|
This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.
|
|
This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.
It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.
|
|
|
|
This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.
This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.
This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).
|
|
|
|
This PR modifies the printers to use Result::Sat, "internal" version of BenchmarkStatus, for printing benchmark status commands.
|
|
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
|
|
on GitHub (#4989)
Signed-off-by: Malte Mues (mail.mues@gmail.com)
|
|
This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.
|
|
This gives theories a finer grained control over explained lemmas and conflicts.
A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.
This is required for the new strings inference manager on proof-new.
This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.
|
|
This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.
It matches that base class almost exactly, with cosmetic changes.
Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.
This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.
|
|
Motivated by #4936, this PR adds a new BV rewrite rule:
(bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false)
Fixes #4936.
|
|
Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.
|
|
Some of the bit-vector operators are directly translated to integers, while others are eliminated before the translation.
This PR changes the set of operators that we eliminate (and as a consequence, also the set of operators that we handle directly):
The only bit-wise operator that is translated is bvand. The rest are now eliminated.
bvneg is now eliminated.
The various division operators are still eliminated, but using different rewrite rules.
zero-extend and sign-extend are now handled directly.
shifting is changed to favor ITEs over non-linear multiplication.
|
|
This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular.
While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager.
This PR is based on #4960.
|
|
This PR tries to make the nonlinear extension more deterministic by keeping the order of input assertion (instead of taking them from a hash set). This makes the ordering somewhat more robust against varying node ids, which proved to be a problem for debugging...
Also adds a few logging messages at interesting places.
|
|
On Debian (for instance), libraries aren't installed into `/usr/lib/`, but into something like `/usr/lib/x86_64-linux-gnu/`. In particular, this means that setting the `LIBRARY_INSTALL_DIR` to `lib` in the top-level `CMakeLists.txt` file is wrong.
Luckily, there is a simple solution: CMake provides [`CMAKE_INSTALL_LIBDIR`](https://cmake.org/cmake/help/v3.0/module/GNUInstallDirs.html) for this very purpose, which has sensible defaults and can be set by the user. In particular, since `CMAKE_INSTALL_LIBDIR` is a standardized variable, tools like the ones used for building Debian packages can set it to what they want it to be, whereas using a custom variable like `LIBRARY_INSTALL_DIR` wouldn't work in this setting.
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
|
|
This makes it so that ExtTheory uses a generic callback instead of relying on Theory.
The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.
It also refactors the use of ExtTheory in strings and arithmetic.
|
|
This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
|
|
This includes more versions of checking whether a proof node is closed and standardizing output.
|
|
This commit fixes builds that include CryptoMiniSat after commit
8ad308b removed them. It also fixes one
of the regressions that requires unsat cores but was run when the build
was configured without them.
|
|
Fixes #4942. The Python API was missing some methods related to
datatypes. Most importantly, it was missing mkDatatypeSorts, which
meant that datatypes with unresolved placeholders could not be resolved.
This commit adds missing methods and ports the corresponding tests of
datatype_api_black.h to Python. The commit also adds support for
__getitem__ in Term.
|
|
This PR removes any usage of the #line directive.
We no longer consider it particularly useful, and it obstructs reproducible builds (see #4980).
Fixes #4980.
|
|
This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.
|
|
This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.
This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This commit changes our `competition` build to include the libraries
that we have used for SMT-COMP by default. This makes it easier for
users to reproduce our SMT-COMP configuration for performance
measurements. We are using GPL libraries for this build type, so the
commit adds color to highlight the fact that this build type produces a
GPL build.
|
|
sensitive (#4972)
This will be used by TermFormulaRemoval.
|
|
release + a set of patches (#4775)
This PR attempts to migrate from @timothy-king's repo for glpk-cut-log to using a set of patches against the official release that 'glpk-cut-log' was based off of (4.52).
This is in preparation of trying to rework these patches to be against the latest GPLK release (4.65). If we can do this, then it makes it easier for CVC4's dependancy on GPLK to be able to follow upstream (rather than being stuck on a release that is 6.5 years old!).
I have added GPLK as an option for CI, but I do not know if we actually want this. My concern with adding this to CI is that we're then not testing non-GPL builds, which doesn't seem ideal.
However, before starting to rework the patches to be against 4.65, I want to make sure that things are actually working/stable against 4.52; so having at least one CI target that does use GPLK would be great.
Signed-off-by: Andrew V. Jones andrew.jones@vector.com
|
|
This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.
|
|
These updates are inspired by the current inference manager for sets.
|
|
This includes using the standard d_conflict flag in TheoryState and splitting its check into 3 callbacks.
It also deletes some unused code and eliminates an assertion (line 791 of theory_arrays.cpp) which doesn't hold in a central architecture.
Further work on standardization for arrays will add an InferenceManager to guard its uses of asserting facts to equality engine (both for proofs and configurable theory combination).
FYI @barrettcw
|
