| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
|
|
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
|
|
This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.
This is in preparation for adding new techniques to the eager solver.
No behavior changes in this PR, only reorganization.
|
|
Changes:
renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)
|
|
While addressing the review on 6898ab9, strings eager conflicts were accidentally disabled, this reenables them.
|
|
This updates the inference manager in strings in two ways:
(1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones.
(2) It has support for proof generation via the InferProofCons utility.
This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This is towards the new standard for theory solvers.
This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.
Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).
|
|
This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.
The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.
Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
|
|
This includes eliminating TheoryBV's call to eqNotifyNewEqClass and fixing an issue with string's eqNotifyNewEqClass method, which was registering constant integers.
It also removes some unnecessary methods in Theory.
|
|
Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.
TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.
This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.
|
|
|
|
Towards theory of sequences.
This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.
|
|
|
|
|
|
Several kinds of splitting lemmas in the strings solver can sometimes be avoided by observing that str.len(x) != 0 implies that x is non-empty. This generalizes the check for whether x is non-empty is explainable in the current context.
|
|
Towards theory of sequences.
|
|
|
|
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
|
|
Code move only, no updates to behavior or content of code in this PR.
|
|
Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.
|
|
|
|
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
This is work towards splitting a "core solver" object from TheoryStrings.
This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.
It also corrects an issue where we were maintaining two `d_conflict` fields.
|
|
This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.
It also deletes some unused/undefined functions in theory_strings.h.
There are no major changes to the behavior of the code or its documentation in this PR.
This is work towards #1881.
|
