summaryrefslogtreecommitdiff
path: root/src/theory/model.cpp
AgeCommit message (Expand)Author
2012-10-05Bug-related:Morgan Deters
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
2012-10-03New model code, mostly workinClark Barrett
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
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-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-14Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.Tim King
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...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-18small change to model-generation function, after discussion w/ AndyMorgan Deters
2012-07-18removing an obsolete assertion in model-generation framework, per Andy's requestMorgan Deters
2012-07-17minor fix to prevent getValue from returning nullAndrew Reynolds
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback