summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.cpp
AgeCommit message (Expand)Author
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ...Tim King
2012-11-26fixup for incremental solvingDejan Jovanović
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-28Public interface review items:Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-05-18This commit removes the dead psuedoboolean code.Tim King
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-25sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)Dejan Jovanović
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
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-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in my...Morgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t...Morgan Deters
2011-09-30fix to CNF undoTranslate(), to support incrementalityMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
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-17new implementation of lemmas on demandDejan Jovanović
2011-07-07removing duplicate clauses in ite cnf conversionDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-04-10merge from replay branchMorgan Deters
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-03-21more bugfixes, some basic propagation, and testcases to cover themDejan Jovanović
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-08-19UF theory bug fixes, code cleanup, and extra debugging output.Morgan Deters
2010-08-16Fixing failures in minisatDejan Jovanović
2010-08-15(no commit message)Dejan Jovanović
2010-07-22incorporate a fix from smtcomp2010 version for handling CNF of (= bool bool);...Morgan Deters
2010-06-29Merging the unate-propagator branch into the trunk. This is a big update so ...Tim King
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-06-01In order for splitting on demand to be able to retract clauses every translat...Dejan Jovanović
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ...Tim King
2010-05-27Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential...Morgan Deters
2010-05-27Preregistration has been turned on. Highly experimental eager splitting suppo...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback