| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Note the change to the unit test makes it so the test is not dependent on Node ID order.
|
|
Fixes #6639. The issue cannot be reproduced on current master and `git
bisect` suggests that commit adf497af7a3fc8b06b875eaf9feca2568d0ba9d8
fixed the issue.
|
|
|
|
Towards support for external proof conversions.
|
|
This issue arises when using the central equality engine on several regressions.
|
|
This is the last 2 remaining theories not to use the default handling of equality proofs.
In preparation for proofs in central equality engine.
|
|
This class will make the uses of the fast enumerator customizable.
|
|
This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.
|
|
This enables default support for equality proofs in the theory of sets.
This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.
|
|
Makes arithEqSolver more robust to propagations from multiple sources, changes the default relationship to congruence manager based on preliminary results on SMT-LIB.
|
|
This adds changes from the centralEeDev branch for datatypes.
The changes in behavior are that the inference manager clears its pending inferences when the state is in conflict, and preCheck processes pending facts immediately (which may have been enqueued prior to the call to check via ee merges). These are required to make datatypes robust to the order in which check / merge / backtracks can occur.
|
|
Allows congruence manager to use its own (non-official) equality engine if both it and the arithmetic equality solver are enabled.
|
|
Currently, the CLN `CONFIGURE_COMMAND` chains multiple commands using
`&&` but this does not seem to work with CMake 3.20.4 and CMake 3.19.7
and is also not the recommended way of doing it. The commit fixes the
issue by using additional `COMMAND`s and also switches to using the
CMake's `chdir` instead of `cd`.
|
|
This commit changes the output of our configuration to show which
dependencies are being built as part of the cvc5 build. For example:
```
ABC : off
CryptoMiniSat : off
GLPK : off
Kissat : off
LibPoly : on (local)
CoCoALib : off
Build libcvc5 only : off
MP library : gmp (system)
Editline : off
```
Indicates that `LibPoly` was not found in the system and is thus built
as part of the cvc5 build and GMP was found in the system.
|
|
Newer compilers, such as GCC 11, default to C++17. CoCoA does not
compile with C++17 and its check for the C++ version used by the
compiler does not take into account newer C++ versions. As a result,
building CoCoA using `--auto-download` fails with GCC 11. This commit
adds a patch that makes the test in CoCoA take into account compilers
that default to C++17 or newer.
|
|
When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead.
This is enabled via option --fp-lazy-wb.
|
|
This makes it so that we do not consider non-singleton equivalence classes of DT for non-datatype terms to be relevant. This impacts how model construction is done for datatypes.
It's not clear why this method considered such terms to be relevant, I believe this was done to mask a previous bug; regressions now pass when this method is simplified.
Doing this is definitely wrong when using central equality engine, hence the motivation for this simplification.
|
|
This class is responsible for setting up the central equality engine. It relies on a new static method Theory::usesCentralEqualityEngine, which will be refined in followup PRs.
This PR does not change the behavior, it only adds the class.
Further PRs will connect this class to CombinationEngine, make it optionally enabled, and make the remaining changes to TheoryEngine to make it compatible.
|
|
|
|
This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.
|
|
|
|
|
|
|
|
On some platforms, autotools installs ANTLR3's libraries into lib but
CMAKE_INSTALL_LIBDIR is set to lib64 (e.g., Fedora 33). This commit
sets --libdir to force autotools to install the library into the
directory specified by CMAKE_INSTALL_LIBDIR.
|
|
On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building CMS (e.g., with `./configure.sh --cryptominisat --auto-download`): CMS adheres to the default value of `CMAKE_INSTALL_LIBDIR` to work out where to install the library files (so `lib64` on openSUSE), which fails when cvc5 tries to find these in `lib`.
Without this change, the build fails as follows:
```
<snip>
src/CMakeFiles/cvc5.dir/theory/type_enumerator.cpp.o -Wl,-rpath,:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: deps/lib/libcadical.a deps/lib/libcryptominisat5.a ../deps/install/lib64/libglpk.a deps/lib/libpicpolyxx.a /usr/lib64/libgmp.so deps/lib/libpicpoly.a /usr/lib64/libgmp.so && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libcryptominisat5.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```
and where:
```
avj@platypus ~/clones/cvc5/master/build$ find . -iname "libcryptominisat5.a"
./deps/src/CryptoMiniSat-EP-build/lib/libcryptominisat5.a
./deps/lib64/libcryptominisat5.a
```
(notice: `lib64` in the second path!)
This commit fixes this discrepancy to ensure that cvc5 checks for CMS on `CMAKE_INSTALL_LIBDIR` as well.
**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
On 64-bit openSUSE (and maybe other distributions), the default install directory for static libraries is `lib64` *not* `lib`. This has an impact on cvc5 when it is automatically building ANTLR3: ANTLR3 follows the system-wide default of `lib64`, which fails when cvc5 tries to find these in `lib`.
Without this change, the build fails as follows:
```
<snip>
src/parser/CMakeFiles/cvc5parser.dir/smt2/Smt2Parser.c.o -Wl,-rpath,/home/avj/clones/cvc5/lib64_cms/build/src:::::::::::::::::::::::: src/libcvc5.so.1 deps/lib/libantlr3c.a && :
/usr/lib64/gcc/x86_64-suse-linux/11/../../../../x86_64-suse-linux/bin/ld: cannot find deps/lib/libantlr3c.a: No such file or directory
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
```
and where:
```
avj@platypus ~/clones/cvc5/lib64_cms/build$ find . -iname "libantlr3c.a"
./deps/src/ANTLR3-EP-runtime/.libs/libantlr3c.a
./deps/lib64/libantlr3c.a
```
(notice: `lib64` in the second path!)
This commit fixes this discrepancy to ensure that cvc5 checks for ANTLR3 on `CMAKE_INSTALL_LIBDIR`, which matches that `autotools` will use.
**Note**: `CMAKE_INSTALL_LIBDIR` comes from `GNUInstallDirs`, and this is `include`'d in cvc5's top-level `CMakeLists.txt`
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
Initial work towards rewrite rule reconstruction
|
|
This makes FMF not handle quantified formulas when FMF options are disabled, apart from those marked internal.
This is required for combinations of sequences + quantified formulas.
|
|
Fixes #6866. The `theory_airth_cad_white` unit test has been failing on
some platforms (e.g., macOS) due to statically linking libpoly in
libcvc5 and then separately linking it in the unit tests. This resulted
in issues with `static` variables. This commit fixes the issue by
avoiding linking libpoly in the unit tests and instead relying solely on
libcvc5.
Co-authored-by: Ouyancheng <1024842937@qq.com>
|
|
Fixes #6047. The test was disabled because ASan found a use-after-free
due to an object allocated in the top scope being destroyed after the
scope (see #2607 for a detailed explanation). At first, the plan was to
add support for this use case. However, we have decided that we
currently don't need support for this feature and added a guard against
it (#6082). This commit reenables the test but changes it to destroy the
object allocated in the top level scope before the corresponding level
is popped. It additionally adds a test of the guard from #6082.
|
|
Caught by a regression on proof-new, where an instantiation was the symmetric equality of an instantiation on a previous call to check-sat. Proofs of instantiation should be user-context dependent.
|
|
|
|
--arith-eq-solver is a new option to enable the equality solver in arithmetic, disabled by default.
This PR connects the equality solver to TheoryArith when this option is enabled.
This is in preparation for the central equality engine.
|
|
This is work towards the central equality engine. This adds a module of arithmetic that uses the equality engine in the default way.
This class will be incorporated into theory_arith.cpp. It will be the replacement for CongruenceManager when we use the central equality engine architecture.
|
|
Preparation for central equality engine.
|
|
Adds a utility for converting nodes. This is the first step towards the LFSC proof conversion.
|
|
|
|
|
|
|
|
|
|
Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.
So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.
|
|
|
|
Previously we were not considering proofs for HO equalities (i.e., between operators) that were transitivity chains. This commit generalizes the elaboration procedure in eq_proof to do so.
|
|
The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.
This also refactors the debugging traces in this class.
|
|
In preparation for more extensions to this aspect of the synthesis solver.
|
|
Users of an equality engine should each use the same proof equality engine that wraps it. This ensures that theory inference managers do so, by tracking the official proof equality engine for an equality engine in theory inference manager.
This is in preparation for (proper equality proofs for) central equality engine.
It also adds some debugging code that is highly useful for debugging issues related to when equalities are processed in theory inference manager.
|
|
This fixes our model construction for sequences of infinite element type.
We were relying on getModelValue in our model construction which is incorrect since it assumes that the element type's theory can provide concrete values during model generation time. This makes the sequence model construction more robust by generalizing how model values are assigned: we use skeletons instead of concrete values when the element type is infinite.
This fixes some open model generation issues with Facebook benchmarks.
|
|
This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.
|
|
|
