Merge pull request #211 from CVC4/fix_warn_sygus

Fix compiler warning in theory/quantifiers/term_database_sygus.cpp

Optionally split regression tests into test groups (#207)

To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.

Fix compiler warning in theory/quantifiers/term_database_sygus.cpp

Change sygus output for failed reconstruction case.

Make quantifier elimination more robust to preprocessing.

Reorganized bitvector.h

Fix comments

Fix typos in comments

Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.

Disable debug symbols for production builds.

Minor improvement for enumerative instantiation.

Fix memory leak in symbol table (#209)

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.

Change remaining hash_set -> unordered_set (#208)

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

Add support for charat in native language, minor cleanup.

Fix cache issues for cyclic string equations.

-Og for non-opt build, parallel pcvc4 check (#206)

-Og enables optimizations that do not interfere with debugging. This is the new
default for debug builds if the compiler supports the flag. This commit also
enables parallel checking for the portfolio build on Travis.

Use TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in configure.ac. (#200)

CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file.

Disabling compiling unit tests with coverity scan for now.

Deprecating the unused convenience_node_builders.h (#203)

Consolidating the opaque pointers in SymbolTable. (#204)

* 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.

Moving from the gnu extensions for hash maps to the c++11 hash maps

* 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.

Fix a few bugs related to sygus.

Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.

Fix simple_vc_compat_cxx example (#202)

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.

Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage.

Use is_sorted, merge, copy from std (#199)

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.

Remove PtrCloser (#198)

With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.

Moving to static_assert now that c++11 is available.

Use CXXFLAGS when compiling parsers (#197)

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).

Fix warning about unknown escape sequence (#196)

Disable separate gnu++11 tests on Travis (#193)

Given that we are now always compiling with gnu++11, we don't need
separate tests anymore.

Removing BOOST_FOREACH usage.

Merge pull request #188 from aniemetz/cx11

autoconf: make -std=gnu++11 mandatory

autoconf: make -std=gnu++11 mandatory

Fix unit tests for subranges. Fix destructors for context objs in unit tests.

Fix .i files from last commit.

Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).

Remove trailing slashes from directories if specified via command line.

Do not exit when value/model/unsat-core/proof is requested at wrong time, for bug 831.

Add nl regression.

Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.

Separate sygus term utilities to new file, minor cleanup from last commit.

Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes 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.

Prerelease versioning for master.

Cutting release 1.5.

Disable tarball signing for now.

Merge branch 'master' of github.com:CVC4/CVC4

Update copyright year and refer to authors URL.

Remove unused stacking_vector class (#185)

Avoid invoking copy constructor when safe printing (#184)

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.

Update copyright headers.

Update files that are part of the CVC4 license, exclude minisat files.

Use consistent author names for the copyright headers.

Use new copyright header format.

Escape left brace in regex in update-copyright script.

Fix passing antlr arguments to configure in contrib/cut-release

Also fixes passing of makeargs.

cut-release: git co -> git checkout

cut-release: option handling, get-antlr

+ easier-to-maintain option handling
+ new option for compiling release with local antlr

Fix for logic info, update regressions. Update casc tfa script.

updated INSTALL for version 1.5

Update unit test, news.

Non-linear supported in ALL logics. Minor fixes for set logic with sygus.

Update README for 1.5 release (#182)

Updates to AUTHORS and THANKS for 1.5 (mostly done by Tim).

Updated NEWS, README, RELEASE-NOTES.

Fix use-after-free with unsat cores/proofs (#174)

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().

Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.

Enable non-linear solve by default, update regressions.

Fix assertion failure due to missing clause id (#180)

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 unsat cores script for SMT-COMP (#179)

Merge pull request #175 from CVC4/fix_uninit

Fix uninitialized value

Properly handle subtypes in smt2 printer.

Add run script for unsat cores track at SMT-COMP (#177)

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.

Merge pull request #176 from CVC4/smtcomp2017

Better configuration for QF_NRA

Update casc and sygus comp scripts.

Check for sigaltstack in configure (#172)

Fix SIGILL handler

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().

Better configuration for QF_NRA

Fix assertion

Minor change to ensureTheoryAtoms for bug 828.

Change language in competition script to smt2.6 (#171)

* 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.

Fix stream parsing

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.

Merge pull request #170 from CVC4/fix_2_6_parser3

Parse 'is', 'match' differently for non-DT input

Fix segfault by making unit conflict CDMaybe

This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.

Parse 'is', 'match' differently for non-DT input

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.

Fix for bug 639.

Make comp script more robust

In certain cases, the trace executor inserts empty lines, which threw off
our competition script. This commit adds code to ignores empty lines.

Fix for issue related to cbqi + E-matching.

Add regression.

Fix relevant domain for datatypes, fixes bug 824.

Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.

Merge pull request #167 from CVC4/fix_div

Remove UdivSelf rewrite, add UdivZero rewrite

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.

Fix uninitialized value

Fix compile error

Minor to smt comp script.

Fix regression.

Incorporate datatypes into smt comp script, add regression.

Minor optimizations related to cbqi.

Fix model construction for BV with cbqi. Minor change to defaults.