unsigned int testerIndex = -1;
for( unsigned int i=0; i<possibleCons.size(); i++ ) {
if( possibleCons[i] ){
- Assert( testerIndex==-1 );
+ Assert( testerIndex==unsigned(-1) );
testerIndex = i;
}
}
- Assert( testerIndex!=-1 );
+ Assert( testerIndex!=unsigned(-1) );
assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep );
Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
d_em.addNode( assertionRep, exp, Reason::idt_texhaust );
if( n.getKind() == APPLY_CONSTRUCTOR ){
for( int i=0; i<(int)n.getNumChildren(); i++ ) {
Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl;
- bool result = d_cycle_check.addEdgeNode( n, n[i] );
+ bool result CVC4_UNUSED = d_cycle_check.addEdgeNode( n, n[i] );
Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before)
}
}else{
uint64_t bothTags = parentTag | childTag;
// Create or update the SharedData for n
- SharedData* pData;
+ SharedData* pData = NULL;
if(n.getAttribute(SharedAttr(), pData)) {
// The attribute already exists, just update it if necessary
uint64_t tags = pData->getTheories();
TNode x = eq[0];
TNode y = eq[1];
- SharedData* pDataX;
- SharedData* pDataY;
+ SharedData* pDataX = NULL;
+ SharedData* pDataY = NULL;
// Grab the SharedData for each side of the equality, create if necessary
if(!x.getAttribute(SharedAttr(), pDataX)) {
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Output utility classes and functions.
+ ** \brief Output utility classes and functions
**
** Output utility classes and functions.
**/
-#include <iostream>
-
#include "util/output.h"
+#include <iostream>
+
using namespace std;
namespace CVC4 {
null_streambuf null_sb;
ostream null_os(&null_sb);
-NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
NullC nullCvc4Stream CVC4_PUBLIC;
-#ifndef CVC4_MUZZLE
-
DebugC DebugChannel CVC4_PUBLIC (&cout);
-WarningC Warning CVC4_PUBLIC (&cerr);
-MessageC Message CVC4_PUBLIC (&cout);
-NoticeC Notice CVC4_PUBLIC (&cout);
-ChatC Chat CVC4_PUBLIC (&cout);
+WarningC WarningChannel CVC4_PUBLIC (&cerr);
+MessageC MessageChannel CVC4_PUBLIC (&cout);
+NoticeC NoticeChannel CVC4_PUBLIC (&cout);
+ChatC ChatChannel CVC4_PUBLIC (&cout);
TraceC TraceChannel CVC4_PUBLIC (&cout);
+#ifndef CVC4_MUZZLE
+
+# ifdef CVC4_DEBUG
+
int DebugC::printf(const char* tag, const char* fmt, ...) {
if(d_tags.find(string(tag)) == d_tags.end()) {
return 0;
return retval;
}
+# endif /* CVC4_DEBUG */
+
int WarningC::printf(const char* fmt, ...) {
// chop off output after 1024 bytes
char buf[1024];
return retval;
}
+# ifdef CVC4_TRACING
+
int TraceC::printf(const char* tag, const char* fmt, ...) {
if(d_tags.find(string(tag)) == d_tags.end()) {
return 0;
return retval;
}
-#else /* ! CVC4_MUZZLE */
-
-NullDebugC Debug CVC4_PUBLIC;
-NullC Warning CVC4_PUBLIC;
-NullC Message CVC4_PUBLIC;
-NullC Notice CVC4_PUBLIC;
-NullC Chat CVC4_PUBLIC;
-NullDebugC Trace CVC4_PUBLIC;
+# endif /* CVC4_TRACING */
#endif /* ! CVC4_MUZZLE */
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Output utility classes and functions.
+ ** \brief Output utility classes and functions
**
** Output utility classes and functions.
**/
/** A null output stream singleton */
extern std::ostream null_os CVC4_PUBLIC;
-#ifndef CVC4_MUZZLE
-
class CVC4_PUBLIC CVC4ostream {
std::ostream* d_os;
// Current indentation
/** The debug output singleton */
extern DebugC DebugChannel CVC4_PUBLIC;
-#ifdef CVC4_DEBUG
-# define Debug ::CVC4::DebugChannel
-#else /* CVC4_DEBUG */
-# define Debug ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::DebugChannel
-#endif /* CVC4_DEBUG */
-
/** The warning output singleton */
-extern WarningC Warning CVC4_PUBLIC;
-#define Warning() (! ::CVC4::Warning.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Warning()
-
+extern WarningC WarningChannel CVC4_PUBLIC;
/** The message output singleton */
-extern MessageC Message CVC4_PUBLIC;
-#define Message() (! ::CVC4::Message.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Message()
-
+extern MessageC MessageChannel CVC4_PUBLIC;
/** The notice output singleton */
-extern NoticeC Notice CVC4_PUBLIC;
-#define Notice() (! ::CVC4::Notice.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Notice()
-
+extern NoticeC NoticeChannel CVC4_PUBLIC;
/** The chat output singleton */
-extern ChatC Chat CVC4_PUBLIC;
-#define Chat() (! ::CVC4::Chat.isOn()) ? ::CVC4::debugNullCvc4Stream : ::CVC4::Chat()
-
+extern ChatC ChatChannel CVC4_PUBLIC;
/** The trace output singleton */
extern TraceC TraceChannel CVC4_PUBLIC;
-#ifdef CVC4_TRACING
-# define Trace ::CVC4::TraceChannel
-#else /* CVC4_TRACING */
-# define Trace ::CVC4::__cvc4_true() ? ::CVC4::debugNullCvc4Stream : ::CVC4::TraceChannel
-#endif /* CVC4_TRACING */
+
+#ifdef CVC4_MUZZLE
+
+# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+# define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+# define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+# define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+# define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int WarningC::printf(const char* fmt, ...) { return 0; }
+inline int MessageC::printf(const char* fmt, ...) { return 0; }
+inline int NoticeC::printf(const char* fmt, ...) { return 0; }
+inline int ChatC::printf(const char* fmt, ...) { return 0; }
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+
+#else /* CVC4_MUZZLE */
+
+# ifdef CVC4_DEBUG
+# define Debug ::CVC4::DebugChannel
+# else /* CVC4_DEBUG */
+# define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+# endif /* CVC4_DEBUG */
+# define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+# define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+# define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+# define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+# ifdef CVC4_TRACING
+# define Trace ::CVC4::TraceChannel
+# else /* CVC4_TRACING */
+# define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+# endif /* CVC4_TRACING */
+
+#endif /* CVC4_MUZZLE */
// Disallow e.g. !Debug("foo").isOn() forms
// because the ! will apply before the ? .
#endif /* CVC4_TRACING */
-#else /* ! CVC4_MUZZLE */
-
-class CVC4_PUBLIC ScopedDebug {
-public:
- ScopedDebug(std::string tag, bool newSetting = true) {}
- ScopedDebug(const char* tag, bool newSetting = true) {}
-};/* class ScopedDebug */
-
-class CVC4_PUBLIC ScopedTrace {
-public:
- ScopedTrace(std::string tag, bool newSetting = true) {}
- ScopedTrace(const char* tag, bool newSetting = true) {}
-};/* class ScopedTrace */
-
-extern NullDebugC Debug CVC4_PUBLIC;
-extern NullC Warning CVC4_PUBLIC;
-extern NullC Message CVC4_PUBLIC;
-extern NullC Notice CVC4_PUBLIC;
-extern NullC Chat CVC4_PUBLIC;
-extern NullDebugC Trace CVC4_PUBLIC;
-
-#endif /* ! CVC4_MUZZLE */
-
/**
- * Same shape as DebugC/TraceC, but does nothing; designed for
- * compilation of non-debug/non-trace builds. None of these should ever be called
- * in such builds, but we offer this to the compiler so it doesn't complain.
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds. None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
*/
-class CVC4_PUBLIC NullDebugC {
-public:
- operator bool() { return false; }
- operator CVC4ostream() { return CVC4ostream(); }
- operator std::ostream&() { return null_os; }
-};/* class NullDebugC */
-
-/**
- * Same shape as WarningC/etc., but does nothing; designed for
- * compilation of muzzled builds. None of these should ever be called
- * in muzzled builds, but we offer this to the compiler so it doesn't
- * complain. */
class CVC4_PUBLIC NullC {
public:
-/*
- NullC() {}
- NullC(std::ostream* os) {}
-
- int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { return 0; }
-
- std::ostream& operator()() { return null_os; }
-
- std::ostream& setStream(std::ostream& os) { return null_os; }
- std::ostream& getStream() { return null_os; }
-*/
operator bool() { return false; }
operator CVC4ostream() { return CVC4ostream(); }
operator std::ostream&() { return null_os; }
};/* class NullC */
-extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
extern NullC nullCvc4Stream CVC4_PUBLIC;
}/* CVC4 namespace */
void tearDown() {
delete d_exprManager;
}
-};
+};/* class ParserBlack */
-class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
+class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
public:
}
void testBadCvc4Inputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadInput("ASSERT;"); // no args
tryBadInput("QUERY");
tryBadInput("CHECKSAT");
tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;");
tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;");
tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodCvc4Exprs() {
}
void testBadCvc4Exprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadInput("a AND"); // wrong arity
tryBadInput("AND(a,b)"); // not infix
tryBadInput("(OR (AND a b) c)"); // not infix
tryBadInput("a IMPLIES b"); // should be =>
tryBadInput("a NOT b"); // wrong arity, not infix
tryBadInput("a and b"); // wrong case
+#endif /* ! CVC4_COMPETITION_MODE */
}
-};
+};/* class Cvc4ParserTest */
class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
}
void testBadSmtInputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadInput("(benchmark foo)"); // empty benchmark is not OK
tryBadInput("(benchmark bar :assumption)"); // no args
tryBadInput("(benchmark bar :formula)");
tryBadInput("(benchmark baz :extrapreds ( (a) (a) ) )"); // double decl
tryBadInput("(benchmark zub :extrasorts (a) :extrapreds (p a))"); // (p a) needs parens
+#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodSmtExprs() {
}
void testBadSmtExprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadExpr("(and)"); // wrong arity
tryBadExpr("(and a b"); // no closing paren
tryBadExpr("(a and b)"); // infix
tryBadExpr("(a b)"); // using non-function as function
tryBadExpr(".5"); // rational constants must have integer prefix
tryBadExpr("1."); // rational constants must have fractional suffix
+#endif /* ! CVC4_COMPETITION_MODE */
}
-};
+};/* class SmtParserTest */
class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
typedef ParserBlack super;
}
void testBadSmt2Inputs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadInput("(assert)"); // no args
tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg
// strict mode
tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
+#endif /* ! CVC4_COMPETITION_MODE */
}
void testGoodSmt2Exprs() {
}
void testBadSmt2Exprs() {
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
tryBadExpr("(and)"); // wrong arity
tryBadExpr("(and a b"); // no closing paren
tryBadExpr("(a and b)"); // infix
tryBadExpr("(and a)", true); // no unary and's
tryBadExpr("(or a)", true); // no unary or's
tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant
+#endif /* ! CVC4_COMPETITION_MODE */
}
-};
+};/* class Smt2ParserTest */
}
- static int expensiveFunction() {
+ static int failure() {
// this represents an expensive function that should NOT be called
// when debugging/tracing is turned off
- TS_FAIL("a function was evaluated under Debug() or Trace() when it should not have been");
+ TS_FAIL("a function was evaluated under an output operation when it should not have been");
return 0;
}
- void testEvaluationOffWhenItsSupposedToBe() {
+ void testEvaluationOffWhenItIsSupposedToBe() {
+ Debug.on("foo");
+#ifndef CVC4_DEBUG
+ TS_ASSERT( !( Debug.isOn("foo") ) );
+ Debug("foo") << failure() << endl;
+ Debug.printf("foo", "%d\n", failure());
+#else /* ! CVC4_DEBUG */
+ TS_ASSERT( Debug.isOn("foo") );
+#endif /* ! CVC4_DEBUG */
+ Debug.off("foo");
+ //Debug("foo") << failure() << endl;
+ //Debug.printf("foo", "%d\n", failure());
+
Trace.on("foo");
#ifndef CVC4_TRACING
TS_ASSERT( !( Trace.isOn("foo") ) );
- Trace("foo") << expensiveFunction() << endl;
-#else /* CVC4_TRACING */
+ Trace("foo") << failure() << endl;
+ Trace.printf("foo", "%d\n", failure());
+#else /* ! CVC4_TRACING */
TS_ASSERT( Trace.isOn("foo") );
-#endif /* CVC4_TRACING */
+#endif /* ! CVC4_TRACING */
+ Trace.off("foo");
+ //Trace("foo") << failure() << endl;
+ //Trace.printf("foo", "%d\n", failure());
- Debug.on("foo");
-#ifndef CVC4_DEBUG
+#ifdef CVC4_MUZZLE
TS_ASSERT( !( Debug.isOn("foo") ) );
- Debug("foo") << expensiveFunction() << endl;
-#else /* CVC4_DEBUG */
- TS_ASSERT( Debug.isOn("foo") );
-#endif /* CVC4_DEBUG */
+ TS_ASSERT( !( Trace.isOn("foo") ) );
+ TS_ASSERT( !( Warning.isOn() ) );
+ TS_ASSERT( !( Message.isOn() ) );
+ TS_ASSERT( !( Notice.isOn() ) );
+ TS_ASSERT( !( Chat.isOn() ) );
+
+ cout << "debug" << std::endl;
+ Debug("foo") << failure() << endl;
+ cout << "trace" << std::endl;
+ Trace("foo") << failure() << endl;
+ cout << "warning" << std::endl;
+ Warning() << failure() << endl;
+ cout << "message" << std::endl;
+ Message() << failure() << endl;
+ cout << "notice" << std::endl;
+ Notice() << failure() << endl;
+ cout << "chat" << std::endl;
+ Chat() << failure() << endl;
+
+ cout << "debug:printf" << std::endl;
+ Debug.printf("foo", "%d\n", failure());
+ cout << "trace:printf" << std::endl;
+ Trace.printf("foo", "%d\n", failure());
+ cout << "warning:printf" << std::endl;
+ Warning.printf("%d\n", failure());
+ cout << "message:printf" << std::endl;
+ Message.printf("%d\n", failure());
+ cout << "notice:printf" << std::endl;
+ Notice.printf("%d\n", failure());
+ cout << "chat:printf" << std::endl;
+ Chat.printf("%d\n", failure());
+#endif /* CVC4_MUZZLE */
}
void testSimplePrint() {
#ifdef CVC4_MUZZLE
Debug.off("yo");
- Debug("yo", "foobar");
+ Debug("yo") << "foobar";
TS_ASSERT_EQUALS(d_debugStream.str(), string());
d_debugStream.str("");
Debug.on("yo");
- Debug("yo", "baz foo");
+ Debug("yo") << "baz foo";
TS_ASSERT_EQUALS(d_debugStream.str(), string());
d_debugStream.str("");
Trace.off("yo");
- Trace("yo", "foobar");
+ Trace("yo") << "foobar";
TS_ASSERT_EQUALS(d_traceStream.str(), string());
d_traceStream.str("");
Trace.on("yo");
- Trace("yo", "baz foo");
+ Trace("yo") << "baz foo";
TS_ASSERT_EQUALS(d_traceStream.str(), string());
d_traceStream.str("");
- Warning("baz foo");
+ Warning() << "baz foo";
TS_ASSERT_EQUALS(d_warningStream.str(), string());
d_warningStream.str("");
- Chat("baz foo");
+ Chat() << "baz foo";
TS_ASSERT_EQUALS(d_chatStream.str(), string());
d_chatStream.str("");
- Message("baz foo");
+ Message() << "baz foo";
TS_ASSERT_EQUALS(d_messageStream.str(), string());
d_messageStream.str("");
- Notice("baz foo");
+ Notice() << "baz foo";
TS_ASSERT_EQUALS(d_noticeStream.str(), string());
d_noticeStream.str("");
public:
void testStats() {
-
+#ifdef CVC4_STATISTICS_ON
// StatisticsRegistry
//static void flushStatistics(std::ostream& out);
TS_ASSERT_EQUALS(zero, sTimer.getData());
sTimer.stop();
TS_ASSERT_LESS_THAN(zero, sTimer.getData());
+#endif /* CVC4_STATISTICS_ON */
}
};
projects / cvc5.git / commitdiff