| Age | Commit message (Collapse) | Author |
|---|
|
Currently, `NodeBuilder` takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the `d_inlineNvChildSpace` array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a `NodeValue` on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the `NodeBuilder` code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
|
|
An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.
An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).
This PR ensures we are robust to these cases.
This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
|
|
This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.
This fixes the second benchmark from #6203.
This PR also improves our traces for checking models in strings.
|
|
|
|
|
|
This makes it so that the decision manager is accessible from TheoryInferenceManager.
This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.
|
|
String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode.
This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered.
The PR also simplifies our policies for when string terms are registered slightly.
Fixes #6072.
|
|
Helps debugging model issues.
|
|
Also eliminates use of raw output channel in strings.
|
|
Fixes #6142.
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.
It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
|
|
This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.
As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:
(P (witness ((x T)) (A x)))
now we return:
(P k), with skolem lemma ( (A k), k )
Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.
|
|
Fixes #6075.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.
These errors were caught by the LFSC proof checker.
|
|
This changes things so we process inferences with AND conclusions as lemmas always.
This fixes #6056, that benchmark times out.
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
This case was previously unhandled and exercised by a recently added regression.
|
|
Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.
It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.
Fixes #5940.
Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.
|
|
This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
|
|
Fixes model soundness issue (fixes #5915).
|
|
This is now subsumed by the general stat in TheoryInferenceManager
|
|
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 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 PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
|
|
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
|
|
Fixes #5816.
|
|
This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.
Current results on the eager solver on SMT-LIB shows this change has very little performance impact.
Fixes #5692, fixes #5610.
|
|
This adds a missing inference for disequality between seq.unit terms, which was not handled previously.
Fixes #5666.
|
|
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
|
|
Rename strings::InferInfo::d_newSkolem to InferInfo::d_skolems to match bags::InferInfo:d_skolems
|
|
This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.
Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.
|
|
This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.
This is in preparation for adding new techniques to the eager solver.
No behavior changes in this PR, only reorganization.
|
|
Changes:
renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)
|
|
This PR adds inference generator for basic bag rules.
|
|
Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.
This also does some minor refactoring in some preprocessing. No behavior is changed.
|
|
|
|
Renamed InferInfo::getAntecedant to InferInfo::getAntecedent
|
|
This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.
This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.
|
|
This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.
Fixes #5547.
This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.
It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.
I will do performance testing on this PR.
|
|
There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.
Fixes #5611.
Note this inference was not previously covered in our coverage build.
|
|
|
|
|
|
This is required for handling inputs that combine strings and sequences.
Fixes #5542.
|
|
Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.
This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.
To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.
Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.
|
