Dejan Jovanovic <dejan@cs.nyu.edu> <dejan@cs.nyu.edu>
Dejan Jovanovic <dejan@cs.nyu.edu> <dejan.jovanovic@gmail.com>
Francois Bobot <francois@bobot.eu> <francois@bobot.eu>
+Liana Hadarean <lianah@cs.nyu.edu> <lianah@cs.nyu.edu>
Liana Hadarean <lianah@cs.nyu.edu> <lianahady@gmail.com>
Andrew Reynolds <andrew.j.reynolds@gmail.com> <andrew.j.reynolds@gmail.com>
Andrew Reynolds <andrew.j.reynolds@gmail.com> <reynolds@laraserver2.epfl.ch>
%typemap(throws) CVC4::ScopeException = CVC4::Exception;
%typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
%typemap(throws) CVC4::AssertionException = CVC4::Exception;
+%typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception;
%typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
%typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
#endif /* SWIGJAVA */
%include "util/exception.i"
+%include "util/unsafe_interrupt_exception.i"
%include "util/integer.i"
%include "util/rational.i"
%include "util/language.i"
%include "util/regexp.i"
%include "util/uninterpreted_constant.i"
%include "util/proof.i"
+%include "util/resource_manager.i"
%include "expr/kind.i"
%include "expr/expr.i"
#include "theory/decision_attributes.h"
#include "util/ite_removal.h"
#include "util/output.h"
+#include "smt/smt_engine_scope.h"
using namespace std;
using namespace CVC4::prop;
/** Gets the next decision based on strategies that are enabled */
SatLiteral getNext(bool &stopSearch) {
+ NodeManager::currentResourceManager()->spendResource();
Assert(d_cnfStream != NULL,
"Forgot to set cnfStream for decision engine?");
Assert(d_satSolver != NULL,
const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
+const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted();
std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
c.toStream(out,
return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
}
+bool Command::interrupted() const throw() {
+ return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
+}
+
void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
invoke(smtEngine);
if(!(isMuted() && ok())) {
try {
smtEngine->assertFormula(d_expr, d_inUnsatCore);
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
try {
smtEngine->push();
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
try {
smtEngine->pop();
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
try {
d_result = smtEngine->simplify(d_term);
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
}
d_result = em->mkExpr(kind::SEXPR, result);
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
try {
d_result = smtEngine->getAssignment();
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
d_result = smtEngine->getModel();
d_smtEngine = smtEngine;
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
try {
d_result = smtEngine->getProof();
d_commandStatus = CommandSuccess::instance();
+ } catch(UnsafeInterruptException& e) {
+ d_commandStatus = new CommandInterrupted();
} catch(exception& e) {
d_commandStatus = new CommandFailure(e.what());
}
CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
};/* class CommandSuccess */
+class CVC4_PUBLIC CommandInterrupted : public CommandStatus {
+ static const CommandInterrupted* s_instance;
+public:
+ static const CommandInterrupted* instance() throw() { return s_instance; }
+ CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); }
+};/* class CommandInterrupted */
+
class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
public:
CommandStatus& clone() const { return *new CommandUnsupported(*this); }
*/
bool fail() const throw();
+ /**
+ * The command was ran but was interrupted due to resource limiting.
+ */
+ bool interrupted() const throw();
+
/** Get the command status (it's NULL if we haven't run yet). */
const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
return d_nodeManager->getOptions();
}
+ResourceManager* ExprManager::getResourceManager() throw() {
+ return d_nodeManager->getResourceManager();
+}
+
BooleanType ExprManager::booleanType() const {
NodeManagerScope nms(d_nodeManager);
return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
class IntStat;
struct ExprManagerMapCollection;
class StatisticsRegistry;
+class ResourceManager;
namespace expr {
namespace pickle {
*/
~ExprManager() throw();
- /** Get this node manager's options */
+ /** Get this expr manager's options */
const Options& getOptions() const;
+ /** Get this expr manager's resource manager */
+ ResourceManager* getResourceManager() throw();
+
/** Get the type for booleans */
BooleanType booleanType() const;
#include "expr/attribute.h"
#include "util/cvc4_assert.h"
#include "options/options.h"
+#include "smt/options.h"
#include "util/statistics_registry.h"
+#include "util/resource_manager.h"
#include "util/tls.h"
#include "expr/type_checker.h"
NodeManager::NodeManager(ExprManager* exprManager) :
d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
+ d_resourceManager(new ResourceManager()),
next_id(0),
d_attrManager(new expr::attr::AttributeManager()),
d_exprManager(exprManager),
const Options& options) :
d_options(new Options(options)),
d_statisticsRegistry(new StatisticsRegistry()),
+ d_resourceManager(new ResourceManager()),
next_id(0),
d_attrManager(new expr::attr::AttributeManager()),
d_exprManager(exprManager),
d_operators[i] = mkConst(Kind(k));
}
}
+ d_resourceManager->setHardLimit((*d_options)[options::hardLimit]);
+ if((*d_options)[options::perCallResourceLimit] != 0) {
+ d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false);
+ }
+ if((*d_options)[options::cumulativeResourceLimit] != 0) {
+ d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true);
+ }
+ if((*d_options)[options::perCallMillisecondLimit] != 0) {
+ d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false);
+ }
+ if((*d_options)[options::cumulativeMillisecondLimit] != 0) {
+ d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true);
+ }
+ if((*d_options)[options::cpuTime]) {
+ d_resourceManager->useCPUTime(true);
+ }
}
NodeManager::~NodeManager() {
// defensive coding, in case destruction-order issues pop up (they often do)
delete d_statisticsRegistry;
d_statisticsRegistry = NULL;
+ delete d_resourceManager;
+ d_resourceManager = NULL;
delete d_attrManager;
d_attrManager = NULL;
delete d_options;
namespace CVC4 {
class StatisticsRegistry;
+class ResourceManager;
namespace expr {
namespace attr {
Options* d_options;
StatisticsRegistry* d_statisticsRegistry;
+ ResourceManager* d_resourceManager;
NodeValuePool d_nodeValuePool;
/** The node manager in the current public-facing CVC4 library context */
static NodeManager* currentNM() { return s_current; }
+ /** The resource manager associated with the current node manager */
+ static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
/** Get this node manager's options (const version) */
const Options& getOptions() const {
return *d_options;
}
+ /** Get this node manager's resource manager */
+ ResourceManager* getResourceManager() throw() { return d_resourceManager; }
+
/** Get this node manager's statistics registry */
StatisticsRegistry* getStatisticsRegistry() const throw() {
return d_statisticsRegistry;
// have the replay parser use the declarations input interactively
replayParser->useDeclarationsFrom(shell.getParser());
}
- while((cmd = shell.readCommand())) {
+
+ while(true) {
+ try {
+ cmd = shell.readCommand();
+ } catch(UnsafeInterruptException& e) {
+ *opts[options::out] << CommandInterrupted();
+ break;
+ }
+ if (cmd == NULL)
+ break;
status = pExecutor->doCommand(cmd) && status;
+ if (cmd->interrupted()) {
+ delete cmd;
+ break;
+ }
delete cmd;
}
} else if(opts[options::tearDownIncremental]) {
replayParser->useDeclarationsFrom(parser);
}
bool needReset = false;
- while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
+ // true if one of the commands was interrupted
+ bool interrupted = false;
+ while (status || opts[options::continuedExecution]) {
+ if (interrupted) {
+ *opts[options::out] << CommandInterrupted();
+ break;
+ }
+
+ try {
+ cmd = parser->nextCommand();
+ if (cmd == NULL) break;
+ } catch (UnsafeInterruptException& e) {
+ interrupted = true;
+ continue;
+ }
+
if(dynamic_cast<PushCommand*>(cmd) != NULL) {
if(needReset) {
pExecutor->reset();
- for(size_t i = 0; i < allCommands.size(); ++i) {
- for(size_t j = 0; j < allCommands[i].size(); ++j) {
+ for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+ if (interrupted) break;
+ for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
Command* cmd = allCommands[i][j]->clone();
cmd->setMuted(true);
pExecutor->doCommand(cmd);
+ if(cmd->interrupted()) {
+ interrupted = true;
+ }
delete cmd;
}
}
} else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
allCommands.pop_back(); // fixme leaks cmds here
pExecutor->reset();
- for(size_t i = 0; i < allCommands.size(); ++i) {
- for(size_t j = 0; j < allCommands[i].size(); ++j) {
+ for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+ for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
Command* cmd = allCommands[i][j]->clone();
cmd->setMuted(true);
pExecutor->doCommand(cmd);
+ if(cmd->interrupted()) {
+ interrupted = true;
+ }
delete cmd;
}
}
+ if (interrupted) continue;
*opts[options::out] << CommandSuccess();
} else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
dynamic_cast<QueryCommand*>(cmd) != NULL) {
if(needReset) {
pExecutor->reset();
- for(size_t i = 0; i < allCommands.size(); ++i) {
- for(size_t j = 0; j < allCommands[i].size(); ++j) {
+ for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
+ for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) {
Command* cmd = allCommands[i][j]->clone();
cmd->setMuted(true);
pExecutor->doCommand(cmd);
+ if(cmd->interrupted()) {
+ interrupted = true;
+ }
delete cmd;
}
}
}
+ if (interrupted) {
+ continue;
+ }
+
status = pExecutor->doCommand(cmd);
+ if(cmd->interrupted()) {
+ interrupted = true;
+ continue;
+ }
needReset = true;
} else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
pExecutor->doCommand(cmd);
allCommands.back().push_back(copy);
}
status = pExecutor->doCommand(cmd);
+ if(cmd->interrupted()) {
+ interrupted = true;
+ continue;
+ }
+
if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
delete cmd;
break;
// have the replay parser use the file's declarations
replayParser->useDeclarationsFrom(parser);
}
- while((status || opts[options::continuedExecution]) && (cmd = parser->nextCommand())) {
+ bool interrupted = false;
+ while(status || opts[options::continuedExecution]) {
+ if (interrupted) {
+ *opts[options::out] << CommandInterrupted();
+ pExecutor->reset();
+ break;
+ }
+ try {
+ cmd = parser->nextCommand();
+ if (cmd == NULL) break;
+ } catch (UnsafeInterruptException& e) {
+ interrupted = true;
+ continue;
+ }
+
status = pExecutor->doCommand(cmd);
+ if (cmd->interrupted() && status == 0) {
+ interrupted = true;
+ break;
+ }
+
if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
delete cmd;
break;
#endif /* HAVE_LIBREADLINE */
}
-Command* InteractiveShell::readCommand() {
+Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) {
char* lineBuf = NULL;
string line = "";
#include <string>
#include "util/language.h"
+#include "util/unsafe_interrupt_exception.h"
#include "options/options.h"
namespace CVC4 {
* Read a command from the interactive shell. This will read as
* many lines as necessary to parse a well-formed command.
*/
- Command* readCommand();
+ Command* readCommand() throw (UnsafeInterruptException);
/**
* Return the internal parser being used.
#include "parser/parser_exception.h"
#include "expr/command.h"
#include "expr/expr.h"
+#include "expr/node.h"
#include "expr/kind.h"
#include "expr/type.h"
#include "util/output.h"
+#include "util/resource_manager.h"
+#include "options/options.h"
using namespace std;
using namespace CVC4::kind;
Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
d_exprManager(exprManager),
+ d_resourceManager(d_exprManager->getResourceManager()),
d_input(input),
d_symtabAllocated(),
d_symtab(&d_symtabAllocated),
d_commandQueue.push_back(cmd);
}
-Command* Parser::nextCommand() throw(ParserException) {
+Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) {
Debug("parser") << "nextCommand()" << std::endl;
Command* cmd = NULL;
if(!d_commandQueue.empty()) {
}
}
Debug("parser") << "nextCommand() => " << cmd << std::endl;
+ if (cmd != NULL &&
+ dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
+ dynamic_cast<QuitCommand*>(cmd) == NULL) {
+ // don't count set-option commands as to not get stuck in an infinite
+ // loop of resourcing out
+ d_resourceManager->spendResource();
+ }
return cmd;
}
-Expr Parser::nextExpression() throw(ParserException) {
+Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
Debug("parser") << "nextExpression()" << std::endl;
+ d_resourceManager->spendResource();
Expr result;
if(!done()) {
try {
#include "expr/symbol_table.h"
#include "expr/kind.h"
#include "expr/expr_stream.h"
+#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
class Command;
class FunctionType;
class Type;
+class ResourceManager;
namespace parser {
/** The expression manager */
ExprManager *d_exprManager;
+ /** The resource manager associated with this expr manager */
+ ResourceManager *d_resourceManager;
/** The input that we're parsing. */
Input *d_input;
bool isPredicate(const std::string& name);
/** Parse and return the next command. */
- Command* nextCommand() throw(ParserException);
+ Command* nextCommand() throw(ParserException, UnsafeInterruptException);
/** Parse and return the next expression. */
- Expr nextExpression() throw(ParserException);
+ Expr nextExpression() throw(ParserException, UnsafeInterruptException);
/** Issue a warning to the user. */
inline void warning(const std::string& msg) {
if(tryToStream<CommandSuccess>(out, s) ||
tryToStream<CommandFailure>(out, s) ||
- tryToStream<CommandUnsupported>(out, s)) {
+ tryToStream<CommandUnsupported>(out, s) ||
+ tryToStream<CommandInterrupted>(out, s)) {
return;
}
}
}
+static void toStream(std::ostream& out, const CommandInterrupted* s) throw() {
+ out << "INTERRUPTED" << endl;
+}
+
static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
out << "UNSUPPORTED" << endl;
}
if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
- tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)) {
+ tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) ||
+ tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) {
return;
}
out << "UNSUPPORTED" << endl;
}
+static void toStream(std::ostream& out, const CommandInterrupted* s, bool cvc3Mode) throw() {
+ out << "INTERRUPTED" << endl;
+}
+
static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
out << s->getMessage() << endl;
}
if(tryToStream<CommandSuccess>(out, s, d_variant) ||
tryToStream<CommandFailure>(out, s, d_variant) ||
- tryToStream<CommandUnsupported>(out, s, d_variant)) {
+ tryToStream<CommandUnsupported>(out, s, d_variant) ||
+ tryToStream<CommandInterrupted>(out, s, d_variant)) {
return;
}
}
}
+static void toStream(std::ostream& out, const CommandInterrupted* s, Variant v) throw() {
+ out << "interrupted" << endl;
+}
+
static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) throw() {
#ifdef CVC4_COMPETITION_MODE
// if in competition mode, lie and say we're ok
d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
}
-bool BVMinisatSatSolver::spendResource(){
- // Do nothing for the BV solver.
- return false;
-}
void BVMinisatSatSolver::interrupt(){
d_minisat->interrupt();
d_notify->notify(satClause);
}
+ void spendResource() {
+ d_notify->spendResource();
+ }
void safePoint() {
- d_notify->safePoint();
+ d_notify->safePoint();
}
};
void markUnremovable(SatLiteral lit);
- bool spendResource();
-
void interrupt();
SatValue solve();
*/
virtual void notify(vec<Lit>& learnt) = 0;
+ virtual void spendResource() = 0;
virtual void safePoint() = 0;
};
inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
inline bool Solver::withinBudget() const {
- Assert (notify);
- notify->safePoint();
+ Assert (notify);
+ notify->spendResource();
+ notify->safePoint();
+
return !asynch_interrupt &&
(conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
(propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
#include "prop/minisat/minisat.h"
+#include "smt/smt_engine_scope.h"
#include <queue>
using namespace std;
void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+ if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
+ NodeManager::currentResourceManager()->spendResource();
+ d_convertAndAssertCounter = 0;
+ }
+ ++d_convertAndAssertCounter;
+
switch(node.getKind()) {
case AND:
convertAndAssertAnd(node, negated);
*/
const bool d_fullLitToNodeMap;
+ /**
+ * Counter for resource limiting that is used to spend a resource
+ * every ResourceManager::resourceCounter calls to convertAndAssert.
+ */
+ unsigned long d_convertAndAssertCounter;
+
/** The "registrar" for pre-registration of terms */
Registrar* d_registrar;
Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
// Avoid adding lemmas indefinitely without resource-out
- spendResource();
+ proxy->spendResource();
CRef conflict = CRef_Undef;
return conflict;
}
+
+inline bool Solver::withinBudget() const {
+ Assert (proxy);
+ // spendResource sets async_interrupt or throws UnsafeInterruptException
+ // depending on whether hard-limit is enabled
+ proxy->spendResource();
+
+ bool within_budget = !asynch_interrupt &&
+ (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+ (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
+ return within_budget;
+}
void budgetOff();
void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
void clearInterrupt(); // Clear interrupt indicator flag.
- void spendResource();
// Memory managment:
//
inline void Solver::interrupt(){ asynch_interrupt = true; }
inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
-inline bool Solver::withinBudget() const {
- return !asynch_interrupt &&
- (conflict_budget < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) &&
- (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
-inline void Solver::spendResource() { ++resources_consumed; }
// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
return toSatLiteralValue(d_minisat->solve());
}
-bool MinisatSatSolver::spendResource() {
- d_minisat->spendResource();
- return !d_minisat->withinBudget();
-}
void MinisatSatSolver::interrupt() {
d_minisat->interrupt();
SatValue solve();
SatValue solve(long unsigned int&);
- bool spendResource();
void interrupt();
SatValue value(SatLiteral l);
#include "main/options.h"
#include "util/output.h"
#include "util/result.h"
+#include "util/resource_manager.h"
#include "expr/expr.h"
#include "expr/command.h"
d_satSolver(NULL),
d_registrar(NULL),
d_cnfStream(NULL),
- d_satTimer(*this),
- d_interrupted(false) {
+ d_interrupted(false),
+ d_resourceManager(NodeManager::currentResourceManager()) {
Debug("prop") << "Constructing the PropEngine" << endl;
}
}
-Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
+Result PropEngine::checkSat() {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "PropEngine::checkSat()" << endl;
d_theoryEngine->presolve();
if(options::preprocessOnly()) {
- millis = resource = 0;
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
- // Set the timer
- d_satTimer.set(millis);
-
// Reset the interrupted flag
d_interrupted = false;
// Check the problem
- SatValue result = d_satSolver->solve(resource);
-
- millis = d_satTimer.elapsed();
+ SatValue result = d_satSolver->solve();
if( result == SAT_VALUE_UNKNOWN ) {
- Result::UnknownExplanation why =
- d_satTimer.expired() ? Result::TIMEOUT :
- (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
+
+ Result::UnknownExplanation why = Result::INTERRUPTED;
+ if (d_resourceManager->outOfTime())
+ why = Result::TIMEOUT;
+ if (d_resourceManager->outOfResources())
+ why = Result::RESOURCEOUT;
+
return Result(Result::SAT_UNKNOWN, why);
}
d_interrupted = true;
d_satSolver->interrupt();
- d_theoryEngine->interrupt();
Debug("prop") << "interrupt()" << endl;
}
-void PropEngine::spendResource() throw() {
- if(d_satSolver->spendResource()) {
- d_satSolver->interrupt();
- d_theoryEngine->interrupt();
- }
- checkTime();
+void PropEngine::spendResource() throw (UnsafeInterruptException) {
+ d_resourceManager->spendResource();
}
bool PropEngine::properExplanation(TNode node, TNode expl) const {
#include "expr/node.h"
#include "options/options.h"
#include "util/result.h"
+#include "util/unsafe_interrupt_exception.h"
#include "smt/modal_exception.h"
#include "proof/proof_manager.h"
#include <sys/time.h>
namespace CVC4 {
+class ResourceManager;
class DecisionEngine;
class TheoryEngine;
class PropEngine;
-/**
- * A helper class to keep track of a time budget and signal
- * the PropEngine when the budget expires.
- */
-class SatTimer {
-
- PropEngine& d_propEngine;
- unsigned long d_ms;
- timeval d_limit;
-
-public:
-
- /** Construct a SatTimer attached to the given PropEngine. */
- SatTimer(PropEngine& propEngine) :
- d_propEngine(propEngine),
- d_ms(0) {
- }
-
- /** Is the timer currently active? */
- bool on() const {
- return d_ms != 0;
- }
-
- /** Set a millisecond timer (0==off). */
- void set(unsigned long millis) {
- d_ms = millis;
- // keep track of when it was set, even if it's disabled (i.e. == 0)
- Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
- gettimeofday(&d_limit, NULL);
- Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- d_limit.tv_sec += millis / 1000;
- d_limit.tv_usec += (millis % 1000) * 1000;
- if(d_limit.tv_usec > 1000000) {
- ++d_limit.tv_sec;
- d_limit.tv_usec -= 1000000;
- }
- Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- }
-
- /** Return the milliseconds elapsed since last set(). */
- unsigned long elapsed() {
- timeval tv;
- gettimeofday(&tv, NULL);
- Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
- tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
- Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- return tv.tv_sec * 1000 + tv.tv_usec / 1000;
- }
-
- bool expired() {
- if(on()) {
- timeval tv;
- gettimeofday(&tv, NULL);
- Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
- if(d_limit.tv_sec < tv.tv_sec ||
- (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
- Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
- return true;
- } else {
- Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
- }
- }
- return false;
- }
-
- /** Check the current time and signal the PropEngine if over-time. */
- void check();
-
-};/* class SatTimer */
-
/**
* PropEngine is the abstraction of a Sat Solver, providing methods for
* solving the SAT problem and conversion to CNF (via the CnfStream).
/** The CNF converter in use */
CnfStream* d_cnfStream;
- /** A timer for SAT calls */
- SatTimer d_satTimer;
-
/** Whether we were just interrupted (or not) */
bool d_interrupted;
+ /** Pointer to resource manager for associated SmtEngine */
+ ResourceManager* d_resourceManager;
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
/**
* Checks the current context for satisfiability.
*
- * @param millis the time limit for this call in milliseconds
- * (0==off); on output, it is set to the milliseconds used
- * @param on input, resource the number of resource units permitted
- * for this call (0==off); on output, it is set to the resource used
*/
- Result checkSat(unsigned long& millis, unsigned long& resource);
+ Result checkSat();
/**
* Get the value of a boolean variable.
*/
bool isRunning() const;
- /**
- * Check the current time budget.
- */
- void checkTime();
-
/**
* Interrupt a running solver (cause a timeout).
*/
void interrupt() throw(ModalException);
/**
- * "Spend" a "resource." If the sum of these externally-counted
- * resources and SAT-internal resources exceed the current limit,
- * SAT should terminate.
+ * Informs the ResourceManager that a resource has been spent. If out of
+ * resources, can throw an UnsafeInterruptException exception.
*/
- void spendResource() throw();
+ void spendResource() throw (UnsafeInterruptException);
/**
* For debugging. Return true if "expl" is a well-formed
};/* class PropEngine */
-inline void SatTimer::check() {
- if(d_propEngine.isRunning() && expired()) {
- Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
- d_propEngine.interrupt();
- }
-}
-
-inline void PropEngine::checkTime() {
- d_satTimer.check();
-}
-
}/* CVC4::prop namespace */
}/* CVC4 namespace */
/** Check the satisfiability of the added clauses */
virtual SatValue solve(long unsigned int&) = 0;
- /**
- * Instruct the solver that it should bump its consumed resource count.
- * Returns true if resources are exhausted.
- */
- virtual bool spendResource() = 0;
-
/** Interrupt the solver */
virtual void interrupt() = 0;
* Notify about a learnt clause.
*/
virtual void notify(SatClause& clause) = 0;
+ virtual void spendResource() = 0;
virtual void safePoint() = 0;
};/* class BVSatSolverInterface::Notify */
}
void TheoryProxy::notifyRestart() {
- d_propEngine->checkTime();
+ d_propEngine->spendResource();
d_theoryEngine->notifyRestart();
static uint32_t lemmaCount = 0;
#endif /* CVC4_REPLAY */
}
-void TheoryProxy::checkTime() {
- d_propEngine->checkTime();
+void TheoryProxy::spendResource() {
+ d_theoryEngine->spendResource();
}
bool TheoryProxy::isDecisionRelevant(SatVariable var) {
void logDecision(SatLiteral lit);
- void checkTime();
+ void spendResource();
bool isDecisionEngineDone();
option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
set the diagnostic output channel of the solver
-common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
+common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h"
enable time limiting (give milliseconds)
-common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long"
+common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h"
enable time limiting per query (give milliseconds)
-common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
+common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h"
enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h"
enable resource limiting per query
+common-option hardLimit hard-limit --hard-limit bool :default false
+ the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
+common-option cpuTime cpu-time --cpu-time bool :default false
+ measures CPU time if set to true and wall time if false (default false)
expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
#include "cvc4autoconfig.h"
#include "util/dump.h"
+#include "util/resource_manager.h"
#include "smt/modal_exception.h"
#include "smt/smt_engine.h"
#include "lib/strtok_r.h"
#endif /* CVC4_STATISTICS_ON */
}
+inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ unsigned long ms;
+ std::istringstream convert(optarg);
+ if (!(convert >> ms))
+ throw OptionException("option `"+option+"` requires a number as an argument");
+
+ // make sure the resource is set if the option is updated
+ // if the smt engine is null the resource will be set in the
+ if (smt != NULL) {
+ ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+ rm->setTimeLimit(ms, true);
+ }
+ return ms;
+}
+
+inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ unsigned long ms;
+
+ std::istringstream convert(optarg);
+ if (!(convert >> ms))
+ throw OptionException("option `"+option+"` requires a number as an argument");
+
+ if (smt != NULL) {
+ ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+ rm->setTimeLimit(ms, false);
+ }
+ return ms;
+}
+
+inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ unsigned long ms;
+
+ std::istringstream convert(optarg);
+ if (!(convert >> ms))
+ throw OptionException("option `"+option+"` requires a number as an argument");
+
+ if (smt != NULL) {
+ ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+ rm->setResourceLimit(ms, true);
+ }
+ return ms;
+}
+
+inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+ unsigned long ms;
+
+ std::istringstream convert(optarg);
+ if (!(convert >> ms))
+ throw OptionException("option `"+option+"` requires a number as an argument");
+
+ if (smt != NULL) {
+ ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
+ rm->setResourceLimit(ms, false);
+ }
+ return ms;
+}
+
}/* CVC4::smt namespace */
}/* CVC4 namespace */
#include "main/options.h"
#include "util/unsat_core.h"
#include "util/proof.h"
+#include "util/resource_manager.h"
#include "proof/proof.h"
#include "proof/proof_manager.h"
#include "util/boolean_simplification.h"
*/
class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
+ /**
+ * Manager for limiting time and abstract resource usage.
+ */
+ ResourceManager* d_resourceManager;
/** Learned literals */
vector<Node> d_nonClausalLearnedLiterals;
*
* Returns false if the formula simplifies to "false"
*/
- bool simplifyAssertions() throw(TypeCheckingException, LogicException);
+ bool simplifyAssertions() throw(TypeCheckingException, LogicException, UnsafeInterruptException);
public:
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
+ d_resourceManager(NULL),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
d_booleanTermConverter(NULL),
{
d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
+ d_resourceManager = NodeManager::currentResourceManager();
}
~SmtEnginePrivate() {
d_smt.d_nodeManager->unsubscribeEvents(this);
}
+ ResourceManager* getResourceManager() { return d_resourceManager; }
+ void spendResource() throw(UnsafeInterruptException) {
+ d_resourceManager->spendResource();
+ }
+
void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
0,
* Expand definitions in n.
*/
Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false)
- throw(TypeCheckingException, LogicException);
+ throw(TypeCheckingException, LogicException, UnsafeInterruptException);
/**
* Rewrite Boolean terms in a Node.
d_queryMade(false),
d_needPostsolve(false),
d_earlyTheoryPP(true),
- d_timeBudgetCumulative(0),
- d_timeBudgetPerCall(0),
- d_resourceBudgetCumulative(0),
- d_resourceBudgetPerCall(0),
- d_cumulativeTimeUsed(0),
- d_cumulativeResourceUsed(0),
d_status(),
d_private(NULL),
d_smtAttributes(NULL),
}
d_dumpCommands.clear();
- if(options::perCallResourceLimit() != 0) {
- setResourceLimit(options::perCallResourceLimit(), false);
- }
- if(options::cumulativeResourceLimit() != 0) {
- setResourceLimit(options::cumulativeResourceLimit(), true);
- }
- if(options::perCallMillisecondLimit() != 0) {
- setTimeLimit(options::perCallMillisecondLimit(), false);
- }
- if(options::cumulativeMillisecondLimit() != 0) {
- setTimeLimit(options::cumulativeMillisecondLimit(), true);
- }
-
PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
}
}
// If in arrays, set the UF handler to arrays
- if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() ||
+ if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() ||
(d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
Theory::setUninterpretedSortOwner(THEORY_ARRAY);
} else {
}
Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
- throw(TypeCheckingException, LogicException) {
+ throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
stack< triple<Node, Node, bool> > worklist;
stack<Node> result;
// or upward pass).
do {
+ spendResource();
n = worklist.top().first; // n is the input / original
Node node = worklist.top().second; // node is the output / result
bool childrenPushed = worklist.top().third;
void SmtEnginePrivate::removeITEs() {
d_smt.finalOptionsAreSet();
-
+ spendResource();
Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
// Remove all of the ITE occurrences and normalize
void SmtEnginePrivate::staticLearning() {
d_smt.finalOptionsAreSet();
+ spendResource();
TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime);
// returns false if it learns a conflict
bool SmtEnginePrivate::nonClausalSimplify() {
+ spendResource();
d_smt.finalOptionsAreSet();
if(options::unsatCores()) {
void SmtEnginePrivate::bvToBool() {
Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
+ spendResource();
std::vector<Node> new_assertions;
d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
+ spendResource();
+
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
unsigned numAssertionOnEntry = d_assertions.size();
for (unsigned i = 0; i < d_assertions.size(); ++i) {
+ spendResource();
Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
d_assertions.replace(i, result);
if(result.isConst() && !result.getConst<bool>()){
void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
+ spendResource();
Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
}
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
- throw(TypeCheckingException, LogicException) {
+ throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+ spendResource();
Assert(d_smt.d_pendingPops == 0);
try {
ScopeCounter depth(d_simplifyAssertionsDepth);
Trace("smt") << "SmtEngine::check()" << endl;
+ ResourceManager* resourceManager = d_private->getResourceManager();
+
+ resourceManager->beginCall();
+
+ // Only way we can be out of resource is if cumulative budget is on
+ if (resourceManager->cumulativeLimitOn() &&
+ resourceManager->out()) {
+ Result::UnknownExplanation why = resourceManager->outOfResources() ?
+ Result::RESOURCEOUT : Result::TIMEOUT;
+ return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+ }
+
// Make sure the prop layer has all of the assertions
Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
d_private->processAssertions();
}
}
- unsigned long millis = 0;
- if(d_timeBudgetCumulative != 0) {
- millis = getTimeRemaining();
- if(millis == 0) {
- return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename);
- }
- }
- if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
- millis = d_timeBudgetPerCall;
- }
-
- unsigned long resource = 0;
- if(d_resourceBudgetCumulative != 0) {
- resource = getResourceRemaining();
- if(resource == 0) {
- return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT, d_filename);
- }
- }
- if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
- resource = d_resourceBudgetPerCall;
- }
-
TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
Chat() << "solving..." << endl;
Trace("smt") << "SmtEngine::check(): running check" << endl;
- Result result = d_propEngine->checkSat(millis, resource);
+ Result result = d_propEngine->checkSat();
- // PropEngine::checkSat() returns the actual amount used in these
- // variables.
- d_cumulativeTimeUsed += millis;
- d_cumulativeResourceUsed += resource;
+ resourceManager->endCall();
+ Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage()
+ << ", resources " << resourceManager->getResourceUsage() << endl;
- Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
- << ", conflicts " << d_cumulativeResourceUsed << endl;
return Result(result, d_filename);
}
Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+
+ spendResource();
+
if(d_booleanTermConverter == NULL) {
// This needs to be initialized _after_ the whole SMT framework is in place, subscribed
// to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype
void SmtEnginePrivate::processAssertions() {
TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
-
+ spendResource();
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
<< "applying substitutions" << endl;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
Trace("simplify") << "applying to " << d_assertions[i] << endl;
+ spendResource();
d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
Trace("simplify") << " got " << d_assertions[i] << endl;
}
Chat() << "...doing bvToBool..." << endl;
bvToBool();
dumpAssertions("post-bv-to-bool", d_assertions);
+ Trace("smt") << "POST bvToBool" << endl;
}
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
}
dumpAssertions("post-static-learning", d_assertions);
- Trace("smt") << "POST bvToBool" << endl;
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
// introducing new ones
dumpAssertions("post-everything", d_assertions);
-
+
//set instantiation level of everything to zero
if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
for( unsigned i=0; i < d_assertions.size(); i++ ) {
theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 );
}
}
-
+
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
}
Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
- Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
- SmtScope smts(this);
- finalOptionsAreSet();
- doPendingPops();
+ try {
+ Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
+ SmtScope smts(this);
+ finalOptionsAreSet();
+ doPendingPops();
- Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
+ Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
- if(d_queryMade && !options::incrementalSolving()) {
- throw ModalException("Cannot make multiple queries unless "
- "incremental solving is enabled "
- "(try --incremental)");
- }
+ if(d_queryMade && !options::incrementalSolving()) {
+ throw ModalException("Cannot make multiple queries unless "
+ "incremental solving is enabled "
+ "(try --incremental)");
+ }
- Expr e;
- if(!ex.isNull()) {
- // Substitute out any abstract values in ex.
- e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
- // Ensure expr is type-checked at this point.
- ensureBoolean(e);
- // Give it to proof manager
- PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
- }
+ Expr e;
+ if(!ex.isNull()) {
+ // Substitute out any abstract values in ex.
+ e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
+ // Ensure expr is type-checked at this point.
+ ensureBoolean(e);
+ // Give it to proof manager
+ PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
+ }
- // check to see if a postsolve() is pending
- if(d_needPostsolve) {
- d_theoryEngine->postsolve();
- d_needPostsolve = false;
- }
+ // check to see if a postsolve() is pending
+ if(d_needPostsolve) {
+ d_theoryEngine->postsolve();
+ d_needPostsolve = false;
+ }
- // Push the context
- internalPush();
+ // Push the context
+ internalPush();
- // Note that a query has been made
- d_queryMade = true;
+ // Note that a query has been made
+ d_queryMade = true;
- // Add the formula
- if(!e.isNull()) {
- d_problemExtended = true;
- if(d_assertionList != NULL) {
- d_assertionList->push_back(e);
+ // Add the formula
+ if(!e.isNull()) {
+ d_problemExtended = true;
+ if(d_assertionList != NULL) {
+ d_assertionList->push_back(e);
+ }
+ d_private->addFormula(e.getNode());
}
- d_private->addFormula(e.getNode());
- }
- // Run the check
- Result r = check().asSatisfiabilityResult();
- d_needPostsolve = true;
+ Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ r = check().asSatisfiabilityResult();
+ d_needPostsolve = true;
- // Dump the query if requested
- if(Dump.isOn("benchmark")) {
- // the expr already got dumped out if assertion-dumping is on
- Dump("benchmark") << CheckSatCommand();
- }
+ // Dump the query if requested
+ if(Dump.isOn("benchmark")) {
+ // the expr already got dumped out if assertion-dumping is on
+ Dump("benchmark") << CheckSatCommand();
+ }
- // Pop the context
- internalPop();
+ // Pop the context
+ internalPop();
- // Remember the status
- d_status = r;
+ // Remember the status
+ d_status = r;
- d_problemExtended = false;
+ d_problemExtended = false;
- Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
+ Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
- // Check that SAT results generate a model correctly.
- if(options::checkModels()) {
- if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
- (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
- checkModel(/* hard failure iff */ ! r.isUnknown());
+ // Check that SAT results generate a model correctly.
+ if(options::checkModels()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::SAT ||
+ (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){
+ checkModel(/* hard failure iff */ ! r.isUnknown());
+ }
}
- }
- // Check that UNSAT results generate a proof correctly.
- if(options::checkProofs()) {
- if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
- TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
- checkProof();
+ // Check that UNSAT results generate a proof correctly.
+ if(options::checkProofs()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+ TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+ checkProof();
+ }
}
- }
- return r;
+ return r;
+ } catch (UnsafeInterruptException& e) {
+ AlwaysAssert(d_private->getResourceManager()->out());
+ Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
+ Result::RESOURCEOUT : Result::TIMEOUT;
+ return Result(Result::SAT_UNKNOWN, why, d_filename);
+ }
}/* SmtEngine::checkSat() */
Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
doPendingPops();
Trace("smt") << "SMT query(" << ex << ")" << endl;
+ try {
if(d_queryMade && !options::incrementalSolving()) {
throw ModalException("Cannot make multiple queries unless "
"incremental solving is enabled "
d_private->addFormula(e.getNode().notNode());
// Run the check
- Result r = check().asValidityResult();
+ Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+ r = check().asValidityResult();
d_needPostsolve = true;
// Dump the query if requested
}
return r;
+ } catch (UnsafeInterruptException& e) {
+ AlwaysAssert(d_private->getResourceManager()->out());
+ Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
+ Result::RESOURCEOUT : Result::TIMEOUT;
+ return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
+ }
}/* SmtEngine::query() */
-Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
return realValue;
}
-Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
return n.toExpr();
}
-Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+ d_private->spendResource();
+
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
return n.toExpr();
}
-Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException) {
+Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
return true;
}
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptException) {
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
}
}
-Model* SmtEngine::getModel() throw(ModalException) {
+Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
}
-UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
+UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptException) {
Trace("smt") << "SMT getUnsatCore()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
#endif /* CVC4_PROOF */
}
-Proof* SmtEngine::getProof() throw(ModalException) {
+Proof* SmtEngine::getProof() throw(ModalException, UnsafeInterruptException) {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
}
-void SmtEngine::push() throw(ModalException, LogicException) {
+void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptException) {
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
<< d_userContext->getLevel() << endl;
}
-void SmtEngine::pop() throw(ModalException) {
+void SmtEngine::pop() throw(ModalException, UnsafeInterruptException) {
SmtScope smts(this);
finalOptionsAreSet();
Trace("smt") << "SMT pop()" << endl;
}
void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
- if(cumulative) {
- Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl;
- d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
- } else {
- Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl;
- d_resourceBudgetPerCall = units;
- }
+ d_private->getResourceManager()->setResourceLimit(units, cumulative);
}
-
-void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
- if(cumulative) {
- Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl;
- d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
- } else {
- Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl;
- d_timeBudgetPerCall = millis;
- }
+void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
+ d_private->getResourceManager()->setTimeLimit(milis, cumulative);
}
unsigned long SmtEngine::getResourceUsage() const {
- return d_cumulativeResourceUsed;
+ return d_private->getResourceManager()->getResourceUsage();
}
unsigned long SmtEngine::getTimeUsage() const {
- return d_cumulativeTimeUsed;
+ return d_private->getResourceManager()->getTimeUsage();
}
unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
- if(d_resourceBudgetCumulative == 0) {
- throw ModalException("No cumulative resource limit is currently set");
- }
-
- return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
- d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+ return d_private->getResourceManager()->getResourceRemaining();
}
unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
- if(d_timeBudgetCumulative == 0) {
- throw ModalException("No cumulative time limit is currently set");
- }
-
- return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 :
- d_timeBudgetCumulative - d_cumulativeTimeUsed;
+ return d_private->getResourceManager()->getTimeRemaining();
}
Statistics SmtEngine::getStatistics() const throw() {
#include "util/result.h"
#include "util/sexpr.h"
#include "util/hash.h"
+#include "util/unsafe_interrupt_exception.h"
#include "util/statistics.h"
#include "theory/logic_info.h"
*/
bool d_earlyTheoryPP;
- /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
- unsigned long d_timeBudgetCumulative;
- /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
- unsigned long d_timeBudgetPerCall;
- /** A user-imposed cumulative resource budget. 0 = no limit. */
- unsigned long d_resourceBudgetCumulative;
- /** A user-imposed per-call resource budget. 0 = no limit. */
- unsigned long d_resourceBudgetPerCall;
-
- /** The number of milliseconds used by this SmtEngine since its inception. */
- unsigned long d_cumulativeTimeUsed;
- /** The amount of resource used by this SmtEngine since its inception. */
- unsigned long d_cumulativeResourceUsed;
/**
* Most recent result of last checkSat/query or (set-info :status).
* or INVALID query). Only permitted if CVC4 was built with model
* support and produce-models is on.
*/
- Model* getModel() throw(ModalException);
+ Model* getModel() throw(ModalException, UnsafeInterruptException);
// disallow copy/assignment
SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
* takes a Boolean flag to determine whether to include this asserted
* formula in an unsat core (if one is later requested).
*/
- Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException);
+ Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
/**
* Check validity of an expression with respect to the current set
* @todo (design) is this meant to give an equivalent or an
* equisatisfiable formula?
*/
- Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException);
+ Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
/**
* Expand the definitions in a term or formula. No other
* simplification or normalization is done.
*/
- Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException);
+ Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
/**
* Get the assigned value of an expr (only if immediately preceded
* by a SAT or INVALID query). Only permitted if the SmtEngine is
* set to operate interactively and produce-models is on.
*/
- Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
+ Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException);
/**
* Add a function to the set of expressions whose value is to be
* INVALID query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
- CVC4::SExpr getAssignment() throw(ModalException);
+ CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException);
/**
* Get the last proof (only if immediately preceded by an UNSAT
* or VALID query). Only permitted if CVC4 was built with proof
* support and produce-proofs is on.
*/
- Proof* getProof() throw(ModalException);
+ Proof* getProof() throw(ModalException, UnsafeInterruptException);
/**
* Print all instantiations made by the quantifiers module.
* UNSAT or VALID query). Only permitted if CVC4 was built with
* unsat-core support and produce-unsat-cores is on.
*/
- UnsatCore getUnsatCore() throw(ModalException);
+ UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException);
/**
* Get the current set of assertions. Only permitted if the
/**
* Push a user-level context.
*/
- void push() throw(ModalException, LogicException);
+ void push() throw(ModalException, LogicException, UnsafeInterruptException);
/**
* Pop a user-level context. Throws an exception if nothing to pop.
*/
- void pop() throw(ModalException);
+ void pop() throw(ModalException, UnsafeInterruptException);
/**
* Completely reset the state of the solver, as though destroyed and
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current;
}
+inline bool smtEngineInScope() {
+ return s_smtEngine_current != NULL;
+}
inline ProofManager* currentProofManager() {
#ifdef CVC4_PROOF
#include "prop/sat_solver.h"
#include "theory/valuation.h"
#include "theory/theory_registrar.h"
+#include "util/resource_manager.h"
class Abc_Obj_t_;
typedef Abc_Obj_t_ Abc_Obj_t;
{}
bool notify(prop::SatLiteral lit);
void notify(prop::SatClause& clause);
+ void spendResource();
void safePoint();
};
Statistics(const std::string& name);
~Statistics();
};
- std::string d_name;
+ std::string d_name;
+public:
Statistics d_statistics;
};
MinisatEmptyNotify() {}
bool notify(prop::SatLiteral lit) { return true; }
void notify(prop::SatClause& clause) { }
+ void spendResource() {
+ NodeManager::currentResourceManager()->spendResource();
+ }
void safePoint() {}
};
}
void EagerBitblastSolver::assertFormula(TNode formula) {
+ d_bv->spendResource();
Assert (isInitialized());
Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n";
d_assertionSet.insert(formula);
void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
bool changed = true;
while(changed) {
+ // d_bv->spendResource();
changed = false;
for (unsigned i = 0; i < worklist.size(); ++i) {
// apply current substitutions
// don't bit-blast lemma atoms
continue;
}
- Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
- d_bitblaster->bbAtom(atom);
+ Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
+ {
+ TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
+ d_bitblaster->bbAtom(atom);
+ }
}
}
// We need to ensure we are fully propagated, so propagate now
if (d_useSatPropagation) {
+ d_bv->spendResource();
bool ok = d_bitblaster->propagate();
if (!ok) {
std::vector<TNode> conflictAtoms;
bool CoreSolver::check(Theory::Effort e) {
Trace("bitvector::core") << "CoreSolver::check \n";
+
+ d_bv->spendResource();
+
d_checkCalled = true;
Assert (!d_bv->inConflict());
++(d_statistics.d_numCallstoCheck);
bool InequalitySolver::check(Theory::Effort e) {
Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
++(d_statistics.d_numCallstoCheck);
+ d_bv->spendResource();
bool ok = true;
while (!done() && ok) {
return;
}
+ d_bv->spendResource();
Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
d_termBBStrategies[node.getKind()] (node, bits, this);
return;
}
+ d_bv->spendResource();
Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numTerms;
}
}
+void TLazyBitblaster::MinisatNotify::spendResource() {
+ d_bv->spendResource();
+}
+
void TLazyBitblaster::MinisatNotify::safePoint() {
d_bv->d_out->safePoint();
}
}
}
+void TheoryBV::spendResource() throw(UnsafeInterruptException) {
+ getOutputChannel().spendResource();
+}
+
TheoryBV::Statistics::Statistics():
d_avgConflictSize("theory::bv::AvgBVConflictSize"),
d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
return;
}
Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+ TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
// we may be getting new assertions so the model cache may not be sound
d_invalidateModelCache.set(true);
// if we are using the eager solver
Statistics d_statistics;
+ void spendResource() throw(UnsafeInterruptException);
/**
* Return the uninterpreted function symbol corresponding to division-by-zero
friend class CoreSolver;
friend class InequalitySolver;
friend class AlgebraicSolver;
+ friend class EagerBitblastSolver;
};/* class TheoryBV */
}/* CVC4::theory::bv namespace */
#include "util/cvc4_assert.h"
#include "theory/interrupted.h"
+#include "util/resource_manager.h"
namespace CVC4 {
namespace theory {
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
*/
- virtual void safePoint() throw(Interrupted, AssertionException) {
+ virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) {
}
/**
* unit conflict) which is assigned TRUE (and T-conflicting) in the
* current assignment.
*/
- virtual void conflict(TNode n) throw(AssertionException) = 0;
+ virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
/**
* Propagate a theory literal.
* @param n - a theory consequence at the current decision level
* @return false if an immediate conflict was encountered
*/
- virtual bool propagate(TNode n) throw(AssertionException) = 0;
+ virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
/**
* Tell the core that a valid theory lemma at decision level 0 has
*/
virtual LemmaStatus lemma(TNode n, bool removable = false,
bool preprocess = false)
- throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
/**
* Request a split on a new theory atom. This is equivalent to
* @param n - a theory atom; must be of Boolean type
*/
LemmaStatus split(TNode n)
- throw(TypeCheckingExceptionPrivate, AssertionException) {
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
return splitLemma(n.orNode(n.notNode()));
}
virtual LemmaStatus splitLemma(TNode n, bool removable = false)
- throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+ throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
/**
* If a decision is made on n, it must be in the phase specified.
* @param phase - the phase to decide on n
*/
virtual void requirePhase(TNode n, bool phase)
- throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+ throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
/**
* Flips the most recent unflipped decision to the other phase and
* could be flipped, or if the root decision was re-flipped
*/
virtual bool flipDecision()
- throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+ throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
/**
* Notification from a theory that it realizes it is incomplete at
* this context level. If SAT is later determined by the
* TheoryEngine, it should actually return an UNKNOWN result.
*/
- virtual void setIncomplete() throw(AssertionException) = 0;
+ virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0;
/**
* "Spend" a "resource." The meaning is specific to the context in
* long-running operations, they cannot rely on resource() to break
* out of infinite or intractable computations.
*/
- virtual void spendResource() throw() {}
+ virtual void spendResource() throw(UnsafeInterruptException) {}
/**
* Handle user attribute.
* Using this leads to non-termination issues.
* It is appropriate for prototyping for theories.
*/
- virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
+ virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {}
};/* class OutputChannel */
#include "theory/theory.h"
#include "theory/rewriter.h"
#include "theory/rewriter_tables.h"
+#include "smt/smt_engine_scope.h"
+#include "util/resource_manager.h"
using namespace std;
namespace CVC4 {
namespace theory {
+unsigned long Rewriter::d_iterationCount = 0;
+
static TheoryId theoryOf(TNode node) {
return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
}
}
};
-Node Rewriter::rewrite(TNode node) {
+Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){
return rewriteTo(theoryOf(node), node);
}
vector<RewriteStackElement> rewriteStack;
rewriteStack.push_back(RewriteStackElement(node, theoryId));
+ ResourceManager* rm = NULL;
+ bool hasSmtEngine = smt::smtEngineInScope();
+ if (hasSmtEngine) {
+ rm = NodeManager::currentResourceManager();
+ }
// Rewrite until the stack is empty
for (;;){
+ if (hasSmtEngine &&
+ d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
+ rm->spendResource();
+ d_iterationCount = 0;
+ }
+
// Get the top of the recursion stack
RewriteStackElement& rewriteStackTop = rewriteStack.back();
rewriteStackTop.theoryId = theoryOf(cached);
}
}
-
+
rewriteStackTop.original =rewriteStackTop.node;
// Now it's time to rewrite the children, check if this has already been done
Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
return Node::null();
}/* Rewriter::rewriteTo() */
+void Rewriter::clearCaches() {
+#ifdef CVC4_ASSERTIONS
+ if(s_rewriteStack != NULL) {
+ delete s_rewriteStack;
+ s_rewriteStack = NULL;
+ }
+#endif
+ Rewriter::clearCachesInternal();
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#pragma once
#include "expr/node.h"
+#include "util/unsafe_interrupt_exception.h"
+
//#include "expr/attribute.h"
namespace CVC4 {
class Rewriter {
friend class RewriterInitializer;
-
+ static unsigned long d_iterationCount;
/** Returns the appropriate cache for a node */
static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
* Should be called to clean up any state.
*/
static void shutdown();
-
+ static void clearCachesInternal();
public:
/**
* Rewrites the node using theoryOf() to determine which rewriter to
* use on the node.
*/
- static Node rewrite(TNode node);
+ static Node rewrite(TNode node) throw (UnsafeInterruptException);
/**
* Garbage collects the rewrite caches.
*/
- static void garbageCollect();
-
+ static void clearCaches();
};/* class Rewriter */
}/* CVC4::theory namespace */
${rewrite_shutdown}
}
-void Rewriter::garbageCollect() {
+void Rewriter::clearCachesInternal() {
typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
std::vector<AttributeUniqueId> preids;
${pre_rewrite_attribute_ids}
#include "expr/node_builder.h"
#include "options/options.h"
#include "util/lemma_output_channel.h"
+#include "util/resource_manager.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
d_true(),
d_false(),
d_interrupted(false),
+ d_resourceManager(NodeManager::currentResourceManager()),
d_inPreregister(false),
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
* @param effort the effort level to use
*/
void TheoryEngine::check(Theory::Effort effort) {
-
- d_propEngine->checkTime();
+ // spendResource();
// Reset the interrupt flag
d_interrupted = false;
Node TheoryEngine::preprocess(TNode assertion) {
Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
+ // spendResource();
// Do a topological sort of the subexpressions and substitute them
vector<preprocess_stack_element> toVisit;
{
Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
- d_propEngine->checkTime();
+ // spendResource();
// If we're in conflict, nothing to do
if (d_inConflict) {
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
- d_propEngine->checkTime();
+ // spendResource();
if(Dump.isOn("t-propagations")) {
Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
// For resource-limiting (also does a time check).
- spendResource();
+ // spendResource();
// Do we need to check atoms
if (atomsTo != theory::THEORY_LAST) {
Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
d_iteUtilities->clear();
- Rewriter::garbageCollect();
+ Rewriter::clearCaches();
d_iteRemover.garbageCollect();
nm->reclaimZombiesUntil(options::zombieHuntThreshold());
Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
return th->entailmentCheck(lit, params, seffects);
}
+
+void TheoryEngine::spendResource() {
+ d_resourceManager->spendResource();
+}
#include "util/statistics_registry.h"
#include "util/cvc4_assert.h"
#include "util/sort_inference.h"
+#include "util/unsafe_interrupt_exception.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/uf/equality_engine.h"
#include "theory/bv/bv_to_bool.h"
namespace CVC4 {
+class ResourceManager;
+
/**
* A pair of a theory and a node. This is used to mark the flow of
* propagations between theories.
{
}
- void safePoint() throw(theory::Interrupted, AssertionException) {
+ void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
spendResource();
if (d_engine->d_interrupted) {
throw theory::Interrupted();
}
}
- void conflict(TNode conflictNode) throw(AssertionException) {
+ void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) {
Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
++ d_statistics.conflicts;
d_engine->d_outputChannelUsed = true;
d_engine->conflict(conflictNode, d_theory);
}
- bool propagate(TNode literal) throw(AssertionException) {
+ bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
++ d_statistics.propagations;
d_engine->d_outputChannelUsed = true;
return d_engine->propagate(literal, d_theory);
}
- theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+ theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
++ d_statistics.lemmas;
d_engine->d_outputChannelUsed = true;
return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST);
}
- theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+ theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
++ d_statistics.lemmas;
d_engine->d_outputChannelUsed = true;
return d_engine->lemma(lemma, false, removable, false, d_theory);
}
- void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {
+ void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
NodeManager* curr = NodeManager::currentNM();
Node restartVar = curr->mkSkolem("restartVar",
curr->booleanType(),
}
void requirePhase(TNode n, bool phase)
- throw(theory::Interrupted, AssertionException) {
+ throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
Debug("theory") << "EngineOutputChannel::requirePhase("
<< n << ", " << phase << ")" << std::endl;
++ d_statistics.requirePhase;
}
bool flipDecision()
- throw(theory::Interrupted, AssertionException) {
+ throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
++ d_statistics.flipDecision;
return d_engine->d_propEngine->flipDecision();
}
- void setIncomplete() throw(AssertionException) {
+ void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
d_engine->setIncomplete(d_theory);
}
- void spendResource() throw() {
+ void spendResource() throw(UnsafeInterruptException) {
d_engine->spendResource();
}
d_incomplete = true;
}
- /**
- * "Spend" a resource during a search or preprocessing.
- */
- void spendResource() throw() {
- d_propEngine->spendResource();
- }
/**
* Mapping of propagations from recievers to senders.
/** Whether we were just interrupted (or not) */
bool d_interrupted;
+ ResourceManager* d_resourceManager;
public:
~TheoryEngine();
void interrupt() throw(ModalException);
+ /**
+ * "Spend" a resource during a search or preprocessing.
+ */
+ void spendResource();
/**
* Adds a theory. Only one theory per TheoryId can be present, so if
#include "expr/node.h"
#include "theory/output_channel.h"
#include "theory/interrupted.h"
+#include "util/unsafe_interrupt_exception.h"
#include <vector>
#include <utility>
#include <iostream>
namespace CVC4 {
-
namespace theory {
/**
void safePoint() throw(Interrupted, AssertionException) {}
void conflict(TNode n)
- throw(AssertionException) {
+ throw(AssertionException, UnsafeInterruptException) {
push(CONFLICT, n);
}
bool propagate(TNode n)
- throw(AssertionException) {
+ throw(AssertionException, UnsafeInterruptException) {
push(PROPAGATE, n);
return true;
}
void propagateAsDecision(TNode n)
- throw(AssertionException) {
+ throw(AssertionException, UnsafeInterruptException) {
push(PROPAGATE_AS_DECISION, n);
}
- LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) {
+ LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
- void requirePhase(TNode, bool) throw(Interrupted, AssertionException) {
+ void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) {
}
- bool flipDecision() throw(Interrupted, AssertionException) {
+ bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) {
return true;
}
- void setIncomplete() throw(AssertionException) {}
+ void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
+ }
- void handleUserAttribute( const char* attr, theory::Theory* t ){}
+ void handleUserAttribute( const char* attr, theory::Theory* t ) {
+ }
void clear() {
d_callHistory.clear();
}
- LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){
+ LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
push(LEMMA, n);
return LemmaStatus(Node::null(), 0);
}
return d_callHistory.size();
}
- void printIth(std::ostream& os, int i){
+ void printIth(std::ostream& os, int i) {
os << "[TestOutputChannel " << i;
os << " " << getIthCallType(i);
os << " " << getIthNode(i) << "]";
didyoumean.h \
didyoumean.cpp \
unsat_core.h \
- unsat_core.cpp
+ unsat_core.cpp \
+ resource_manager.h \
+ resource_manager.cpp \
+ unsafe_interrupt_exception.h
libstatistics_la_SOURCES = \
statistics_registry.h \
uninterpreted_constant.i \
chain.i \
regexp.i \
+ resource_manager.i \
proof.i \
unsat_core.i
--- /dev/null
+/********************* */
+/*! \file resource_manager.h
+** \verbatim
+** Original author: Liana Hadarean
+** Major contributors: none
+** Minor contributors (to current version): none
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2014 New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief Manages and updates various resource and time limits.
+**
+** Manages and updates various resource and time limits.
+**/
+
+#include "util/resource_manager.h"
+#include "util/output.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/options.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace std;
+
+void Timer::set(unsigned long millis, bool wallTime) {
+ d_ms = millis;
+ Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl;
+ // keep track of when it was set, even if it's disabled (i.e. == 0)
+ d_wall_time = wallTime;
+ if (d_wall_time) {
+ // Wall time
+ gettimeofday(&d_wall_limit, NULL);
+ Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+ d_wall_limit.tv_sec += millis / 1000;
+ d_wall_limit.tv_usec += (millis % 1000) * 1000;
+ if(d_wall_limit.tv_usec > 1000000) {
+ ++d_wall_limit.tv_sec;
+ d_wall_limit.tv_usec -= 1000000;
+ }
+ Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+ } else {
+ // CPU time
+ d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001);
+ d_cpu_limit = d_cpu_start_time + d_ms;
+ }
+}
+
+/** Return the milliseconds elapsed since last set(). */
+unsigned long Timer::elapsedWall() const {
+ Assert (d_wall_time);
+ timeval tv;
+ gettimeofday(&tv, NULL);
+ Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+ tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000;
+ tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000;
+ Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+ return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+}
+
+unsigned long Timer::elapsedCPU() const {
+ Assert (!d_wall_time);
+ clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time;
+ Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl;
+ return elapsed;
+}
+
+unsigned long Timer::elapsed() const {
+ if (d_wall_time)
+ return elapsedWall();
+ return elapsedCPU();
+}
+
+bool Timer::expired() const {
+ if (!on()) return false;
+
+ if (d_wall_time) {
+ timeval tv;
+ gettimeofday(&tv, NULL);
+ Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+ Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+ if(d_wall_limit.tv_sec < tv.tv_sec ||
+ (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) {
+ Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl;
+ return true;
+ }
+ Debug("limit") << "Timer::expired(): within limit" << std::endl;
+ return false;
+ }
+
+ // cpu time
+ double current = ((double)clock())/(CLOCKS_PER_SEC*0.001);
+ Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl;
+ Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl;
+ if (current >= d_cpu_limit) {
+ Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl;
+ return true;
+ }
+ return false;
+}
+
+const unsigned long ResourceManager::s_resourceCount = 1000;
+
+ResourceManager::ResourceManager()
+ : d_cumulativeTimer()
+ , d_perCallTimer()
+ , d_timeBudgetCumulative(0)
+ , d_timeBudgetPerCall(0)
+ , d_resourceBudgetCumulative(0)
+ , d_resourceBudgetPerCall(0)
+ , d_cumulativeTimeUsed(0)
+ , d_cumulativeResourceUsed(0)
+ , d_thisCallResourceUsed(0)
+ , d_thisCallTimeBudget(0)
+ , d_thisCallResourceBudget(0)
+ , d_isHardLimit()
+ , d_on(false)
+ , d_cpuTime(false)
+ , d_spendResourceCalls(0)
+{}
+
+
+void ResourceManager::setResourceLimit(unsigned long units, bool cumulative) {
+ d_on = true;
+ if(cumulative) {
+ Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl;
+ d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+ d_thisCallResourceBudget = d_resourceBudgetCumulative;
+ } else {
+ Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl;
+ d_resourceBudgetPerCall = units;
+ }
+}
+
+void ResourceManager::setTimeLimit(unsigned long millis, bool cumulative) {
+ d_on = true;
+ if(cumulative) {
+ Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl;
+ d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
+ d_cumulativeTimer.set(millis, !d_cpuTime);
+ } else {
+ Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl;
+ d_timeBudgetPerCall = millis;
+ // perCall timer will be set in beginCall
+ }
+
+}
+
+unsigned long ResourceManager::getResourceUsage() const {
+ return d_cumulativeResourceUsed;
+}
+
+unsigned long ResourceManager::getTimeUsage() const {
+ if (d_timeBudgetCumulative) {
+ return d_cumulativeTimer.elapsed();
+ }
+ return d_cumulativeTimeUsed;
+}
+
+unsigned long ResourceManager::getResourceRemaining() const {
+ if (d_thisCallResourceBudget <= d_thisCallResourceUsed)
+ return 0;
+ return d_thisCallResourceBudget - d_thisCallResourceUsed;
+}
+
+unsigned long ResourceManager::getTimeRemaining() const {
+ unsigned long time_passed = d_cumulativeTimer.elapsed();
+ if (time_passed >= d_thisCallTimeBudget)
+ return 0;
+ return d_thisCallTimeBudget - time_passed;
+}
+
+void ResourceManager::spendResource() throw (UnsafeInterruptException) {
+ ++d_spendResourceCalls;
+ if (!d_on) return;
+
+ Debug("limit") << "ResourceManager::spendResource()" << std::endl;
+ ++d_cumulativeResourceUsed;
+ ++d_thisCallResourceUsed;
+ if(out()) {
+ Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
+ Trace("limit") << " on call " << d_spendResourceCalls << std::endl;
+ if (outOfTime()) {
+ Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl;
+ }
+
+ if (smt::smtEngineInScope()) {
+ theory::Rewriter::clearCaches();
+ }
+ if (d_isHardLimit) {
+ throw UnsafeInterruptException();
+ }
+
+ // interrupt it next time resources are checked
+ if (smt::smtEngineInScope()) {
+ smt::currentSmtEngine()->interrupt();
+ }
+ }
+}
+
+void ResourceManager::beginCall() {
+
+ d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime);
+ d_thisCallResourceUsed = 0;
+ if (!d_on) return;
+
+ if (cumulativeLimitOn()) {
+ if (d_resourceBudgetCumulative) {
+ d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
+ d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+ }
+
+ if (d_timeBudgetCumulative) {
+
+ AlwaysAssert(d_cumulativeTimer.on());
+ // timer was on since the option was set
+ d_cumulativeTimeUsed = d_cumulativeTimer.elapsed();
+ d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 :
+ d_timeBudgetCumulative - d_cumulativeTimeUsed;
+ d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime);
+ }
+ // we are out of resources so we shouldn't update the
+ // budget for this call to the per call budget
+ if (d_thisCallTimeBudget == 0 ||
+ d_thisCallResourceUsed == 0)
+ return;
+ }
+
+ if (perCallLimitOn()) {
+ // take min of what's left and per-call budget
+ if (d_resourceBudgetPerCall) {
+ d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall;
+ }
+
+ if (d_timeBudgetPerCall) {
+ d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall;
+ }
+ }
+}
+
+void ResourceManager::endCall() {
+ unsigned long usedInCall = d_perCallTimer.elapsed();
+ d_perCallTimer.set(0);
+ d_cumulativeTimeUsed += usedInCall;
+}
+
+bool ResourceManager::cumulativeLimitOn() const {
+ return d_timeBudgetCumulative || d_resourceBudgetCumulative;
+}
+
+bool ResourceManager::perCallLimitOn() const {
+ return d_timeBudgetPerCall || d_resourceBudgetPerCall;
+}
+
+bool ResourceManager::outOfResources() const {
+ // resource limiting not enabled
+ if (d_resourceBudgetPerCall == 0 &&
+ d_resourceBudgetCumulative == 0)
+ return false;
+
+ return getResourceRemaining() == 0;
+}
+
+bool ResourceManager::outOfTime() const {
+ if (d_timeBudgetPerCall == 0 &&
+ d_timeBudgetCumulative == 0)
+ return false;
+
+ return d_cumulativeTimer.expired() || d_perCallTimer.expired();
+}
+
+void ResourceManager::useCPUTime(bool cpu) {
+ Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n";
+ d_cpuTime = cpu;
+}
+
+void ResourceManager::setHardLimit(bool value) {
+ Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n";
+ d_isHardLimit = value;
+}
+
+void ResourceManager::enable(bool on) {
+ Trace("limit") << "ResourceManager::enable("<< on <<")\n";
+ d_on = on;
+}
--- /dev/null
+/********************* */
+/*! \file resource_manager.h
+** \verbatim
+** Original author: Liana Hadarean
+** Major contributors: none
+** Minor contributors (to current version): none
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2014 New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief Manages and updates various resource and time limits
+**
+** Manages and updates various resource and time limits.
+**/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RESOURCE_MANAGER_H
+#define __CVC4__RESOURCE_MANAGER_H
+
+#include <cstddef>
+#include <sys/time.h>
+
+#include "util/exception.h"
+#include "util/unsafe_interrupt_exception.h"
+
+namespace CVC4 {
+
+/**
+ * A helper class to keep track of a time budget and signal
+ * the PropEngine when the budget expires.
+ */
+class CVC4_PUBLIC Timer {
+
+ unsigned long d_ms;
+ timeval d_wall_limit;
+ clock_t d_cpu_start_time;
+ clock_t d_cpu_limit;
+
+ bool d_wall_time;
+
+ /** Return the milliseconds elapsed since last set() cpu time. */
+ unsigned long elapsedCPU() const;
+ /** Return the milliseconds elapsed since last set() wall time. */
+ unsigned long elapsedWall() const;
+
+public:
+
+ /** Construct a Timer. */
+ Timer()
+ : d_ms(0)
+ , d_cpu_start_time(0)
+ , d_cpu_limit(0)
+ , d_wall_time(true)
+ {}
+
+ /** Is the timer currently active? */
+ bool on() const {
+ return d_ms != 0;
+ }
+
+ /** Set a millisecond timer (0==off). */
+ void set(unsigned long millis, bool wall_time = true);
+ /** Return the milliseconds elapsed since last set() wall/cpu time
+ depending on d_wall_time*/
+ unsigned long elapsed() const;
+ bool expired() const;
+
+};/* class Timer */
+
+
+class CVC4_PUBLIC ResourceManager {
+
+ Timer d_cumulativeTimer;
+ Timer d_perCallTimer;
+
+ /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
+ unsigned long d_timeBudgetCumulative;
+ /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
+ unsigned long d_timeBudgetPerCall;
+ /** A user-imposed cumulative resource budget. 0 = no limit. */
+ unsigned long d_resourceBudgetCumulative;
+ /** A user-imposed per-call resource budget. 0 = no limit. */
+ unsigned long d_resourceBudgetPerCall;
+
+ /** The number of milliseconds used. */
+ unsigned long d_cumulativeTimeUsed;
+ /** The amount of resource used. */
+ unsigned long d_cumulativeResourceUsed;
+
+ /** The ammount of resource used during this call. */
+ unsigned long d_thisCallResourceUsed;
+
+ /**
+ * The ammount of resource budget for this call (min between per call
+ * budget and left-over cumulative budget.
+ */
+ unsigned long d_thisCallTimeBudget;
+ unsigned long d_thisCallResourceBudget;
+
+ bool d_isHardLimit;
+ bool d_on;
+ bool d_cpuTime;
+ unsigned long d_spendResourceCalls;
+
+ /** Counter indicating how often to check resource manager in loops */
+ static const unsigned long s_resourceCount;
+
+public:
+
+ ResourceManager();
+
+ bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+ bool cumulativeLimitOn() const;
+ bool perCallLimitOn() const;
+
+ bool outOfResources() const;
+ bool outOfTime() const;
+ bool out() const { return d_on && (outOfResources() || outOfTime()); }
+
+ unsigned long getResourceUsage() const;
+ unsigned long getTimeUsage() const;
+ unsigned long getResourceRemaining() const;
+ unsigned long getTimeRemaining() const;
+
+ unsigned long getResourceBudgetForThisCall() {
+ return d_thisCallResourceBudget;
+ }
+
+ void spendResource() throw(UnsafeInterruptException);
+
+ void setHardLimit(bool value);
+ void setResourceLimit(unsigned long units, bool cumulative = false);
+ void setTimeLimit(unsigned long millis, bool cumulative = false);
+ void useCPUTime(bool cpu);
+
+ void enable(bool on);
+
+ /**
+ * Resets perCall limits to mark the start of a new call,
+ * updates budget for current call and starts the timer
+ */
+ void beginCall();
+
+ /**
+ * Marks the end of a SmtEngine check call, stops the per
+ * call timer, updates cumulative time used.
+ */
+ void endCall();
+
+ static unsigned long getFrequencyCount() { return s_resourceCount; }
+
+};/* class ResourceManager */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RESOURCE_MANAGER_H */
--- /dev/null
+%{
+#include "util/resource_manager.h"
+%}
+
+%include "util/resource_manager.h"
--- /dev/null
+/********************* */
+/*! \file modal_exception.h
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when the solver is out of time/resources
+ ** and is interrupted in an unsafe state
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception {
+public:
+ UnsafeInterruptException() :
+ Exception("Interrupted in unsafe state due to "
+ "time/resource limit.") {
+ }
+
+ UnsafeInterruptException(const std::string& msg) :
+ Exception(msg) {
+ }
+
+ UnsafeInterruptException(const char* msg) :
+ Exception(msg) {
+ }
+};/* class UnsafeInterruptException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
--- /dev/null
+%{
+#include "util/unsafe_interrupt_exception.h"
+%}
+
+%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*);
+
+%include "util/unsafe_interrupt_exception.h"
TheoryBVWhite() {}
-
void setUp() {
d_em = new ExprManager();
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
d_scope = new SmtScope(d_smt);
d_smt->setOption("bitblast", SExpr("eager"));
- d_bb = new EagerBitblaster(NULL);
-
+ d_bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]));
}
+
void tearDown() {
- // delete d_bb;
+ delete d_bb;
+ delete d_scope;
+ delete d_smt;
delete d_em;
}
-
void testBitblasterCore() {
Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
bool res = d_bb->solve();
TS_ASSERT (res == false);
}
-
-};
+};/* class TheoryBVWhite */
projects / cvc5.git / commitdiff