| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Also fixes passing of makeargs.
|
|
|
|
+ easier-to-maintain option handling
+ new option for compiling release with local antlr
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
In TSatProof<Solver>::finalizeProof(), we got a clause from the clause
allocator, called resolveUnit() and then size() on the clause. The problem is
that resolveUnit() can reallocate memory (and there is even a comment warning
about that in finalizeProof()), which invalidates the clause. This commit gets
the clause again from the clause allocator before calling size().
|
|
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
|
|
|
|
This commit fixes bug 821. As written in the description of the bug, the issue
is that `id` is not being set on one of the paths in addClause(), specifically
in the case where all but one literal are assigned false and the remaining
literal is assigned true. In that case, we are not actually adding anything and
set the `id` to `ClauseIdUndef`.
|
|
|
|
Fix uninitialized value
|
|
|
|
Note: this was a last minute effort, so we do not use the portfolio build for
this track. This part for example:
https://github.com/CVC4/CVC4/blob/d43e5fb294d89ba69f7d2607a12c8700b7ec9345/src/main/command_executor_portfolio.cpp#L351-L355
Would have to change before we can enable use the portfolio build for unsat
cores in a competition build.
|
|
Better configuration for QF_NRA
|
|
|
|
|
|
As pointed out by @cpitclaudel in pull request #172, we are using the same
handler for SIGSEGV and SIGILL and ill_handler() is unused. This commit changes
the SIGILL handler to ill_handler().
|
|
|
|
|
|
|
|
* Change language in competition script to smt2.6
The benchmark scrambler for the application track cuts out
the :smt-lib-version command, so this commit sets it
manually to 2.6 (all benchmarks in SMT-COMP use the 2.6
standard) instead of 2.0. I have not seen any failures due
to that but might as well be prudent.
* Change language in competition script to smt2.6
The benchmark scrambler (at least for the application
track) cuts out the :smt-lib-version command, so this
commit sets it manually to 2.6 (all benchmarks in SMT-COMP
use the 2.6 standard) instead of 2.0. I have not seen any
failures due to that but might as well be prudent.
|
|
This commit fixes bug 811. Bug 811 was caused because tokens were referring to
a buffer that was reallocated and thus the pointers were not valid anymore.
Background:
The buffered input stream avoids copying the whole input stream before handing
it to ANTLR (in contrast to the non-buffered input stream that first copies
everything into a buffer). This enables interactivity (e.g. with kind2) and may
save memory.
CVC4 uses it when reading from stdin in competition mode for the application
track (the incremental benchmarks) and in non-competition mode. To set the
CVC4_SMTCOMP_APPLICATION_TRACK flag, the {C,CXX}FLAGS have to be modified at
configure time.
Solution:
This commit fixes the issue by changing how a stream gets buffered. Instead of
storing the stream into a single buffer, CVC4 now stores each line in a
separate buffer, making sure that they do not have to move, keeping tokens
valid. The commit adds the LineBuffer class for managing those buffers. It
further modifies CVC4's LA and consume functions to use line number and
position within a line to index into the line buffer. This allows us to use the
standard mark()/etc. functions because they automatically store and
restore that state. The solution also (arguably) simplifies the code.
Disadvantages:
Tokens split across lines would cause problems (seems reasonable to me). One
allocation per line.
Alternatives considered:
Pull request 162 by Tim was a first attempt to solve the problem. The issues
with this solution are: memory usage (old versions of the buffer do not get
deleted), tokens split across buffers would be problematic, and
mark()/rewind()/etc. would have to be overwritten for the approach to work.
I had a partially working fix that used indexes into the stream instead of
pointers to memory. The solution stored the content of the stream into a
segmented buffer (lines were not guaranteed to be consecutive in memory. This
approach was working for basic use cases but had the following issues: ugly
casting (the solution requires casting the index to a pointer and storing it in
the input stream's nextChar because that's where ANTLR is taking the location
information from when creating a token), more modifications (not only would
this solution require overwriting more functions of the input stream such as
substr, it also requires changes to the use of GETCHARINDEX() in the Smt2
parser and AntlrInput::tokenText() for example), more complex code.
|
|
Parse 'is', 'match' differently for non-DT input
|
|
This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.
|
|
In SMT 2.6, Datatypes are being introduced and they come
with testers (indexed identifier of the form (_ is c)) and
match expressions. This lead to failures in UFIDL
benchmarks in SMT-LIB because they declare the function
'is'. This commit changes the parser s.t. it does not
consider 'is' and 'match' special tokens unless the theory
of datatypes is enabled.
|
|
|
|
In certain cases, the trace executor inserts empty lines, which threw off
our competition script. This commit adds code to ignores empty lines.
|
|
|
|
|
|
|
|
cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.
|
|
Remove UdivSelf rewrite, add UdivZero rewrite
|
|
This fixes bug 820. The issue was that (a udiv a) got rewriten to 1, which is
not correct when a is 0 (the result is all ones in that case). Even with the
--bv-div-zero-const flag disabled, the UdivSelf rewrite was incorrect because
it was applied to BITVECTOR_UDIV_TOTAL, which is "defined to be the all-ones
bit pattern, if divisor is 0" according to src/theory/bv/kinds . The commit
adds instead an optimization that returns all ones if the divisor of a
BITVECTOR_UDIV_TOTAL is zero.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
