| Age | Commit message (Collapse) | Author |
|---|
|
This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic.
|
|
This PR uses the new InferenceIds in the separation logic theory.
|
|
This PR collects the InferenceId in the InferenceManagerBuffered class.
|
|
This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.
|
|
This was an experimental option used in combination with separation logic.
|
|
|
|
|
|
Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.
|
|
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.
This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.
Fixes #5343, fixes #4926.
Work towards CVC4/cvc4-wishues#22.
|
|
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.
This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.
This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
|
|
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
|
|
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 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.
|
|
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.
|
|
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 updates the theory of separation logic to the new interface, which involves splitting up its check method based on the 4 check callbacks and using the theory state in the standard way.
No behavior changes, unfortunately a lot of code had to change indentation and was updated to new coding guidelines.
|
|
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 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)".
|
|
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.
|
|
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 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.
|
|
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.
|
|
This commit changes EmptySet to use TypeNode instead of Type.
|
|
This includes 4 changes:
Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.
This PR is also contingent on the performance tests for proof-new on SMT-LIB.
|
|
|
|
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
|
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
singletons in general. Note that the `Rewriter` class is still a
singleton, which will be changed in a future commit.
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
|
|
|
|
|
|
|
|
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
|
|
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|
|
|
