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

Fix for fmf-fun when the option is set by user command.

Fix for some compilers

Add nullary operator metakind.

Bug fix in conjecture generation for --quant-ind.

Change option names for nl.

Merge pull request #143 from FabianWolff/master

Fix several spelling errors

Fix bug 698.

Fixes for nlAlgSolveSubs.

Merge pull request #145 from 4tXJ7f/fix_lfsc_args

[LFSC] Fix segfault

Caching for fun def process, add regression.

[LFSC] Fix segfault

LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.

Remove extraneous portion of an nl regression.

Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.

Fix several spelling errors