summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2011-01-05fix for build errorsDejan Jovanović
2011-01-05Commit 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-16minor fixes for correct doxygen outputMorgan Deters
2010-12-14make some CC module methods private that should not have been publicMorgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported ↵Morgan Deters
from "arrays" branch to trunk
2010-12-14permit PARAMETERIZED operators to be zero-aryMorgan Deters
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan Deters
2010-11-24Changin the get() semantics to a CDQeue-sque semantics. Dejan Jovanović
2010-11-19Merge 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-19add statistics support information to --show-configMorgan Deters
2010-11-17add some stats to UF/CCMorgan Deters
2010-11-17The "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-16Added Theory::presolve().Tim King
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan 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-16fix function signaturesMorgan Deters
2010-11-15cleanup from today's commits: delegate as-yet-unimplemented prettyprinters ↵Morgan Deters
in a better way; fix arith Makefile
2010-11-15Changes to Solver and PropEngine to support lemmasOnDemand during solve but ↵Tim King
not yet in d_checkSat.
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan 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-15This 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-15minor tweaks to last commit, testing infrastructureMorgan Deters
2010-11-15fix some things with the build system (make dist, make install, make check)Morgan Deters
2010-11-12Some bug fixes in the SAT for lemmas, and an experiment with a more complete ↵Dejan Jovanović
(wr propagation) splitter in arithmetic.
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-08command-line flag to disable theory registration, also SMT-LIBv2 compliance ↵Morgan Deters
(per SMT-LIB mailing list this afternoon)
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-11-08fix out-of-date version/copyright for minisatsMorgan Deters
2010-11-05Moving Options fiddling to options.hChristopher L. Conway
2010-11-04competition mode implies --no-checkingMorgan Deters
2010-11-04This commit adds the ejected and un-ejected statistics.Tim King
2010-11-03Adds size() to RowVector.Tim King
2010-11-03Adds statistics for the number of Uservariables and Slack variables used by ↵Tim King
arithmetic.
2010-11-03Adds AverageStat to stats.h.Tim King
2010-10-31small fix to debug segfaultsMorgan Deters
2010-10-31enable 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-31maximize stack limit, handle SEGV signals on an alternate signal stack, and ↵Morgan Deters
try to diagnose stack overflow
2010-10-30Adds 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-29Fix for a problem caused by using a != instead of == in ↵Tim King
generateConflictBelow(). Resolves a bug introduced in -r1063.
2010-10-29minor 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-29Fixes RowVector::has().Tim King
2010-10-29Factors 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-28The 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-28Changing NodeBuilder::debugCheckType() to maybeCheckType()Christopher L. Conway
Changing NodeManager/ExprManager constructors to take Options
2010-10-28Disabling bottom-up algorithm in NodeManager::getType() when type checkingChristopher L. Conway
is not requested or eager type checking is enabled
2010-10-27Small change to documentation in NodeManager::getTypeChristopher L. Conway
2010-10-27Slightly more efficient version of getTypeChristopher L. Conway
2010-10-27Modifying 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-26GetValueCommand 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-26Cleaning up some header filesChristopher L. Conway
2010-10-25for static linking of driver binary, list libmain.a first (fixes link errors ↵Morgan Deters
in last night's regressions)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback