| Age | Commit message (Collapse) | Author |
|---|
|
* 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!)
|
|
and notes; reduces extraneous "unsupported" output
|
|
a typechecking violation
|
|
resolve) bug 212
|
|
ParserBlack unit test initialization
|
|
|
|
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
|
|
arith-indexed-vars merge, and fix the root cause (maybe?) in attribute.cpp: previously, items from the cdnodes attribute table weren't properly being "obliterated" from the table due to a typo
|
|
|
|
|
|
first look at cdvector for code review
|
|
|
|
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)
|
|
|
|
|
|
engine code and unit test
|
|
|
|
doesn't exist, and clean up a few things in NodeManager
|
|
operators (resolves bug #198)
|
|
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().
|
|
fixed order of destruction in smt_engine
|
|
|
|
|
|
|
|
|
|
|
|
0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction
|
|
|
|
re-ran update-copyright.pl, etc.
|
|
|
