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}.

10 files changed, 83 insertions, 98 deletions

diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 7aa37e91b..a2c5907f0 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -28,7 +28,6 @@
 
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
-#include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 
@@ -43,7 +42,7 @@ Expr Word::extendToSize(unsigned newSize) const {
   } else {
     // 0-extend to size
     Expr extendOp = em()->mkConst(BitVectorZeroExtend(newSize - size()));
-    return em()->mkExpr(extendOp, d_expr);    
+    return em()->mkExpr(extendOp, d_expr);
   }
 }
 
@@ -52,8 +51,8 @@ ExprManager* Word::s_manager = 0;
 ExprManager* Word::em() {
   if (s_manager == 0) {
     CVC4::Options options;
-    options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
-    options.set(outputLanguage, language::output::LANG_SMTLIB_V2);
+    options.setInputLanguage(language::input::LANG_SMTLIB_V2);
+    options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     s_manager = new CVC4::ExprManager(options);
   }
   return s_manager;
@@ -173,5 +172,3 @@ cvc4_uchar8::cvc4_uchar8(const Word& b) {
     d_expr = b.getExpr();
   }
 }
-
-
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index 56f326216..38329fba6 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -25,7 +25,6 @@
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -36,7 +35,6 @@
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
-using namespace CVC4::options;
 using namespace CVC4::theory;
 
 int main(int argc, char* argv[])
@@ -47,7 +45,7 @@ int main(int argc, char* argv[])
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2)
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index c541a23fe..7efb5c855 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -22,7 +22,6 @@
 #include <vector>
 
 #include "expr/expr.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -78,13 +77,13 @@ int main(int argc, char* argv[])
 
     // Create the expression manager
     Options options;
-    options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+    options.setInputLanguage(language::input::LANG_SMTLIB_V2);
     ExprManager exprManager(options);
-  
+
     // Create the parser
     ParserBuilder parserBuilder(&exprManager, input, options);
     Parser* parser = parserBuilder.build();
-  
+
     // Variables and assertions
     vector<string> variables;
     vector<string> info_tags;
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 56f323812..331cf894f 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -24,7 +24,6 @@
 
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -36,20 +35,20 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace CVC4::options;
 
-int main(int argc, char* argv[]) 
+int main(int argc, char* argv[])
 {
 
-  // Get the filename 
+  // Get the filename
   string input(argv[1]);
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
-  options.set(outputLanguage, language::output::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
+  options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
 
   cout << expr::ExprDag(0) << expr::ExprSetDepth(-1);
-  
+
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
   Parser* parser = parserBuilder.build();
@@ -82,5 +81,3 @@ int main(int argc, char* argv[])
   // Get rid of the parser
   delete parser;
 }
-
-
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 076d37077..bcfb4a180 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -23,7 +23,6 @@
 #include <vector>
 
 #include "expr/expr.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -50,7 +49,7 @@ int main(int argc, char* argv[])
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
 
   // Create the parser
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index 0ad5bbab5..ec1da2d7c 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -23,7 +23,6 @@
 #include <vector>
 
 #include "expr/expr.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -32,26 +31,25 @@
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
-using namespace CVC4::options;
 
 void translate_to_mathematica(
         string input,
         const vector<string>& info_tags,
         const vector<string>& info_data,
-	const map<Expr, unsigned>& variables, 
+	const map<Expr, unsigned>& variables,
 	const vector<Expr>& assertions);
 
-int main(int argc, char* argv[]) 
+int main(int argc, char* argv[])
 {
 
-  // Get the filename 
+  // Get the filename
   string input(argv[1]);
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
-  
+
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
   Parser* parser = parserBuilder.build();
@@ -325,4 +323,3 @@ void translate_to_mathematica(
   // End resolve
   cout << ", Reals]" << endl;
 }
-
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index c74b0a110..ea9f2a4e6 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -23,7 +23,6 @@
 #include <vector>
 
 #include "expr/expr.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -32,28 +31,26 @@
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
-using namespace CVC4::options;
-
 
 void translate_to_qepcad(
         string input,
         const vector<string>& info_tags,
         const vector<string>& info_data,
-	const map<Expr, unsigned>& variables, 
+	const map<Expr, unsigned>& variables,
 	const vector<Expr>& assertions);
 
-int main(int argc, char* argv[]) 
+int main(int argc, char* argv[])
 {
   std::map<Expr, unsigned> vars2id;
 
-  // Get the filename 
+  // Get the filename
   string input(argv[1]);
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
-  
+
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
   Parser* parser = parserBuilder.build();
@@ -75,7 +72,8 @@ int main(int argc, char* argv[])
       continue;
     }
 
-    DeclareFunctionCommand* declare = dynamic_cast<DeclareFunctionCommand*>(cmd);
+    DeclareFunctionCommand* declare =
+        dynamic_cast<DeclareFunctionCommand*>(cmd);
     if (declare) {
       string name = declare->getSymbol();
       Expr var = parser->getVariable(name);
@@ -84,7 +82,7 @@ int main(int argc, char* argv[])
       delete cmd;
       continue;
     }
-    
+
     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
     if (assert) {
       assertions.push_back(assert->getExpr());
@@ -92,30 +90,32 @@ int main(int argc, char* argv[])
       continue;
     }
 
-    delete cmd;  
+    delete cmd;
   }
 
   // Do the translation
   translate_to_qepcad(input, info_tags, info_data, variables, assertions);
-		
+
   // Get rid of the parser
   delete parser;
 }
 
