| Age | Commit message (Collapse) | Author |
|---|
|
We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.
|
|
This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.
|
|
Miscellaneous changes from proof-new.
|
|
This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
|
|
This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
|
|
The justification heuristic stores a "copy" of assertions as TNode. As witnessed by #5938, these TNodes may invalid.
This PR changes this to store Nodes instead.
Fixes #5938.
|
|
This case was previously unhandled and exercised by a recently added regression.
|
|
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
|
|
Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
|
|
|
|
The static-learning preprocessing sometimes added non-rewritten assertions, despite being used in a part of the preprocessor that assumes all assertions to be rewritten. This may then break other passes further down, in the case of #5729 the non-clausal simplification which explicitly asserts that assertions are rewritten. This PR rewrites the respective assertion properly in the static-learning pass.
Fixes #5729.
|
|
This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
|
|
In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
|
|
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
|
|
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
|
|
When a clause is being explained, the negation of each of its literals, other than the one it propagates, needs to be explained. This process may lead to the creation of new clauses in the SAT solver (because if a literal being explained was propagated and an explanation was not yet given, it will then be computed and added). This may lead to changes in the memory where clauses are, which may break the reference to the original clause being explained. To avoid this issue we store the literals in the reason before we start explaining their negations. We then iterate over them rather than over the clause, as before.
|
|
This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.
|
|
This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
|
|
Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.
|
|
This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.
|
|
This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly.
This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout.
This is in preparation for further improvements to enumerative instantiation.
|
|
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.
|
