Age | Commit message (Collapse) | Author |
|
Towards theory of sequences.
|
|
Towards proofs for string rewrites. All return statements all now associated with an enum value.
An indentation in a block of code changed in rewriteMembership.
|
|
Towards support for the strings standard.
This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).
This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.
Also fixes #4161.
|
|
Fixes #4180, fixes CVC4/cvc4-projects#133, fixes CVC4/cvc4-projects#134.
|
|
Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
|
|
In preparation for string proof infrastructure.
This introduces an enumeration type to track string rewrites.
It also makes inference printing more consistent.
|
|
* Attempting to split transcendental function solver
* Clean
* Format
* More
* Format
* Attempt link
* Format
* Fix
* Another refactor
* More
* More
* Rename
* Format
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
Moves the string file to string.h. This is required since other required utilities will soon need to be added to regexp.h.
|
|
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.
|
|
* 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>
|
|
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.
|
|
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.
|
|
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
|
|
|
|
(#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.
|
|
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.
|
|
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()`.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
I'll remove the error later
|
|
Before, a "simple farkas proof" was one that just applied the farkas
lemma.
Now it allows for the antecedents to (optionally) be tightened.
Note that hasSimpleFarkasProof was (and is) dead code.
We will use it to decide whether to print a proof or a hole.
|
|
Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.
|
|
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.
|
|
|
|
Towards theory of sequences.
|
|
Fixes #4050.
|
|
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
|
|
|
|
Fixes #3955.
Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context.
This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR.
A block of code changed indentation in this commit.
|