Andrew Reynolds [Wed, 26 Sep 2012 21:44:22 +0000 (21:44 +0000)]
updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes
Morgan Deters [Wed, 26 Sep 2012 18:51:48 +0000 (18:51 +0000)]
Fix a handful of things for Mac, and Java bindings.
Also add a "mac-build" script that sets up prerequisites for Mac.
Morgan Deters [Wed, 26 Sep 2012 16:42:40 +0000 (16:42 +0000)]
bug #398 test (bug was resolved last night), and a script to download all bug attachments from bugzilla and put them in the tree
Morgan Deters [Wed, 26 Sep 2012 03:50:57 +0000 (03:50 +0000)]
Fix type checking for define-funs (resolves bug 398).
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Wed, 26 Sep 2012 03:07:01 +0000 (03:07 +0000)]
The Tuesday Afternoon Catch-All Commit (TACAC):
* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)
* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).
* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Tue, 25 Sep 2012 20:32:18 +0000 (20:32 +0000)]
fix
Morgan Deters [Tue, 25 Sep 2012 18:57:48 +0000 (18:57 +0000)]
fix some Mac issues
Morgan Deters [Tue, 25 Sep 2012 15:16:41 +0000 (15:16 +0000)]
some buggy examples for incrementality, and make bug326 run as part of make regress, because the bug was fixed.
Also make QuantifiersModule's destructor virtual (it has virtual members).
(this commit was certified error- and warning-free by the test-and-commit script.)
Dejan Jovanović [Mon, 24 Sep 2012 20:55:58 +0000 (20:55 +0000)]
some api changes
Morgan Deters [Mon, 24 Sep 2012 18:37:22 +0000 (18:37 +0000)]
Fix the memout issue seen in recent nightly regressions (was due to a
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Sat, 22 Sep 2012 21:10:51 +0000 (21:10 +0000)]
Separate public-facing and internal-facing interfaces to Statistics.
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
Dejan Jovanović [Sat, 22 Sep 2012 14:34:52 +0000 (14:34 +0000)]
another fix for the equality class iterator
Morgan Deters [Fri, 21 Sep 2012 21:09:18 +0000 (21:09 +0000)]
Fixes for datatype dumping and printing. Add a new test case for dumping.
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Fri, 21 Sep 2012 20:34:19 +0000 (20:34 +0000)]
SMT-LIBv2 compliance updates:
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default
Also:
* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Fri, 21 Sep 2012 10:24:08 +0000 (10:24 +0000)]
better verbosity support (so it's sensible when the library is used via the API)
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Thu, 20 Sep 2012 18:59:26 +0000 (18:59 +0000)]
map C++ exceptions to Java exceptions correctly when they are thrown, and give a build error for Java component if it is misconfigured
Morgan Deters [Thu, 20 Sep 2012 13:36:12 +0000 (13:36 +0000)]
some bugfixes that come as a result of debugging some CASCADE/C stuff..
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Wed, 19 Sep 2012 21:21:00 +0000 (21:21 +0000)]
General subscriber infrastructure for NodeManager, as discussed in the
meeting last week. The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.
The way to create a skolem is now:
nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")
The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name). Without a "$$", a "_$$"
is automatically appended to the given name.
The second argument is the type.
The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.
An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name). Look at the documentation for details on these.
In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment. This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.
Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit. Some remains to be cleaned up.
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Wed, 19 Sep 2012 21:11:41 +0000 (21:11 +0000)]
fix subtle bug in NodeValue::toStream()
Dejan Jovanović [Wed, 19 Sep 2012 20:06:27 +0000 (20:06 +0000)]
fix for bug 370.
some internal nodes in eq engine were treated as constants incorrectly
Dejan Jovanović [Wed, 19 Sep 2012 18:56:41 +0000 (18:56 +0000)]
Changing the equality engines's euivalence class iterator. Andy please check if this does what you want it to do.
Morgan Deters [Tue, 18 Sep 2012 14:50:45 +0000 (14:50 +0000)]
SMT-LIBv2 compliance regarding outputting "unknown".
Thanks to Peter Collingbourne for the report, and the patch!
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Mon, 17 Sep 2012 22:38:32 +0000 (22:38 +0000)]
speed up option-file generation on Mac OS by an order of magnitude
Morgan Deters [Mon, 17 Sep 2012 21:14:37 +0000 (21:14 +0000)]
more bindings fixes
Andrew Reynolds [Mon, 17 Sep 2012 16:39:48 +0000 (16:39 +0000)]
minor fix for models, added simple cliques option for uf strong solver
Morgan Deters [Sun, 16 Sep 2012 01:24:24 +0000 (01:24 +0000)]
enable bug regression for bug 382
(this commit was certified error- and warning-free by the test-and-commit script.)
Andrew Reynolds [Sun, 16 Sep 2012 00:49:04 +0000 (00:49 +0000)]
store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.
Morgan Deters [Sat, 15 Sep 2012 22:41:03 +0000 (22:41 +0000)]
minor interface improvements, compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Sat, 15 Sep 2012 22:32:34 +0000 (22:32 +0000)]
another bindings fix (should fix debian build)
Morgan Deters [Sat, 15 Sep 2012 22:27:23 +0000 (22:27 +0000)]
bug testcase for model generation
Morgan Deters [Fri, 14 Sep 2012 19:25:58 +0000 (19:25 +0000)]
a fix for the java bindings for wei
Morgan Deters [Fri, 14 Sep 2012 17:16:26 +0000 (17:16 +0000)]
Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).
Also fix an issue where --check-model didn't take user define-funs into account.
Also make preprocessing a bit more chatty (with -v -v).
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Fri, 14 Sep 2012 15:13:37 +0000 (15:13 +0000)]
Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.
Andrew Reynolds [Thu, 13 Sep 2012 20:39:13 +0000 (20:39 +0000)]
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
Morgan Deters [Wed, 12 Sep 2012 20:31:59 +0000 (20:31 +0000)]
Adding model assertions after SAT responses.
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.
By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems:
make regress CVC4_REGRESSION_ARGS=--check-models
To see it work, use -v in addition to --check-models.
There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.
--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).
Also:
* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
Andrew Reynolds [Tue, 11 Sep 2012 23:44:49 +0000 (23:44 +0000)]
added getCardinality to model
Tim King [Tue, 11 Sep 2012 00:20:51 +0000 (00:20 +0000)]
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.
Andrew Reynolds [Mon, 10 Sep 2012 22:29:17 +0000 (22:29 +0000)]
modified getValue to return Expr instead of Node
Tim King [Mon, 10 Sep 2012 20:38:35 +0000 (20:38 +0000)]
Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.)
Morgan Deters [Mon, 10 Sep 2012 14:26:48 +0000 (14:26 +0000)]
list portfolio_util.h in Makefile, so it gets distributed (fixes debian build)
Morgan Deters [Sat, 8 Sep 2012 23:00:23 +0000 (23:00 +0000)]
Add [*] footnotes to --help output indicating for many options --FOO that there are --no-FOO variants.
Morgan Deters [Sat, 8 Sep 2012 22:31:44 +0000 (22:31 +0000)]
Some minor changes after reviewing the portfolio "unified driver" commit.
(this commit was certified error- and warning-free by the test-and-commit script.)
Kshitij Bansal [Sat, 8 Sep 2012 14:25:25 +0000 (14:25 +0000)]
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Morgan Deters [Thu, 6 Sep 2012 22:15:56 +0000 (22:15 +0000)]
allow SmtEngine::setOption() for trace and debug tags
Morgan Deters [Thu, 6 Sep 2012 20:05:20 +0000 (20:05 +0000)]
fixes to the compatibility layer; this fixes the broken system test
Morgan Deters [Thu, 6 Sep 2012 02:38:39 +0000 (02:38 +0000)]
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only used by the compatibility layer.
Make SmtEngine::internalPop() delay popping. This fixes a bug in model generation.
Morgan Deters [Thu, 6 Sep 2012 00:53:18 +0000 (00:53 +0000)]
add --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)
Morgan Deters [Wed, 5 Sep 2012 20:51:34 +0000 (20:51 +0000)]
add a THANKS file for listing external source code contributors
Morgan Deters [Tue, 4 Sep 2012 22:22:41 +0000 (22:22 +0000)]
Accepted some patches from the Multicore Programming Group at Imperial College London (via Peter Collingbourne):
cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)
These patches will help the group build Boogie support for CVC4.
(this commit was certified error- and warning-free by the test-and-commit script.)
Andrew Reynolds [Mon, 3 Sep 2012 17:52:07 +0000 (17:52 +0000)]
minor cleanup leftover from fmf-devel
Andrew Reynolds [Fri, 31 Aug 2012 16:48:20 +0000 (16:48 +0000)]
merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
Morgan Deters [Thu, 30 Aug 2012 21:13:44 +0000 (21:13 +0000)]
set the default expression-printing depth to "unlimited"
Morgan Deters [Wed, 29 Aug 2012 20:36:35 +0000 (20:36 +0000)]
* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
Morgan Deters [Wed, 29 Aug 2012 11:50:15 +0000 (11:50 +0000)]
To the build system:
* Fix "make distclean." This should fix the "local regressions fail"
that caused documentation, debian, and "distcheck" nightly build targets
to fail.
* "make clean" now removes some options stuff that previously required a
"make distclean."
* Cosmetic and portability adjustments.
Morgan Deters [Tue, 28 Aug 2012 18:38:19 +0000 (18:38 +0000)]
test summaries for automake 1.12 test harness
Morgan Deters [Tue, 28 Aug 2012 17:14:59 +0000 (17:14 +0000)]
fix a bug in CLN rational printing where the base was ignored (was causing the new CVC3-compatibility-API system test to fail)
Morgan Deters [Tue, 28 Aug 2012 15:26:46 +0000 (15:26 +0000)]
fix regression tests for automake 1.11 and automake 1.12---both versions should work now
Morgan Deters [Tue, 28 Aug 2012 01:10:16 +0000 (01:10 +0000)]
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Morgan Deters [Tue, 28 Aug 2012 00:44:55 +0000 (00:44 +0000)]
fixes for Mac and automake 1.12 detection
Morgan Deters [Mon, 27 Aug 2012 20:37:17 +0000 (20:37 +0000)]
fix a destruction-order issue that was (1) causing valgrind to complain loudly about invalid reads and writes, and (2) apparently causing problems deleting the decision engine (which is now being properly deleted)
(this commit was certified error- and warning-free by the test-and-commit script.)
Morgan Deters [Mon, 27 Aug 2012 19:27:28 +0000 (19:27 +0000)]
* Reversing commit r4258 (which disabled failing regressions). Fixed the problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381.
* Added LAMBDA kind and type rule, and Node::isClosure().
(this commit was certified error- and warning-free by the test-and-commit script.)
Kshitij Bansal [Sun, 26 Aug 2012 19:53:14 +0000 (19:53 +0000)]
minor, lying around in a wd (related to investigating bug 374)
Kshitij Bansal [Sun, 26 Aug 2012 19:39:03 +0000 (19:39 +0000)]
disabling failing regressions
Clark Barrett [Sun, 26 Aug 2012 17:56:55 +0000 (17:56 +0000)]
Array constants finished and working. Unit tests for array constants.
Morgan Deters [Sat, 25 Aug 2012 21:27:17 +0000 (21:27 +0000)]
fix unit tests
Morgan Deters [Fri, 24 Aug 2012 23:23:34 +0000 (23:23 +0000)]
* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
Morgan Deters [Fri, 24 Aug 2012 23:20:22 +0000 (23:20 +0000)]
disallow assertions to inactive theories.
this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results.
Morgan Deters [Fri, 24 Aug 2012 21:40:46 +0000 (21:40 +0000)]
fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theories; resolves bug 380
Morgan Deters [Fri, 24 Aug 2012 01:03:20 +0000 (01:03 +0000)]
fix warning in arrays rewriter
Morgan Deters [Fri, 24 Aug 2012 00:29:52 +0000 (00:29 +0000)]
fix get-value output in a couple ways; this fixes bug #378
Morgan Deters [Thu, 23 Aug 2012 23:33:52 +0000 (23:33 +0000)]
attribute stuff for Clark's array constants
Clark Barrett [Thu, 23 Aug 2012 18:53:26 +0000 (18:53 +0000)]
Array constant coding done except for the attributes needed
Morgan Deters [Wed, 22 Aug 2012 22:31:59 +0000 (22:31 +0000)]
Cap finite cardinalities at 2^64, as discussed in the meeting last week.
Replace all cardinality comparison functions <=, ==, !=, >=, <, >, with a single compare() function that can return UNKNOWN in the case of unknown (or large-finite and thus not *precisely* known) cardinalities.
Morgan Deters [Wed, 22 Aug 2012 20:19:27 +0000 (20:19 +0000)]
fix some build dependencies in options-building; should fix a strange bug Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be
Clark Barrett [Wed, 22 Aug 2012 18:04:10 +0000 (18:04 +0000)]
More progress on array constants.
Here's a fun way to give yourself a week-long headache: try to figure out how
to write efficient code to normalize array constants.
It's mostly there now - just need to figure out how to use type enumerators and
update once the new cardinality stuff is in place.
Morgan Deters [Tue, 21 Aug 2012 22:13:12 +0000 (22:13 +0000)]
add some incremental in-tree regressions
François Bobot [Tue, 21 Aug 2012 20:53:49 +0000 (20:53 +0000)]
rewriterules: fix a correction bug with --simplification=batch
Rewriterules used ppAssert to obtain early the rewriterules in order
to use them in ppRewrite. But all the simplifications (ex. f x = b :
[f x/b]) are not done at that point. Since --simplification=batch
remove the equality (unlike =incremental), for
reachability_bbttf_eT_arrays.smt2 the answer was sat instead of
unsat (thx Andy).
Partial fix: don't take the rewriterules during ppAssert. That changes
nothing since early rewrite was already disabled. But the complete
fix (when early rewrite will be enabled again) will need to take the
rewriterules more than once.
Morgan Deters [Mon, 20 Aug 2012 22:01:14 +0000 (22:01 +0000)]
remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplicate of TheoryEngine::theoryOf(TheoryId)
Morgan Deters [Mon, 20 Aug 2012 21:12:00 +0000 (21:12 +0000)]
removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 differ in the answer), so it doesn't really test anything
Morgan Deters [Mon, 20 Aug 2012 19:55:33 +0000 (19:55 +0000)]
minor cleanup
Morgan Deters [Mon, 20 Aug 2012 19:37:30 +0000 (19:37 +0000)]
fixes for java bindings
Clark Barrett [Sun, 19 Aug 2012 02:08:15 +0000 (02:08 +0000)]
1. Fix for inst_match.cpp to allow compilation on fedora
2. Initial implementation of computeIsConst for arrays - still needs
additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL
Morgan Deters [Thu, 16 Aug 2012 22:41:07 +0000 (22:41 +0000)]
The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic(). This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses. setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.
This means that the CVC language can now take advantage of statistics.
Also added the ability to set the logic from CVC presentation language via (e.g.)
OPTION "logic" "QF_UFLIA";
Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality. Kshitij may have a fix (I warned him about this commit).
Kshitij Bansal [Thu, 16 Aug 2012 21:40:41 +0000 (21:40 +0000)]
bug 374 (was found through fuzzing 2012-07-18)
"Possible soundness problem somewhere in the solver
(assertion failure in DE)"
Morgan Deters [Thu, 16 Aug 2012 21:30:41 +0000 (21:30 +0000)]
Replace propagateAsDecision() with Theory::getNextDecisionRequest():
* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups
Morgan Deters [Thu, 16 Aug 2012 19:58:32 +0000 (19:58 +0000)]
ArrayStoreAll should (for now) only allow constant expressions, as it is itself a CONSTANT.
Morgan Deters [Thu, 16 Aug 2012 01:58:41 +0000 (01:58 +0000)]
fix exceptions and mkConst() in java binding
Morgan Deters [Thu, 16 Aug 2012 01:29:19 +0000 (01:29 +0000)]
some fixes for language bindings
Morgan Deters [Tue, 14 Aug 2012 20:08:29 +0000 (20:08 +0000)]
Fixes to integer wrapper classes:
* more uniform interface between the CLN and GMP wrappers
* support base inference (base == 0) on parsing strings with the CLN wrapper; this was a difference from the GMP wrapper (resolves bug #372)
Tim King [Tue, 14 Aug 2012 18:01:02 +0000 (18:01 +0000)]
Implements TheoryArith::collectModelInfo(). The current implementation is quite basic. This may need to be revisited.
Tim King [Tue, 14 Aug 2012 17:55:33 +0000 (17:55 +0000)]
Adds substituteDelta() to DeltaRational which given a value for delta returns the corresponding rational value.
Tim King [Tue, 14 Aug 2012 17:52:54 +0000 (17:52 +0000)]
Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.
Tim King [Tue, 14 Aug 2012 17:50:57 +0000 (17:50 +0000)]
Switched a number of EqClassIterator operations to const as well as the internal EqualityEngine pointer.
Morgan Deters [Mon, 13 Aug 2012 20:56:15 +0000 (20:56 +0000)]
fix integer parsing error.. thanks dejan for the report. this indicates that we have a problem with our Integer class though; it appears to behave differently for GMP and CLN
Morgan Deters [Mon, 13 Aug 2012 20:47:59 +0000 (20:47 +0000)]
Make a few functions in TheoryEngine (like theoryOf()) const.
Morgan Deters [Mon, 13 Aug 2012 19:46:27 +0000 (19:46 +0000)]
Minor cleanup. No performance difference expected.
Morgan Deters [Thu, 9 Aug 2012 13:48:37 +0000 (13:48 +0000)]
minor isConst()-related fixes to printing; also add some debugging stuff to see how isConst() operates: use -d isConst
Morgan Deters [Wed, 8 Aug 2012 22:20:39 +0000 (22:20 +0000)]
Fix --no-checking option.
Morgan Deters [Wed, 8 Aug 2012 05:13:53 +0000 (05:13 +0000)]
Public interface review items:
* don't document internal-only stuff (like DefaultCleanup for CDLists)
* NoSuchFunctionException -> TypeCheckingException
Dejan Jovanović [Tue, 7 Aug 2012 22:47:22 +0000 (22:47 +0000)]
small fixes