diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/bindings/Makefile.am | 2 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/parser.i | 4 | ||||
-rw-r--r-- | src/util/cardinality.i | 28 | ||||
-rw-r--r-- | src/util/datatype.i | 10 | ||||
-rw-r--r-- | src/util/integer.i | 1 | ||||
-rw-r--r-- | src/util/output.i | 18 | ||||
-rw-r--r-- | src/util/rational.i | 1 | ||||
-rw-r--r-- | src/util/stats.h | 49 | ||||
-rw-r--r-- | src/util/stats.i | 22 |
10 files changed, 98 insertions, 45 deletions
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index e35ec5e67..e14527ede 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -136,7 +136,7 @@ python.lo: python.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $< python.cpp: ocaml.cpp: -python.lo: ruby.cpp +ruby.lo: ruby.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $< ruby.cpp: tcl.cpp: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 955f3a1f4..96c0933d8 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -596,10 +596,10 @@ mainCommand[CVC4::Command*& cmd] { cmd = new SetOptionCommand(s, sexpr); } /* push / pop */ - | PUSH_TOK k=numeral? - { cmd = REPEAT_COMMAND(k, PushCommand()); } - | POP_TOK k=numeral? - { cmd = REPEAT_COMMAND(k, PopCommand()); } + | PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); } + | { cmd = new PushCommand(); } ) + | POP_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PopCommand()); } + | { cmd = new PopCommand(); } ) | POPTO_TOK k=numeral? { UNSUPPORTED("POPTO command"); } diff --git a/src/parser/parser.i b/src/parser/parser.i index dd52bfcda..5e10973d4 100644 --- a/src/parser/parser.i +++ b/src/parser/parser.i @@ -12,8 +12,8 @@ namespace CVC4 { class ParserExprStream : public CVC4::ExprStream { Parser* d_parser; public: - ExprStream(Parser* parser) : d_parser(parser) {} - ~ExprStream() { delete d_parser; } + ParserExprStream(Parser* parser) : d_parser(parser) {} + ~ParserExprStream() { delete d_parser; } Expr nextExpr() { return d_parser->nextExpression(); } };/* class Parser::ExprStream */ diff --git a/src/util/cardinality.i b/src/util/cardinality.i index 760f746c0..82f67382b 100644 --- a/src/util/cardinality.i +++ b/src/util/cardinality.i @@ -20,4 +20,32 @@ %ignore CVC4::operator<<(std::ostream&, const Cardinality&); %ignore CVC4::operator<<(std::ostream&, Cardinality::Beth); + class Beth { + Integer d_index; + + public: + Beth(const Integer& beth) : d_index(beth) { + CheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); + } + + const Integer& getNumber() const throw() { + return d_index; + } + };/* class Cardinality::Beth */ + + class Unknown { + public: + Unknown() throw() {} + ~Unknown() throw() {} + };/* class Cardinality::Unknown */ + %include "util/cardinality.h" + +%{ +namespace CVC4 { + typedef CVC4::Cardinality::Beth Beth; + typedef CVC4::Cardinality::Unknown Unknown; +} +%} diff --git a/src/util/datatype.i b/src/util/datatype.i index b62033e17..fe696029d 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -1,8 +1,5 @@ %{ #include "util/datatype.h" -namespace CVC4 { -//typedef CVC4::Datatype::Constructor DatatypeConstructor; -} %} namespace CVC4 { @@ -33,6 +30,11 @@ namespace CVC4 { %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const; %ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const; +%rename(beginConst) CVC4::Constructor::begin() const; +%rename(endConst) CVC4::Constructor::end() const; + +%rename(getArg) CVC4::Constructor::operator[](size_t) const; + %ignore CVC4::operator<<(std::ostream&, const Datatype&); %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&); %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&); @@ -226,7 +228,6 @@ namespace CVC4 { const Arg& operator[](size_t index) const; };/* class Datatype::Constructor */ -} class SelfType { };/* class Datatype::SelfType */ @@ -245,6 +246,7 @@ namespace CVC4 { inline UnresolvedType(std::string name); inline std::string getName() const throw(); };/* class Datatype::UnresolvedType */ +} %{ namespace CVC4 { diff --git a/src/util/integer.i b/src/util/integer.i index 4aaa532a7..bad6b196f 100644 --- a/src/util/integer.i +++ b/src/util/integer.i @@ -4,6 +4,7 @@ %ignore CVC4::Integer::Integer(int); %ignore CVC4::Integer::Integer(unsigned int); +%ignore CVC4::Integer::Integer(const std::string&); %rename(assign) CVC4::Integer::operator=(const Integer&); %rename(equals) CVC4::Integer::operator==(const Integer&) const; diff --git a/src/util/output.i b/src/util/output.i index 10653c2f8..b9c0e32ee 100644 --- a/src/util/output.i +++ b/src/util/output.i @@ -11,4 +11,22 @@ %ignore CVC4::null_os; %ignore CVC4::DumpC::dump_cout; +%ignore operator<<; +%ignore on(std::string); +%ignore isOn(std::string); +%ignore off(std::string); +%ignore printf(std::string, const char*, ...); +%ignore operator()(std::string); + +%ignore CVC4::ScopedDebug::ScopedDebug(std::string); +%ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool); + +%ignore CVC4::ScopedTrace::ScopedTrace(std::string); +%ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool); + +%rename(getostream) operator std::ostream&; +%rename(getCVC4ostream) operator CVC4ostream; +%rename(get) operator(); +%rename(ok) operator bool; + %include "util/output.h" diff --git a/src/util/rational.i b/src/util/rational.i index 512d3ea50..135302c66 100644 --- a/src/util/rational.i +++ b/src/util/rational.i @@ -6,6 +6,7 @@ %ignore CVC4::Rational::Rational(unsigned int); %ignore CVC4::Rational::Rational(int, int); %ignore CVC4::Rational::Rational(unsigned int, unsigned int); +%ignore CVC4::Rational::Rational(const std::string&); %rename(assign) CVC4::Rational::operator=(const Rational&); %rename(equals) CVC4::Rational::operator==(const Rational&) const; diff --git a/src/util/stats.h b/src/util/stats.h index 3a2847512..e955a7d28 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -45,8 +45,6 @@ class ExprManager; class CVC4_PUBLIC Stat; -inline std::ostream& operator<<(std::ostream& os, const timespec& t); - /** * The main statistics registry. This registry maintains the list of * currently active statistics and is able to "flush" them all. @@ -643,12 +641,14 @@ inline bool operator>=(const timespec& a, const timespec& b) { } /** Output a timespec on an output stream. */ +inline std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& os, const timespec& t) { // assumes t.tv_nsec is in range return os << t.tv_sec << "." << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; } +class CVC4_PUBLIC CodeTimer; /** * A timer statistic. The timer can be started and stopped @@ -666,27 +666,7 @@ class CVC4_PUBLIC TimerStat : public BackedStat< timespec > { public: - /** - * Utility class to make it easier to call stop() at the end of a - * code block. When constructed, it starts the timer. When - * destructed, it stops the timer. - */ - class CodeTimer { - TimerStat& d_timer; - - /** Private copy constructor undefined (no copy permitted). */ - CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; - - public: - CodeTimer(TimerStat& timer) : d_timer(timer) { - d_timer.start(); - } - ~CodeTimer() { - d_timer.stop(); - } - };/* class TimerStat::CodeTimer */ + typedef CVC4::CodeTimer CodeTimer; /** * Construct a timer statistic with the given name. Newly-constructed @@ -713,6 +693,29 @@ public: /** + * Utility class to make it easier to call stop() at the end of a + * code block. When constructed, it starts the timer. When + * destructed, it stops the timer. + */ +class CVC4_PUBLIC CodeTimer { + TimerStat& d_timer; + + /** Private copy constructor undefined (no copy permitted). */ + CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + +public: + CodeTimer(TimerStat& timer) : d_timer(timer) { + d_timer.start(); + } + ~CodeTimer() { + d_timer.stop(); + } +};/* class CodeTimer */ + + +/** * To use a statistic, you need to declare it, initialize it in your * constructor, register it in your constructor, and deregister it in * your destructor. Instead, this macro does it all for you (and diff --git a/src/util/stats.i b/src/util/stats.i index 48828cb7e..5d3b81d4d 100644 --- a/src/util/stats.i +++ b/src/util/stats.i @@ -2,20 +2,20 @@ #include "util/stats.h" %} -%ignore CVC4::operator<<(std::ostream&, const ::timespec&); +%ignore CVC4::operator<<(std::ostream&, const timespec&); %rename(increment) CVC4::IntStat::operator++(); %rename(plusAssign) CVC4::IntStat::operator+=(int64_t); -%rename(plusAssign) CVC4::operator+=(::timespec&, const ::timespec&); -%rename(minusAssign) CVC4::operator-=(::timespec&, const ::timespec&); -%rename(plus) CVC4::operator+(const ::timespec&, const ::timespec&); -%rename(minus) CVC4::operator-(const ::timespec&, const ::timespec&); -%rename(equals) CVC4::operator==(const ::timespec&, const ::timespec&); -%ignore CVC4::operator!=(const ::timespec&, const ::timespec&); -%rename(less) CVC4::operator<(const ::timespec&, const ::timespec&); -%rename(lessEqual) CVC4::operator<=(const ::timespec&, const ::timespec&); -%rename(greater) CVC4::operator>(const ::timespec&, const ::timespec&); -%rename(greaterEqual) CVC4::operator>=(const ::timespec&, const ::timespec&); +%rename(plusAssign) CVC4::operator+=(timespec&, const timespec&); +%rename(minusAssign) CVC4::operator-=(timespec&, const timespec&); +%rename(plus) CVC4::operator+(const timespec&, const timespec&); +%rename(minus) CVC4::operator-(const timespec&, const timespec&); +%rename(equals) CVC4::operator==(const timespec&, const timespec&); +%ignore CVC4::operator!=(const timespec&, const timespec&); +%rename(less) CVC4::operator<(const timespec&, const timespec&); +%rename(lessEqual) CVC4::operator<=(const timespec&, const timespec&); +%rename(greater) CVC4::operator>(const timespec&, const timespec&); +%rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&); %include "util/stats.h" |