| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This marks methods const where possible and adds missing documentation.
|
|
|
|
literals (#7108)
Similarly to the issue when explaining literals, it's necassary to save the
reference to the reason for propagating a redundant literal, as adding
explanations that may be added to the SAT solver during the recursive
elimination of redundant literals may change the original reference.
|
|
This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
Fixed TestTheoryWhiteBagsRewriter.map failure
|
|
Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.
This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.
This makes us safer in several places related to double SYMM steps.
|
|
|
|
This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).
|
|
This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().
|
|
This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.
This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).
Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
|
|
This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.
|
|
This PR ensures that the possible modes returned in getOptionInfo() are always sorted. Their order would depend on the python dictionary ordering, which changed with a somewhat recent python version and thereby breaks our tests.
|
|
This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.
|
|
This corrects an issue in our context-dependent simplification which limited the cases it was applied.
Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.
|
|
This ensures we don't try to apply e.g. enumerative instantiation to quantified formulas over regular expressions, since no type enumerator exists for RE.
Fixes #6750.
|
|
This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.
|
|
This PR adds kind BAG_MAP to bags.
|
|
This introduces standard methods for checking incompatible with models, unsat-cores, incremental, proofs.
There is one minor change in behavior in this PR.When bitblast=eager and models were enabled in combined logics, then the set defaults would change the bitblast mode to lazy. However, it would then in the same block complain that eager cannot be used in combination with incremental. After this PR, we won't complain in this case since we've already decided to change the bitblast mode to lazy.
|
|
This PR simplifies how we store the current input file name and handle setting and getting it.
It is now an option, that can also be set and get via setInfo() and getInfo().
|
|
There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.
This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.
This corrects some proof checking errors on string benchmarks.
|
|
|
|
Fixes #6838.
|
|
This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.
|
|
This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.
|
|
Eliminates another call to currentSmtEngine.
This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.
|
|
Towards rewrite rule reconstruction
|
|
This adds the last two remaining API methods required for implementing the text output of get-model on the API side.
A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.
This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
|
|
While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.
|
|
The docs-cleanup job squashes all commits from the docs-ci repository that are older than one month. The current solution to retrieve the newest commit older than this one month erroneously relied on the commit date. As the script cherry-picks all newer commits, it should rather use the author date, though. Unfortunately, rev-list does not support filtering by author date, hence we use awk now...
|
|
This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
|
|
This fixes a minor issue where models should be dumped for "not entailed" results. This fix was required when preparing the submission to CASC this year.
|
|
This eliminates another call to currentSmtEngine.
After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).
|
|
The nonlinear extension used to be called only during model construction, a rather atypical place which lead to a series of subtle issues. This PR moves it into the postCheck method. To do that, a few other changes are necessary, most notably collectAssertedTerms and collectTerms are moved back from the model manager into the theory class.
|
|
This commit fixes the conversion of signed bit-vector values to integers in the int-to-bv preprocessing pass.
|
|
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
|
|
This adds a missing include. Compilation fails right now, if libpoly is disabled.
|
|
Work towards supporting multiple solvers running in parallel.
There are now only 5 remaining internal calls to smt::currentSmtEngine.
More will be eliminated on future PRs.
|
|
This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
|
|
This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.
It also integrates the sygus enumerator callback into the fast enumerator.
|
|
This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.
Here we focus on the translation of nodes without children.
Unit tests are included.
|
|
This breaks setDefaults into three functions that summarize the high-level behavior of setDefaults.
|
|
Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
|
|
|
|
Required for properly checking proofs for quantifiers rewrites.
|
|
This fixes an issue in strings proof reconstruction where sequential substitutions are used over possibly non-atomic terms like (str.replace x a b) and x simultaneously.
This leads to cases where we failed to reconstruct proofs, since a substitution x -> c, (str.replace x a b) -> d may unintentionally generate the term (str.replace c a b), after which the second substitution fails to apply.
|
|
This generalizes our inequality elimination technique to handle disequalities as well as inequalities.
#6999 is an example where a variable can be eliminated: if a variable x occurs only in an equality with negative required polarity, then the variable and that literal can be eliminated.
Fixes #6999.
|
|
It was not robust to cases where a function-to-synthesize occurred in a higher-order context.
Also does general clean up of the single invocation utility.
|
