Variable patterns only look at eligible terms. Minor refactoring of quantifiers...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 24 Jan 2015 18:42:21 +0000 (19:42 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 24 Jan 2015 18:42:21 +0000 (19:42 +0100)
commit79ad2d6ec3ebd5c45dce4e13e895d0bed0a6f525
tree7524e1376337c2b3d6544eeda832f8f3d574b409
parent73cecf65a750b9ee59486083af5ee55734da0a6a
Variable patterns only look at eligible terms.  Minor refactoring of quantifiers check for sat.
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quant_util.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h