| Age | Commit message (Collapse) | Author |
|---|
|
assertion-failure string construction) and addition of an assert_white unit test check for the issue
|
|
CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration.
|
|
|
|
|
|
|
|
(now that they are allowed for the datatypes theory, as in (APPLY_CONSTRUCTOR nil) or (APPLY_CONSTRUCTOR zero)). It does this by treating such terms with zero children as non-candidates for congruence, even though they have the congruence kind APPLY_CONSTRUCTOR.
|
|
(I think) that Tim found with TimerStat involving wild, sometimes negative, timer statistic values. (It was due to improper initialization.)
|
|
- Adds 3 choices of heuristic variable orders to use in ArithPriorityQueue.
- Adds the pivot-rule command line option.
|
|
caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.
|
|
|
|
|
|
from "arrays" branch to trunk
|
|
* 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
|
|
|
|
|
|
* swap in backtracking data structures (that use and maintain their own
undo stack) in some places instead of the usual Context-aware
paradigm (MUCH faster).
* cosmetic changes to UF, CC modules.
|
|
implemented. This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0. Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)
|
|
|
|
(per SMT-LIB mailing list this afternoon)
|
|
|
|
|
|
|
|
documentation, and make it possible to "make doc" on a clean source tree (post-configure)
|
|
private copy constructors and assignment, for instance) that generates better, compile-time error messages if the function is used (before, you'd have to wait until link time); also some minor cleanup
|
|
|
|
|
|
util/options.h,cpp
|
|
bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere)
|
|
* Add ContextMemoryAllocator<T> allocator type, conforming to
STL allocator requirements.
* Extend the CDList<> template to take an allocator (defaults
to std::allocator<T>).
* Add a specialized version of the CDList<> template (in
src/context/cdlist_context_memory.h) that allocates a list
in segments, in context memory.
* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
and cdset_forward.h. Use these in public headers, and other
places where you don't need the full header (just the
forward-declaration). These types justify their own header
(instead of just forward-declaring yourself), because they
are complex templated types, with default template parameters,
specializations, etc.
* theory_engine.h no longer depends on individual theory headers.
(Instead it forward-declares Theory implementations.) This is
especially important now that theory .cpp files depend on
TheoryEngine (to implement Theory::getValue()). Previously,
any modification to any theory header file required *all*
theories, and the engine, to be completely rebuilt.
* Support memory cleanup for nontrivial CONSTANT kinds. This
resolves an issue with arithmetic where memory leaked for
each distinct Rational or Integer that was wrapped in a Node.
|
|
|
|
supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
|
|
define-fun; several set-info, set-option, get-option, get-info improvementss
|
|
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work). Closes bug #213.
|
|
(resolves bug #212)
* also closed some other type checking loopholes in SmtEngine
* small fixes to define-sort (resolves bug #214)
* infrastructural support for printing expressions in languages
other than the internal representation language using an IO
manipulator, e.g.:
cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;
main() sets the output language for all streams to correspond to
the input language
* support delaying type checking in debug builds, so that one can debug
the type checker itself (before it was difficult, because debug builds did
all the type checking on Node creation!): new command-line flag
--no-early-type-checking (only makes sense for debug builds)
* disallowed copy-construction of ExprManager and NodeManager, and made other
constructors explicit; previously it was easy to unintentionally create
duplicate managers, with really weird results (i.e., disappearing
attributes!)
|
|
resolve) bug 212
|
|
preprocessing time
|
|
working (just need to decide where to expand)
|
|
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
|
|
regression script
|
|
coding standards
|
|
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)
|
|
doesn't exist, and clean up a few things in NodeManager
|
|
also configure script auto-detection of __thread support and syntax
|
|
array that dynamically can increase in size. This has functionality similar to vector<T>. The main difference is that it can be constructed in an ill-formed manner. This means that it can generalize CDList<T>.
- CDVector<T> has been added. This is intended to allow for context-dependent destructive updates, while the vector size increases are permanent. Behaviorally, this is most similar to vector< CDO<T> >. The differences between the two are: only one ContextObj is registered to the Context, backtracks are done in a lazy fashion, CDVector::push_back(val) sets the value of back() at context level 0 to val where vector<CDO<T>>::push_back(val) sets back() at the current context level to val and back() at context level 0 to the default constructor T().
|
|
|
|
|
|
|
|
* 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()
|
