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

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

Enable multi-trigger-linear by default, add option.

Simplify Theory::collectModelInfo interface to not take deprecated fullModel argument.

Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regressions.

Merge pull request #141 from 4tXJ7f/remove_def

Remove decl. of getStatisticsRegistry(SmtEngine*)

Merge pull request #142 from timothy-king/nlAlgMerge

Adding a model based axiom instantiation scheme for multiplication. M…

Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.

Remove decl. of getStatisticsRegistry(SmtEngine*)

Commit f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition
of getStatisticsRegistry(SmtEngine*) but not the declaration.

Add option multi-trigger-linear, minor optimization to E-matching.

Merge pull request #139 from 4tXJ7f/remove_throw

[Coverity] Remove throw qualifiers in src/smt

[Coverity] Remove throw qualifiers in src/smt

Addresses coverity issues:

1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413

Minor fixes for trigger selection max.

Add quantifiers options related to model and master equality engine.

Merge pull request #138 from PaulMeng/master

Refactor the standard effort of relational solver

Refactor the standard effort of relational solver

Fix bug 787.

Fix for bug 733

Minor refactoring sygus.

More work on sygus. Add regress4 to Makefile.

Fixing a bug for checking whether a node was visited.

Minor cleanups to ExtTheory.

Removing the friend class modifier from ExtTheory to Theory.

Merge pull request #137 from 4tXJ7f/throw_quals

Remove throw qualifiers in type enumerators

Making the ExtTheory object a private member of Theory.

Making ppNotifyAssertions take a const vector.

Moving the CareGraph into its own file.

Moving the theory::Assertion struct into its own file.

Remove throw qualifiers in type enumerators

This addresses Coverity issues:

- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155

Alphabetizing libcvc4_la_SOURCES.

Add some regressions. Minor.

Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.

Fixing warning message.

support incremental unsat cores

Fix more cases of rewritten explanations in strings for bug 784. Minor.

Minor fix for bounded integers.

Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.

Improve computeCareGraph functions to check shared term equality status once per equivalence class pair.

Merge pull request #135 from PaulMeng/master

fixed cvc4 parser for set complement

fixed cvc4 parser for set complement

Fix for bug 707.