Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
This commit adds the Evaluator class that can be used to quickly
evaluate terms under a given substitution without going through the
rewriter. This has been shown to lead to significant performance
improvements on SyGuS PBE problems with a large number of inputs because
candidate solutions are evaluated on those inputs. With this commit, the
evaluator only gets called from the SyGuS solver but there are
potentially other places in the code that could profit from it.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds support for string concatenation, charat, and length
operators in the CVC printer and support for re.nostr, re.allchar, and
insert into a set in the SMT2 printer.
|
|
|
|
|
|
In the CVC printer, function definitions without arguments are printed
like constants but when actually using that function we were printing in
the form of `x()`.
For example:
```
(set-logic QF_BV)
(define-fun x1480 () Bool true)
(define-fun x2859 () Bool true)
(define-fun x2387 () Bool x2859)
(check-sat)
```
Was dumped as:
```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```
This commit removes these parentheses when prefix functions with zero arguments
are printed, so the example above becomes:
```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```
|
|
|
|
This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.
|
|
As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions
in floatingpoint.h, which was problematic when installing the header
files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and
simply including the header files in another project would be missing
that definition. This commit moves floatingpoint.h to a template file
floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at
configure-time when generating floatingpoint.h (this is the same
solution that integer.h and rational.h use). I have tested the fix with
the examples provided in #2013 and they work.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit adds the following rewrite:
(str.replace x (str.replace y z w) u) --> x
if (str.contains x y) = false and (str.contains x w) = false
Reasoning: (str.contains x y) checks that x does not contain y if the
inner replacement does not change y. (str.contains x w) checks that if
the inner replacement changes anything in y, the w makes it impossible
for it to occur in x.
|
|
|
|
|
|
In cases such as (str.replace x (str.++ ... (str.substr y i j)) z), we
can restrict j to len(x) + 1 - len(...) if j > len(x) + 1. Because if
the string to be replaced is longer than x, then it does not matter how
much longer it is, the result is always x. Thus, it is fine to only look
at the prefix of length len(x) + 1 - len(...).
|
|
|
|
|
|
|
|
|