| Age | Commit message (Collapse) | Author |
|---|
|
This makes all methods for constructing skolems local to SkolemManager.
It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.
This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
|
|
The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.
Fixes #7537.
|
|
This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.
|
|
These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.
Instead, these rewrites are now moved to the extended rewriter.
|
|
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).
The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.
It does some minor refactoring of ExprMinerManager to support the new module.
|
|
Fixes #7439. That benchmark is now "unknown".
|
|
Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).
|
|
This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder.
It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.
|
|
Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead.
Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV.
|
|
Required for doing options-specific internal fuzzing using SyGuS.
|
|
Towards a new module for enumerating unsat queries via SyGuS.
|
|
This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts.
It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method.
It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding.
This addresses several of the issues raised in #6605.
|
|
spurious (#7390)
This makes the check for when an instantiation is "propagating" faster by not constructing the substitution + rewriting of the entire formula, and instead threading the substitution through the entailment check utility's evaluateTerm utility.
On a handful of challenge Facebook benchmarks, we go 35 seconds -> 18 seconds with this change.
This also eliminates the argument exp to the evaluateTerm method, which is no longer used, and eliminates hasSubs from several methods, which is redundant.
|
|
This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.
This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.
This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.
|
|
Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.
Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.
|
|
Towards addressing some bottlenecks on Facebook benchmarks.
|
|
Fixes #7353.
|
|
|
|
This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.
|
|
Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.
This is work towards a major refactoring of conflict-based instantiation / entailment checks.
|
|
The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.
|
|
|
|
This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().
|
|
This is in preparation to make the "lemma context" configurable.
|
|
This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them. It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself. This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.
|
|
In preparation for breaking more dependencies on TheoryEngine.
|
|
|
|
|
|
This is in preparation for renaming SmtEngine to SolverEngine.
|
|
This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.
It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.
|
|
There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.
|
|
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
|
|
This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent.
It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.
|
|
Makes a few places do multiplication for Rational directly instead of invoking the rewriter.
|
|
This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.
Construction of Evaluator utilities is now discouraged.
The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.
This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
|
|
Fixes #6531.
This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.
It does some cleanup on relevant domain in the process.
|
|
|
|
|
|
This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
|
|
Currently, we are using non-standard attributes. With C++17, all the
attributes that we use regularly are now standardized. This commit
replaces the compiler-specific attributes with standard ones.
|
|
|
|
The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.
This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.
|
|
This commit removes TheoryState::options() by changing more classes to
EnvObjs.
|
|
This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.
This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.
Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.
|
|
This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.
It makes minor cleanup to the dependencies of this method.
|
|
This PR:
Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.
|
|
This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.
|
|
This derives sygus unification utility objects from EnvObj where
necessary. There's one remaining occurrence of Rewriter::rewrite in
sygus_unif_rl.cpp, which is a bit tricky to address and thus subject to
a future PR.
|
|
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
|
|
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
|
