| Age | Commit message (Collapse) | Author |
|---|
|
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
|
|
This moves the utility class beneath quantifiers registry.
|
|
Also moves several proof-specific options to proof_options.
|
|
This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.
|
|
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.
|
|
(#5939)
Required for work on external proof conversions.
|
|
Adds an option to optionally print conclusion in the AST proof.
|
|
This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.
|
|
This PR introduces a new arithmetic kind for indexed root predicates.
An indexed root predicate compares a real variable to the k'th root of a given polynomial as follows:
Let IRP_k(x ~ 0, p) an indexed root predicate with k a non-negative number, x some real variable, ~ an arithmetic relation (e.g. =, <, ...), and p a polynomial over x (and possibly other variables).
If p contains variables apart from x, we can only evaluate the expression over a suitable assignment for at least these variables.
The evaluation of this expression is equivalent to computing the k'th real root of p in x (with all other variables evaluated over a given assignment) and comparing this real root to zero (according to the relation symbol ~).
Note that we currently do not intend to use this structure for solving, but require it for representing and printing CAD proofs.
|
|
This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.
|
|
This PR merges some cleanup in the transcendental solver from proof-new.
It adds a new struct ApproximationBounds that replaces an opaque std::vector and does some general refactoring in the TaylorGenerator class, removing dead code and using fixed-width integers.
|
|
Adds a simple helper for CAD to prune redundant intervals. It is just a wrapper for cleanIntervals right now, but will be responsible to making sure the CAD proof is pruned as well.
|
|
Accidentally was not sending lemmas in one interface when proofs are enabled due to recent refactoring.
|
|
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.
|
