| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.
This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
|
|
This commit extends `--show-config` to show whether the current build is
an ASAN build or not. This is done by moving a detection that was
previously done for the unit tests into base/configuration_private.h.
In addition to being convenient, this allows us to easily exclude
regression tests from ASAN builds.
|
|
|
|
This implements solution number 2 for issue #2613.
|
|
|
|
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`.
|
|
|
|
|
|
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).
|
|
|
|
|
|
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
|
|
|
|
|
|
|
|
|
|
|
|
This commit changes the unit test for the string rewriter to use the
extended rewriter instead of the regular rewriter to make it more
robust, e.g. to different orderings in conjunctions.
|
|
|
|
Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
|
|
|
|
|
|
Targets 'check', 'units', 'systemtests' and 'regress' are now run in
parallel with the number of available cores by default. This can be
overriden by passing ARGS=-jN.
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
|
|
|
|
|
|
|
|
* Removing support for T* and const T* attributes. These are unused.
|
|
The static initialization in the CxxTest runner was causing problems
when having `std::unique_ptr`s in test classes. When the ExprManager's
deconstructor is called, we count on certain static objects to be around
(e.g.
https://github.com/CVC4/CVC4/blob/0a02fd2b69c0c0f454fc33d8028b24f4fcf431de/src/expr/attribute_internals.h#L508).
If the ExprManager is (indirectly) owned by a `std::unique_ptr` in a
static class, however, there are no such guarantees as the destruction
order of static objects is not defined. This commit adds a flag for
CxxTest to not use static initialization in the test runner, which
solves the issue. Additionally, the commit fixes a warning about a
missing virtual deconstructor in ParserBlack that came up after using
the new flags.
This fixes an issue reported in the nightly builds.
|
|
|
|
* Proposal for adding map utility functions to CVC4.
|
|
|
|
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
|
|
|
|
|
|
|
|
|
