diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /examples | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
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}.
Diffstat (limited to 'examples')
-rw-r--r-- | examples/hashsmt/word.cpp | 9 | ||||
-rw-r--r-- | examples/nra-translate/normalize.cpp | 4 | ||||
-rw-r--r-- | examples/nra-translate/smt2info.cpp | 7 | ||||
-rw-r--r-- | examples/nra-translate/smt2todreal.cpp | 13 | ||||
-rw-r--r-- | examples/nra-translate/smt2toisat.cpp | 3 | ||||
-rw-r--r-- | examples/nra-translate/smt2tomathematica.cpp | 13 | ||||
-rw-r--r-- | examples/nra-translate/smt2toqepcad.cpp | 101 | ||||
-rw-r--r-- | examples/nra-translate/smt2toredlog.cpp | 24 | ||||
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 3 | ||||
-rw-r--r-- | examples/translator.cpp | 4 |
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, "-")) { |