Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2010-09-02 | * add TimerStat statistic type | Morgan Deters | |
* 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() | |||
2010-09-01 | "make check" now places binaries in the proper place before doing the ↵ | Morgan Deters | |
checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago | |||
2010-09-01 | reflect in build strings that -gmp is now the default and -cln is an option | Morgan Deters | |
2010-09-01 | added documentation, closes bug 97 | Morgan Deters | |
2010-08-24 | Making GMP default, CLN opt-in with --with-cln | Christopher L. Conway | |
2010-08-20 | updating the minisat restart parameters after running some experiments | Dejan Jovanović | |
2010-08-20 | turn off extra-checking (which does extra theory-rewriter checking); it was ↵ | Morgan Deters | |
enabled by mistake in the last commit | |||
2010-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters | |
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. | |||
2010-08-18 | more tests, configuration for UF | Morgan Deters | |
2010-08-17 | Merge from "cc" branch: | Morgan Deters | |
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. | |||
2010-08-17 | Add "no trash" CDMap elements, so that CDMap elements can themselves | Morgan Deters | |
be allocated in context memory. CDMap black-box test extended. | |||
2010-08-17 | Change TheoryEngine to use pointers to theories instead of | Morgan Deters | |
calling them directly. In tests this doesn't appear to lead to slowdown. | |||
2010-08-16 | add zlib checks to configure (new minisat requires it?) | Morgan Deters | |
2010-08-16 | Fixing failures in minisat | Dejan Jovanović | |
2010-08-15 | (no commit message) | Dejan Jovanović | |
2010-08-15 | (no commit message) | Dejan Jovanović | |
2010-08-13 | renaming minisat .C to .cc | Dejan Jovanović | |
2010-08-13 | Adding the changes to the original copy | Dejan Jovanović | |
2010-08-13 | Importing MiniSat2 070721 into trunk | Christopher L. Conway | |
2010-08-13 | Removing newer version of MiniSat for Dejan's preferred import | Christopher L. Conway | |
2010-08-13 | Importing MiniSat2 2.2.0 into trunk | Christopher L. Conway | |
2010-08-13 | Removing old version of MiniSat for proper vendor import | Christopher L. Conway | |
2010-07-29 | Adding configuration_private.h to allow inlining of configuration checks | Christopher L. Conway | |
2010-07-29 | fix TheoryEngineWhite, add documentation; related to bug #188 | Morgan Deters | |
2010-07-28 | Adding TypeCheckingException to throws clause in SMT parsers | Christopher L. Conway | |