| Age | Commit message (Collapse) | Author |
|---|
|
Towards theory of sequences.
This PR also adds support for sequences in default sygus grammars.
Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
|
|
Fixes #4620.
The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.
A general example of this unsoundness:
(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.
Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.
|
|
This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation.
This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).
|
|
|
|
Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.
This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
|
|
Separates them from the core datatype utilities.
Code move only.
|
|
This makes the method for substiutiton and generalization of sygus datatypes a generic utility method. It updates the abduction method to use it. Interpolation is another target user of this utility.
|
|
Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
|
|
This PR removes a hack in counterexample-guided quantifier instantiation.
The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.
Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.
This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.
|
|
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
|
|
Fixes #4476.
|
|
Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.
This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.
Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
|
|
|
|
When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.
This PR ensures we only eliminate variables when v contains only evaluated operators.
Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.
Fixes #4500.
|
|
Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.
Fixes #4383.
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
Fixes #4288.
When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.
|
|
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
|
|
|
|
Fixes regress1.
|
|
|
|
In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.
Fixes #4293.
|
|
conflict-based instantiation (#4280)
Conflict-based instantiation would sometimes initialize a match x -> getRepresentative(t) when a quantified formula contained x = t. This leads to issues where getRepresentative(t) is an illegal term (say, in combination with CEGQI). This makes it so the representative is accessed when necessary instead of being set as part of the match.
Fixes #4275.
|
|
Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.
Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.
|
|
Fixes #4228. That benchmark now times out.
|
|
These options are not robust and are not used.
Fixes #4282 and fixes #4291.
|
|
Fixes #4290 and fixes #4292.
|
|
Fixes #4273 and fixes #4274 .
This also removes a spurious assertion from the Node::substitute method that the result node is not equal to the domain. This is violated for f(f(x)) { f(x) -> x }.
|
|
Previously we were doing rewriting/expand definitions during grammar normalization, which overwrote the original sygus operators. The connection to the original grammar was maintained via the SygusPrintCallback utility, which ensured that a sygus term printed in a way that matched the grammar.
We now have several use cases where solutions from SyGuS will be directly exported to the user, including the current use of get-abduct. This means that the terms must match the grammar, and we cannot simply rely on the print callback.
This moves the code to normalize sygus operators to datatypes utils, where the conversion between sygus and builtin terms takes place. This allows a version of this function where isExternal = true, which constructs terms matching the original grammar.
This PR enables the SyGuS API to have an accurate getSynthSolution method. It also will eliminate the need for SygusPrintCallback altogether, once the v1 parser is deleted.
|
|
|
|
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
|
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
Work towards support for the strings standard.
This updates the string solver and parser such that:
The internal representation of strings is vectors of code points,
Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models,
The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings,
Handle unicode escape sequences according to the SMT-LIB standard in String,
Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary,
Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.
|
|
Towards theory of sequences.
|
|
Fixes #4143.
|
|
An assertion is triggered for some V2 versions of SyGuS V1 benchmarks during sygus grammar reduction. This PR updates this technique so that it only applies to sygus constructors whose sygus operators are lambdas of the form
lambda x1 ... xn. f( x1 ... xn ).
FYI @abdoo8080 .
|
|
The V2 parser always turns sygus operators into lambdas for consistency. This PR ensures that we nevertheless infer when a sygus operator is equivalent to a builtin operator, e.g.
(lambda x y. (+ x y)) is equivalent to +.
The main reason this is required is to ensure that solution reconstruction heuristics work optimally when we make the switch SyGuS V1 -> V2 (see 5 failing benchmarks due to --cegqi-si=all on #4136).
|
|
Fixes #3849 and fixes #4062.
Overall, the effect of this PR is that CEGQI will generate better instantiations more frequently for quantified formulas that involve the introduction of auxiliary variables.
In CEGQI, auxiliary variables introduced in CEX lemmas must be given special treatment (since the instantiations should not involve them, thus they must be solved for as well). Previously, auxiliary variables that are introduced as parts of CEX lemmas were currently assumed to be:
(1) Only occurring from ITE removal, e.g. s[(ite C t1 t2]) ---> s[k] ^ ite( C, k = t1, k = t2 )
(2) Always trivially solvable by looking at which literal was asserted (k = t1 or k = t2).
Both of these assumption do not hold in general (aux variables can come from other kinds of terms e.g. choice functions, and the user can force options that rewrite arithmetic equalities to inequalities).
This makes auxiliary variable handling in CEGQI more robust by treating auxiliary variables as standard variables. Effectively, this means that the entire procedure for determining instantiations is run for auxiliary variables. This PR removes the specific hacks that were used previously that were based on the assumptions above.
Additionally, #3849 triggered a second issue: SyGuS solution reconstruction that involves auxiliary variables that are introduced as part of instantiation lemmas should not be considered valid solutions. Previously, only a warning was given.
|
|
Fixes #3931.
Currently we print a warning for unimplemented types when constructing default SyGuS grammars. We should additionally throw an exception when the unimplemented type would lead to a non-well-founded datatype.
|
|
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
|
|
|
|
Organization towards theory of sequences.
The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
|
|
If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.
|
|
robust (#4034)
Fixes #4002 (that benchmark is now unknown).
The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.
The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.
A block of code changed indentation in this PR, which was updated to the new standards.
|
|
Fixes #4106.
The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).
|
|
Fixes #4105.
It appears that the two (experimental) options in that issue were incompatible.
A block of code changed indentation in this PR and was updated to guidelines.
|
|
Fixes #4086.
Quantifier instantiation involves two symbolic representations of infinities for real and int and was not handled correctly previously.
|
|
Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant.
Fixes #4096 and fixes #4089.
|
|
|
|
Fixes #4050.
|
