| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
Fixes an issue with --proof-eager-checking and --bitblast=eager.
|
|
Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.
|
|
Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
|
|
Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.
|
|
assignment (#6868)
This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.
This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.
This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.
|
|
This commit changes BV proof logging to record coarse-grained bit-blast steps during solving and expanding these steps on-demand in the proof post processor.
|
|
This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module.
The next PR will connect this module to theory_arith / theory_arith_private.
Towards ensuring type constraints are met for linear arithmetic models.
|
|
Fixes #4791.
|
|
With CMake 3.11 and later, `<DOWNLOAD_DIR>` is substituted in
`ExternalProject_Add` but not in older versions [0]. To maintain
compatibility with older versions of CMake, this commit changes
`ExternalProject_Add` to use `<DOWNLOADED_FILE>` instead, which is both
nicer and substituted in older versions of CMake.
[0] https://cmake.org/cmake/help/latest/release/3.11.html#modules
|
|
This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.
This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.
|
|
Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.
|
|
Currently, `cvc5::Exception` does not have default visibility, which can
cause cvc5 to terminate when trying to catch it in `main.cpp`.
Presumably, this is because the necessary typeinfo is missing [0]. Due
to this issue, production builds for M1 on macOS crashed when parser
exceptions were thrown. The commit changes the visibility of the
exception.
[0] https://gcc.gnu.org/wiki/Visibility,
"Problems with C++ exceptions (please read!)"
|
|
This makes it so that debug-check-models applies in production mode, not just in debug mode. It also verifies that type constraints are met.
|
|
Have unsat cores regression tested also with default mode.
|
|
When compiling and running cvc5 on macOS with an M1 CPU, the regression
test regress0/cores/issue4971-0.smt2 returned unsat instead of the
expected unknown for the first (check-sat) command. This commit
makes the regression more robust by adding --cegqi-full and expecting
unsat.
|
|
When building cvc5 on macOS for M1 natively, ANTLR's version of
`config.sub` does not recognize `aarch64-apple-darwin20.5.0`. This
commit fixes that issue by downloading the latest version of
`config.sub` (similar to what we are already doing for `config.guess`).
The commit also updates the URLs for `config.guess` and `config.sub` to
the URLs recommended in the files themselves. The commit also does some
minor cleanup/simplifications of the commands for building ANTLR.
|
|
This fixes an unsoundness issue in the sets + cardinality solver.
One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:
if T = (union T S), then (intersect T S) = S.
The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.
This PR also does some minor cleanup.
|
|
This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.
|
|
|
|
This PR adds a script for building a wheel distribution for pycvc5. It automatically reads the top-level CMakeLists.txt to obtain the current version number, and then runs the standard setup from setuptools with an extension command class that configures and builds cvc5 with Python bindings. This wheel file is sufficient for uploading to Pypi. Although, note that we need to build for different operating systems and different Python versions because of the extension modules.
Note: another option is to use the scikit-build instead of doing the configuring and building manually. However, I ran into some issues when the setup.py file was not at the top-level. Because we prefer to have it hidden in a sub-folder, I took the manual route for now. In the future, we could consider changing this.
|
|
The let map is printed as JSON-like dictionary via a comment of the dot output.
|
|
Adds remaining regressions from issue #4791, which we can handle with the different new unsat-core modes. Note that issue4971-1.smt2 requires the sat-proof mode for unsat cores.
|
|
|
|
This name is the name of the symbol we parse. Internally, we still call
it POW2. This is a fix for the problem that `pow2` may clash (and
already does clash on SMT-LIB benchmarks) with user-defined symbols.
|
|
Fixes one of the issues in the nightlies.
|
|
Fixes #6259.
|
|
This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.
|
|
This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.
|
