| Age | Commit message (Collapse) | Author |
|---|
|
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 a followup to #4945 which simplifies the contract for computeRelevantTerms.
|
|
This updates the theory of floating points to the new interface (see #4929).
Notice that TheoryFP was not adding trigger terms to its equality engine (which should be done during notifySharedTerm), and thus was not propagating equalities between shared terms in combined theories. This PR updates its notifySharedTerm method to the default one.
FYI @martin-cs
|
|
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 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.
|
|
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
|
|
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.
|
|
|
|
Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().
|
|
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).
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
|
|
Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
|
|
The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack.
This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.
|
|
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.
|
|
|
|
This commit enables SymFPU assertions in production. The reason for this
is that there are some known problems with certain bit-widths, so we
prefer to be conservative. The commit also updates the run scripts for SMT-COMP 2019 to use `--fp-exp` since we have those additional checks in place now.
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
For a simple query `(not (= (fp.isSubnormal x) false))`, we were getting
a wrong model. The issue was that `(sign x)` was not assigned a value
and did not appear in the shared terms. In
`TheoryFp::collectModelInfo()`, however, we generate an expression that
connects the components of `x` to `x`, which contains `(sign x)`. As a
result, the normalization while building a model did not result in a
constant. This commit fixes the issue by marking `(sign x)` (and
`(significand x)`) as assignable. Assignable terms can take any value
while building a model if there is no existing value.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This should fix Coverity issues 1473025 and 1459599.
|
|
`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring
|
|
|
|
|
|
|
|
|
|
|
|
* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.
* Enable the bit-vector theory when setting the logic, not in expandDefinition.
This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.
* Use symfpu to implement the literal floating-point objects.
* Add kinds for bit-blasted components.
* Print the new kinds.
* Typing rules for the new kinds.
* Constant folding for the component kinds.
* Add support for components to the theory solver.
* Add explicit equivalences between classification functions and equalities.
* Use symfpu to do symbolic conversions of floating-point operations.
* Implement conversions via (over-)approximation and refinement.
* Correct a copy and paste error in the generation of uninterpretted functions for conversions.
|
|
* 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.
|
|
|
|
|
|
|
|
|