-void translate_to_qepcad_term(const std::map<Expr, unsigned>& variables, const Expr& term) {
+void translate_to_qepcad_term(const std::map<Expr, unsigned>& variables,
+                              const Expr& term)
+{
   bool first;
 
   unsigned n = term.getNumChildren();
-  
+
   if (n == 0) {
     if (term.getKind() == kind::CONST_RATIONAL) {
       cout << term.getConst<Rational>();
-    } else {      
+    } else {
       assert(variables.find(term) != variables.end());
       cout << "x" << variables.find(term)->second;
     }
   } else {
-        
+
     switch (term.getKind()) {
       case kind::PLUS:
         cout << "(";
@@ -140,12 +140,12 @@ void translate_to_qepcad_term(const std::map<Expr, unsigned>& variables, const E
           translate_to_qepcad_term(variables, term[i]);
         }
         cout << ")";
-        break;      
+        break;
       case kind::MINUS:
         cout << "(";
         translate_to_qepcad_term(variables, term[0]);
         cout << " - ";
-        translate_to_qepcad_term(variables, term[1]);        
+        translate_to_qepcad_term(variables, term[1]);
         cout << ")";
         break;
       case kind::UMINUS:
@@ -167,25 +167,27 @@ void translate_to_qepcad_term(const std::map<Expr, unsigned>& variables, const E
         assert(false);
         break;
     }
-  }  
+  }
 }
 
-void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr& assertion) {
+void translate_to_qepcad(const std::map<Expr, unsigned>& variables,
+                         const Expr& assertion)
+{
   bool first;
-  
+
   unsigned n = assertion.getNumChildren();
-  
+
   if (n == 0) {
     assert(false);
   } else {
-    
+
     std::string op;
     bool theory = false;
     bool binary = false;
-    
+
     switch (assertion.getKind()) {
-      case kind::NOT: 
-        cout << "[~";  
+      case kind::NOT:
+        cout << "[~";
         translate_to_qepcad(variables, assertion[0]);
         cout << "]";
         break;
@@ -212,7 +214,7 @@ void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr&
           translate_to_qepcad(variables, assertion[i]);
         }
         cout << "]";
-        break;      
+        break;
       case kind::IMPLIES:
         op = "==>";
         binary =  true;
@@ -220,7 +222,7 @@ void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr&
       case kind::IFF:
         op = "<==>";
         binary =  true;
-        break;            
+        break;
       case kind::EQUAL:
         op = "=";
         theory =  true;
@@ -252,7 +254,7 @@ void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr&
       cout << " " << op << " ";
       translate_to_qepcad_term(variables, assertion[1]);
       cout << "]";
-    }      
+    }
 
     if (binary) {
       cout << "[";
@@ -260,15 +262,15 @@ void translate_to_qepcad(const std::map<Expr, unsigned>& variables, const Expr&
       cout << " " << op << " ";
       translate_to_qepcad(variables, assertion[1]);
       cout << "]";
-    }      
-  }  
+    }
+  }
 }
 
 void translate_to_qepcad(
         string input,
         const vector<string>& info_tags,
         const vector<string>& info_data,
-	const std::map<Expr, unsigned>& variables, 
+	const std::map<Expr, unsigned>& variables,
 	const vector<Expr>& assertions)
 {
   bool first;
@@ -277,22 +279,22 @@ void translate_to_qepcad(
   cout << "[ translated from " << input << " ";
 
   bool dump_tags = false;
-  if (dump_tags) {  
-    first = true;  
+  if (dump_tags) {
+    first = true;
     for (unsigned i = 0; i < info_tags.size(); ++ i) {
       if (!first) {
-        cout << ", "; 
+        cout << ", ";
       }
       first = false;
       cout << info_tags[i] << " = " << info_data[i];
     }
   }
-  
-  cout << "]" << endl;   
+
+  cout << "]" << endl;
 
   // Declare the variables
   cout << "(";
-  
+
   first = true;
   for (unsigned i = 0; i < variables.size(); ++ i) {
     if (!first) {
@@ -301,17 +303,17 @@ void translate_to_qepcad(
     first = false;
     cout << "x" << i;;
   }
-  
+
   cout << ")" << endl;
 
-  // Number of free variables 
+  // Number of free variables
   cout << "0" << endl;
 
-  // The quantifiers first 
+  // The quantifiers first
   for (unsigned i = 0; i < variables.size(); ++ i) {
     cout << "(Ex" << i << ")";
   }
-  
+
   // Now the formula
   cout << "[";
   if (assertions.size() > 1) {
@@ -319,35 +321,34 @@ void translate_to_qepcad(
     for (unsigned i = 0; i < assertions.size(); ++ i) {
       if (!first) {
         cout << " /\\ ";
-      } 
+      }
       first = false;
       translate_to_qepcad(variables, assertions[i]);
     }
   } else {
     translate_to_qepcad(variables, assertions[0]);
   }
-  cout << "]." << endl;  
+  cout << "]." << endl;
 
   // Before normalization
   cout << "go" << endl;
-  
+
   // Before projection
   if (variables.size() > 3) {
     cout << "proj-op (m,m";
     for (unsigned i = 3; i < variables.size(); ++ i) {
       cout << ",h";
-    } 
+    }
     cout << ")" << endl;
   }
   cout << "go" << endl;
-  
+
   // Before choice
   cout << "d-stat" << endl;
-  
+
   // Before solution
-  cout << "go" << endl;  
+  cout << "go" << endl;
 
   // Finish up
   cout << "finish" << endl;
 }
-
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 7a6f87122..934906b74 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -23,7 +23,6 @@
 #include <vector>
 
 #include "expr/expr.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -40,22 +39,22 @@ void translate_to_redlog(
         string command,
         const vector<string>& info_tags,
         const vector<string>& info_data,
-	const map<Expr, unsigned>& variables, 
+	const map<Expr, unsigned>& variables,
 	const vector<Expr>& assertions);
 
-int main(int argc, char* argv[]) 
+int main(int argc, char* argv[])
 {
 
-  // Get the filename 
+  // Get the filename
   string input(argv[1]);
   // Get the redlog command
   string command(argv[2]);
 
   // Create the expression manager
   Options options;
-  options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+  options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
-  
+
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
   Parser* parser = parserBuilder.build();
@@ -169,14 +168,14 @@ void translate_to_redlog_term(const map<Expr, unsigned>& variables, const Expr&
         assert(false);
         break;
     }
-  }  
+  }
 }
 
 void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& assertion) {
   bool first;
-  
+
   unsigned n = assertion.getNumChildren();
-  
+
   if (n == 0) {
     if (assertion.isConst()) {
       if (assertion.getConst<bool>()) {
@@ -188,13 +187,13 @@ void translate_to_redlog(const map<Expr, unsigned>& variables, const Expr& asser
       assert(false);
     }
   } else {
-    
+
     std::string op;
     bool binary = false;
     bool theory = false;
-    
+
     switch (assertion.getKind()) {
-      case kind::NOT: 
+      case kind::NOT:
         cout << "(not ";
         translate_to_redlog(variables, assertion[0]);
         cout << ")";
@@ -326,4 +325,3 @@ void translate_to_redlog(
   cout << "quit;" << endl;
 
 }
-
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index a310a2e6b..c07369661 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -24,7 +24,6 @@
 
 #include "expr/expr.h"
 #include "options/language.h"
-#include "options/base_options.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -265,7 +264,7 @@ int main(int argc, char* argv[])
 
     // Create the expression manager
     Options options;
-    options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+    options.setInputLanguage(language::input::LANG_SMTLIB_V2);
     cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
     // cout << Expr::dag(0);
     ExprManager exprManager(options);
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 248dadd5f..94f5ad1b8 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -24,8 +24,8 @@
 
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
-#include "options/base_options.h"
 #include "options/language.h"
+#include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -103,7 +103,7 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag
   *out << language::SetLanguage(toLang);
 
   Options opts;
-  opts.set(options::inputLanguage, fromLang);
+  opts.setInputLanguage(fromLang);
   ExprManager exprMgr(opts);
   ParserBuilder parserBuilder(&exprMgr, filename, opts);
   if(!strcmp(filename, "-")) {