Age | Commit message (Collapse) | Author | |
---|---|---|---|
2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now ↵ | Morgan Deters | |
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 | |||
2010-10-09 | reverting some changes to parser from last commit | Morgan Deters | |
2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ↵ | Morgan Deters | |
define-fun; several set-info, set-option, get-option, get-info improvementss | |||
2010-10-09 | fix to unit tests | Morgan Deters | |
2010-10-09 | bug fixes to model gen | Morgan Deters | |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters | |
(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. | |||
2010-10-08 | * (define-fun...) now has proper type checking in non-debug builds | Morgan Deters | |
(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!) | |||
2010-10-08 | support (set-info) on status, source, category, difficulty, smt-lib-version, ↵ | Morgan Deters | |
and notes; reduces extraneous "unsupported" output | |||
2010-10-07 | oops, reverting a change to a regression test that had intentionally caused ↵ | Morgan Deters | |
a typechecking violation | |||
2010-10-07 | type checking for define-fun in production builds; related to (and might ↵ | Morgan Deters | |
resolve) bug 212 | |||
2010-10-07 | NodeSelfIterator implementation and unit test (resolves bug #204); also fix ↵ | Morgan Deters | |
ParserBlack unit test initialization | |||
2010-10-07 | Small tableau optimization. | Tim King | |
2010-10-07 | SMT-LIBv2 (define-fun...) command now functional; does eager expansion at ↵ | Morgan Deters | |
preprocessing time | |||
2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ↵ | Morgan Deters | |
working (just need to decide where to expand) | |||
2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, ↵ | Morgan Deters | |
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... | |||
2010-10-04 | fix gdb issues (at least for static builds); resolves bug 194 | Morgan Deters | |
2010-10-04 | fix regular expressions in build system | Morgan Deters | |
2010-10-04 | fixing CLN builds, which had broken the build tonight; will re-run ↵ | Morgan Deters | |
regression script | |||
2010-10-04 | re-add a dependency to fix compile warnings | Morgan Deters | |
2010-10-04 | remove/shuffle some #include dependencies; fix some documentation; apply ↵ | Morgan Deters | |
coding standards | |||
2010-10-04 | Fix to bug 211. ArithVar is now typedefed to uint32_t. | Tim King | |
2010-10-03 | file header documentation regenerated with contributors names; no code ↵ | Morgan Deters | |
modified in this commit | |||
2010-10-02 | revert a workaround fix to CDMap that was committed as part of the ↵ | Morgan Deters | |
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 | |||
2010-10-02 | dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout... | Morgan Deters | |
2010-10-02 | branches/arith-indexed-variables merged into the main trunk. | Tim King | |
2010-10-01 | re-add no-deprecated to C sources; update some file-level documentation; ↵ | Morgan Deters | |
first look at cdvector for code review | |||
2010-10-01 | last update broke the parser inadvertently, fixing... | Morgan Deters | |
2010-10-01 | replacement implementation for clock_gettime() on mac os x, build ↵ | Morgan Deters | |
portability (resolving mac os x issues), code cleanup, fix compiler warnings | |||
2010-09-30 | fixed a number of problems with mac os x builds. build now works on mac os ↵ | Morgan Deters | |
x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208) | |||
2010-09-28 | fix predicate bug in UF; code cleanup in theory.cpp | Morgan Deters | |
2010-09-28 | node iterator work | Morgan Deters | |
2010-09-28 | fix pre-registration of operator, previously committed; clean up theory ↵ | Morgan Deters | |
engine code and unit test | |||
2010-09-28 | fix unit test for kinded iterators in Node/TNode | Morgan Deters | |
2010-09-28 | fix TLS support for platforms (e.g. Mac OS X) where __thread storage class ↵ | Morgan Deters | |
doesn't exist, and clean up a few things in NodeManager | |||
2010-09-28 | comment fix as per this morning's meeting; also, don't theory-rewrite ↵ | Morgan Deters | |
operators (resolves bug #198) | |||
2010-09-27 | add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵ | ACSYS | |
also configure script auto-detection of __thread support and syntax | |||
2010-09-27 | - This update adds DynamicArray<T>. This is a bare bones heap allocated ↵ | Tim King | |
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(). | |||
2010-09-24 | equality triggers for the equality engine | Dejan Jovanović | |
fixed order of destruction in smt_engine | |||
2010-09-24 | roll back an unintended change with r900 | Morgan Deters | |
2010-09-24 | Fix build system for Mac OS X builds (resolves bug #203) | Morgan Deters | |
2010-09-24 | basic union find for bitvectors | Dejan Jovanović | |
2010-09-22 | Fixing NodeBuilderBlack | Christopher L. Conway | |
2010-09-21 | Rm'ing automatic type check in NodeBuilder for vars/constants | Christopher L. Conway | |
2010-09-21 | remove assertion in TNode destructor and ensure all TNode methods check rc > ↵ | Morgan Deters | |
0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction | |||
2010-09-21 | fix statistics-registry-related memory leaks | Morgan Deters | |
2010-09-21 | part of review (bug #197): coding conventions, file-level documentation, ↵ | Morgan Deters | |
re-ran update-copyright.pl, etc. | |||
2010-09-21 | svn:ignore properties for new bv stuff | Morgan Deters | |
2010-09-21 | some code cleanup, documentation, review of "kinded-iterator" code, and ↵ | Morgan Deters | |
addition of a unit test | |||
2010-09-21 | iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wants | Dejan Jovanović | |
2010-09-21 | Rm'ing Makefile.in's | Christopher L. Conway | |