Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
TypeNode child2, TypeNode child3) {
- return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();;
+ return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
}
// N-ary version for types
prop_engine.h \
sat.h \
sat.cpp \
+ sat_timer.h \
cnf_stream.h \
cnf_stream.cpp
PropEngine::PropEngine(TheoryEngine* te, Context* context) :
d_inCheckSat(false),
d_theoryEngine(te),
- d_context(context) {
+ d_context(context),
+ d_satSolver(NULL),
+ d_cnfStream(NULL),
+ d_satTimer(*this),
+ d_interrupted(false) {
+
Debug("prop") << "Constructing the PropEngine" << endl;
d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
}
}
-Result PropEngine::checkSat() {
+Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "PropEngine::checkSat()" << endl;
d_theoryEngine->presolve();
if(Options::current()->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
- bool result = d_satSolver->solve();
+ SatLiteralValue result = d_satSolver->solve(resource);
+
+ millis = d_satTimer.elapsed();
- if( result && Debug.isOn("prop") ) {
+ if( result == l_Undef ) {
+ Result::UnknownExplanation why =
+ d_satTimer.expired() ? Result::TIMEOUT :
+ (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
+ return Result(Result::SAT_UNKNOWN, why);
+ }
+
+ if( result == l_True && Debug.isOn("prop") ) {
printSatisfyingAssignment();
}
- Debug("prop") << "PropEngine::checkSat() => "
- << (result ? "true" : "false") << endl;
- if(result && d_theoryEngine->isIncomplete()) {
+ Debug("prop") << "PropEngine::checkSat() => " << result << endl;
+ if(result == l_True && d_theoryEngine->isIncomplete()) {
return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
}
- return Result(result ? Result::SAT : Result::UNSAT);
+ return Result(result == l_True ? Result::SAT : Result::UNSAT);
}
Node PropEngine::getValue(TNode node) {
return d_cnfStream->hasLiteral(node);
}
+bool PropEngine::isTranslatedSatLiteral(TNode node) {
+ return d_cnfStream->isTranslated(node);
+}
+
bool PropEngine::hasValue(TNode node, bool& value) {
Assert(node.getType().isBoolean());
SatLiteral lit = d_cnfStream->getLiteral(node);
Debug("prop") << "pop()" << endl;
}
+void PropEngine::interrupt() throw(ModalException) {
+ if(! d_inCheckSat) {
+ throw ModalException("SAT solver is not currently solving anything; "
+ "cannot interrupt it");
+ }
+
+ d_interrupted = true;
+ d_satSolver->interrupt();
+ Debug("prop") << "interrupt()" << endl;
+}
+
+void PropEngine::spendResource() throw() {
+ // TODO implement me
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
#include "expr/node.h"
#include "util/options.h"
#include "util/result.h"
+#include "smt/modal_exception.h"
+
+#include <sys/time.h>
namespace CVC4 {
class CnfStream;
class SatSolver;
+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).
class PropEngine {
/**
- * Indicates that the sat solver is currently solving something and we should
+ * Indicates that the SAT solver is currently solving something and we should
* not mess with it's internal state.
*/
bool d_inCheckSat;
/** The theory engine we will be using */
TheoryEngine *d_theoryEngine;
+ /** The context */
context::Context* d_context;
/** The SAT solver proxy */
/** 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;
+
+ /** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
public:
void shutdown() { }
/**
- * Converts the given formula to CNF and assert the CNF to the sat solver.
+ * Converts the given formula to CNF and assert the CNF to the SAT solver.
* The formula is asserted permanently for the current context.
* @param node the formula to assert
*/
void assertFormula(TNode node);
/**
- * Converts the given formula to CNF and assert the CNF to the sat solver.
- * The formula can be removed by the sat solver after backtracking lower
+ * Converts the given formula to CNF and assert the CNF to the SAT solver.
+ * The formula can be removed by the SAT solver after backtracking lower
* than the (SAT and SMT) level at which it was asserted.
*
* @param node the formula to assert
- * @param negated whether the node should be considered to be negated at the top level (or not)
- * @param removable whether this lemma can be quietly removed based on an activity heuristic (or not)
+ * @param negated whether the node should be considered to be negated
+ * at the top level (or not)
+ * @param removable whether this lemma can be quietly removed based
+ * on an activity heuristic (or not)
*/
void assertLemma(TNode node, bool negated, bool removable);
/**
* 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();
+ Result checkSat(unsigned long& millis, unsigned long& resource);
/**
* Get the value of a boolean variable.
*/
Node getValue(TNode node);
- /*
- * Return true if node has an associated SAT literal
+ /**
+ * Return true if node has an associated SAT literal.
*/
bool isSatLiteral(TNode node);
+ /**
+ * Return true if node has an associated SAT literal that is
+ * currently translated (i.e., it's relevant to the current
+ * user push/pop level).
+ */
+ bool isTranslatedSatLiteral(TNode node);
+
/**
* Check if the node has a value and return it if yes.
*/
*/
void pop();
+ /**
+ * 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.
+ */
+ void spendResource() throw();
+
};/* class PropEngine */
+
+inline void SatTimer::check() {
+ if(expired()) {
+ Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
+ d_propEngine.interrupt();
+ }
+}
+
+inline void PropEngine::checkTime() {
+ d_satTimer.check();
+}
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
}
void SatSolver::notifyRestart() {
+ d_propEngine->checkTime();
d_theoryEngine->notifyRestart();
}
#endif /* CVC4_REPLAY */
}
+void SatSolver::checkTime() {
+ d_propEngine->checkTime();
+}
}/* CVC4::prop namespace */
}/* CVC4 namespace */
virtual void unregisterVar(SatLiteral lit) = 0;
/** Register the variable (of the literal) for solving */
virtual void renewVar(SatLiteral lit, int level = -1) = 0;
+ /** Interrupt the solver */
+ virtual void interrupt() = 0;
};
/**
virtual ~SatSolver();
- bool solve();
+ SatLiteralValue solve(unsigned long& resource);
void addClause(SatClause& clause, bool removable);
void renewVar(SatLiteral lit, int level = -1);
+ void interrupt();
+
TNode getNode(SatLiteral lit);
void notifyRestart();
void logDecision(SatLiteral lit);
+ void checkTime();
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
delete d_minisat;
}
-inline bool SatSolver::solve() {
- return d_minisat->solve();
+inline SatLiteralValue SatSolver::solve(unsigned long& resource) {
+ Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+ if(resource == 0) {
+ d_minisat->budgetOff();
+ } else {
+ d_minisat->setConfBudget(resource);
+ }
+ Minisat::vec<SatLiteral> empty;
+ unsigned long conflictsBefore = d_minisat->conflicts;
+ SatLiteralValue result = d_minisat->solveLimited(empty);
+ d_minisat->clearInterrupt();
+ resource = d_minisat->conflicts - conflictsBefore;
+ Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+ return result;
}
inline void SatSolver::addClause(SatClause& clause, bool removable) {
d_minisat->renewVar(lit, level);
}
+inline void SatSolver::interrupt() {
+ d_minisat->interrupt();
+}
+
#endif /* __CVC4_USE_MINISAT */
inline size_t
SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_context(em->getContext()),
+ d_userLevels(),
d_userContext(new UserContext()),
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
+ d_theoryEngine(NULL),
+ d_propEngine(NULL),
+ d_definedFunctions(NULL),
+ d_assertionList(NULL),
+ d_assignments(NULL),
+ d_logic(""),
+ d_problemExtended(false),
+ d_queryMade(false),
+ d_timeBudgetCumulative(0),
+ d_timeBudgetPerCall(0),
+ d_resourceBudgetCumulative(0),
+ d_resourceBudgetPerCall(0),
+ d_cumulativeTimeUsed(0),
+ d_cumulativeResourceUsed(0),
+ d_status(),
d_private(new smt::SmtEnginePrivate(*this)),
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
- d_assertionList = NULL;
if(Options::current()->interactive) {
d_assertionList = new(true) AssertionList(d_userContext);
}
- d_assignments = NULL;
- d_problemExtended = false;
- d_queryMade = false;
+ if(Options::current()->perCallResourceLimit != 0) {
+ setResourceLimit(Options::current()->perCallResourceLimit, false);
+ }
+ if(Options::current()->cumulativeResourceLimit != 0) {
+ setResourceLimit(Options::current()->cumulativeResourceLimit, true);
+ }
+ if(Options::current()->perCallMillisecondLimit != 0) {
+ setTimeLimit(Options::current()->perCallMillisecondLimit, false);
+ }
+ if(Options::current()->cumulativeMillisecondLimit != 0) {
+ setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
+ }
}
void SmtEngine::shutdown() {
Result SmtEngine::check() {
Trace("smt") << "SmtEngine::check()" << endl;
- // make sure the prop layer has all assertions
- Trace("smt") << "SmtEngine::check(): processing assertion" << endl;
+ // 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);
+ }
+ }
+ 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);
+ }
+ }
+ if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
+ resource = d_resourceBudgetPerCall;
+ }
+
Trace("smt") << "SmtEngine::check(): running check" << endl;
- return d_propEngine->checkSat();
+ Result result = d_propEngine->checkSat(millis, resource);
+
+ // PropEngine::checkSat() returns the actual amount used in these
+ // variables.
+ d_cumulativeTimeUsed += millis;
+ d_cumulativeResourceUsed += resource;
+
+ Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
+ << ", conflicts " << d_cumulativeResourceUsed << std::endl;
+
+ return result;
}
Result SmtEngine::quickCheck() {
if(!Options::current()->incrementalSolving) {
throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
}
+ if(d_userContext->getLevel() == 0) {
+ throw ModalException("Cannot pop beyond the first user frame");
+ }
AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
while (d_userLevels.back() < d_userContext->getLevel()) {
internalPop();
}
}
+void SmtEngine::interrupt() throw(ModalException) {
+ d_propEngine->interrupt();
+}
+
+void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
+ if(cumulative) {
+ Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl;
+ d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+ } else {
+ Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl;
+ d_resourceBudgetPerCall = units;
+ }
+}
+
+void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
+ if(cumulative) {
+ Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl;
+ d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
+ } else {
+ Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl;
+ d_timeBudgetPerCall = millis;
+ }
+}
+
+unsigned long SmtEngine::getResourceUsage() const {
+ return d_cumulativeResourceUsed;
+}
+
+unsigned long SmtEngine::getTimeUsage() const {
+ return d_cumulativeTimeUsed;
+}
+
+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;
+}
+
+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;
+}
+
StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
return d_exprManager->d_nodeManager->getStatisticsRegistry();
}
/** Our expression manager */
ExprManager* d_exprManager;
- /** Out internal expression/node manager */
+ /** Our internal expression/node manager */
NodeManager* d_nodeManager;
/** The decision engine */
TheoryEngine* d_theoryEngine;
*/
bool d_queryMade;
+ /** 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).
*/
*/
void pop();
+ /**
+ * Interrupt a running query. This can be called from another thread
+ * or from a signal handler. Throws a ModalException if the SmtEngine
+ * isn't currently in a query.
+ */
+ void interrupt() throw(ModalException);
+
+ /**
+ * Set a resource limit for SmtEngine operations. This is like a time
+ * limit, but it's deterministic so that reproducible results can be
+ * obtained. However, please note that it may not be deterministic
+ * between different versions of CVC4, or even the same version on
+ * different platforms.
+ *
+ * A cumulative and non-cumulative (per-call) resource limit can be
+ * set at the same time. A call to setResourceLimit() with
+ * cumulative==true replaces any cumulative resource limit currently
+ * in effect; a call with cumulative==false replaces any per-call
+ * resource limit currently in effect. Time limits can be set in
+ * addition to resource limits; the SmtEngine obeys both. That means
+ * that up to four independent limits can control the SmtEngine
+ * at the same time.
+ *
+ * When an SmtEngine is first created, it has no time or resource
+ * limits.
+ *
+ * Currently, these limits only cause the SmtEngine to stop what its
+ * doing when the limit expires (or very shortly thereafter); no
+ * heuristics are altered by the limits or the threat of them expiring.
+ * We reserve the right to change this in the future.
+ *
+ * @param units the resource limit, or 0 for no limit
+ * @param cumulative whether this resource limit is to be a cumulative
+ * resource limit for all remaining calls into the SmtEngine (true), or
+ * whether it's a per-call resource limit (false); the default is false
+ */
+ void setResourceLimit(unsigned long units, bool cumulative = false);
+
+ /**
+ * Set a time limit for SmtEngine operations.
+ *
+ * A cumulative and non-cumulative (per-call) time limit can be
+ * set at the same time. A call to setTimeLimit() with
+ * cumulative==true replaces any cumulative time limit currently
+ * in effect; a call with cumulative==false replaces any per-call
+ * time limit currently in effect. Resource limits can be set in
+ * addition to time limits; the SmtEngine obeys both. That means
+ * that up to four independent limits can control the SmtEngine
+ * at the same time.
+ *
+ * Note that the cumulative timer only ticks away when one of the
+ * SmtEngine's workhorse functions (things like assertFormula(),
+ * query(), checkSat(), and simplify()) are running. Between calls,
+ * the timer is still.
+ *
+ * When an SmtEngine is first created, it has no time or resource
+ * limits.
+ *
+ * Currently, these limits only cause the SmtEngine to stop what its
+ * doing when the limit expires (or very shortly thereafter); no
+ * heuristics are altered by the limits or the threat of them expiring.
+ * We reserve the right to change this in the future.
+ *
+ * @param millis the time limit in milliseconds, or 0 for no limit
+ * @param cumulative whether this time limit is to be a cumulative
+ * time limit for all remaining calls into the SmtEngine (true), or
+ * whether it's a per-call time limit (false); the default is false
+ */
+ void setTimeLimit(unsigned long millis, bool cumulative = false);
+
+ /**
+ * Get the current resource usage count for this SmtEngine. This
+ * function can be used to ascertain reasonable values to pass as
+ * resource limits to setResourceLimit().
+ */
+ unsigned long getResourceUsage() const;
+
+ /**
+ * Get the current millisecond count for this SmtEngine.
+ */
+ unsigned long getTimeUsage() const;
+
+ /**
+ * Get the remaining resources that can be consumed by this SmtEngine
+ * according to the currently-set cumulative resource limit. If there
+ * is not a cumulative resource limit set, this function throws a
+ * ModalException.
+ */
+ unsigned long getResourceRemaining() const throw(ModalException);
+
+ /**
+ * Get the remaining number of milliseconds that can be consumed by
+ * this SmtEngine according to the currently-set cumulative time limit.
+ * If there is not a cumulative resource limit set, this function
+ * throws a ModalException.
+ */
+ unsigned long getTimeRemaining() const throw(ModalException);
+
/**
* Permit access to the underlying StatisticsRegistry.
*/
template<>
Node RewriteRule<ReflexivityEq>::apply(Node node) {
BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
- return node[1].eqNode(node[0]);;
+ return node[1].eqNode(node[0]);
}
}
*/
virtual void setIncomplete() throw(AssertionException) = 0;
+ /**
+ * "Spend" a "resource." The meaning is specific to the context in
+ * which the theory is operating, and may even be ignored. The
+ * intended meaning is that if the user has set a limit on the "units
+ * of resource" that can be expended in a search, and that limit is
+ * exceeded, then the search is terminated. Note that the check for
+ * termination occurs in the main search loop, so while theories
+ * should call OutputChannel::spendResource() during particularly
+ * long-running operations, they cannot rely on resource() to break
+ * out of infinite or intractable computations.
+ */
+ virtual void spendResource() throw() {
+ }
+
};/* class OutputChannel */
}/* CVC4::theory namespace */
*/
void TheoryEngine::check(Theory::Effort effort) {
+ d_propEngine->checkTime();
+
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
bool value;
if (conflict.getKind() == kind::AND) {
for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
- if (!getPropEngine()->hasValue(conflict[i], value)) return false;
- if (!value) return false;
+ if (! getPropEngine()->hasValue(conflict[i], value)) {
+ Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+ << conflict[i] << endl;
+ return false;
+ }
+ if (! value) {
+ Debug("properConflict") << "Bad conflict is due to false atom: "
+ << conflict[i] << endl;
+ return false;
+ }
}
} else {
- if (!getPropEngine()->hasValue(conflict, value)) return false;
- return value;
+ if (! getPropEngine()->hasValue(conflict, value)) {
+ Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+ << conflict << endl;
+ return false;
+ }
+ if(! value) {
+ Debug("properConflict") << "Bad conflict is due to false atom: "
+ << conflict << endl;
+ return false;
+ }
}
return true;
}
bool TheoryEngine::properPropagation(TNode lit) const {
- Assert(!lit.isNull());
-#warning implement TheoryEngine::properPropagation()
- return true;
+ if(!getPropEngine()->isTranslatedSatLiteral(lit)) {
+ return false;
+ }
+ bool b;
+ return !getPropEngine()->hasValue(lit, b);
}
bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
{
Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+ d_propEngine->checkTime();
+
// Get the atom
TNode atom = node.getKind() == kind::NOT ? node[0] : node;
void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl;
+
+ d_propEngine->checkTime();
if(Dump.isOn("t-propagations")) {
Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
void setIncomplete() throw(AssertionException) {
d_engine->setIncomplete(d_theory);
}
+
+ void spendResource() throw() {
+ d_engine->spendResource();
+ }
+
};/* class EngineOutputChannel */
/**
void conflict(TNode conflict) {
- Assert(properConflict(conflict));
+ Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str());
// Mark that we are in conflict
d_inConflict = true;
d_incomplete = true;
}
+ /**
+ * "Spend" a resource during a search or preprocessing.
+ */
+ void spendResource() throw() {
+ d_propEngine->spendResource();
+ }
+
/**
* Is the theory active.
*/
--disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
--disable-arithmetic-propagation turns on arithmetic propagation\n\
--disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
- --incremental | -i enable incremental solving\n";
+ --incremental | -i enable incremental solving\n\
+ --time-limit=MS enable time limiting (give milliseconds)\n\
+ --time-limit-per=MS enable time limiting per query (give milliseconds)\n\
+ --limit=N enable resource limiting\n\
+ --limit-per=N enable resource limiting per query\n";
#warning "Change CL options as --disable-variable-removal cannot do anything currently."
ARITHMETIC_PROPAGATION,
ARITHMETIC_PIVOT_THRESHOLD,
ARITHMETIC_PROP_MAX_LENGTH,
- DISABLE_SYMMETRY_BREAKER
+ DISABLE_SYMMETRY_BREAKER,
+ TIME_LIMIT,
+ TIME_LIMIT_PER,
+ LIMIT,
+ LIMIT_PER
};/* enum OptionValue */
/**
{ "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
{ "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
{ "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
+ { "time-limit" , required_argument, NULL, TIME_LIMIT },
+ { "time-limit-per", required_argument, NULL, TIME_LIMIT_PER },
+ { "limit" , required_argument, NULL, LIMIT },
+ { "limit-per" , required_argument, NULL, LIMIT_PER },
{ NULL , no_argument , NULL, '\0' }
};/* if you add things to the above, please remember to update usage.h! */
ufSymmetryBreaker = false;
break;
+ case TIME_LIMIT:
+ {
+ int i = atoi(optarg);
+ if(i < 0) {
+ throw OptionException("--time-limit requires a nonnegative argument.");
+ }
+ cumulativeMillisecondLimit = (unsigned long) i;
+ }
+ break;
+ case TIME_LIMIT_PER:
+ {
+ int i = atoi(optarg);
+ if(i < 0) {
+ throw OptionException("--time-limit-per requires a nonnegative argument.");
+ }
+ perCallMillisecondLimit = (unsigned long) i;
+ }
+ break;
+ case LIMIT:
+ {
+ int i = atoi(optarg);
+ if(i < 0) {
+ throw OptionException("--limit requires a nonnegative argument.");
+ }
+ cumulativeResourceLimit = (unsigned long) i;
+ }
+ break;
+ case LIMIT_PER:
+ {
+ int i = atoi(optarg);
+ if(i < 0) {
+ throw OptionException("--limit-per requires a nonnegative argument.");
+ }
+ perCallResourceLimit = (unsigned long) i;
+ break;
+ }
+
case RANDOM_SEED:
satRandomSeed = atof(optarg);
break;
*/
bool interactiveSetByUser;
+ /** Per-query resource limit. */
+ unsigned long perCallResourceLimit;
+ /** Cumulative resource limit. */
+ unsigned long cumulativeResourceLimit;
+
+ /** Per-query time limit in milliseconds. */
+ unsigned long perCallMillisecondLimit;
+ /** Cumulative time limit in milliseconds. */
+ unsigned long cumulativeMillisecondLimit;
+
/** Whether we should "spin" on a SIG_SEGV. */
bool segvNoSpin;
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = TIMEOUT;
+ } else if(s == "resourceout") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = RESOURCEOUT;
} else if(s == "memout") {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
d_unknownExplanation = MEMOUT;
+ } else if(s == "interrupted") {
+ d_which = TYPE_SAT;
+ d_sat = SAT_UNKNOWN;
+ d_unknownExplanation = INTERRUPTED;
} else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) {
d_which = TYPE_SAT;
d_sat = SAT_UNKNOWN;
case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
case Result::INCOMPLETE: out << "INCOMPLETE"; break;
case Result::TIMEOUT: out << "TIMEOUT"; break;
+ case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
case Result::MEMOUT: out << "MEMOUT"; break;
+ case Result::INTERRUPTED: out << "INTERRUPTED"; break;
case Result::NO_STATUS: out << "NO_STATUS"; break;
+ case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
case Result::OTHER: out << "OTHER"; break;
case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
default: Unhandled(e);
REQUIRES_FULL_CHECK,
INCOMPLETE,
TIMEOUT,
+ RESOURCEOUT,
MEMOUT,
+ INTERRUPTED,
NO_STATUS,
UNSUPPORTED,
OTHER,
void renewVar(SatLiteral lit, int level = -1) {
}
+ void interrupt() {
+ }
};
class CnfStreamBlack : public CxxTest::TestSuite {
projects / cvc5.git / commitdiff