| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Fixes #5074. This commit fixes an issue in the rewriter of
`str.replace_re` and `str.replace_re_all`. For both operators, we do two
kinds of rewrites: (1) If the first argument is a constant, then we
check whether the regular expression appears in that constant and (2) we
check whether the regular expression matches the empty string. Both of
those checks were assuming a constant regular expression but there was
no guard in place for it. This commit adds the missing guard.
|
|
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
|
|
This makes TheorySep use a standard buffered inference manager. Notice the behavior in TheorySep::doPending was simplified to assert both facts and lemmas. Previously, this was doing something strange: if there were any lemmas, then both facts and lemmas would be processed as lemmas, otherwise the facts would be processed as facts. Notice that TheorySep currently does not use facts by default. This design can be addressed in the future.
Note this PR eliminates the need for a custom explain method in TheorySep.
|
|
A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
|
|
This is work towards updating the arithmetic solver to the new standard, and in particular isolating TheoryArithPrivate as the "linear solver", and TheoryArith as the overall approach for arithmetic.
This transfers ownership of the non-linear extension from TheoryArithPrivate to TheoryArith. The former still has a pointer to the non-linear extension, which will be removed with further refactoring.
This PR additionally moves the code that handles the interplay of the non-linear extension in TheoryArithPrivate::collectModelInfo to TheoryArith, and simplifies the model interface for TheoryArithPrivate.
|
|
Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.
The changes in this PR:
All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.
Remark: disabling white-spaces when reviewing this PR is recommended.
|
|
|
|
|
|
This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
All uses of proof equality engine are now guarded such that the ordinary equality engine is used when proofs are not enabled. Thus, we can make proofs mandatory in proof equality engine. This eliminates the need for some guards.
Some indentation changed, but there are no additions in this PR.
|
|
This eliminates the parent relationship from solver state to theory sets.
|
|
|
|
This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine.
Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers.
This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit.
The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.
|
|
There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019.
Fixes #5019.
|
|
This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added.
Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed.
|
|
For some reason, our ABC build was including cnf_stream.h in an
extern "C" block instead of outside of it, which made the build fail
because the header indirectly includes cdqueue.h, which uses
templates. This change is older
(e9bfbb2)
but only started causing problems with our nightly builds recently.
|
|
Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
|
|
This PR makes the translation of plus and times by:
using plain mod rather than introducing a skolem. If this proves to be a bottleneck, we can try to tackle it where mod is treated in the solver in the future. This will make it easier to introduce support for quantifiers, as we don't need to introduce new variables under quantification.
Making sure everything is binarized in more places of the translation.
|
|
Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements.
The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants.
Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)).
It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.
|
|
The BVToInt preprocessing pass was using uint, which appears to be
undefined when we cross-compile for Windows. This commit fixes the issue
by using size_t.
|
|
Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should.
In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes. The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.
|
|
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.
This PR includes setting up some connections into the various modules for proof production.
|
|
This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.
This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
|
|
This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).
Fixes #4850.
|
|
mkScope (#5012)
This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.
A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
|
|
Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
|
|
|
|
This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass.
Many parts are wrapped by helper functions and so the main loop becomes smaller.
remark: selecting "Hide whitespace changes" cuts the diff by ~50%.
|
|
Fixes #4973.
|
|
Previously, in case we encountered a term we cannot translate to integers (e.g. a bit-vector array), we would fail.
This PR improves that behavior by keeping the original term, and potentially wrapping it BV_TO_NAT and INT_TO_BV operators.
A test which includes a bit-vector array is included, which was not supported before.
In addition, the treatment of uninterpreted functions is refactored and documented better.
|
|
Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.
|
|
This includes some changes to proof node updater that are not currently on master.
This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.
It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.
|
|
Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).
|
|
This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.
|
|
Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.
|
|
This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:
(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.
|
|
Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies.
This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas.
Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative.
A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.
|
|
Fixes #5032
|
|
This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.
|
|
This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.
|
|
This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.
It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.
|
|
|
|
This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.
This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.
This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).
|
|
|
|
This PR modifies the printers to use Result::Sat, "internal" version of BenchmarkStatus, for printing benchmark status commands.
|
|
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
|
|
on GitHub (#4989)
Signed-off-by: Malte Mues (mail.mues@gmail.com)
|
|
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.
|
