summaryrefslogtreecommitdiff
path: root/src/prop
AgeCommit message (Expand)Author
2012-03-02Remove some commented out code from sat.hKshitij Bansal
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-29This should fix the debian build fails:Liana Hadarean
2012-02-29consistency in how the Dump output stream is usedMorgan Deters
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2012-02-22Added OutputChannel::propagateAsDecision() functionality, allowing a theoryMorgan Deters
2012-02-22minor change to order fn in sat solver's ElimLtKshitij Bansal
2012-02-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my...Morgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody merg...Dejan Jovanović
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic no...Tim King
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-02fully implement the always-check-again-after-the-output-channel-is-used fix f...Morgan Deters
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
2011-10-17Sharing workDejan Jovanović
2011-10-13fix make distMorgan Deters
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t...Morgan Deters
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30fix to CNF undoTranslate(), to support incrementalityMorgan Deters
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes: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-17new implementation of lemmas on demandDejan Jovanović
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10changing the sat solver remove clauses constantsDejan Jovanović
2011-07-09surprize surprizeDejan Jovanović
2011-07-07removing duplicate clauses in ite cnf conversionDejan Jovanović
2011-07-06Fixing two bugs:Dejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-04-14reverting back the minisat code and adding a simpler one that shouldn't chang...Dejan Jovanović
2011-04-14Three things:Morgan Deters
2011-04-14fixing an uninitialized literal variableDejan Jovanović
2011-04-13adding support for unit conflicts in minisat...Dejan Jovanović
2011-04-13fix compiler warning in non-replay buildsMorgan Deters
2011-04-10merge from replay branchMorgan Deters
2011-04-09changing the sat solver to assert propagated literals back to the theoriesDejan Jovanović
2011-04-05Added options for setting the random decision frequency and random seed for t...Tim King
2011-04-05Minor adjustments to the Registrar commit in 1644, documentation.Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory preregistratio...Tim King
2011-04-02minor fixesMorgan Deters
2011-04-01minor bugfixes (fixes broken dynamic-library build from last night)Morgan Deters
2011-04-01documentation fixMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback