| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
A benchmark went unknown -> sat, likely due to the arith-brab commit, thus leading to a failure on regress1.This updates the status on this benchmark (also adds --nl-ext-tplanes to it).
|
|
Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.
|
|
This PR removes the requirement in the NodeManager that argument types to the function sort are first class.
Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633
Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.
FYI @abdoo8080 .
|
|
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.
|
|
This moves SmtEngine::setDefaults to its own file.
This design is not final. One could imagine this being a part of a "OptionsSetter" utility. I am leaving this as is until we refactor the relationship between SmtEngine and Options.
Regardless, the general file structure should be such that this method is separate from SmtEngine, since setting default options is a large task that should be addressed independently from the core of SmtEngine.
This is initial preparation towards converting the SmtEngine from Expr -> Node.
A few very minor changes were made to the code to make the separation possible.
|
|
* unit-cude test wip
* test for wip unit cube test
* fixed simple rounding
* wip
* Passing tests except for sat vs unknown ones
* added flag for cube test
* put example back to normal
* Fixed for style guidelines.
* fixed rewrite bug
* removed extra comments
* unit-cude test wip
* test for wip unit cube test
* fixed simple rounding
* wip
* Passing tests except for sat vs unknown ones
* added flag for cube test
* put example back to normal
* Fixed for style guidelines.
* fixed rewrite bug
* removed extra comments
* Small fixes based on PR feedback
* replace NodeManager::currentNM with nm and clang formatted
* renamed test
* Added a regression test that triggers branch and bound
* Added ; COMMAND-LINE: --arith-brab
* Updated arith-brab test
* arith-brab enabled by default
* Added --nl-ext-tplanes to regress0/nl/ext-rew-aggr-test.smt2
Co-authored-by: Amalee Wilson <amalee@cis.uab.edu>
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
Should fix timeout in asan build.
|
|
This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).
Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
|
|
Towards theory of sequences.
Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field.
|
|
Towards theory of sequences.
To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.
|
|
Commit c9b7c3d introduced code for
counting the number of string inferences done per type of inference.
However, it did not add support for printing the inference names in an
async-signal-safe manner via safe_print() (note that printing in
signal handlers is done differently from the regular stats printing).
This commit adds the corresponding code, s.t. we get the inference names
when printing the stats when CVC4 is interrupted or crashes.
|
|
|
|
Towards theory of sequences.
|
|
This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.
|
|
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.
|
|
Fixes #4112.
|
|
This commit adds code to count the number of inferences made of each
inference type for normal form inferences. It extends the Inference
enum in `infer_info.h` and adds two new `sendInference()` methods in the
`InferenceManager` to send and count inferences that have a corresonding
entry in the `Inference` enum.
|
|
Fixes #4092 and fixes #4134.
Typically, APPLY_UF has special treatment in sort inference. It is significantly more complicated when higher-order logic is enabled. This disables special handling when ufHo() is enabled.
|
|
|
|
This commit removes a special case in `CoreSolver::processNEqc()` where
we stopped looking for inferences for a given normal form as soon as we
found the highest priority inference (currently that an element in the
normal form is empty). This effectively elevates the priority of this
inference to the other inferences that are done immediately instead of
being added to the `pinfer` vector that holds the possible inferences.
The experiments that I've run seem to confirm that it is unnecessary to
have this special case.
|
|
This commit should fix the nightlies.
|
|
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
|
|
This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options.
Fixes #4083.
|
|
|
|
(#4074)
Fixes #4068 and fixes #4085 and fixes #4063.
|
|
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.
|
|
This adds a useful error message that recognizes a divergence in the expected input format (version 1 vs. version 2), which will be useful when we switch to SyGuS version 2 by default. This warning message is already potentially useful for users who are using --lang=sygus2.
|
|
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.
|
|
Towards theory of sequences. This separates out a virtual base class and utility class for the strings enumerator, which will be extended for sequences later.
|
|
|
|
Postpone failure in bv-to-int preprocessing pass.
|
|
Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.
|
|
Our SyGuS utilities are not designed to deal with partial bitvector division. If a user forced an older version of SMT-LIB semantics while using SyGuS, this led to a number of issues.
For now, we disable this option when it is combined with SyGuS, regardless of whether the user turns it on.
A more permanent solution will be to remove the old SMT-LIB semantics option bv-div-zero-const entirely.
Fixes #4097 and fixes #4088 and fixes #4104.
|
|
CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.
|
|
Fixes #4106.
The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).
|
|
The function TypeNode::isFinite is designed to compute finiteness without computing cardinality for the sake of efficiency; there was a missing case for rounding modes, leading to an assertion failure.
Fixes #4101.
|
|
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.
|
|
Done by:
Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes
Moving the file
Changing src/expr/CMakeLists.txt and src/CMakeLists.txt
clang-format, omitting node_visitor.h.
In reference to discussion, here.
|
|
|
|
|
|
|
