| Age | Commit message (Collapse) | Author |
|---|
|
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.)
|
|
1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)
The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:
* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***
Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).
Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).
Benefits of the new options system include:
1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose
I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
|
|
Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine. Otherwise, theories register the
same statistic twice. This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed. Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
|
|
|
|
* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.
Also:
Stop #defining NULL ((void*) 0). This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea. In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type. We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.
New exception-free Command architecture. Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error. This is much more consistent now. Each Command invocation
results in a CommandStatus. The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.) All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.
Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess. In the future we might put other
options into a compliance mode, or we might choose to make it the
default.
|
|
|
|
|
|
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
|
|
|
|
|
|
* Makes Options an "omnipresent thread-local global" (like the notion
of the "current NodeManager" was already). Options::current() accesses
this structure.
* Removes Options from constructors and data structures everywhere
(this cleans up a lot of things).
* No longer uses StatisticsRegistry statically. An instance of the
registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
registry; this is needed by main() to reach in and get the registry,
for flushing statistics at the end.
|
|
|
|
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).
Other changes include:
* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
text to make 'clang --analyze' happy.
|
|
CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration.
|
|
|
|
(I think) that Tim found with TimerStat involving wild, sometimes negative, timer statistic values. (It was due to improper initialization.)
|
|
* Theory::staticLearning() for statically adding new T-stuff before
normal preprocessing. UF's staticLearning() does transitivity of
equality/iff, solving the diamonds.
* more aggressive T-propagation for UF
* new KEEP_STATISTIC macro to hide Theories from having to
register/deregister statistics (and also has the advantage of
keeping the statistic type, field name, and the 'tag' used to output
the statistic in the same place---instead of scattered in the theory
definition and constructor initializer list. See documentation for
KEEP_STATISTIC in src/util/stats.h for more of an explanation).
* more statistics for UF
* restart notifications from SAT (through TheoryEngine) via
Theory::notifyRestart()
* StackingMap and UnionFind unit tests
* build fixes/adjustments
* code cleanup; minor other improvements
|
|
|
|
|
|
define-fun; several set-info, set-option, get-option, get-info improvementss
|
|
modified in this commit
|
|
portability (resolving mac os x issues), code cleanup, fix compiler warnings
|
|
x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)
|
|
|
|
* add Stats black-box unit test
* new make target: "make units" now runs unit tests only
* revised make target: "make regress" now runs regressions only
* configure.ac: pull in librt for clock_gettime()
|
|
|
|
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
|
|
again.
|
|
documentation.
|
|
this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
|
