| Age | Commit message (Collapse) | Author |
|---|
|
EnvObj. (#7130)
|
|
Note: the diff in theory.h is only huge because of small changes that caused huge reformat. The effective change is only that it now derives from EnvObj, does not have a member d_env (because it inherits it) and does not need getLogicInfo (because that's in EnvObj).
|
|
Towards replacing that option with a logic check throughout.
|
|
backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.
|
|
PR #7103 did not quite fix the unit test: The types of the lambda and
the expected bags were still off. This fixes the unit test.
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
|
|
More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
|
|
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 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 PR adds kind BAG_MAP to bags.
|
|
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.
|
|
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.
|
|
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.
|
|
This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
|
|
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 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.
|
|
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.
|
|
Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.
This should avoid some more "unknown" responses on facebook benchmarks.
Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.
FYI @barrettcw .
|
|
This makes INST_ATTRIBUTE (optionally) take multiple children, giving a way for the user to set attributes on quantified formulas, which does not require a new API command.
This is a special case of term annotations that occur as the body of a quantified formula.
If we need to extend our API to support further user-provided attributes, we should use a similar approach, e.g. a new kind ANNOTATE.
|
|
A few minor changes to which options are enabled for sygus, otherwise no intended changes.
|
|
Previously, we had a special case to support users who directly accessed the model object pointer in the old API.
The special case ensure that the information in the model was eagerly updated after each "sat" response, in the case that the user did not re-request a pointer to the model.
Since users no longer can access the internal model pointer (apart from GetModelCommand), this special case is no longer necessary.
This PR should make us slightly faster for incremental benchmarks where the user asks for the model on some but not all "sat" responses.
|
|
This PR refactors the nonlinear extension(s) to access options only via the environment class.
|
|
We previously incorrectly allowed this, leading to problems that were unsolvable but where we would not warn the user this combination is not supported.
FYI @polgreen
|
|
This PR refactors part of the arithmetic theory to use the options via the Env object.
|
|
This PR moves the collectAssertedTerms utility function from the model manager to the theory class. This allows to use the utility also when we are not currently building the model.
|
|
PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:
the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.
|
|
Because we are now using C++17, we can get rid of Maybe and instead
use std::optional, which offers the same functionality.
|
|
No behavior changes in this PR, just code reorganization.
|
|
This also consolidates the option strictTriggers into userPatMode.
Fixes #6996.
|
|
|
|
Mainly just indentation / formatting changes. In preparation for playing around with heuristics to datatypes theory motivated by Facebook benchmarks.
|
|
Work towards a new expression miner for caching satisfiability queries.
|
|
This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
|
|
This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel.
|
|
This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.
|
