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.

A more informative error message when a theory is not yet supported by the proof infrastructure (e.g., quantifiers)

Minor fix to last commit.

Change to-int, div, int-div skolems from CDAttribute to stored in CDHashMap. Minor changes to smt comp script.

Minor change to defaults, update smt comp script, minor changes to options in regressions.

print only labeled assertions as part of the unsat core
added the option dump-unsat-cores-full for printing the entire core, as before

Merge pull request #164 from CVC4/fix_comp

[Competition] Fix ABC, fix CryptoMiniSat req

[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

Checking that equalities belong to the arithmetic theory in the solve() routine.

Fix use-after-free with ResChains

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

Quote unsat core names if applicable, fixes bug 816.

Initial draft of 2017 competition scripts.

Fix bug 812.

Merge pull request #155 from makaimann/conditional_coverage

Conditional coverage

Merge pull request #161 from 4tXJ7f/fix_parser

Avoid tokenizing FP tokens in non-FP input

Merge pull request #160 from 4tXJ7f/fix_win_build

Fix error in Windows build

Avoid tokenizing FP tokens in non-FP input

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.

Fix error in Windows build

The Windows build was missing the `print_statistics()` function, this commit
moves the function out of the `#ifndef __WIN32__` guard.

Merge pull request #156 from 4tXJ7f/fix_safe_print

Minor fix in safe_print function

Minor fix in safe_print function

This commit fixes two issues reported by Coverity:

- Fixes the check whether the buffer is full in safe_print_hex
- Removes dead code in safe_print for floating-point values

Additionally, it fixes an issue reported by Andy where the names of the
statistics were printed as "<unsupported>" due to calling the const char*
version instead of the std::string version of safe_print.

Finally, this fixes an issue where --segv-spin would not print the program name
because it was a const char*. The program name is now stored as a string.

NOTE: As a side effect, the last part also fixes Coverity issue 1362944, which
has been in CVC4 for a long time.

Cleanup handling of division (possible fix for bugs 803, 804, 805).

Merge pull request #159 from 4tXJ7f/fix_set_types

Fix type checks for relation operators

Fix type checks for relation operators

This commit fixes an assertion error when applying transpose or transitive
closure to a set instead of a relation. Instead it now prints a parse error.

Merge pull request #158 from 4tXJ7f/fix_sets_rewriter

Fix minor bug in sets rewriter

Fix minor bug in sets rewriter

As reported by Coverity, one of the switches in the sets rewriter had a missing
break. This could lead to an assertion failure when rewriting the cardinality
of a transpose as in the test case included in this commit.

Fix bug 806. Minor fixes to remove term formula pass.

Merge pull request #157 from 4tXJ7f/fix_iterator

Fix condition in upwards closure check for sets

Fix condition in upwards closure check for sets

Coverity reported this mismatched iterator.

Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.

Make conflict-based instantiation abort if a ground conflict is found in the master equality engine during term indexing, fixes bug 801.

Merge pull request #154 from 4tXJ7f/fix_test

Fix out-of-bounds access in test

Fix out-of-bounds access in test

Adding VPATH back in

Conditional coverage build

Make signal handlers safer

As reported in bug 769, the signal handlers currently use unsafe
functions such as dynamic memory allocations and fprintf. This commit
fixes the issue by introducing functions for printing statistics in
signal handlers (functions with the `safe` prefix). It also avoids
copying statistics, which further avoids dynamic memory allocation. The
safe printing of statistics has some limitations (it does not support
SExprStats or printing CVC4::Result), which should not matter much in
practice. Printing statistics in a non-signal handler is not affected by
these changes as that uses a separate code path (the functions without
the `safe` prefix).

Additional changes:
- Remove ListStat as it is not used anywhere
- Add unit test for safe printing statistics

Do not split on cardinality for string equivalence classes with non-constant lengths if disequalities already imply sufficient lower bound. Fixes bug 799.

Change str.replace for empty string.

Do not eliminate extended arithmetic symbols when finite model finding is on, add regression.

Fix error message.

skolemization manager may be called also when just unsatCores are on (related to bug 717)

fixing bug 790: track dependencies when the unsatCores() option is on

Partial fix for bug 717.

Minor fixes

Fix bug for real division.

Do not eliminate non-standard arithmetic operators in recursive function definitions, add regression.

Fixes and simplifications for fmf mbqi.

Fix parsing selectors for nullary constructors in smtlib 2.6 format.

Merge pull request #152 from timothy-king/delta-rational-value-cases-second-submission

Updating TheoryArithPrivate::getDeltaValue() to eagerly use the parti…

Changing spaces to tabs in Makefile.

Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial model value if exists.

Merge pull request #151 from 4tXJ7f/fix_debug

Move assertion out of loop for better performance

Disabled bug639.smt2 which still fails.

Add test cases for bugs 639 and 681.

Fix for bug 681 (now gives reasonable error message about using constant
arrays).

Move assertion out of loop for better performance

This is related to bug 508. The debug build was taking much longer than the
production build to compute the result. The issue was an assertion in a loop in
nonClausalSimplify(). By moving the assertion outside of the loop, the debug
build is now roughly an order of magnitude slower than the production build
(instead of two orders of magnitude), which seems to be roughly in line with
the difference for other benchmarks:

Debug version before change:
- Bug (minified version): 1065.6s
- regress3/friedman_n6_i4.smt: 6.9s
- regress2/uflia-error0.smt2: 6.3s
- regress2/fuzz_2.smt: 2.3s

Debug version after change:
- Bug (minified version): 131.4s
- regress3/friedman_n6_i4.smt: 6.7s
- regress2/uflia-error0.smt2: 6.2s
- regress2/fuzz_2.smt: 1.9s

Production version:
- Bug (minified version): 18.8s
- regress3/friedman_n6_i4.smt: 0.8s
- regress2/uflia-error0.smt2: 0.8s
- regress2/fuzz_2.smt: 0.2s

Merge pull request #150 from 4tXJ7f/check_exceptions2

Add check for C++ exceptions to config script

Fix new relations regressions to use sets-ext.

Handle subtypes in sets. Bug fixes for tuples with subtypes.

Add check for C++ exceptions to config script

Bug 687 was caused by the configuration not properly supporting C++
exceptions. To avoid such an incidence in the future, this commit adds a
simple check to `configure.ac` (when not cross compiling).

Merge pull request #149 from PaulMeng/master

Support for relational operators identity and join image

Minor fixes.

Support for relational operators identity and join image

Fix mktheoryrewriter and mktheorytraits for nullaryoperator.

Fixes for handling set universe: restrict upwards rule for universe to memberships into variable sets, do not variable eliminate sets during ppAssert.

Merge pull request #147 from makaimann/coverage_fix

Coverage fix

Fix for bug 639.

Coverage fix

Forcing some make variables to be absolute paths
lcov does not (officially) support relative paths
src/expr and src/options in particular were breaking it

Actively split for upwards closusure intersection. Minor clean up, add regressions.

Fix bug related to portfolio with nullary operators.

Fix nullary operator printers, minor.