| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
proof infrastructure (e.g., quantifiers)
|
|
|
|
Minor changes to smt comp script.
|
|
in regressions.
|
|
added the option dump-unsat-cores-full for printing the entire core, as before
|
|
[Competition] Fix ABC, fix CryptoMiniSat req
|
|
This commit fixes two issues that caused the competition configuration to fail on the cluster machines:
We used an ancient version of ABC that declared a function (factorial()
luckySimple.c) in a source file as inline but not static. This issue was fixed
in the following commit:
https://bitbucket.org/alanmi/abc/commits/e0aa7af0d73538fb786c4dcc72745578f0068a38
The issue with non-static inline functions in source files is described in the
following Stackoverflow post:
https://stackoverflow.com/questions/16740515/simple-c-inline-linker-error
This commit updates ABC to a much newer version (commit tagged as abc20160717),
which fixes the issue. One of the modifications previously performed by
contrib/get-abc does not need to be necessary anymore.
CryptoMiniSat was always linked against m4ri, even though it was not getting
compiled with it (-DNOM4RI="ON" in contrib/get-cryptominisat4). This commit
removes the part of config/cryptominisat.m4 that explicitly sets the libraries
linked to and instead uses the result of CVC4_TRY_CRYPTOMINISAT_WITH (which
seems to work even though there is comment indicating otherwise). Further, it
adds -pthread to the libraries required by CryptoMiniSat because it is required
by the version of CryptoMiniSat that we use (a newer version supports disabling
that behavior, so it might be a good idea to update). Previously, this would
lead to linker errors.
Tested with the following configuration:
./configure competition --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 --enable-static-binary --enable-gpl --with-cln --with-glpk --with-glpk-dir=`pwd`/glpk-cut-log --with-abc --with-abc-dir=`pwd`/abc/alanmi-abc-53f39c11b58d --disable-thread-support --without-readline --disable-shared --with-cryptominisat --with-cryptominisat-dir=`pwd`/cryptominisat4
|
|
|
|
This commit fixes an issue where the ResChain in `d_resolutionChains` gets
deleted here:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729
The condition immediately after is false because the condition on line 727 is
true. Thus, `d_resolutionChains` now has a deleted entry for `id`.
When CVC4 afterwards gets the ResChain associated with `id` in
`checkResolution()`, it accesses the deleted entry:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
|
|
|
|
|
|
|
|
Conditional coverage
|
|
Avoid tokenizing FP tokens in non-FP input
|
|
Fix error in Windows build
|
|
This commit addresses bug 807. CVC4 was parsing floating-point related tokens
such as NaN as floating-point tokens even for inputs that do not use the FP
theory, which lead to failing SMT-LIB benchmarks that declare functions named
NaN.
|
|
The Windows build was missing the `print_statistics()` function, this commit
moves the function out of the `#ifndef __WIN32__` guard.
|
