Age | Commit message (Collapse) | Author | |
---|---|---|---|
2011-01-05 | fix for build errors | Dejan Jovanović | |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial ↵ | Dejan Jovanović | |
and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later. | |||
2010-12-16 | minor fixes for correct doxygen output | Morgan Deters | |
2010-12-14 | make some CC module methods private that should not have been public | Morgan Deters | |
2010-12-14 | congruence closure module now supports things other than APPLY_UF; ported ↵ | Morgan Deters | |
from "arrays" branch to trunk | |||
2010-12-14 | permit PARAMETERIZED operators to be zero-ary | Morgan Deters | |
2010-12-14 | fix to static learning application in UF, resolves bug# 239 | Morgan Deters | |
2010-11-24 | Changin the get() semantics to a CDQeue-sque semantics. | Dejan Jovanović | |
2010-11-19 | Merge from ufprop branch, including: | Morgan Deters | |
* Theory::staticLearning() for statically adding new T-stuff before normal preprocessing. UF's staticLearning() does transitivity of equality/iff, solving the diamonds. * more aggressive T-propagation for UF * new KEEP_STATISTIC macro to hide Theories from having to register/deregister statistics (and also has the advantage of keeping the statistic type, field name, and the 'tag' used to output the statistic in the same place---instead of scattered in the theory definition and constructor initializer list. See documentation for KEEP_STATISTIC in src/util/stats.h for more of an explanation). * more statistics for UF * restart notifications from SAT (through TheoryEngine) via Theory::notifyRestart() * StackingMap and UnionFind unit tests * build fixes/adjustments * code cleanup; minor other improvements | |||
2010-11-19 | add statistics support information to --show-config | Morgan Deters | |
2010-11-17 | add some stats to UF/CC | Morgan Deters | |
2010-11-17 | The "UF engineering issues" release, after much profiling. | Morgan Deters | |
* swap in backtracking data structures (that use and maintain their own undo stack) in some places instead of the usual Context-aware paradigm (MUCH faster). * cosmetic changes to UF, CC modules. | |||
2010-11-16 | Added Theory::presolve(). | Tim King | |
2010-11-16 | SmtEngine now fails with a ModalException if --incremental is not enabled | Morgan Deters | |
but a push/pop or multiple query is attempted (previously it could give incorrect answers) Also, fix some multi-query and push-pop tests that had wrong answers, and support a new "% COMMAND-LINE: " gesture in regression tests so that a test can pass additional, specific command line flags it wants to run with (here, --incremental). Also fix mkbuilddir script for when it's called from contrib/switch-config. | |||
2010-11-16 | fix function signatures | Morgan Deters | |
2010-11-15 | cleanup from today's commits: delegate as-yet-unimplemented prettyprinters ↵ | Morgan Deters | |
in a better way; fix arith Makefile | |||
2010-11-15 | Changes to Solver and PropEngine to support lemmasOnDemand during solve but ↵ | Tim King | |
not yet in d_checkSat. | |||
2010-11-15 | Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer | Morgan Deters | |
implemented. This new infrastructure removes support for pretty-printing (even in the AST language) an Expr with reference count 0. Previously, this was supported in a few places internally to the expr package, for example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you must extract the Node before printing it.) | |||
2010-11-15 | This commit merges the arith-prop-opt branch into the main trunk. This was ↵ | Tim King | |
done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out. | |||
2010-11-15 | minor tweaks to last commit, testing infrastructure | Morgan Deters | |
2010-11-15 | fix some things with the build system (make dist, make install, make check) | Morgan Deters | |
2010-11-12 | Some bug fixes in the SAT for lemmas, and an experiment with a more complete ↵ | Dejan Jovanović | |
(wr propagation) splitter in arithmetic. | |||
2010-11-09 | Lemmas on demand work, push-pop, some cleanup. | Dejan Jovanović | |
2010-11-08 | command-line flag to disable theory registration, also SMT-LIBv2 compliance ↵ | Morgan Deters | |
(per SMT-LIB mailing list this afternoon) | |||
2010-11-08 | cleanup, documentation, SMT-LIBv2 compliance | Morgan Deters | |
2010-11-08 | fix out-of-date version/copyright for minisats | Morgan Deters | |
2010-11-05 | Moving Options fiddling to options.h | Christopher L. Conway | |
2010-11-04 | competition mode implies --no-checking | Morgan Deters | |
2010-11-04 | This commit adds the ejected and un-ejected statistics. | Tim King | |
2010-11-03 | Adds size() to RowVector. | Tim King | |
2010-11-03 | Adds statistics for the number of Uservariables and Slack variables used by ↵ | Tim King | |
arithmetic. | |||
2010-11-03 | Adds AverageStat to stats.h. | Tim King | |
2010-10-31 | small fix to debug segfaults | Morgan Deters | |
2010-10-31 | enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some ↵ | Morgan Deters | |
documentation, and make it possible to "make doc" on a clean source tree (post-configure) | |||
2010-10-31 | maximize stack limit, handle SEGV signals on an alternate signal stack, and ↵ | Morgan Deters | |
try to diagnose stack overflow | |||
2010-10-30 | Adds a hueristic from Alberto's thesis. For a fixed window the row count is ↵ | Tim King | |
used to select which non-basic variable is a row in made basic. | |||
2010-10-29 | Fix for a problem caused by using a != instead of == in ↵ | Tim King | |
generateConflictBelow(). Resolves a bug introduced in -r1063. | |||
2010-10-29 | minor fixes as a result of review of Chris's getType() rewrite; also fix ↵ | Morgan Deters | |
some macros to make various GCC versions happy | |||
2010-10-29 | Fixes RowVector::has(). | Tim King | |
2010-10-29 | Factors out the QF_LRA decision procedure from TheoryArith and puts this ↵ | Tim King | |
into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3). | |||
2010-10-28 | The Row implementation has no been replaced by RowVector and ↵ | Tim King | |
ReducedRowVector. A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable. The Tableau is now a collection of ReduceRowVector's. A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator. | |||
2010-10-28 | Changing NodeBuilder::debugCheckType() to maybeCheckType() | Christopher L. Conway | |
Changing NodeManager/ExprManager constructors to take Options | |||
2010-10-28 | Disabling bottom-up algorithm in NodeManager::getType() when type checking | Christopher L. Conway | |
is not requested or eager type checking is enabled | |||
2010-10-27 | Small change to documentation in NodeManager::getType | Christopher L. Conway | |
2010-10-27 | Slightly more efficient version of getType | Christopher L. Conway | |
2010-10-27 | Modifying getType to use a non-recursive algorithm (Fixes: #228) | Christopher L. Conway | |
2010-10-27 | "make dist" fixes; a distribution tarball can now build and pass tests. ↵ | Morgan Deters | |
"make distcheck" fails only because one of the "clean" targets needs work in test/unit | |||
2010-10-26 | GetValueCommand now gives a TUPLE as output, with the first operand the ↵ | Morgan Deters | |
input expression and the second the value (resolves bug 227) | |||
2010-10-26 | Cleaning up some header files | Christopher L. Conway | |
2010-10-25 | for static linking of driver binary, list libmain.a first (fixes link errors ↵ | Morgan Deters | |
in last night's regressions) |