| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.
This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).
Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
|
|
This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.
|
|
This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.
|
|
This corrects an issue in our context-dependent simplification which limited the cases it was applied.
Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.
|
|
This PR adds kind BAG_MAP to bags.
|
|
There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.
This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.
This corrects some proof checking errors on string benchmarks.
|
|
Fixes #6838.
|
|
Eliminates another call to currentSmtEngine.
This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.
|
|
This adds the last two remaining API methods required for implementing the text output of get-model on the API side.
A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.
This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
|
|
This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
|
|
This eliminates another call to currentSmtEngine.
After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).
|
