Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

1 files changed, 43 insertions, 43 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 3d700c388..d997d6e23 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -30,8 +30,6 @@
 
 namespace CVC4 {
 
-class SmtGlobals;
-
 namespace theory {
 class Theory;
 }
@@ -89,7 +87,7 @@ typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
 typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
 typedef std::vector<LetOrderElement> Bindings; 
 
-class TheoryProof; 
+class TheoryProof;
 typedef unsigned ClauseId;
 
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
@@ -99,67 +97,69 @@ class TheoryProofEngine {
 protected:
   ExprSet d_registrationCache;
   TheoryProofTable d_theoryProofTable;
-  
+
   /**
    * Returns whether the theory is currently supported in proof
    * production mode.
    */
   bool supportedTheory(theory::TheoryId id);
 public:
-  SmtGlobals* d_globals;
-  
-  TheoryProofEngine(SmtGlobals* globals);
+
+  TheoryProofEngine();
   virtual ~TheoryProofEngine();
-  /** 
-   * Print the theory term (could be atom) by delegating to the
-   * proper theory
-   * 
-   * @param term 
-   * @param os 
-   * 
-   * @return 
+
+  /**
+   * Print the theory term (could be an atom) by delegating to the proper theory.
+   *
+   * @param term
+   * @param os
    */
   virtual void printLetTerm(Expr term, std::ostream& os) = 0;
-  virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
-  /** 
+  virtual void printBoundTerm(Expr term, std::ostream& os,
+                              const LetMap& map) = 0;
+
+  /**
    * Print the proof representation of the given sort.
-   * 
-   * @param os 
+   *
+   * @param os
    */
-  virtual void printSort(Type type, std::ostream& os) = 0; 
-  /** 
+  virtual void printSort(Type type, std::ostream& os) = 0;
+
+  /**
    * Print the theory assertions (arbitrary formulas over
    * theory atoms)
-   * 
-   * @param os 
+   *
+   * @param os
    * @param paren closing parenthesis
    */
   virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
-  /** 
+
+  /**
    * Print proofs of all the theory lemmas (must prove
    * actual clause used in resolution proof).
-   * 
-   * @param os 
-   * @param paren 
+   *
+   * @param os
+   * @param paren
    */
-  virtual void printTheoryLemmas(const IdToSatClause& lemmas,
-                                 std::ostream& os,
+  virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os,
                                  std::ostream& paren) = 0;
-  /** 
-   * Register theory atom (ensures all terms and atoms are declared). 
-   * 
-   * @param atom 
+
+  /**
+   * Register theory atom (ensures all terms and atoms are declared).
+   *
+   * @param atom
    */
   void registerTerm(Expr atom);
-  /** 
-   * Ensures that a theory proof class for the given theory
-   * is created.
-   * 
-   * @param theory 
+
+  /**
+   * Ensures that a theory proof class for the given theory is created.
+   *
+   * @param theory
    */
   void registerTheory(theory::Theory* theory);
+
   theory::TheoryId getTheoryForLemma(ClauseId id);
-  TheoryProof* getTheoryProof(theory::TheoryId id); 
+  TheoryProof* getTheoryProof(theory::TheoryId id);
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -167,9 +167,9 @@ class LFSCTheoryProofEngine : public TheoryProofEngine {
   void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map);
   void bind(Expr term, LetMap& map, Bindings& let_order);
 public:
-  LFSCTheoryProofEngine(SmtGlobals* globals)
-    : TheoryProofEngine(globals) {}
-  
+  LFSCTheoryProofEngine()
+    : TheoryProofEngine() {}
+
   void printDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printLetTerm(Expr term, std::ostream& os);
@@ -178,7 +178,7 @@ public:
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
                                  std::ostream& paren);
-  virtual void printSort(Type type, std::ostream& os); 
+  virtual void printSort(Type type, std::ostream& os);
 };
 
 class TheoryProof {