| Age | Commit message (Collapse) | Author |
|---|
|
Towards the strings array solver.
Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.
|
|
This does not yet clean up the usage of Rewriter::rewrite in the arrays
type enumerator yet. Will be cleaned up in a follow-up PR.
|
|
This further cleans up the class declaration in the header to comply
with code style guidelines.
|
|
This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.
|
|
Fixes #7056. Currently, we introduce a UF for conversions between FP
numbers and reals. This is done as part of `ppRewrite()`. The problem is
that terms sent to `ppRewrite()` are not fully preprocessed yet and the
FP theory solver was storing terms that were not fully preprocessed in a
map for later lookup. For the issue at hand, the conversion term
contained an `ite`, which was later removed. As a result, the theory
solver did not consider the term to be relevant when refining
abstractions. This commit changes the handling of conversion functions
to instead adding purification lemmas for conversion terms when they are
registered. The purification lemmas are needed, because otherwise, we
can't retrieve the model values for the term without the rewriter
interferring.
|
|
|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.
|
|
This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.
|
|
Fixes #6531.
This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.
It does some cleanup on relevant domain in the process.
|
|
|
|
|
|
This refactor additionally removes the caching for urem/udiv cases when
bit-blasting udiv/urem and eliminates the only rewrite() calls in the
bit-blaster. Caching is not required since repeated calls to udiv/urem
with the same arguments will produce the same circuit. Further, the rewrite()
calls during bit-blasting would further complicate the recording of
bit-blasting proofs and hence is removed.
|
|
This commit refactors the proof bit-blaster to properly track the pre- and post-rewrites in bbAtom(). The individual bit-blast steps are recorded in a term conversion proof generator. The overall bit-blast proof is stored in a BitblastProofGenerator, which tracks the pre- and post-rewrite and includes the bit-blast proof of the TCPG.
|
|
This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
|
|
This also introduces the produceDifficulty option which is analogous to produceUnsatCores.
It requires another unsat cores mode PP_ONLY, indicating that we are only tracking proofs of preprocessing. This option should perhaps be renamed to proofMode instead of unsatCoresMode, since its use is more general than for unsat cores. This will be addressed in a future refactoring.
|
|
|
|
This commit better integrates the StatisticsRegistry with the environment. It makes the registry an `EnvObj` itself and adds a getter to `EnvObj` to get the registry. It also refactors parts of cvc5 to use this new mechanism to obtain the registry instead of using the (global, static) `smtStatisticsRegistry()` function.
|
|
IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule.
|
|
|
|
This PR is based on #7171
|
|
|
|
Fixes #7002.
|
|
Currently, we are using non-standard attributes. With C++17, all the
attributes that we use regularly are now standardized. This commit
replaces the compiler-specific attributes with standard ones.
|
|
|
|
|
|
Towards supporting a (get-difficulty) command.
This tracks an estimate of the difficulty of preprocessed assertions during solving. It will be connected to TheoryEngine (via RelevanceManager) in a followup PR.
|
|
The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.
This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.
|
|
This commit removes TheoryState::options() by changing more classes to
EnvObjs.
|
|
This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.
This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.
Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.
|
|
This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
|
|
This PR:
Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.
|
|
The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.
|
|
|
|
This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.
|
|
This derives sygus unification utility objects from EnvObj where
necessary. There's one remaining occurrence of Rewriter::rewrite in
sygus_unif_rl.cpp, which is a bit tricky to address and thus subject to
a future PR.
|
|
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
|
|
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
|
|
|
|
This moves the standard method for rewrites in proofs from TheoryBuiltinProofRuleChecker to Rewriter. The motivation for this change is to make various kinds of rewrite methods (standard rewrite, extended rewrite, extended equality rewrite, evaluate) accessible throughout the code in a standard way. After this PR, it is possible to know variants of the REWRITE proof rule application by having access to the rewriter, instead of having to get the builtin proof rule checker. Note that TheoryBuiltinProofRuleChecker::applyRewrite *cannot* be static since access to the rewriter is not longer permitted to be static.
It also removes some unused infrastructure from Rewriter.
Followup PRs will remove applyRewrite for TheoryBuiltinProofRuleChecker in favor of calling the rewriter directly.
|
|
|
|
This further reorders the header according to the code style guidelines.
|
|
EnvObj. (#7130)
|
|
Note: the diff in theory.h is only huge because of small changes that caused huge reformat. The effective change is only that it now derives from EnvObj, does not have a member d_env (because it inherits it) and does not need getLogicInfo (because that's in EnvObj).
|
|
Towards replacing that option with a logic check throughout.
|
|
backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.
|
|
PR #7103 did not quite fix the unit test: The types of the lambda and
the expected bags were still off. This fixes the unit test.
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
