| Age | Commit message (Collapse) | Author |
|---|
|
This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.
|
|
This further renames kind SET_INTERSECTION to SET_INTER.
|
|
This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.
|
|
This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.
|
|
This is the result of a global replace Rewriter::rewrite( -> rewrite( + patching the results.
It makes several classes into EnvObj. Many calls to Rewriter::rewrite remain (that are embedded in classes that should not be EnvObj).
|
|
This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.
|
|
Fixes #5341.
|
|
We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.
|
|
This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.
|
|
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.
|
|
This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.
|
|
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.
|
|
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.
|
|
This tightens the interface of the sygus solver, which was a product of not using subsolver calls in the original design.
|
|
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 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.
|
|
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 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.
|
|
|
|
This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
|
|
|
|
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 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 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 further reorders the header according to the code style guidelines.
|
|
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 eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
|
|
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.
|
|
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 moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.
It also integrates the sygus enumerator callback into the fast enumerator.
|
|
Required for properly checking proofs for quantifiers rewrites.
|
|
A few minor changes to which options are enabled for sygus, otherwise no intended changes.
|
|
Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.
This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.
|
|
The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.
|
|
Work towards integrating the enumerator callback into the fast enumerator.
|
|
This allows one to use a fast enumerator without having access to sygus term database, statistics, etc.
|
|
This class will make the uses of the fast enumerator customizable.
|
|
In preparation for more extensions to this aspect of the synthesis solver.
|
|
Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.
Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.
This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.
|
|
This commit replaces (old) internal string kind names to match the API / smt2 standard names.
|
