summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-27* Reversing commit r4258 (which disabled failing regressions). Fixed the pro...Morgan Deters
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-20remove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplic...Morgan Deters
2012-08-20minor cleanupMorgan Deters
2012-08-191. Fix for inst_match.cpp to allow compilation on fedoraClark Barrett
2012-08-16Replace propagateAsDecision() with Theory::getNextDecisionRequest():Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-07-31Moving some instantiation-related stuff from src/theory to src/theory/quantif...Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-08another signed-ness warning fix for newer GCCMorgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-14fix quantifier non-bugKshitij Bansal
2012-06-14* removing rewriteEquality from the rewriterDejan Jovanović
2012-06-11mark a quantifiers global var as "static" so we can find it easier laterMorgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback