| Age | Commit message (Collapse) | Author |
|---|
|
This PR fixes an issue with one of our nightlies.
|
|
This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.
|
|
(#6452)
If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.
|
|
This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.
|
|
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
|
|
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
|
|
This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.
|
|
This PR does a bit of cleanup on our didyoumean code.
|
|
|
|
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
|
|
Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.
The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.
However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.
|
|
This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)
|
|
This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.
|
|
|
|
This PR protects two methods of the IntStat class in case statistics are disabled.
|
|
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
|
|
Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.
With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.
We should retest unsat-cores-mode=assumptions after this PR is merged.
|
|
propositional) (#6423)
Conclusion and rule are placed on the same node (records nodes in the dot format).
Nodes are colored based on the view they will belong to.
Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
|
|
This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.
This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.
|
|
This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.
|
|
Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.
|
|
|
|
This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals.
This significantly improves run time on a challenge benchmark from @makaimann.
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.
|
|
This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
|
|
This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.
It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.
As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:
|
|
This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.
|
|
One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.
|
|
|
|
|
|
This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.
This makes the proof generation in trust substitution map lazy.
Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.
|
|
In preparation for using this class as part of our proof checker.
This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.
|
|
|
|
This PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.
|
|
This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.
|
|
Towards setting up the proper callbacks into the new justification heuristic.
Moves ownership of skolem definition manager from TheoryProxy to PropEngine.
|
|
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.
|
|
This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
|
|
|
|
|
|
This PR adds missing cmake dependencies for the base library. This makes sure that Debug_tags.h and Trace_tags.h are already present when we start compiling.
|
|
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
|
|
|
|
This sets up the core utilities for the new implementation of justification heuristic
|
|
Add getNumIndices to Op
|
