Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 1f4a04218..1ba0b6572 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -143,6 +143,9 @@ private:
   quantifiers::QuantAntiSkolem * d_anti_skolem;
   /** quantifiers instantiation propagtor */
   quantifiers::InstPropagator * d_inst_prop;
+private:
+  /** whether we are tracking instantiation lemmas */
+  bool d_trackInstLemmas;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -363,6 +366,10 @@ public:
   void printSynthSolution( std::ostream& out );
   /** get instantiations */
   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+  /** get unsat core lemmas */
+  bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas );
+  /** get inst for lemmas */
+  void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); 
   /** statistics class */
   class Statistics {
   public: