cvc5.git
7 years agoMerge pull request #155 from makaimann/conditional_coverage
Clark Barrett [Wed, 17 May 2017 23:16:04 +0000 (16:16 -0700)]
Merge pull request #155 from makaimann/conditional_coverage

Conditional coverage

7 years agoMerge pull request #161 from 4tXJ7f/fix_parser
Clark Barrett [Tue, 16 May 2017 22:23:41 +0000 (15:23 -0700)]
Merge pull request #161 from 4tXJ7f/fix_parser

Avoid tokenizing FP tokens in non-FP input

7 years agoMerge pull request #160 from 4tXJ7f/fix_win_build
Clark Barrett [Tue, 16 May 2017 22:10:42 +0000 (15:10 -0700)]
Merge pull request #160 from 4tXJ7f/fix_win_build

Fix error in Windows build

7 years agoAvoid tokenizing FP tokens in non-FP input
Andres Noetzli [Tue, 16 May 2017 18:33:38 +0000 (11:33 -0700)]
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.

7 years agoFix error in Windows build
Andres Noetzli [Tue, 16 May 2017 18:08:30 +0000 (11:08 -0700)]
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.

7 years agoMerge pull request #156 from 4tXJ7f/fix_safe_print
Andrew Reynolds [Tue, 16 May 2017 00:12:08 +0000 (19:12 -0500)]
Merge pull request #156 from 4tXJ7f/fix_safe_print

Minor fix in safe_print function

7 years agoMinor fix in safe_print function
Andres Noetzli [Mon, 15 May 2017 15:39:16 +0000 (08:39 -0700)]
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.

7 years agoCleanup handling of division (possible fix for bugs 803, 804, 805).
ajreynol [Mon, 15 May 2017 21:43:50 +0000 (16:43 -0500)]
Cleanup handling of division (possible fix for bugs 803, 804, 805).

7 years agoMerge pull request #159 from 4tXJ7f/fix_set_types
Andrew Reynolds [Mon, 15 May 2017 18:10:56 +0000 (13:10 -0500)]
Merge pull request #159 from 4tXJ7f/fix_set_types

Fix type checks for relation operators

7 years agoFix type checks for relation operators
Andres Noetzli [Mon, 15 May 2017 17:09:45 +0000 (10:09 -0700)]
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.

7 years agoMerge pull request #158 from 4tXJ7f/fix_sets_rewriter
Andrew Reynolds [Mon, 15 May 2017 16:56:43 +0000 (11:56 -0500)]
Merge pull request #158 from 4tXJ7f/fix_sets_rewriter

Fix minor bug in sets rewriter

7 years agoFix minor bug in sets rewriter
Andres Noetzli [Mon, 15 May 2017 16:50:45 +0000 (09:50 -0700)]
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.

7 years agoFix bug 806. Minor fixes to remove term formula pass.
ajreynol [Mon, 15 May 2017 16:44:15 +0000 (11:44 -0500)]
Fix bug 806. Minor fixes to remove term formula pass.

7 years agoMerge pull request #157 from 4tXJ7f/fix_iterator
Andrew Reynolds [Mon, 15 May 2017 15:56:22 +0000 (10:56 -0500)]
Merge pull request #157 from 4tXJ7f/fix_iterator

Fix condition in upwards closure check for sets

7 years agoFix condition in upwards closure check for sets
Andres Noetzli [Mon, 15 May 2017 15:50:21 +0000 (08:50 -0700)]
Fix condition in upwards closure check for sets

Coverity reported this mismatched iterator.

7 years agoFix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.
ajreynol [Mon, 15 May 2017 14:48:07 +0000 (09:48 -0500)]
Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.

7 years agoMake conflict-based instantiation abort if a ground conflict is found in the master...
ajreynol [Mon, 15 May 2017 14:07:21 +0000 (09:07 -0500)]
Make conflict-based instantiation abort if a ground conflict is found in the master equality engine during term indexing, fixes bug 801.

7 years agoMerge pull request #154 from 4tXJ7f/fix_test
Clark Barrett [Sun, 14 May 2017 03:02:24 +0000 (20:02 -0700)]
Merge pull request #154 from 4tXJ7f/fix_test

Fix out-of-bounds access in test

7 years agoFix out-of-bounds access in test
Andres Notzli [Sat, 13 May 2017 23:09:58 +0000 (16:09 -0700)]
Fix out-of-bounds access in test

7 years agoAdding VPATH back in
makaimann [Fri, 12 May 2017 20:09:13 +0000 (13:09 -0700)]
Adding VPATH back in

7 years agoConditional coverage build
makaimann [Fri, 12 May 2017 19:47:16 +0000 (12:47 -0700)]
Conditional coverage build

7 years agoMake signal handlers safer
Andres Notzli [Fri, 31 Mar 2017 21:27:05 +0000 (14:27 -0700)]
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

7 years agoDo not split on cardinality for string equivalence classes with non-constant lengths...
ajreynol [Wed, 10 May 2017 15:35:38 +0000 (10:35 -0500)]
Do not split on cardinality for string equivalence classes with non-constant lengths if disequalities already imply sufficient lower bound. Fixes bug 799.

7 years agoChange str.replace for empty string.
ajreynol [Tue, 9 May 2017 22:16:06 +0000 (17:16 -0500)]
Change str.replace for empty string.

7 years agoDo not eliminate extended arithmetic symbols when finite model finding is on, add...
ajreynol [Fri, 5 May 2017 22:41:18 +0000 (17:41 -0500)]
Do not eliminate extended arithmetic symbols when finite model finding is on, add regression.

7 years agoFix error message.
ajreynol [Fri, 5 May 2017 14:35:12 +0000 (09:35 -0500)]
Fix error message.

7 years agoskolemization manager may be called also when just unsatCores are on (related to...
guykatzz [Thu, 4 May 2017 20:51:36 +0000 (13:51 -0700)]
skolemization manager may be called also when just unsatCores are on (related to bug 717)

7 years agofixing bug 790: track dependencies when the unsatCores() option is on
guykatzz [Thu, 4 May 2017 18:24:41 +0000 (11:24 -0700)]
fixing bug 790: track dependencies when the unsatCores() option is on

7 years agoPartial fix for bug 717.
Clark Barrett [Fri, 28 Apr 2017 22:00:01 +0000 (15:00 -0700)]
Partial fix for bug 717.

7 years agoMinor fixes
ajreynol [Fri, 28 Apr 2017 20:52:17 +0000 (15:52 -0500)]
Minor fixes

7 years agoFix bug for real division.
ajreynol [Fri, 28 Apr 2017 20:48:13 +0000 (15:48 -0500)]
Fix bug for real division.

7 years agoDo not eliminate non-standard arithmetic operators in recursive function definitions...
ajreynol [Fri, 28 Apr 2017 16:46:53 +0000 (11:46 -0500)]
Do not eliminate non-standard arithmetic operators in recursive function definitions, add regression.

7 years agoFixes and simplifications for fmf mbqi.
ajreynol [Mon, 24 Apr 2017 21:56:23 +0000 (16:56 -0500)]
Fixes and simplifications for fmf mbqi.

7 years agoFix parsing selectors for nullary constructors in smtlib 2.6 format.
ajreynol [Mon, 24 Apr 2017 15:14:19 +0000 (10:14 -0500)]
Fix parsing selectors for nullary constructors in smtlib 2.6 format.

7 years agoMerge pull request #152 from timothy-king/delta-rational-value-cases-second-submission
Andrew Reynolds [Mon, 24 Apr 2017 01:07:54 +0000 (20:07 -0500)]
Merge pull request #152 from timothy-king/delta-rational-value-cases-second-submission

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

7 years agoChanging spaces to tabs in Makefile.
Tim King [Sun, 23 Apr 2017 20:05:10 +0000 (13:05 -0700)]
Changing spaces to tabs in Makefile.

7 years agoUpdating TheoryArithPrivate::getDeltaValue() to eagerly use the partial model value...
Tim King [Thu, 13 Apr 2017 07:21:30 +0000 (00:21 -0700)]
Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial model value if exists.

7 years agoMerge pull request #151 from 4tXJ7f/fix_debug
Clark Barrett [Sat, 22 Apr 2017 04:45:23 +0000 (21:45 -0700)]
Merge pull request #151 from 4tXJ7f/fix_debug

Move assertion out of loop for better performance

7 years agoDisabled bug639.smt2 which still fails.
Clark Barrett [Sat, 22 Apr 2017 04:39:53 +0000 (21:39 -0700)]
Disabled bug639.smt2 which still fails.

7 years agoAdd test cases for bugs 639 and 681.
Clark Barrett [Fri, 21 Apr 2017 23:01:34 +0000 (16:01 -0700)]
Add test cases for bugs 639 and 681.

7 years agoFix for bug 681 (now gives reasonable error message about using constant
Clark Barrett [Fri, 21 Apr 2017 22:09:33 +0000 (15:09 -0700)]
Fix for bug 681 (now gives reasonable error message about using constant
arrays).

7 years agoMove assertion out of loop for better performance
Andres Noetzli [Fri, 21 Apr 2017 21:39:56 +0000 (14:39 -0700)]
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

7 years agoMerge pull request #150 from 4tXJ7f/check_exceptions2
Clark Barrett [Fri, 21 Apr 2017 16:43:50 +0000 (09:43 -0700)]
Merge pull request #150 from 4tXJ7f/check_exceptions2

Add check for C++ exceptions to config script

7 years agoFix new relations regressions to use sets-ext.
ajreynol [Fri, 21 Apr 2017 14:33:26 +0000 (09:33 -0500)]
Fix new relations regressions to use sets-ext.

7 years agoHandle subtypes in sets. Bug fixes for tuples with subtypes.
ajreynol [Fri, 21 Apr 2017 14:26:04 +0000 (09:26 -0500)]
Handle subtypes in sets. Bug fixes for tuples with subtypes.

7 years agoAdd check for C++ exceptions to config script
Andres Notzli [Wed, 19 Apr 2017 15:46:59 +0000 (08:46 -0700)]
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).

7 years agoMerge pull request #149 from PaulMeng/master
Andrew Reynolds [Thu, 20 Apr 2017 22:08:08 +0000 (17:08 -0500)]
Merge pull request #149 from PaulMeng/master

Support for relational operators identity and join image

7 years agoMinor fixes.
ajreynol [Thu, 20 Apr 2017 19:19:51 +0000 (14:19 -0500)]
Minor fixes.

7 years agoSupport for relational operators identity and join image
Paul Meng [Thu, 20 Apr 2017 19:04:24 +0000 (14:04 -0500)]
Support for relational operators identity and join image

7 years agoFix mktheoryrewriter and mktheorytraits for nullaryoperator.
ajreynol [Wed, 19 Apr 2017 21:29:01 +0000 (16:29 -0500)]
Fix mktheoryrewriter and mktheorytraits for nullaryoperator.

7 years agoFixes for handling set universe: restrict upwards rule for universe to memberships...
ajreynol [Wed, 19 Apr 2017 21:16:35 +0000 (16:16 -0500)]
Fixes for handling set universe: restrict upwards rule for universe to memberships into variable sets, do not variable eliminate sets during ppAssert.

7 years agoMerge pull request #147 from makaimann/coverage_fix
Clark Barrett [Wed, 19 Apr 2017 03:30:42 +0000 (20:30 -0700)]
Merge pull request #147 from makaimann/coverage_fix

Coverage fix

7 years agoFix for bug 639.
Clark Barrett [Tue, 18 Apr 2017 23:57:40 +0000 (16:57 -0700)]
Fix for bug 639.

7 years agoCoverage fix
makaimann [Tue, 18 Apr 2017 15:49:17 +0000 (08:49 -0700)]
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

7 years agoActively split for upwards closusure intersection. Minor clean up, add regressions.
ajreynol [Fri, 14 Apr 2017 22:25:18 +0000 (17:25 -0500)]
Actively split for upwards closusure intersection. Minor clean up, add regressions.

7 years agoFix bug related to portfolio with nullary operators.
ajreynol [Fri, 14 Apr 2017 22:03:44 +0000 (17:03 -0500)]
Fix bug related to portfolio with nullary operators.

7 years agoFix nullary operator printers, minor.
ajreynol [Fri, 14 Apr 2017 21:34:59 +0000 (16:34 -0500)]
Fix nullary operator printers, minor.

7 years agoFix for fmf-fun when the option is set by user command.
ajreynol [Fri, 14 Apr 2017 16:06:45 +0000 (11:06 -0500)]
Fix for fmf-fun when the option is set by user command.

7 years agoFix for some compilers
Clark Barrett [Thu, 13 Apr 2017 18:57:19 +0000 (11:57 -0700)]
Fix for some compilers

7 years agoAdd nullary operator metakind.
ajreynol [Wed, 12 Apr 2017 21:47:12 +0000 (16:47 -0500)]
Add nullary operator metakind.

7 years agoBug fix in conjecture generation for --quant-ind.
ajreynol [Tue, 11 Apr 2017 16:14:42 +0000 (11:14 -0500)]
Bug fix in conjecture generation for --quant-ind.

7 years agoChange option names for nl.
ajreynol [Fri, 7 Apr 2017 16:22:44 +0000 (11:22 -0500)]
Change option names for nl.

7 years agoMerge pull request #143 from FabianWolff/master
Clark Barrett [Thu, 6 Apr 2017 06:32:12 +0000 (23:32 -0700)]
Merge pull request #143 from FabianWolff/master

Fix several spelling errors

7 years agoFix bug 698.
ajreynol [Wed, 5 Apr 2017 18:32:35 +0000 (13:32 -0500)]
Fix bug 698.

7 years agoFixes for nlAlgSolveSubs.
ajreynol [Wed, 5 Apr 2017 18:19:21 +0000 (13:19 -0500)]
Fixes for nlAlgSolveSubs.

7 years agoMerge pull request #145 from 4tXJ7f/fix_lfsc_args
Andrew Reynolds [Wed, 5 Apr 2017 18:15:31 +0000 (13:15 -0500)]
Merge pull request #145 from 4tXJ7f/fix_lfsc_args

[LFSC] Fix segfault

7 years agoCaching for fun def process, add regression.
ajreynol [Wed, 5 Apr 2017 14:56:00 +0000 (09:56 -0500)]
Caching for fun def process, add regression.

7 years ago[LFSC] Fix segfault
Andres Notzli [Sun, 26 Mar 2017 21:39:07 +0000 (23:39 +0200)]
[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.

7 years agoRemove extraneous portion of an nl regression.
ajreynol [Wed, 5 Apr 2017 14:09:55 +0000 (09:09 -0500)]
Remove extraneous portion of an nl regression.

7 years agoAdd non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_M...
ajreynol [Wed, 5 Apr 2017 14:01:55 +0000 (09:01 -0500)]
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.

7 years agoFix several spelling errors
Fabian Wolff [Tue, 4 Apr 2017 22:47:10 +0000 (00:47 +0200)]
Fix several spelling errors

7 years agoEnable multi-trigger-linear by default, add option.
ajreynol [Tue, 4 Apr 2017 17:54:26 +0000 (12:54 -0500)]
Enable multi-trigger-linear by default, add option.

7 years agoSimplify Theory::collectModelInfo interface to not take deprecated fullModel argument.
ajreynol [Tue, 4 Apr 2017 16:21:30 +0000 (11:21 -0500)]
Simplify Theory::collectModelInfo interface to not take deprecated fullModel argument.

7 years agoDo not solve for 0-ary non-constant symbols (for which isVar returns true), add regre...
ajreynol [Tue, 4 Apr 2017 14:59:45 +0000 (09:59 -0500)]
Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regressions.

7 years agoMerge pull request #141 from 4tXJ7f/remove_def
Clark Barrett [Tue, 4 Apr 2017 06:17:42 +0000 (23:17 -0700)]
Merge pull request #141 from 4tXJ7f/remove_def

Remove decl. of getStatisticsRegistry(SmtEngine*)

7 years agoMerge pull request #142 from timothy-king/nlAlgMerge
Andrew Reynolds [Mon, 3 Apr 2017 14:38:54 +0000 (09:38 -0500)]
Merge pull request #142 from timothy-king/nlAlgMerge

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

7 years agoAdding a model based axiom instantiation scheme for multiplication. Merge commit...
Tim King [Mon, 3 Apr 2017 02:29:36 +0000 (19:29 -0700)]
Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.

7 years agoRemove decl. of getStatisticsRegistry(SmtEngine*)
Andres Notzli [Fri, 31 Mar 2017 22:02:39 +0000 (15:02 -0700)]
Remove decl. of getStatisticsRegistry(SmtEngine*)

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

7 years agoAdd option multi-trigger-linear, minor optimization to E-matching.
ajreynol [Fri, 31 Mar 2017 13:43:29 +0000 (08:43 -0500)]
Add option multi-trigger-linear, minor optimization to E-matching.

7 years agoMerge pull request #139 from 4tXJ7f/remove_throw
Clark Barrett [Thu, 30 Mar 2017 19:49:38 +0000 (12:49 -0700)]
Merge pull request #139 from 4tXJ7f/remove_throw

[Coverity] Remove throw qualifiers in src/smt

7 years ago[Coverity] Remove throw qualifiers in src/smt
Andres Notzli [Wed, 29 Mar 2017 21:27:56 +0000 (23:27 +0200)]
[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

7 years agoMinor fixes for trigger selection max.
ajreynol [Thu, 30 Mar 2017 14:11:52 +0000 (09:11 -0500)]
Minor fixes for trigger selection max.

7 years agoAdd quantifiers options related to model and master equality engine.
ajreynol [Wed, 29 Mar 2017 18:49:51 +0000 (13:49 -0500)]
Add quantifiers options related to model and master equality engine.

7 years agoMerge pull request #138 from PaulMeng/master
PaulMeng [Wed, 29 Mar 2017 14:36:29 +0000 (09:36 -0500)]
Merge pull request #138 from PaulMeng/master

Refactor the standard effort of relational solver

7 years agoRefactor the standard effort of relational solver
Paul Meng [Wed, 29 Mar 2017 04:08:52 +0000 (23:08 -0500)]
Refactor the standard effort of relational solver

7 years agoFix bug 787.
ajreynol [Wed, 29 Mar 2017 03:22:05 +0000 (22:22 -0500)]
Fix bug 787.

7 years agoFix for bug 733
Clark Barrett [Wed, 29 Mar 2017 01:29:48 +0000 (18:29 -0700)]
Fix for bug 733

7 years agoMinor refactoring sygus.
ajreynol [Tue, 28 Mar 2017 21:21:12 +0000 (16:21 -0500)]
Minor refactoring sygus.

7 years agoMore work on sygus. Add regress4 to Makefile.
ajreynol [Tue, 28 Mar 2017 14:35:43 +0000 (09:35 -0500)]
More work on sygus. Add regress4 to Makefile.

7 years agoFixing a bug for checking whether a node was visited.
Tim King [Tue, 28 Mar 2017 06:26:34 +0000 (23:26 -0700)]
Fixing a bug for checking whether a node was visited.

7 years agoMinor cleanups to ExtTheory.
Tim King [Tue, 28 Mar 2017 05:15:23 +0000 (22:15 -0700)]
Minor cleanups to ExtTheory.

7 years agoRemoving the friend class modifier from ExtTheory to Theory.
Tim King [Tue, 28 Mar 2017 03:59:48 +0000 (20:59 -0700)]
Removing the friend class modifier from ExtTheory to Theory.

7 years agoMerge pull request #137 from 4tXJ7f/throw_quals
Clark Barrett [Mon, 27 Mar 2017 20:20:27 +0000 (13:20 -0700)]
Merge pull request #137 from 4tXJ7f/throw_quals

Remove throw qualifiers in type enumerators

7 years agoMaking the ExtTheory object a private member of Theory.
Tim King [Mon, 27 Mar 2017 19:26:14 +0000 (12:26 -0700)]
Making the ExtTheory object a private member of Theory.

7 years agoMaking ppNotifyAssertions take a const vector.
Tim King [Mon, 27 Mar 2017 17:24:13 +0000 (10:24 -0700)]
Making ppNotifyAssertions take a const vector.

7 years agoMoving the CareGraph into its own file.
Tim King [Mon, 27 Mar 2017 17:02:11 +0000 (10:02 -0700)]
Moving the CareGraph into its own file.

7 years agoMoving the theory::Assertion struct into its own file.
Tim King [Mon, 27 Mar 2017 16:40:30 +0000 (09:40 -0700)]
Moving the theory::Assertion struct into its own file.

7 years agoRemove throw qualifiers in type enumerators
Andres Notzli [Mon, 27 Mar 2017 09:40:45 +0000 (11:40 +0200)]
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

7 years agoAlphabetizing libcvc4_la_SOURCES.
Tim King [Mon, 27 Mar 2017 04:59:36 +0000 (21:59 -0700)]
Alphabetizing libcvc4_la_SOURCES.

7 years agoAdd some regressions. Minor.
ajreynol [Fri, 24 Mar 2017 14:56:12 +0000 (09:56 -0500)]
Add some regressions. Minor.