summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-26Fix type checking for define-funs (resolves bug 398).Morgan Deters
2012-09-26The Tuesday Afternoon Catch-All Commit (TACAC):Morgan Deters
2012-09-25some buggy examples for incrementality, and make bug326 run as part of make r...Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-22another fix for the equality class iterator Dejan Jovanović
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-19fix for bug 370.Dejan Jovanović
2012-09-19Changing the equality engines's euivalence class iterator. Andy please check ...Dejan Jovanović
2012-09-17minor fix for models, added simple cliques option for uf strong solverAndrew Reynolds
2012-09-16store values returned by get-value in TheoryModel::d_reps if necessary, fixes...Andrew Reynolds
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-11added getCardinality to modelAndrew Reynolds
2012-09-11Partially reverting the changes made in 4308. There is now both an Expr and N...Tim King
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-09-10Fixed an error in the rewriter Pascal pointed out. This was in effectively de...Tim King
2012-09-03minor cleanup leftover from fmf-develAndrew Reynolds
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-29* Numerous documentation fixes (fix doxygen warnings, add missing documentati...Morgan Deters
2012-08-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-27* Reversing commit r4258 (which disabled failing regressions). Fixed the pro...Morgan Deters
2012-08-26Array constants finished and working. Unit tests for array constants.Clark Barrett
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-24disallow assertions to inactive theories.Morgan Deters
2012-08-24fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on activ...Morgan Deters
2012-08-24fix warning in arrays rewriterMorgan Deters
2012-08-24fix get-value output in a couple ways; this fixes bug #378Morgan Deters
2012-08-23attribute stuff for Clark's array constantsMorgan Deters
2012-08-23Array constant coding done except for the attributes neededClark Barrett
2012-08-22More progress on array constants.Clark Barrett
2012-08-21add some incremental in-tree regressionsMorgan Deters
2012-08-21rewriterules: fix a correction bug with --simplification=batchFrançois Bobot
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-16The SmtEngine now ensures that setLogicInternal() is called even if there is ...Morgan Deters
2012-08-16Replace propagateAsDecision() with Theory::getNextDecisionRequest():Morgan Deters
2012-08-14Implements TheoryArith::collectModelInfo(). The current implementation is qu...Tim King
2012-08-14Adds substituteDelta() to DeltaRational which given a value for delta returns...Tim King
2012-08-14Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.Tim King
2012-08-14Switched a number of EqClassIterator operations to const as well as the inter...Tim King
2012-08-13Make a few functions in TheoryEngine (like theoryOf()) const.Morgan Deters
2012-08-13Minor cleanup. No performance difference expected.Morgan Deters
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback