| Age | Commit message (Collapse) | Author |
|---|
|
Does not support InstMatch interfaces anymore, which are spurious.
|
|
Also updates its inference manager to not track stats since the standard ones are now used.
This also sets up some dependencies in the sygus extension which will be used to implement InferenceId for the sygus extension, to be done on a separate PR.
|
|
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 cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
|
|
|
|
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 introduces new InferenceId for the theory of sets and uses them instead of InferenceId::UNKNOWN.
|
|
This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
|
|
Document UF entries of InferenceId enum.
|
|
This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
|
|
This moves the derived model class used in finite model finding to its own file, in the src/theory/quantifiers/fmf directory.
Updates the code to meet guidelines, no behavior changes.
|
|
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
|
|
This is necessary for the planned refactoring of TheoryInference::process. This forces datatypes to decide lemma vs. fact prior to buffering inferences.
|
|
This PR uses the new InferenceIds in the separation logic theory.
|
|
This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
|
|
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
|
|
This PR collects the InferenceId in the InferenceManagerBuffered class.
|
|
This PR adds a new statistics class that improves on HistogramStat if we know that the type is integral (also supporting enums).
Instead of using a comparably slow std::map like HistogramStat, IntegralHistogramStat uses a std::vector that is resized appropriately.
The integral values are simply cast to std::int64_t and used as indices into the vector.
|
|
This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.
|
|
|
|
This PR removes some obsolete code from the nonlinear solver.
The statistics will soon be replaced by a generic statistic in the theory inference manager.
|
|
Towards eliminating dependencies on quantifiers engine.
|
|
Theory BV now sets up the default equality engine for BV solvers that do not use their own equality engine like e.g. the BV bitblast solver. This commit also adds the missing equality engine pieces to the BV bitblast solver (getEqualityStatus, explain).
|
|
This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
|
|
There are compelling use cases not to automatically introduce SYMM steps in CDProof, e.g. in CDProofs used within ProofNodeUpdater for external conversions.
|
|
|
|
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.
|
|
The ensureLiteral method in CnfStream may apply CNF conversion to the given literal (for example if it's an IFF), which needs to be recorded in the proof. This commit adds a proof-producing ensureLiteral to ProofCnfStream, which is called by the prop engine if proofs are enabled.
This commit also simplifies the interfaces on ensureLit and convertAtom by removing the preRegistration flag, which was never used.
|
|
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 does a minor simplification to the interface for preprocessor. It has a postProcess call that is called after another unrelated call at the SmtSolver level (notifyPreprocessedAssertions) is made. This makes it so that Preprocessor::postProcess is inlined as the last step of process.
|
|
This refactors the term registration visitors (PreRegisterVisitor and SharedTermsVisitor), which are responsible for calling Theory::preRegisterTerm and Theory::addSharedTerm.
The purpose of this PR is to resolve a subtle bug in the implementation of PreRegisterVisitor (see explanation below), and to improve performance in particular on the Facebook benchmarks (where preregistering terms is currently 25-35% of runtime on certain challenge benchmarks).
This PR makes it so that that SharedTermsVisitor now subsumes PreRegisterVisitor and should be run when sharing is enabled only. Previously, we ran both PreRegisterVisitor and SharedTermsVisitor, and moreover the former misclassified when a literal had multiple theories since the d_theories field of PreRegisterVisitor is never reset. This meant we would consider a literal to have multiple theories as soon as we saw any literal that had multipleTheories. After this PR, we run SharedTermsVisitor only which also handles calling preRegisterTerm, since it has the ability to anyways (it computes the same information as PreRegisterVisitor regarding which theories care about a term).
The refactoring merges the blocks of code that were copy and pasted in term_registration_visitor.cpp and makes them more optimal, by reducing our calls to Theory::theoryOf.
FYI @barrettcw
|
|
We need to add to the current proof, regardless of whether we have used the factor skolem previously.
Fixes bugs found by @HanielB on SMT-LIB runs.
|
|
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 was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
|
|
This method is used to determine which skolems have definitions according to term formula removal. This optimizes the method using attributes similar to how expr::getFreeVariables works.
It will be used heavily for SAT relevancy. We should also consider updating the justification heuristic to use this method.
|
|
Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation.
|
|
./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.
|
|
Towards eliminating dependence on QuantifierEngine from inst_match_trie.
|
|
This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.
This uncovered 2 issues:
The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.
|
|
|
|
|
|
|
|
|
|
Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector.
Fixes #5693
|
|
|
|
Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
|
