| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
|
|
recursively (#2270)
|
|
|
|
This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.
|
|
This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.
|
|
We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!
My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`
and that I could not provide random other option values.
|
|
|
|
|
|
|
|
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
|
|
Seems to have no impact on Norn, and is helpful for a number of applications.
|
|
|
|
|
|
|
|
|
|
|
|
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
|
|
|
|
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
|
|
|
|
|
|
This implements solution number 2 for issue #2613.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
|
|
(#2478)
|
|
|
|
|
|
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
|
|
This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
|
|
Further, remove redundant gmp.h include in options_handler.cpp.
|
|
|
|
|
