Age | Commit message (Collapse) | Author |
|
+ 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)
|
|
|
|
|
|
When we do solving in incremental mode, we store substitutions at a
special index in our list of assertions. Previously, we used a
context-dependent variable for that. However, this is not needed since
the list of assertions just consists of the assertions currently being
processed, which are independent of the assertions seen so far. This
commit changes the index to be an ordinary integer and moves it to the
AssertionPipeline. Additionally, it abstracts access to the index in
preparation for splitting AssertionPipeline into three vectors (see
issue #2473).
|
|
|
|
Fixes #3272.
This was caused by not explaining the last equal component in a flat form inference. For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error.
Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`. #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Add support for constant arrays to new C++ API
* Fix macro usage in unit test
* Add not null check
* Add test for null term
* Formatting
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
constructors (#3259)
|
|
|
|
|
|
|