summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-09-16fix debian build without breaking anything (i hope)Morgan Deters
2011-09-15tim's fixes for context-dependent pre-registrationDejan Jovanović
2011-09-15adding --show-debug-tags to list all available debug tracing tagsDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-07fixes for uf/equality engine from the quantifiers branch. mainly backtracking...Dejan Jovanović
2011-09-03this should fix the build; doxygen documentation now gets built in srcdir/doc...Morgan Deters
2011-09-03Disable a warning to address bug 277. (This doesn't really resolve the issue...Morgan Deters
2011-09-03removing an assert i forgot to remove that andy foundDejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02Ensure that assignment gestures through CDMap iterators like:Morgan Deters
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ...Dejan Jovanović
2011-08-30Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK wil...Dejan Jovanović
2011-08-27Removing Theory::registerTerm() as discussed in the meeting. Now pre-register...Dejan Jovanović
2011-08-25Fixing the broken unit testsDejan Jovanović
2011-08-24Simplification of the preregister and register throught a NodeVisitor class. ...Dejan Jovanović
2011-08-23some uf cleanupDejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
2011-07-12forgot to reflect naming change in makefile. fixedMorgan Deters
2011-07-12fix bug 272, array unsoundness, and some array cleanupMorgan Deters
2011-07-11remove some array regressions from "make check" so nightly regressions runMorgan Deters
2011-07-11status of examplesMorgan Deters
2011-07-11new array bugs ?Morgan Deters
2011-07-11fixing out of place typename (error on g++ 4.4.3-4ubuntu5)Morgan Deters
2011-07-11submission scriptMorgan Deters
2011-07-11Adding static_fact_managerClark Barrett
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11fix some confusing debug output (bogus counter)Morgan Deters
2011-07-11mark the new minimized benchmark as unsatMorgan Deters
2011-07-11if running in QF_AX, equalities over terms of uninterpreted sort go to arrays...Morgan Deters
2011-07-11minimized exampleMorgan Deters
2011-07-11array benchmarksMorgan Deters
2011-07-11adding disequality propagationDejan Jovanović
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10Reverting mistaken check-inClark Barrett
2011-07-10changing the sat solver remove clauses constantsDejan Jovanović
2011-07-10Fixed bug in default solve - wasn't returning when it was supposed toClark Barrett
2011-07-10another typoDejan Jovanović
2011-07-10yet another uf bug fix, hopefully the lastDejan Jovanović
2011-07-10another bugfix for ufDejan Jovanović
2011-07-09some immediate bug fixesDejan Jovanović
2011-07-09fix submission makefileMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-07removing duplicate clauses in ite cnf conversionDejan Jovanović
2011-07-07cudd-building prefs with --with-cudd / --without-cuddMorgan Deters
2011-07-06Fixing two bugs:Dejan Jovanović
2011-07-05missing test caseDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback