summaryrefslogtreecommitdiff
path: root/src/prop
AgeCommit message (Expand)Author
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
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-31Fixes to Valuation.Tim King
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-21more bugfixes, some basic propagation, and testcases to cover themDejan Jovanović
2011-03-15real fix for bug 245, previous one was faultyDejan Jovanović
2011-03-15fix for bug 254, lemmas were propagating at lower levels, and the conflict cl...Dejan Jovanović
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-03-03fixing a type that caused the segfaults in the regressionsDejan Jovanović
2011-03-02fixing the big with lemma reallocation in minisat garbage collectionDejan Jovanović
2011-02-26Commit to fix bug 241 (improper "using namespace std" in a header). This cau...Morgan Deters
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-16Added Theory::presolve().Tim King
2010-11-15Changes to Solver and PropEngine to support lemmasOnDemand during solve but n...Tim King
2010-11-15This commit merges the arith-prop-opt branch into the main trunk. This was do...Tim King
2010-11-12Some bug fixes in the SAT for lemmas, and an experiment with a more complete ...Dejan Jovanović
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-11-08fix out-of-date version/copyright for minisatsMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-27"make dist" fixes; a distribution tarball can now build and pass tests. "make...Morgan Deters
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
2010-10-12hooked up "we are incomplete" flag after conversation with Tim (a theory noti...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback