| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This adds a missing inference for disequality between seq.unit terms, which was not handled previously.
Fixes #5666.
|
|
|
|
Previously we were unable to dump assertions in ProcessAssertions::apply for the definition-expansion, simplify and repeat-simplify passes.
|
|
This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
|
|
|
|
|
|
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
|
|
In rare cases, theory combination would be run when theory engine still needs check. This was limited to cases where the output channel is used but no lemmas were sent (TheoryEngine::needCheck() vs. d_lemmasAdded).
This led to problems in the theory of sets, which does not run a full effort check if theory engine needs check (since it knows it will be called to check again). However, running theory combination in these cases is not safe since theory of sets computes information pertaining to the care graph during its full effort check. Running theory combination otherwise would lead to theory of sets using stale data, leading to crashes due to terms not appearing in the equality engine.
This fixes #4124 (which appears not to trigger on master anyways currently).
This bug has also appeared on my sat relevancy development branch, hence fixing on master.
|
|
|
|
This member is currently unused.
|
|
|
|
|
|
|
|
This statistic is unused, I believe it is leftover from deleted code.
|
|
This PR makes the optimization introduced in bbca987 optional.
|
|
This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
|
|
The documentation regarding --static-binary is improved.
|
|
This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.
|
|
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from
l1 v l2 ~l1 v l3 ~l2 v l3
(ok) ------------------------------
l3
in which l3 = l1 v l2, to
l1 v l2 ~l1 v l3 ~l2 v l3
(bad) ------------------------------
l3 v l3
---------
l3
This commit now catches the trivial cycle before it's generated.
|
|
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
|
|
(#5850)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.
Also improves a bit tracing and some comments.
|
|
|
|
This simplifies our algorithm for theory preprocessing. The motivation is two-fold:
(1) Proofs are currently incorrect in rare cases due to incorrectly tracking pre vs post rewrites.
(2) We can avoid traversing Boolean connectives with term formula removal. Note that this PR relies on the observation that term formula removal leaves Boolean structure unchanged and can apply locally to theory atoms.
Furthermore, notice that our handling of lemmas generated by term formula removal is now more uniform. In the second algorithm, term formula removal is not applied to fixed point anymore. In other words, we do not remove skolems from lemmas generated by term formula removal recursively. Instead, since lemmas are theory-preprocessed recursively, we use the fixed point that runs outside the above algorithm instead of relying on the inner fixed point in term formula removal.
This PR resolves several open issues with proof production on proof-new.
I will performance test this change on SMT-LIB.
|
|
This is a duplicate of https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 and moreover is slow on proof-new.
|
|
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
|
|
This makes it so that -t nl-ext is a concise summary of what the nl-ext solver is doing, which I use frequently for debugging.
This is a temporary solution, we should consider a deeper refactoring of traces throughout NL at some point.
|
