summaryrefslogtreecommitdiff
path: root/src/theory/theory.cpp
AgeCommit message (Expand)Author
2012-07-31Moving some instantiation-related stuff from src/theory to src/theory/quantif...Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-11merge from arrays-clark branchMorgan Deters
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-29fixing bug310Dejan Jovanović
2012-02-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
2011-10-17Sharing workDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-08-24Simplification of the preregister and register throught a NodeVisitor class. ...Dejan Jovanović
2010-09-28fix predicate bug in UF; code cleanup in theory.cppMorgan Deters
2010-07-06Moved registration to theory engineClark Barrett
2010-07-02re-generated comment headers of source filesMorgan 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-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-02-25* src/expr/node.h: add a copy constructor. Apparently GCC doesn'tMorgan Deters
2010-02-24Committing small changes to attribute, and theory to avoid future merge probl...Tim King
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04Added theory output channel interfaces and "Interrupted" exception.Morgan Deters
2009-12-17update-copyright.pl now retrieves and incorporates author information from re...Morgan Deters
2009-12-10cleanups, assert work, add a stubbed uf theory, fix driverMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback