| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
|
|
Currently, the subsolver created by the `ExprMiner` copies all the
options from the main solver, including the input language. When
synthesizing rewrites and checking them with the subsolver, this is
problematic because the default decision engine used by SyGuS is
`--decision=internal` but we want `--decision=justification` for solving
string queries for example. This commit changes the `ExprMiner` to set
the input language of the subsolver to `smt2`, s.t.
`SmtEngine::setDefaults()` chooses the correct decision engine.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
|
|
|
|
|
|
Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).
Asan reported errors for the corresponing unit test because of this.
|
|
Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test,
it was therefore required to include this cpp file in order to test
these functions. This factors out these functions into a
theory/quantifiers/bv_inverter_utils.(cpp|h).
|
|
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
|
|
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
|
|
|
|
|
|
This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.
|
|
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
|
|
|
|
|
|
|
|
|
|
|
|
|
