| Age | Commit message (Collapse) | Author |
|---|
|
This class is a wrapper around OutputChannel and EqualityEngine. It is preferred that the Theory use this interface when asserting "internal facts" to the equality engine, and for sending lemmas, conflicts and propagations on the output channel.
This class will be useful when trying new methods for theory combination, where all theories behavior can be modified in a standard way based on modifications to the base inference manager class.
|
|
This updates TheoryUF to use the 4 check callbacks instead of implementing check, and uses the official TheoryState object instead of its context::CDO<bool> d_conflict field.
It also makes a minor change to collectModelValues for const and to preNotifyFact to include an isInternal flag.
|
|
This connects the implementation of CombinationEngine into TheoryEngine. By default, the combination engine of theory engine is CombinationCareGraph.
This PR also consolidates and simplifies how models are built, note that:
The TheoryModel object no longer tracks whether it is built, instead that is the job of ModelManager,
The TheoryModelBuilder object is no longer responsible for calling TheoryEngine's collect model info method.
Quantifiers engine uses a simpler interface for ensuring that TheoryEngine's model is built.
This PR also makes some minor simplifications to TheoryEngine from the centralEe branch.
Note that no significant behavior changes are intended in this PR.
|
|
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
|
|
checking unsat cores (#4941)
Doing it via commands being added to the coreChecker SMT engine is not necessary since we can directly add assertions after expansion from the original SMT engine.
|
|
This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR.
FYI @barrettcw
The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.
|
|
This includes a standard method for safe explanations and the option to disable all trigger terms.
|
|
The `parseErrorHelper` message can run into memory errors when the it prints the last line and this last line is not terminated by a newline. I suspect other conditions may trigger it as well (like only using `\r` as line terminator).
This comit computes the size of the buffer from the start of the current line to the end of the buffer and makes sure that we never go beyond this buffer. The calculation looks a bit awkward, I've not been able to obtain this information from the ANTLR input stream in a nicer way...
(I found this issue when looking at #4866).
Fixes #4069 .
|
|
This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.
|
|
|
|
This class is responsible for model building when using a distributed approach for equality engines.
This PR defines the class but does not yet activate it in TheoryEngine.
This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.
|
|
Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.
This includes:
A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).
Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.
FYI @barrettcw
Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.
|
|
|
|
This makes the equality engine manager responsible for initializing the equality engine of the model.
It also moves the base equality engine manager class to its own file.
Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior.
|
|
There is a non-standard use of trigger terms in the array theory via `EqualityEngine::addTriggerTerm`.
Trigger terms are only supposed to be shared terms, and are added to the equality engine for the sake of propagating equalities between shared terms. The array theory does two non-standard things:
(1) it registers (possibly) non-shared terms as triggers in its `preRegisterInternal` method,
(2) it filters propagations between anything except non-shared arrays in its `eqNotifyTriggerTermEquality` method.
The latter is only necessary because of the former. It is unnecessary to do *either* of these things. Instead, the array theory should simply add the terms to the equality engine (as non-triggers) during preRegisterInternal. Note that it additionally correctly adds trigger terms in its `notifySharedTerm` method.
With this commit, the array theory uses the equality engine (wrt propagation) in a standard way.
|
|
This PR removes spurious theory method calls that are not implemented.
It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)".
|
|
arithmetic (#4930)
This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.
This addresses CVC4/cvc4-projects#113.
Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:
QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.
Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.
|
|
We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.
Fixes #4990.
|
|
This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.
FYI @aniemetz @mpreiner
|
|
This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).
Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.
Notice this PR does not update the theories to use these states yet, it simply adds the objects.
|
|
Towards refactoring SmtEngine / converting Expr -> Node.
|
|
This is further work towards a centralized approach for equality engines.
This PR merges the eqNotifyTriggerEquality callback with the eqNotifyTriggerPredicate callback, and adds assertions that capture the current behavior. It furthermore makes addTriggerEquality private in equality engine and invoked as a special case of addTriggerPredicate. Note this PR does not impact the internal implementation of these methods in equality engine, which indeed is different.
There are two reasons to merge these callbacks:
(1) all theories implement exactly the same method for the two callbacks, whenever they implement both. It would be trivial to do something different (by case splitting on the kind of predicate that is being notified), and moreover it is not recommended they do anything other than immediately propagate the predicate (regardless of whether it is an equality).
(2) It leads to some confusion with eqNotifyTriggerTermEquality, which is invoked when two trigger terms are merged.
|
|
This code is unused and obsolete.
|
|
str.at expands to str.substr, thus this benchmark (may) require strings-exp if things do not rewrite/preprocess. This triggers a regress0 failure on proof-new currently.
|
|
This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...
|
|
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).
|
|
Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.
|
|
Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.
|
|
In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.
|
|
Calling (reset) multiple times produced parsing problems (#4866) and could probably lead to all kinds of interesting issues.
In a nutshell, reset() failed to properly reset d_initialOptions (which is used to properly reset d_options) so that all options defaulted after the second call to reset().
This PR properly sets d_initialOptions after a reset (and the filename as well).
Fixes #4866.
|
|
This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.
|
|
This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.
|
|
This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods.
The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers.
The next step will be to have the SolverState objects in theory of sets and strings inherit from this class.
|
|
This is work towards a configurable approach to equality engine management. This PR does not change any behavior, it only reorganizes the code.
This PR introduces the standard template for collectModelInfo, which isolates the usage of equality engine in relation to the model. In the future, theories will be encouraged to use the standard template for collectModelInfo and override collectRelevantTerms/collectModelValues only. This is to allow custom theory-independent modifications to building models (e.g. don't assert equality engine to model if we are using a centralized approach).
This PR standardizes TheoryArrays and TheoryDatatypes custom implementation of collectRelevantTerms as work towards using the standard template for collectModelInfo. Notice this required separating two portions of a loop in TheoryArrays::collectModelInfo which was doing two different things (collecting arrays and relevant terms).
|
|
|
|
This is the callback class for processing the final proof, which connects proofs of preprocessing and expands unwanted macro steps based on proof granularity mode.
The next step will be to add the ProofNodeUpdater that uses this callback and runs final sanity checks for checking proofs.
|
|
This is work towards a configurable approach to theory combination.
Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.
|
|
This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.
This PR updates Expr -> Node for the sygus interface in SmtEngine.
SmtEnginePrivate is no longer needed and is deleted with this PR.
|
|
This PR adds the relevance manager module, which will be used in forthcoming PRs to query assignments for whether a literal is "relevant" (e.g. critical for satisfying the input formula). Leveraging this technique has led to noticeable improvements for non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager).
This PR does not enable it, but adds the module only.
|
|
Callbacks for term-context-sensitive terms.
It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.
These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.
|
|
```
(! sc (^ ...)
^ this is the identifier!
```
We require that side-conditions have an identifier. We usually provide
this identifier, but in this one case we did not.
The old lexer accepted the side condition without the identifier. The
new one does not.
|
|
Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.
|
|
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 updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.
Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.
For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.
This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.
|
|
A recent commit (77e9881) simplified the form of the conclusion in regular expression star unfolding for the sake of uniformity in our internal proof calculus. However, this led to a noticeable drop in performance on a few specific RE benchmarks (the Norn set). This preserves the old behavior by extending the core rule for RE unfolding.
It also makes one minor change to the strings proof checker carried over from the proof-new branch.
|
|
This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.
|
|
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.
|
|
This changes an initialization issue in regarding PropEngine and TheoryEngine.
In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.
The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.
|
|
It also adds enumeration for two new rules that have been recently added.
|
|
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.
|
