| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.
It also deletes some unused/undefined functions in theory_strings.h.
There are no major changes to the behavior of the code or its documentation in this PR.
This is work towards #1881.
|
|
This commit updates the line numbers in templates to address warnings
due to wrong line numbers.
|
|
This commit removes references to Boost and Autotools in the copyright
information and CMakeLists.txt.
|
|
In theory_engine.cpp, we were calling `theoryOf()` with
`THEORY_SAT_SOLVER` as the theory id. However, `THEORY_SAT_SOLVER` is
defined as `THEORY_LAST` and thus out-of-bounds of the `d_theoryTable`
defined in theory_engine.h (which is of size `THEORY_LAST`. This commit
adds an assertion that detects the out-of-bound access and introduces a
method to turn a theory id into a string which correctly handles
`THEORY_SAT_SOLVER`.
|
|
PR #3388 didn't disable the regression correctly (due to using `REQUIRE`
instead of `REQUIRES`). This commit fixes the issue.
|
|
This commit disables a regression test that was failing for the
competition build due to not emitting the expected error message.
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #1399.
|
|
|
|
This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.
|
|
Fixes #2517.
This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.
This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.
I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993
|
|
|
|
TS_UTILS_EXPECT_ABORT can be used if an expression in a unit test is
expected to abort() instead of throwing an exception. This can happen if
CVC4_CHECK or CVC4_DCHECK fail.
|
|
|
|
|
|
|
|
CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.
The issue was likely introduced with #3062.
|
|
Only include Java targets if Java bindings are enabled.
|
|
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
|
|
This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.
It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.
Fixes #3250 and fixes #3356.
|
|
|
|
Detected with cppcheck static analyser, which said: (performance) Prefer
prefix ++/-- operators for non-primitive types. Reformat with clang-format
as needed.
Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
|
|
Detected with cppcheck static analyser, which said: (performance) Function
parameter should be passed by reference. Reformat with clang-format as
needed.
Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
|
|
|
|
|
|
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
|
|
Previously, competition builds for incremental tracks required to
manually pass in -DCVC4_SMTCOMP_APPLICATION_TRACK as compiler flag. This
introduces an additional build type for incremental competition builds
to simplify configuration for such builds.
|
|
+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()
Co-Authored-By: makaimann <makaim@stanford.edu>
|
|
This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.
|
|
|
|
This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string.
This fixes #3357.
|
|
We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas.
|
|
This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported).
Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.
|
|
|
|
Our `CDMapBlack` test failed to compile with newer versions of libstdc++
because they require the `value_type` to be defined for the iterator
(accessed via `std::iterator_traits`). Due to the implementation of
`std::iterator_traits`, we also need to define `iterator_category`,
`difference_type`, `pointer`, and `reference`.
|
|
This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.
|
|
|
|
Fixes #3058. Commit a7c4cd3ecacb1e484a076edde0274c282bb43ffb changed
CVC4's behavior to emit an error when `--unconstrained-simp` is used
with `--incremental`. Before, we were silently disabling it. For some
reason, we had that option enabled for the incremental QF_LIA track of
SMT-COMP, so CVC4 failed on those benchmarks. This commit changes the
corresponding competition script to not use the option.
|
|
This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.
|
|
|
|
|
|
|
|
|
|
This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:
- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)
|
|
|
