Remove instantiation model true option (#4861)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 11 Aug 2020 20:36:38 +0000 (15:36 -0500)
committerGitHub <noreply@github.com>
Tue, 11 Aug 2020 20:36:38 +0000 (13:36 -0700)
commit1339e2a3b884d34a9c27eb45bb6847a493fe0365
treeeee01493ebe789c8c1b09e5f977273c360a52bc7
parent1c859fd0f43fa2081bdb247423e81d9174a5f474
Remove instantiation model true option (#4861)

This was an option that rejected instantiations that are true according to the current
model's equality engine.

This option was never helpful and will be burdensome to maintain with new updates
 to equality engine infrastructure.
src/options/quantifiers_options.toml
src/theory/quantifiers/equality_query.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/instantiate.h
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h