summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/command.cpp8
-rw-r--r--src/expr/command.h7
-rw-r--r--src/expr/expr_manager_template.cpp14
-rw-r--r--src/expr/expr_template.cpp9
-rw-r--r--src/expr/expr_template.h13
-rw-r--r--src/expr/pickler.cpp9
-rw-r--r--src/expr/pickler.h12
-rw-r--r--src/main/command_executor.h6
-rw-r--r--src/main/command_executor_portfolio.cpp69
-rw-r--r--src/main/command_executor_portfolio.h3
-rw-r--r--src/main/portfolio_util.cpp3
-rw-r--r--src/main/portfolio_util.h4
12 files changed, 91 insertions, 66 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 938f28635..a62a9421f 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1273,12 +1273,8 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
}
Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
- throw ExportToUnsupportedException();
- // vector<DatatypeType> params;
- // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params),
- // ExportTransformer(exprManager, variableMap));
- // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params);
- // return c;
+ throw ExportUnsupportedException
+ ("export of DatatypeDeclarationCommand unsupported");
}
Command* DatatypeDeclarationCommand::clone() const {
diff --git a/src/expr/command.h b/src/expr/command.h
index 5786f4e71..e120deed6 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,13 +50,6 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
-class CVC4_PUBLIC ExportToUnsupportedException : public Exception {
-public:
- ExportToUnsupportedException() throw() :
- Exception("exportTo unsupported for command") {
- }
-};/* class ExportToUnsupportedException */
-
/** The status an SMT benchmark can have */
enum BenchmarkStatus {
/** Benchmark is satisfiable */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index be2804fd5..457491445 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -928,13 +928,21 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
Debug("export") << "type: " << n << std::endl;
- Assert(n.getKind() == kind::SORT_TYPE ||
- n.getMetaKind() != kind::metakind::PARAMETERIZED,
- "PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+ if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+ throw ExportUnsupportedException
+ ("export of types belonging to theory of DATATYPES kinds unsupported");
+ }
+ if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
+ n.getKind() != kind::SORT_TYPE) {
+ throw ExportUnsupportedException
+ ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+ }
if(n.getKind() == kind::TYPE_CONSTANT) {
return to->mkTypeConst(n.getConst<TypeConstant>());
} else if(n.getKind() == kind::BITVECTOR_TYPE) {
return to->mkBitVectorType(n.getConst<BitVectorSize>());
+ } else if(n.getKind() == kind::SUBRANGE_TYPE) {
+ return to->mkSubrangeType(n.getSubrangeBounds());
}
Type from_t = from->toType(n);
Type& to_t = vmap.d_typeMap[from_t];
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f39c0e7ea..2f9e27c0c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -114,7 +114,12 @@ namespace expr {
static Node exportConstant(TNode n, NodeManager* to);
Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
- if(n.isConst()) {
+ if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+ throw ExportUnsupportedException
+ ("export of node belonging to theory of DATATYPES kinds unsupported");
+ }
+
+ if(n.getMetaKind() == metakind::CONSTANT) {
return exportConstant(n, NodeManager::fromExprManager(to));
} else if(n.isVar()) {
Expr from_e(from, new Node(n));
@@ -132,7 +137,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
// a check that mkVar isn't called internally
NodeManagerScope nullScope(NULL);
- if(n.getKind() == kind::BOUND_VAR_LIST) {
+ if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) {
to_e = to->mkBoundVar(name, type);// FIXME thread safety
} else if(n.getKind() == kind::VARIABLE) {
to_e = to->mkVar(name, type);// FIXME thread safety
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 96c7cfadf..4255e3454 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -132,6 +132,19 @@ public:
friend class ExprManager;
};/* class TypeCheckingException */
+/**
+ * Exception thrown in case of failure to export
+ */
+class CVC4_PUBLIC ExportUnsupportedException : public Exception {
+public:
+ ExportUnsupportedException() throw():
+ Exception("export unsupported") {
+ }
+ ExportUnsupportedException(const char* msg) throw():
+ Exception(msg) {
+ }
+};/* class DatatypeExportUnsupportedException */
+
std::ostream& operator<<(std::ostream& out,
const TypeCheckingException& e) CVC4_PUBLIC;
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index a41db794d..6548cf98a 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -129,7 +129,7 @@ Pickler::~Pickler() {
}
void Pickler::toPickle(Expr e, Pickle& p)
- throw(AssertionException, PicklingException) {
+ throw(PicklingException) {
Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
Assert(d_private->atDefaultState());
@@ -471,6 +471,13 @@ Pickle::~Pickle() {
delete d_data;
}
+uint64_t MapPickler::variableFromMap(uint64_t x) const
+{
+ VarMap::const_iterator i = d_fromMap.find(x);
+ Assert(i != d_fromMap.end());
+ return i->second;
+}
+
}/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index a6427ad47..dee4f06e6 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -67,7 +67,7 @@ class CVC4_PUBLIC Pickler {
protected:
virtual uint64_t variableToMap(uint64_t x) const
- throw(AssertionException, PicklingException) {
+ throw(PicklingException) {
return x;
}
virtual uint64_t variableFromMap(uint64_t x) const {
@@ -87,7 +87,7 @@ public:
*
* @return the pickle, which should be dispose()'d when you're done with it
*/
- void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException);
+ void toPickle(Expr e, Pickle& p) throw(PicklingException);
/**
* Constructs a node from a Pickle.
@@ -116,7 +116,7 @@ public:
protected:
virtual uint64_t variableToMap(uint64_t x) const
- throw(AssertionException, PicklingException) {
+ throw(PicklingException) {
VarMap::const_iterator i = d_toMap.find(x);
if(i != d_toMap.end()) {
return i->second;
@@ -125,11 +125,7 @@ protected:
}
}
- virtual uint64_t variableFromMap(uint64_t x) const {
- VarMap::const_iterator i = d_fromMap.find(x);
- Assert(i != d_fromMap.end());
- return i->second;
- }
+ virtual uint64_t variableFromMap(uint64_t x) const;
};/* class MapPickler */
}/* CVC4::expr::pickle namespace */
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 435299ce3..a5bd78abe 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -38,14 +38,8 @@ protected:
StatisticsRegistry d_stats;
public:
- // Note: though the options are not cached (instead a reference is
- // used), the portfolio command executer currently parses them
- // during initalization, creating thread-specific options and
- // storing them
CommandExecutor(ExprManager &exprMgr, Options &options);
- ~CommandExecutor() {}
-
/**
* Executes a command. Recursively handles if cmd is a command
* sequence. Eventually uses doCommandSingleton (which can be
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 32a507d78..b9bf39002 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -48,9 +48,13 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
d_lastWinner(0),
d_channelsOut(),
d_channelsIn(),
- d_ostringstreams()
+ d_ostringstreams(),
+ d_statLastWinner("portfolio::lastWinner")
{
- Assert(d_threadOptions.size() == d_numThreads);
+ assert(d_threadOptions.size() == d_numThreads);
+
+ d_statLastWinner.setData(d_lastWinner);
+ d_stats.registerStat_(&d_statLastWinner);
/* Duplication, Individualisation */
d_exprMgrs.push_back(&d_exprMgr);
@@ -64,7 +68,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
}
- Assert(d_vmaps.size() == 0);
+ assert(d_vmaps.size() == 0);
for(unsigned i = 0; i < d_numThreads; ++i) {
d_vmaps.push_back(new ExprManagerMapCollection());
}
@@ -72,15 +76,15 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
CommandExecutorPortfolio::~CommandExecutorPortfolio()
{
- Assert(d_seq != NULL);
+ assert(d_seq != NULL);
delete d_seq;
- Assert(d_smts.size() == d_numThreads);
+ assert(d_smts.size() == d_numThreads);
for(unsigned i = 1; i < d_numThreads; ++i) {
// the 0-th one is responsibility of parent class
- delete d_exprMgrs[i];
delete d_smts[i];
+ delete d_exprMgrs[i];
}
d_exprMgrs.clear();
d_smts.clear();
@@ -89,8 +93,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio()
void CommandExecutorPortfolio::lemmaSharingInit()
{
/* Sharing channels */
- Assert(d_channelsIn.size() == 0);
- Assert(d_channelsOut.size() == 0);
+ assert(d_channelsIn.size() == 0);
+ assert(d_channelsOut.size() == 0);
if(d_numThreads == 1) {
// Disable sharing
@@ -130,10 +134,14 @@ void CommandExecutorPortfolio::lemmaSharingInit()
/* Output to string stream */
if(d_options[options::verbosity] == 0
|| d_options[options::separateOutput]) {
- Assert(d_ostringstreams.size() == 0);
+ assert(d_ostringstreams.size() == 0);
for(unsigned i = 0; i < d_numThreads; ++i) {
d_ostringstreams.push_back(new ostringstream);
d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+
+ // important even for muzzled builds (to get result output right)
+ *d_threadOptions[i][options::out]
+ << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
}
}
}
@@ -141,11 +149,11 @@ void CommandExecutorPortfolio::lemmaSharingInit()
void CommandExecutorPortfolio::lemmaSharingCleanup()
{
- Assert(d_numThreads == d_options[options::threads]);
+ assert(d_numThreads == d_options[options::threads]);
// Channel cleanup
- Assert(d_channelsIn.size() == d_numThreads);
- Assert(d_channelsOut.size() == d_numThreads);
+ assert(d_channelsIn.size() == d_numThreads);
+ assert(d_channelsOut.size() == d_numThreads);
for(unsigned i = 0; i < d_numThreads; ++i) {
delete d_channelsIn[i];
delete d_channelsOut[i];
@@ -157,7 +165,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
// sstreams cleanup (if used)
if(d_ostringstreams.size() != 0) {
- Assert(d_ostringstreams.size() == d_numThreads);
+ assert(d_ostringstreams.size() == d_numThreads);
for(unsigned i = 0; i < d_numThreads; ++i) {
d_threadOptions[i].set(options::out, d_options[options::out]);
delete d_ostringstreams[i];
@@ -180,12 +188,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
// mode = 1 : run a porfolio
// mode = 2 : run the last winner
- // if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
- // dynamic_cast<QueryCommand*>(cmd) != NULL) {
- // mode = 1;
- // } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
- // mode = 2;
- // }
+ if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
+ dynamic_cast<QueryCommand*>(cmd) != NULL) {
+ mode = 1;
+ } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
+ mode = 2;
+ }
if(mode == 0) {
d_seq->addCommand(cmd->clone());
@@ -213,7 +221,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
*/
try {
seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
- }catch(ExportToUnsupportedException& e){
+ }catch(ExportUnsupportedException& e){
return CommandExecutor::doCommandSingleton(cmd);
}
}
@@ -244,9 +252,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
);
}
- Assert(d_channelsIn.size() == d_numThreads);
- Assert(d_channelsOut.size() == d_numThreads);
- Assert(d_smts.size() == d_numThreads);
+ assert(d_channelsIn.size() == d_numThreads);
+ assert(d_channelsOut.size() == d_numThreads);
+ assert(d_smts.size() == d_numThreads);
boost::function<void()>
smFn = boost::bind(sharingManager<ChannelFormat>,
d_numThreads,
@@ -269,9 +277,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
// << std::endl;
if(d_ostringstreams.size() != 0) {
- Assert(d_numThreads == d_options[options::threads]);
- Assert(portfolioReturn.first >= 0);
- Assert(unsigned(portfolioReturn.first) < d_numThreads);
+ assert(d_numThreads == d_options[options::threads]);
+ assert(portfolioReturn.first >= 0);
+ assert(unsigned(portfolioReturn.first) < d_numThreads);
*d_options[options::out]
<< d_ostringstreams[portfolioReturn.first]->str();
@@ -286,7 +294,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
cmd,
d_threadOptions[d_lastWinner][options::out]);
} else {
- Unreachable();
+ // Unreachable();
+ assert(false);
}
}/* CommandExecutorPortfolio::doCommandSingleton() */
@@ -297,15 +306,15 @@ std::string CommandExecutorPortfolio::getSmtEngineStatus()
}
void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
- Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
+ assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
for(size_t i = 0; i < d_numThreads; ++i) {
- string emTag = "ExprManager thread #"
+ string emTag = "thread#"
+ boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
Statistics stats = d_exprMgrs[i]->getStatistics();
stats.setPrefix(emTag);
stats.flushInformation(out);
- string smtTag = "SmtEngine thread #"
+ string smtTag = "thread#"
+ boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
stats = d_smts[i]->getStatistics();
stats.setPrefix(smtTag);
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index 72a677789..867b62d31 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -52,6 +52,9 @@ class CommandExecutorPortfolio : public CommandExecutor {
std::vector< SharedChannel<ChannelFormat>* > d_channelsIn;
std::vector<std::ostringstream*> d_ostringstreams;
+ // Stats
+ ReferenceStat<int> d_statLastWinner;
+
public:
CommandExecutorPortfolio(ExprManager &exprMgr,
Options &options,
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index b208b2479..b16ac2d34 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -14,6 +14,7 @@
** \brief Code relevant only for portfolio builds
**/
+#include <cassert>
#include <vector>
#include <unistd.h>
#include "options/options.h"
@@ -97,7 +98,7 @@ vector<Options> parseThreadSpecificOptions(Options opts)
}
}
- Assert(numThreads >= 1); //do we need this?
+ assert(numThreads >= 1); //do we need this?
return threadOptions;
}
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 1955a29a7..416b9f44a 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -155,7 +155,7 @@ void sharingManager(unsigned numThreads,
/* Alert if channel full, so that we increase sharingChannelSize
or decrease sharingBroadcastInterval */
- Assert(not channelsOut[t]->full());
+ assert(not channelsOut[t]->full());
T data = channelsOut[t]->pop();
@@ -177,7 +177,7 @@ void sharingManager(unsigned numThreads,
for(unsigned t = 0; t < numThreads; ++t){
/* Alert if channel full, so that we increase sharingChannelSize
or decrease sharingBroadcastInterval */
- Assert(not channelsIn[t]->full());
+ assert(not channelsIn[t]->full());
while(!queues[t].empty() && !channelsIn[t]->full()){
Trace("sharing") << "sharing: pushing on channel " << t << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback