cvc5.git
9 years agoadded initial AX rules;
Tianyi Liang [Wed, 7 Jan 2015 16:02:01 +0000 (10:02 -0600)]
added initial AX rules;
fixed a bug for empty string in regex

9 years agoDisable prenex by default when using fmf bound int, minor improvement to datatypes...
ajreynol [Sun, 28 Dec 2014 04:42:28 +0000 (05:42 +0100)]
Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter

9 years agoAdding an option to the equality engine constructor to treat all constants as
Dejan Jovanovic [Sat, 27 Dec 2014 03:15:13 +0000 (19:15 -0800)]
Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 22 Dec 2014 22:24:08 +0000 (16:24 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agobug fix for constant regular expression model building
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building

9 years agobug fix for constant regular expression model building
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building

9 years agoDo not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.
ajreynol [Mon, 22 Dec 2014 22:21:40 +0000 (23:21 +0100)]
Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.

9 years agoAdd misc trigger options.
ajreynol [Sun, 21 Dec 2014 23:49:27 +0000 (00:49 +0100)]
Add misc trigger options.

9 years agoFix oversight in dumping assertions in preprocessing.
Morgan Deters [Tue, 16 Dec 2014 23:04:47 +0000 (18:04 -0500)]
Fix oversight in dumping assertions in preprocessing.

9 years agoAdd cvc parsing support for cardinality constraints. Bug fix for enumerating element...
ajreynol [Fri, 12 Dec 2014 11:03:26 +0000 (12:03 +0100)]
Add cvc parsing support for cardinality constraints.  Bug fix for enumerating elements to meet cardinality lower bounds.

9 years agoMinor fixes to language bindings. (Resolves #607.)
Morgan Deters [Thu, 11 Dec 2014 22:04:29 +0000 (17:04 -0500)]
Minor fixes to language bindings. (Resolves #607.)

9 years agoOption to enable/disable cyclicity check in datatypes.
ajreynol [Thu, 11 Dec 2014 13:09:54 +0000 (14:09 +0100)]
Option to enable/disable cyclicity check in datatypes.

9 years agobug fix, thanks to Guy's example.
Tianyi Liang [Thu, 11 Dec 2014 02:59:32 +0000 (20:59 -0600)]
bug fix, thanks to Guy's example.

9 years agoBetter error description (related to bug 605).
Morgan Deters [Tue, 9 Dec 2014 23:48:55 +0000 (18:48 -0500)]
Better error description (related to bug 605).

9 years agoCleanup.
Morgan Deters [Tue, 9 Dec 2014 23:48:43 +0000 (18:48 -0500)]
Cleanup.

9 years agoAdded string constant in java api example.
Tianyi Liang [Sat, 6 Dec 2014 21:28:52 +0000 (15:28 -0600)]
Added string constant in java api example.

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 6 Dec 2014 19:26:39 +0000 (13:26 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agoAdded C++/Java api examples;
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

9 years agoAdded C++/Java api examples;
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

9 years agoFix dt.size care graph.
ajreynol [Sat, 6 Dec 2014 00:26:44 +0000 (01:26 +0100)]
Fix dt.size care graph.

9 years agoRelaxed the constant requirement for regular expression loop;
Tianyi Liang [Fri, 5 Dec 2014 00:17:55 +0000 (18:17 -0600)]
Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).

9 years agoclean up and improve intersection
Tianyi Liang [Thu, 4 Dec 2014 22:13:41 +0000 (16:13 -0600)]
clean up and improve intersection

9 years agoFix valgrind-flagged error about uninitialized value.
Morgan Deters [Thu, 4 Dec 2014 06:40:21 +0000 (01:40 -0500)]
Fix valgrind-flagged error about uninitialized value.

9 years agoFix segfault in lambdas when constructed via API.
Morgan Deters [Thu, 4 Dec 2014 06:39:53 +0000 (01:39 -0500)]
Fix segfault in lambdas when constructed via API.

9 years agoFix UnsatCore in language bindings.
Morgan Deters [Thu, 4 Dec 2014 02:58:50 +0000 (21:58 -0500)]
Fix UnsatCore in language bindings.

9 years agoFloating point infrastructure.
Martin Brain [Thu, 4 Dec 2014 02:29:43 +0000 (21:29 -0500)]
Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Wed, 3 Dec 2014 17:09:14 +0000 (12:09 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agoRevert "Disable constants sharing in eq engine, disable hack in theory engine."
Kshitij Bansal [Wed, 3 Dec 2014 16:38:36 +0000 (11:38 -0500)]
Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.

9 years agodisable inter cache
Tianyi Liang [Wed, 3 Dec 2014 05:44:26 +0000 (23:44 -0600)]
disable inter cache

10 years agoSynchronize conjecture generation with E-matching. Minor fix to --full-saturate...
ajreynol [Fri, 28 Nov 2014 15:27:19 +0000 (16:27 +0100)]
Synchronize conjecture generation with E-matching.  Minor fix to --full-saturate-quant.

10 years agoadd intersection rewriting
Tianyi Liang [Thu, 27 Nov 2014 04:09:38 +0000 (22:09 -0600)]
add intersection rewriting

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 27 Nov 2014 01:34:37 +0000 (19:34 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting

10 years agoadd more functions for regular expressions
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions

10 years agoadd more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting

10 years agoadd more functions for regular expressions
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions

10 years agoFix bug in --term-db-mode=relevant with variable triggers. Support inst-closure...
ajreynol [Tue, 25 Nov 2014 15:15:10 +0000 (16:15 +0100)]
Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.

10 years agoadded number of resource units used as a stat
lianah [Sat, 22 Nov 2014 18:11:19 +0000 (10:11 -0800)]
added number of resource units used as a stat

10 years agoThrow error when pattern is not list of terms.
ajreynol [Fri, 21 Nov 2014 09:48:17 +0000 (10:48 +0100)]
Throw error when pattern is not list of terms.

10 years agoChange default option to --inst-when=full-last-call (interleave instantiation and...
ajreynol [Fri, 21 Nov 2014 08:42:07 +0000 (09:42 +0100)]
Change default option to --inst-when=full-last-call (interleave instantiation and theory combination).  Fix inefficiency in NNF, enable by default.  Set best defaults for --mbqi=abs.

10 years agoDisable constants sharing in eq engine, disable hack in theory engine. Changes to...
ajreynol [Thu, 20 Nov 2014 09:56:20 +0000 (10:56 +0100)]
Disable constants sharing in eq engine, disable hack in theory engine.  Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine.

10 years agoFix #lines in template.
Morgan Deters [Thu, 20 Nov 2014 05:30:33 +0000 (00:30 -0500)]
Fix #lines in template.

10 years agoMaking construction of trigger sets not use the global engine state.
Dejan Jovanović [Thu, 20 Nov 2014 03:42:31 +0000 (22:42 -0500)]
Making construction of trigger sets not use the global engine state.

10 years agoDistribute UnsafeInterruptException interface file for SWIG.
Morgan Deters [Wed, 19 Nov 2014 15:27:59 +0000 (10:27 -0500)]
Distribute UnsafeInterruptException interface file for SWIG.

10 years agoMerge pull request #70 from kbansal/sets-for-merge-squashed
Kshitij Bansal [Wed, 19 Nov 2014 02:50:33 +0000 (21:50 -0500)]
Merge pull request #70 from kbansal/sets-for-merge-squashed

Set Constant's normal form and other short fixes

10 years agoSet Constant's normal form and other short fixes
Kshitij Bansal [Mon, 10 Nov 2014 18:11:20 +0000 (13:11 -0500)]
Set Constant's normal form and other short fixes

Other short fixes:
* use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT
* theoryof-mode fix in smt_engine.cpp
* hack in TheoryModel::getModelValue [TODO: notify Clark/Andy]
* Lemma generation when it rewrites to true/false fix
* TermInfoManager::addTerm(..) fix
* Move SUBSET rewrite to preRewrite
* On preRegister, queue up propagation to be done upfront
** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code.
* TheorySetsProperties::getCardinality(..) fix

Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!

10 years agoclear model cache in BVQuickCheck clearSolver() (fixes bug 587)
Liana Hadarean [Tue, 18 Nov 2014 22:58:34 +0000 (14:58 -0800)]
clear model cache in BVQuickCheck clearSolver() (fixes bug 587)

10 years agoAll Minisat solve calls now return lbool (fixes bug 599)
lianah [Tue, 18 Nov 2014 19:35:02 +0000 (14:35 -0500)]
All Minisat solve calls now return lbool (fixes bug 599)

10 years agoCompute model basis only for fmf. Add another co-datatype regression.
ajreynol [Tue, 18 Nov 2014 17:44:48 +0000 (18:44 +0100)]
Compute model basis only for fmf.  Add another co-datatype regression.

10 years agoAdd local theory extensions instantiation strategy (incomplete). Refactor how defaul...
ajreynol [Tue, 18 Nov 2014 16:39:05 +0000 (17:39 +0100)]
Add local theory extensions instantiation strategy (incomplete).  Refactor how default options are set for quantifiers.  Minor improvement to datatypes.  Add unsat co-datatype regression.  Clean up instantiation engine.  Set inst level 0 on introduced constants for types with no ground terms.  Return introduced constant for variable trigger when no ground terms exist.

10 years agoadded command line option for extractArith bv rewrite
lianah [Mon, 17 Nov 2014 23:40:26 +0000 (18:40 -0500)]
added command line option for extractArith bv rewrite

10 years agoShort-circuit in TheoryArithPrivate::check(), care of Tim.
Morgan Deters [Mon, 17 Nov 2014 14:33:55 +0000 (09:33 -0500)]
Short-circuit in TheoryArithPrivate::check(), care of Tim.

10 years agoNew, uniform checkTime statistic for all theories (as discussed in meeting).
Morgan Deters [Thu, 13 Nov 2014 00:42:23 +0000 (19:42 -0500)]
New, uniform checkTime statistic for all theories (as discussed in meeting).

10 years agoResource-limiting work.
Liana Hadarean [Mon, 17 Nov 2014 20:26:42 +0000 (15:26 -0500)]
Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
10 years agoAdd term db mode. Minor changes to quantifiers rewriter: split ITE's where equality...
ajreynol [Sun, 16 Nov 2014 15:38:50 +0000 (16:38 +0100)]
Add term db mode.  Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches.  Minor cleanup.

10 years agoBe lazier to consider EQC in UF+cardinality solver. Minor cleanup.
ajreynol [Fri, 14 Nov 2014 11:25:07 +0000 (12:25 +0100)]
Be lazier to consider EQC in UF+cardinality solver.  Minor cleanup.

10 years agoMinor changes to AUTHORS and COPYING
Clark Barrett [Thu, 13 Nov 2014 23:13:49 +0000 (15:13 -0800)]
Minor changes to AUTHORS and COPYING

10 years agoMinor adjustments to wording.
Morgan Deters [Thu, 13 Nov 2014 22:02:24 +0000 (17:02 -0500)]
Minor adjustments to wording.

10 years agoCopyright text fixes.
Morgan Deters [Thu, 13 Nov 2014 21:37:19 +0000 (16:37 -0500)]
Copyright text fixes.

10 years agoMerge pull request #69 from mdeters/bug594
Morgan Deters [Thu, 13 Nov 2014 18:35:46 +0000 (13:35 -0500)]
Merge pull request #69 from mdeters/bug594

Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).

10 years agoRemove two obsolete versions of MBQI.
ajreynol [Thu, 13 Nov 2014 11:17:46 +0000 (12:17 +0100)]
Remove two obsolete versions of MBQI.

10 years agoMore preparation for filtering relevant terms in TermDb.
ajreynol [Thu, 13 Nov 2014 09:43:57 +0000 (10:43 +0100)]
More preparation for filtering relevant terms in TermDb.

10 years agoPossible fix for bug594
Morgan Deters [Tue, 11 Nov 2014 21:21:37 +0000 (16:21 -0500)]
Possible fix for bug594

10 years agoMerge pull request #65 from mdeters/bv-ineq-cachefix
Morgan Deters [Thu, 13 Nov 2014 04:26:16 +0000 (23:26 -0500)]
Merge pull request #65 from mdeters/bv-ineq-cachefix

Fix BV inequality solver caching, and TNode fix.

10 years agoBV inequality graph TNode fix.
Morgan Deters [Wed, 12 Nov 2014 17:31:00 +0000 (12:31 -0500)]
BV inequality graph TNode fix.

10 years agoFix BV inequality solver caching.
Morgan Deters [Wed, 12 Nov 2014 12:46:02 +0000 (07:46 -0500)]
Fix BV inequality solver caching.

10 years agoFix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.
Morgan Deters [Wed, 12 Nov 2014 13:29:00 +0000 (08:29 -0500)]
Fix tokenization of "reset" in SMT-LIB v2.0.  It's a reserved word only in 2.5.

10 years agoMinor cleanup.
Morgan Deters [Mon, 10 Nov 2014 14:34:32 +0000 (09:34 -0500)]
Minor cleanup.

10 years agoMerge pull request #64 from mdeters/theorysets-hashset-iteration
Kshitij Bansal [Tue, 11 Nov 2014 19:01:47 +0000 (14:01 -0500)]
Merge pull request #64 from mdeters/theorysets-hashset-iteration

Update TheorySets to use CDHashSet<>::key_begin() / key_end().

10 years agoWork on synchronizing decision=justification and E-matching.
ajreynol [Tue, 11 Nov 2014 10:38:35 +0000 (11:38 +0100)]
Work on synchronizing decision=justification and E-matching.

10 years agoMerge pull request #63 from mdeters/theorystrings-hashset-iteration
Tianyi Liang [Mon, 10 Nov 2014 19:48:17 +0000 (13:48 -0600)]
Merge pull request #63 from mdeters/theorystrings-hashset-iteration

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

10 years agoBug 593 fix: if the type is finite, it is now considered for detecting theories of...
Dejan Jovanović [Fri, 7 Nov 2014 17:31:26 +0000 (12:31 -0500)]
Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.

10 years agoDo not eliminate variables only occurring in patterns. Minor improvements to sort...
ajreynol [Mon, 10 Nov 2014 14:53:51 +0000 (15:53 +0100)]
Do not eliminate variables only occurring in patterns.  Minor improvements to sort inference.  Remove unused code.

10 years agoMerge branch '1.4.x'
Morgan Deters [Mon, 10 Nov 2014 00:02:42 +0000 (19:02 -0500)]
Merge branch '1.4.x'

10 years agoUpdate TheorySets to use CDHashSet<>::key_begin() / key_end().
Morgan Deters [Sun, 9 Nov 2014 23:20:28 +0000 (18:20 -0500)]
Update TheorySets to use CDHashSet<>::key_begin() / key_end().

10 years agoUpdate TheoryStrings to use CDHashSet<>::key_begin() / key_end().
Morgan Deters [Sun, 9 Nov 2014 23:20:32 +0000 (18:20 -0500)]
Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

10 years agoWork around an apparent bug in libc++ that was causing crashes on Mac..
Morgan Deters [Sat, 8 Nov 2014 20:13:24 +0000 (15:13 -0500)]
Work around an apparent bug in libc++ that was causing crashes on Mac..

10 years agoFix a deterministic assignment-ordering for get-assignment (fixes a regression failur...
Morgan Deters [Sun, 9 Nov 2014 23:20:04 +0000 (18:20 -0500)]
Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).

10 years agoIncrease stack size when running regressions (fixes some regression crashes on Mac).
Morgan Deters [Sun, 9 Nov 2014 23:53:11 +0000 (18:53 -0500)]
Increase stack size when running regressions (fixes some regression crashes on Mac).

10 years agoFix dt shared terms issue, reenable regression.
ajreynol [Sun, 9 Nov 2014 11:17:55 +0000 (12:17 +0100)]
Fix dt shared terms issue, reenable regression.

10 years agoFix bug with incremental+datatypes. Minor cleanup. Disable regression bug484, enabl...
ajreynol [Sat, 8 Nov 2014 16:42:50 +0000 (17:42 +0100)]
Fix bug with incremental+datatypes.  Minor cleanup.  Disable regression bug484, enable parsing_ringer.

10 years agoMerge pull request #62 from mdeters/bv-cleanup
Morgan Deters [Sat, 8 Nov 2014 15:52:22 +0000 (10:52 -0500)]
Merge pull request #62 from mdeters/bv-cleanup

Remove some unused variables.

10 years agoRemove some unused variables.
Morgan Deters [Sat, 8 Nov 2014 01:43:53 +0000 (20:43 -0500)]
Remove some unused variables.

10 years agoFixed bug in model builder with subtypes
Clark Barrett [Sat, 8 Nov 2014 00:40:54 +0000 (16:40 -0800)]
Fixed bug in model builder with subtypes

10 years agoRemove some dead code.
Morgan Deters [Fri, 7 Nov 2014 23:59:36 +0000 (18:59 -0500)]
Remove some dead code.

10 years agoFix a memory leak in SatSolverRegistry (re: bug #594).
Morgan Deters [Fri, 7 Nov 2014 22:55:30 +0000 (17:55 -0500)]
Fix a memory leak in SatSolverRegistry (re: bug #594).

10 years agoFix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves...
Morgan Deters [Fri, 7 Nov 2014 22:24:35 +0000 (17:24 -0500)]
Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).

10 years agoMerge branch '1.4.x'
Morgan Deters [Fri, 7 Nov 2014 21:59:09 +0000 (16:59 -0500)]
Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp
test/regress/regress0/Makefile.am

10 years agoFix missing case in Boolean terms rewriting. (Resolves bug #596.)
Morgan Deters [Fri, 7 Nov 2014 21:57:58 +0000 (16:57 -0500)]
Fix missing case in Boolean terms rewriting.  (Resolves bug #596.)

10 years agoMerge branch '1.4.x'
Morgan Deters [Fri, 7 Nov 2014 21:51:26 +0000 (16:51 -0500)]
Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp

10 years agoCorrected fix for missing case in model postprocessor (resolves bug #595).
Morgan Deters [Fri, 7 Nov 2014 21:16:57 +0000 (16:16 -0500)]
Corrected fix for missing case in model postprocessor (resolves bug #595).

10 years agoEnable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement...
ajreynol [Fri, 7 Nov 2014 16:38:53 +0000 (17:38 +0100)]
Enable --quant-cf by default.  Fix bug in qcf for mixed Int/Real.  Minor improvement to performance of E-matching.

10 years agoRevert "Fix missing case in model postprocessor (resolves bug #595)."
Morgan Deters [Fri, 7 Nov 2014 15:16:00 +0000 (10:16 -0500)]
Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

10 years agoRevert "Fix missing case in model postprocessor (resolves bug #595)."
Morgan Deters [Fri, 7 Nov 2014 15:15:41 +0000 (10:15 -0500)]
Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Conflicts:
test/regress/regress0/Makefile.am

10 years agoUpdate competition build rules.
Morgan Deters [Mon, 27 Oct 2014 23:29:22 +0000 (19:29 -0400)]
Update competition build rules.

10 years agoMerge branch '1.4.x'
Morgan Deters [Fri, 7 Nov 2014 14:24:15 +0000 (09:24 -0500)]
Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

10 years agoFix missing case in model postprocessor (resolves bug #595).
Morgan Deters [Fri, 7 Nov 2014 14:22:11 +0000 (09:22 -0500)]
Fix missing case in model postprocessor (resolves bug #595).

10 years agoProperly distinguish which EQC to assign values in datatypes, use assertRepresentativ...
ajreynol [Fri, 7 Nov 2014 10:37:43 +0000 (11:37 +0100)]
Properly distinguish which EQC to assign values in datatypes, use assertRepresentative.  Disable regression related to records.  Enable fmf-fun related regression (modified).  Apply modified version of Morgan's patch to fix tuples/records in model.  Fix bug with sort inference + patterns.  Minor infrastructure.

10 years agoMinor fix for getInstCons
ajreynol [Thu, 6 Nov 2014 13:05:08 +0000 (14:05 +0100)]
Minor fix for getInstCons

10 years agoReenable regression. Add (for now, disabled) changes to datatypes theory combination...
ajreynol [Thu, 6 Nov 2014 10:41:35 +0000 (11:41 +0100)]
Reenable regression.  Add (for now, disabled) changes to datatypes theory combination.  Relax communication of dt facts.