| Age | Commit message (Collapse) | Author |
|---|
|
|
|
sygus), update regressions.
|
|
|
|
Commit 4cab39bd4f166716cd3d357a175c346afb838137 moved d_exprMap, d_typeMap,
and d_functions into SymbolTable::Implementation but did not move the deletion
of those objects from SymbolTable to the SymbolTable::Implementation
desconstructor, resulting in a memory leak. This commit fixes the issue.
|
|
The nightly competition build has been failing due to a remaining use of
hash_set in approx_simplex.cpp. This commit changes the remaining uses
of hash_set to unordered_set.
The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC
required changing the configure.ac for LFSC to require C++11 support to
make sure that it can be compiled independently from the rest of CVC4 (some
of our Travis tests do that as well). To have the macros for these additional
checks available, the commit adds a symlink to the files in config that contain
the macros). I did not find a way to add macros from a parent's folder that
did not break `make distcheck
|
|
|
|
|
|
|
|
* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header.
* Removing the guard for SymbolTable for the move constructor.
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
|
Removing it as well.
|
|
The CVC3 compatibility layer was broken because it was setting
simplification mode to SIMPLIFICATION_MODE_INCREMENTAL, which
is not supported anymore since commit
2dbe1f150d30f0fb0c8522f891104270ce09db4c . This commit changes
the compatibility layer to not set the option anymore.
This addresses bug 833, which had been reported on the cvc-bugs mailing list.
|
|
CDHashMap garbage.
|
|
Previously, we were checking whether we should use is_sorted
from std or __gnu_cxx. With C++11, std::is_sorted is
guaranteed to exist. This commit changes
arith/normal_form.{h,cpp} to always use std::is_sorted and
also removes the custom implementations for merge and copy by
using the std implementations instead.
|
|
With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.
|
|
|
|
ANTLR generates C files that we compile with the C++ compiler.
To do so, we set CC=CXX in the `Makefile.am`s of the parsers.
Previously, we did not copy the CXXFLAGS to the CFLAGS, which
could result in problems, e.g. when using -std=gnu++11 in the
CXXFLAGS, compiling the parsers would fail if they used C++11
features (configure.ac usually modifies CXX to include the
-std=gnu++11 flag but if it is included in CXXFLAGS, the CXX
is not changed).
|
|
|
|
|
|
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
for bug 831.
|
|
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
|
|
|
|
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
|
|
|
|
|
|
|
|
When CVC4 gets interrupted, we use async-signal safe printing functions
to print statistics. Unfortunately, the code for that was invoking copy
constructors, which is problematic due to memory allocation; for example
with statistics such as ReferenceStat<std::string>. This commit adds a
getDataRef() method for statistics that returns a const reference to the
object being printed such that the copy constructor is not called. Note:
modifying getData() was unfortunately not an option because in the case
of TimerStat, we can't return a reference to an object on the stack. We
could remove the const modifier on getData() and use d_data to store the
information but then we would have to remove it on
safeFlushInformation() and potentially other methods as well, which
seems like a worse solution.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
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().
|
|
|
|
|
|
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.
|
|
|
|
|
