summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2011-07-09surprize surprizeDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-05-02fix a performance issue from last commitMorgan Deters
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ...Morgan Deters
2011-04-25Monday tasks:Morgan Deters
2011-04-22fix to last commitMorgan Deters
2011-04-22Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for fin...Morgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-04-13cache the LET rewriting (and defined-function expansion too)---it wasn't befo...Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory preregistratio...Tim King
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan Deters
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
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan 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-22removing unused functionality from util; related to bug #222Morgan Deters
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-22comment out the "interactive" check in SmtEngine::getValue() for now (resolve...Morgan Deters
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
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-12check last result in (get-assignment); some context cleanupMorgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-10-09support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ...Morgan Deters
2010-10-09bug fixes to model genMorgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-10-08support (set-info) on status, source, category, difficulty, smt-lib-version, ...Morgan Deters
2010-10-07type checking for define-fun in production builds; related to (and might reso...Morgan Deters
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre...Morgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
2010-09-24equality triggers for the equality engineDejan Jovanović
2010-08-17Merge from "cc" branch:Morgan Deters
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-06-15fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)Morgan Deters
2010-06-15remove warnings about unknown #pragma GCC diagnostic on older compilersMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-25Some initial changes to allow for lemmas on demand. Dejan Jovanović
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-04-01PARSER STUFF:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback