Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2010-09-21 | Moving automatic type check to NodeBuilder (Fixes: #199) | Christopher L. Conway | |
2010-09-20 | hooking up the bitvector tests | Dejan Jovanović | |
2010-09-20 | bitvector rewriting for the core theory and testcases | Dejan Jovanović | |
2010-09-16 | Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. ↵ | Tim King | |
test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default. Tiny documentation fix for the arithmetic normal form. | |||
2010-09-14 | * added test/regress/regress0/arith for easy arithmetic regress tests. | Tim King | |
2010-09-14 | ensure uf/congruence closure debugging stuff isn't called in production builds | Morgan Deters | |
2010-09-13 | make Node iterators more STL-friendly, resolves bug #196 | Morgan Deters | |
2010-09-13 | build system consistency in target names for unit test targets | Morgan Deters | |
2010-09-13 | statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given | Morgan Deters | |
2010-09-13 | link TAGS file into builds/ directory, when built. Resolves bug #195 | Morgan Deters | |
2010-09-13 | * New normal form for arithmetic is in place. | Tim King | |
* src/theory/arith/normal_form.{h,cpp} contains the description for the new normal form as well as utilities for dealing with the normal form. * src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter. The new rewriter implements preRewrite() and postRewrite() for arithmetic. * src/theory/arith/arith_rewriter.{h,cpp} have been removed. * TheoryArith::rewrite() has been removed. * Arithmetic with the new normal form outperforms the trunk where the branch occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable difference.) Some important optimizations are stilling pending to the code for handling the new normal form. (Bug 196.) | |||
2010-09-02 | "Leftist NodeBuilders" are now supported. | Morgan Deters | |
That is, "nb << a << b << c << OR << d << AND" turns into (AND (OR a b c) d) The rule is: pushing a kind onto a NodeBuilder with a nonzero number of child Nodes in it, the action "collapses" it. If a kind is already associated to the NodeBuilder, it is an error. Thus: NodeBuilder<> nb(AND); nb << AND; and NodeBuilder<> nb; nb << AND << OR; are both errors (if assertions are on). In reality, though, the implementation is trickier, as the collapsing is done lazily on the following push. This complicates things a bit, but by placing an Assert(false), I found that we aren't depending on the old behavior (at least for any unit tests or regressions in the source tree). The Assert(false) is now removed and leftist NodeBuilders are in business. Fixes bug 101. | |||
2010-09-02 | recategorize eq_diamond14 as a regress2 test (instead of regress0) | Morgan Deters | |
2010-09-02 | fix an error in TimerStat | Morgan Deters | |
2010-09-02 | neglected build system update from r848 (last commit) | Morgan Deters | |