summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
AgeCommit message (Expand)Author
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03New model code, mostly workinClark Barrett
2012-10-03added support for interrupting TheoryBVLiana Hadarean
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-12Adding model assertions after SAT responses.Morgan Deters
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-24disallow assertions to inactive theories.Morgan Deters
2012-08-24fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on activ...Morgan Deters
2012-08-21add some incremental in-tree regressionsMorgan Deters
2012-08-16Replace propagateAsDecision() with Theory::getNextDecisionRequest():Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-18small bug fix and performance fix in ite simplifierClark Barrett
2012-06-16small change to equality assertions so that one doesn't get x = y and y = xDejan Jovanović
2012-06-16This is an attempt to fix the bug in the justification heuristic. TheKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-15Fixes some assertion failuresClark Barrett
2012-06-14fixing the problems with the bvminisat. there was a case when things would ge...Dejan Jovanović
2012-06-14fixes for the hasTerm issues in the shared database under the decision heuristicDejan Jovanović
2012-06-14* removing rewriteEquality from the rewriterDejan Jovanović
2012-06-13Adds debugging output to theory_engine.cpp.Tim King
2012-06-12bufixes and the bugsDejan Jovanović
2012-06-12conflicts from theories are removableDejan Jovanović
2012-06-11Fixing type comparision assertion in getEqualityStatus().Tim King
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-10adding an assertion to trigger the problem of bug349 and the testcaseDejan Jovanović
2012-06-10fixes for bug347Dejan Jovanović
2012-06-07fixing some bugs in propagation of disequalitiesDejan Jovanović
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-06-06Fixed problem causing crash at destruction timeClark Barrett
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-05-28Added some BV rewrites, fixed bugs in array theory, made ite simp work with BVClark Barrett
2012-05-25init bug fixKshitij Bansal
2012-05-16Changes to SAT solver:Dejan Jovanović
2012-05-15Fixed several bugs in shared terms databaseClark Barrett
2012-05-14fixing up preregistration againDejan Jovanović
2012-05-11Added some ITE rewrites,Clark Barrett
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-05-02Changing d_sharedTermsExist to logicInfo.isSharingEnabled()Clark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback