| Age | Commit message (Collapse) | Author |
|---|
|
|
|
* LRA proof signature fixes and a first proof
The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.
* Add dependency info to signatures
I chose to indicate shallow dependencies only.
|
|
Fixes issue #2720. Between versions 2.0 and 2.5, the SMT-LIB standard changed
the way that string literals esacpe double quotes (") within strings from \" to
"". As a consequence, we have two different ways of lexing string literals
depending on the language used. The code produced by ANTLR first uses a
Deterministic Finite Automata (DFA) to predict the next token. Because the DFA
is static, it considers both versions of the string literal. If we are parsing
a string without esacpe sequences, e.g. "foo", it ends up reading three
characters past the closing double quote (I am not sure whether this is by
design or a bug). This is problematic in interactive mode because the third
character may be on the next line, which may not be available yet. Consider the
example from the issue mentioned above:
```
import subprocess
p = subprocess.Popen(['cvc4', '--lang', 'smt'], stdout=subprocess.PIPE, stdin=subprocess.PIPE)
p.stdin.write(b'(echo "foo")\n')
p.stdin.flush()
print(p.stdout.readline())
```
In this example, "foo" is a valid string for both types of string literals and
ANTLR reads ", \n, and then tries to access the character on the next line,
which leads to a deadlock because CVC4 is waiting for the next line on stdin
and the Python program is waiting for the output of CVC4. Note: this is why
writing `(echo "foo")\n\n` or `(echo "foo" )\n` both do not lead to a deadlock.
The solution this commit implements is to reorganize the way the string
literals are parsed: we now have a single token `STRING_LITERAL` for both types
of string literals, which is actually a bit simpler because it allows us to
share common code for processing the literal. Additionally, the commit removes
`SYGUS_QUOTED_LITERAL`, which was unused and was also had overlapping matches
with the string literals.
As to why it worked with older versions: we allocated memory for the input in
increments of 1024 bytes and in our `myConsume` method, we did not actually
check whether we were reading a character from the input or just from the
buffer that had not been filled in yet---so I am assuming that we got lucky.
|
|
This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.
|
|
We found that the `ss-combine` rewrite hurts solving performance, so
this commit is moving it to the extended rewriter.
|
|
This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0
>= str.len(s)`.
|
|
|
|
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
|
|
|
|
|
|
|
|
|
|
Proof steps were in a std::list, which is a linked list, but really, we
only needed a stack, so I changed it to a vector, because LL's are
usually slower.
Also added an iterator for the proof steps, and << implementations
|
|
|
|
initialized (#2708)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR adds/revises tests in order to increase coverage in some preprocessing passes and in proofs done with --fewer-preprocessing-holes flag.
|
|
The assignment operators of `Term`, `OpTerm`, and `Sort` currently have
an issue. The operators dereference their `shared_ptr` member and assign
the corresponding member of the other object. This is problematic
because if we have for example two `Term`s pointing to the same `Expr`,
then the assignment changes both `Term`s even though we only assign to
one, which is not what we want (see the unit test in this commit for a
concrete example of the desired behavior). To fix the issue, the
assignment operator should just copy the pointer of the other object.
This happens to be the behavior of the default assignment operator, so
this commit simply removes the overloaded assignment operators.
Testing: I did `make check` with an ASAN build and no errors other than
the one fixed in #2607 were reported.
|
|
|
|
|
|
Improves the existing implementation for sygus-active-gen=basic.
|
|
|
|
|
|
|
|
|
|
|
|
Currently, when installing CVC4 with a custom installation directory on
macOS, the resulting binary cannot be executed because the linker cannot
find the required libraries (e.g. our parser). This commit changes our
build system to use the `CMAKE_INSTALL_RPATH` variable to add the
installation directory to the RPATH list in the exectuable.
|
|
|
|
Ran into this bug when compiling with python3 bindings: https://github.com/swig/swig/issues/588
Instantiating any object crashes python. Since swig3.0.8 is currently the apt-get install for Ubuntu 16.04, I thought it'd be good to have a check for that. If python3 is preferred and the swig version is 3.0.8, it errors out and asks users to downgrade or upgrade SWIG.
|
|
Back when we used Autotools, we set the PORTFOLIO_BUILD macro when
building pcvc4. Our CMake build system is currently not doing that, so
setting thread options when running pcvc4 results in an error message
saying that "thread options cannot be used with sequential CVC4."
This commit fixes that behavior by recompiling driver_unified.cpp with
different options for the cvc4 and the pcvc4 binary.
[0] https://github.com/CVC4/CVC4/blob/7de0540252b62080ee9f98617f5718cb1ae08579/src/main/Makefile.am#L36
|
|
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
|
|
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
|
|
Is not required anymore since we don't use autotools anymore.
|
|
|
|
|
|
`make check` builds the examples but does not run them. This commit
changes our Travis script to run the examples after building them and
removes `makeExamples()` to avoid building them twice.
|
|
(#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
|
|
const. (#2647)
|
|
|
|
|
