| Age | Commit message (Collapse) | Author |
|---|
|
The theory property `postsolve` was not used by any of the theories.
This commit removes the property and associated infrastructure.
|
|
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
|
|
We now use std::unique_ptr instead of std::shared_ptr when storing TheoryInference objects.
|
|
This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory.
Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.
|
|
This updates the theory of sets to the new interface (see #4929).
|
|
When testing the API examples, Python examples were not included. This
commit changes that and fixes multiple minor issues that came up once
the tests were enabled:
- It adds `Solver::supportsFloatingPoint()` as an API method that
returns whether CVC4 is configured to support floating-point numbers
or not (this is useful for failing gracefully when floating-point
support is not available, e.g. in the case of our floating-point
example).
- It updates the `expections.py` example to use the new API.
- It fixes the `sygus-fun.py` example. The example was passing a _set_
of non-terminals to `Solver::mkSygusGrammar()` but the order in which
the non-terminals are passed in matters because the first non-terminal
is considered to be the starting terminal. The commit also updates the
documentation of that function.
- It fixes the Python API for datatypes. The `__getitem__` function had
a typo and the `datatypes.py` example was crashing as a result.
|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
Updates it to use the new inference manager as well as updating its check to the standard callbacks.
|
|
This introduces a TheoryInference base class, which is a generalization and cleaner version of the former Lemma object. This changes the name of Lemma -> SimpleTheoryLemma, and makes the callback responsible for calling the inference manager.
This PR also updates the datatypes inference manager to use the new style. This required adding some additional interfaces to TheoryInferenceManager.
|
|
|
|
We'll use this to gate farkas-coefficient machinery after we remove the
old proof-macros.
I've changed the macros slightly from the proof-new branch: I removed the dependence on options::proof() (no longer wanted) and options::unsatCores() (I had copied this from the original proof macros, but it's not needed either, since we're in a theory).
|
|
When using CMake with Unix Makefiles, one can invoke `make install` as
```
make install DESTDIR=/a/b/c
```
so that the files will be installed into `$DESTDIR$CMAKE_INSTALL_PREFIX` (see the [documentation](https://cmake.org/cmake/help/latest/envvar/DESTDIR.html) for details). This currently doesn't work with the `fix-install-headers.sh` script:
```
[...]
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/integer.h
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/rational.h
find: ‘/usr/include/cvc4/’: No such file or directory
```
Here, `CMAKE_INSTALL_PREFIX` is `/usr` but `DESTDIR` is `/<<PKGBUILDDIR>>/debian/tmp/`.
This commit makes the script consider `DESTDIR` (if it is not set, then `$DESTDIR` will be empty and nothing changes) to fix this issue.
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
|
|
This is in preparation for converting datatypes to the new standard. It adds a specialized version of inference manager buffered that datatypes uses. This required adding several utility methods to its base classes.
A follow up PR will connect this to TheoryDatatypes.
|
|
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
|
|
This updates theory of strings to the new standard.
This makes strings use the standard template for check and collectModelInfo. It also updates its inference manager to the standard and makes use of assertFactInternal for processing internal facts. This now enables preNotifyFact and notifyFact to be defined in TheoryStrings instead of inside inference manager, which is clearer and eliminates some dependencies within inference manager.
Note that the inference manager of strings for now inherits from TheoryInferenceManager. Further standardization will make it inherit from the new InferenceManagerBuffered class.
This design will be merged into proof-new, which also has significant changes to strings inference manager.
|
|
equal selects (#4981)
The implementation of --ackermann mishandled selects in a subtle way:
If select is applied to two syntactically different arrays (that may be semantically equal), the ackermann preprocessing failed to generate the "all arguments equal implies terms equal" lemmas.
The problem is that we used the first argument (that is: the array) as lookup to identify terms that need to be considered for these lemmas. Instead we now use their operator (select) just like for uninterpreted function applications.
Fixes #4957 . Also adds a regression.
|
|
This is a followup to #4945 which simplifies the contract for computeRelevantTerms.
|
|
Cython has been causing issues recently, see e.g.
https://github.com/CVC4/CVC4/pull/4982/checks?check_run_id=1052433862.
It looks like the issue is that globally installed packages can't be
found by Python (maybe the global site-package directories changed/are
not included in the search paths anymore?). This commit changes the
installation of Cython to install it locally to the user instead of
globally. It also adds `bin` in the user base directory to `PATH` s.t.
CMake is able to find the `cython` binary.
|
|
This adds basic support for asserting internal facts with proofs in the inference manager class.
The purpose of this PR is twofold:
(1) From the point of view of proofs, this PR standardizes the management of proof equality engine within inference manager. Theories no longer have to manually construct proof equality engines, and instead are recommended to create inference managers.
(2) From the point of view of the new approach to theory combination, this PR ensures standard theory callbacks (preNotifyFact / notifyFact) are used for internal facts, regardless of whether proofs are enabled.
This will simplify several of the current (unmerged) changes for proof production in theory solvers on proof-new.
Notice this PR adds the utility method NodeManager::mkAnd, which is arguably long overdue.
Also notice this code is not yet active, but will be used on proof-new after this PR is merged.
|
|
These utilities will be used for making some of the core proof utilities term-context-sensitve.
|
|
|
|
This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine.
This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h.
It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h.
This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.
|
|
This PR adds support for incremental solving in bv_to_int.
This amounts to:
using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
|
|
Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.
|
|
TheoryQuantifiers is a theory that passes quantified formulas to QuantifiersEngine. This updates it to the new check template (see #4929).
Also does some minor cleanup in the cpp file.
|
|
This PR adds the proof post-processor, which is the final authority on putting together the overall proof. It additionally implements lazy pedantic failures and statistics.
This PR also corrects a subtle bug in the elimination of SUBS which requires a TRUE_INTRO/FALSE_INTRO in certain cases.
|
|
This updates the theory of floating points to the new interface (see #4929).
Notice that TheoryFP was not adding trigger terms to its equality engine (which should be done during notifySharedTerm), and thus was not propagating equalities between shared terms in combined theories. This PR updates its notifySharedTerm method to the default one.
FYI @martin-cs
|
|
The lemma generation for partial cad checks had a number of issues that have been fixed in this PR.
The previous version had both soundness issues and a very naive approach to handling algebraic numbers.
This new version is sound (fingers crossed) and allows to construct more precise, but also more complex lemmas.
To avoid constructing very large lemmas, a (somewhat arbitrary) limit based on the size of coefficients was added.
|
