Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index c6f4affc5..d4be58636 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -723,6 +723,9 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
       }else{
         Trace("qip-prop-debug") << it->first << " ";
       }
+    }else{
+      //mark the quantified formula as relevant
+      d_qe->markRelevant( it->second.d_q );
     }
   }
   Trace("qip-prop-debug") << std::endl;