mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

checkpoint

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-29 17:52:07 -08:00
parent cf28cbab0a
commit 722cce0cff
3 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/util/gparams.cpp
View file

@ -173,7 +173,8 @@ public:
}
std::string get_value(char const * name) {
// TODO
return "";
}
@ -200,9 +201,19 @@ void gparams::set(char const * name, char const * value) {
g_imp->set(name, value);
}
void gparams::set(symbol const & name, char const * value) {
SASSERT(g_imp != 0);
g_imp->set(name.bare_str(), value);
}
std::string gparams::get_value(char const * name) {
SASSERT(g_imp != 0);
g_imp->get_value(name);
return g_imp->get_value(name);
}
std::string gparams::get_value(symbol const & name) {
SASSERT(g_imp != 0);
return g_imp->get_value(name.bare_str());
}
void gparams::register_global(param_descrs & d) {

5
src/util/gparams.h
View file

@ -24,8 +24,9 @@ Notes:
class gparams {
struct imp;
static imp * g_imp;
typedef z3_exception exception;
public:
typedef default_exception exception;
/**
\brief Set a global parameter \c name with \c value.
@ -44,6 +45,7 @@ public:
An exception is thrown if the the parameter name is unknown, or if the value is incorrect.
*/
static void set(char const * name, char const * value);
static void set(symbol const & name, char const * value);
/**
\brief Auxiliary method used to implement get-option in SMT 2.0 front-end.
@ -53,6 +55,7 @@ public:
An exception is thrown if the the parameter name is unknown.
*/
static std::string get_value(char const * name);
static std::string get_value(symbol const & name);
/**
\brief Register additional global parameters

4
src/util/params.h
View file

@ -85,8 +85,8 @@ public:
It displays 'default' if k is not in the parameter set.
*/
void display(std::ostream & out, char const * k);
void display(std::ostream & out, symbol const & k);
void display(std::ostream & out, char const * k) const;
void display(std::ostream & out, symbol const & k) const;
};
inline std::ostream & operator<<(std::ostream & out, params_ref const & ref) {