Replace propagateAsDecision() with Theory::getNextDecisionRequest():
authorMorgan Deters <mdeters@gmail.com>
Thu, 16 Aug 2012 21:30:41 +0000 (21:30 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 16 Aug 2012 21:30:41 +0000 (21:30 +0000)
commitdd30200795d4b37398c29f0d20998c9bd63a7fe7
tree494e235520553c0f20654bb991e8359e6b0f1b9e
parentd260caa58d462f7e1eb0d94f73789f844f5f5596
Replace propagateAsDecision() with Theory::getNextDecisionRequest():

* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups
14 files changed:
src/context/cdqueue.h
src/theory/arith/kinds
src/theory/arrays/kinds
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/builtin/kinds
src/theory/mktheorytraits
src/theory/output_channel.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/kinds
src/theory/uf/theory_uf_strong_solver.cpp