Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
`stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)`
was cutting off "A" because it is a non-digit. This is wrong, however,
because `(int.to.str n)` can return the empty string. This commit
makes `stripConstantEndpoints()` less aggressive by not using
`str.to.int` terms to cut off non-digits anymore.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
|
|
|
|
|
|
This required fixing the OpTerm handling for mkTerm functions in the API.
|
|
Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.
|
|
|
|
`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
|
|
|
|
|
|
|
|
Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.
|
|
* Extended DRAT signature to operational DRAT
The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.
The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).
You can run the new AND old DRAT tests by running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```
* Apply suggestions from code review (Yoni)
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
|
|
|
|
This reverts commit b6dcaeb9b1e430941f1f4345152ebad21634a0be.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.
|
|
|
|
|
|
This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.
|