| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
addition of a unit test
|
|
|
|
|
|
|
|
test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default. Tiny documentation fix for the arithmetic normal form.
|
|
|
|
|
|
|
|
* 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.)
|
|
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.
|
|
|
|
* 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()
|
|
|
|
|
|
Enabled new UF theory by default.
Added some UF regressions.
Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing. (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)
Added pre-rewriting to TheoryBool which rewrites:
* (IFF true x) => x
* (IFF false x) => (NOT x)
* (IFF x true) => x
* (IFF x false) => (NOT x)
* (IFF x x) => true
* (IFF x (NOT x)) => false
* (IFF (NOT x) x) => false
* (ITE true x y) => x
* (ITE false x y) => y
* (ITE cond x x) => x
Added post-rewriting that does all of the above, plus normalize IFF and ITE:
* (IFF x y) => (IFF y x), if y < x
* (ITE (NOT cond) x y) => (ITE cond y x)
(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)
A little more debugging output from CNF stream, context pushes/pops,
ITE removal.
Some more documentation.
Fixed some typos.
|
|
|
|
CongruenceClosure implementation; CongruenceClosure white-box test.
New UF theory implementation based on new CC module. This one
supports predicates. The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").
Added type infrastructure for TUPLE.
Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).
Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)
Other minor changes.
|
|
be allocated in context memory. CDMap black-box test extended.
|
|
calling them directly. In tests this doesn't appear to
lead to slowdown.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
