summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/compat/cvc3_compat.cpp12
-rw-r--r--src/smt/smt_engine.cpp49
-rw-r--r--src/smt/smt_engine.h14
3 files changed, 49 insertions, 26 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 96cef406f..fafc8ccb2 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2228,7 +2228,7 @@ Proof ValidityChecker::getProofClosure() {
}
int ValidityChecker::stackLevel() {
- return d_smt->getStackLevel();
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
}
void ValidityChecker::push() {
@@ -2240,15 +2240,7 @@ void ValidityChecker::pop() {
}
void ValidityChecker::popto(int stackLevel) {
- CheckArgument(stackLevel >= 0, stackLevel,
- "Cannot pop to a negative stack level %u", stackLevel);
- CheckArgument(unsigned(stackLevel) <= d_smt->getStackLevel(), stackLevel,
- "Cannot pop to a level higher than the current one! "
- "At level %u, user requested level %d",
- d_smt->getStackLevel(), stackLevel);
- while(unsigned(stackLevel) < d_smt->getStackLevel()) {
- pop();
- }
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
}
int ValidityChecker::scopeLevel() {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 832779944..b9732c32e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -143,7 +143,8 @@ class SmtEnginePrivate {
* holds the last substitution from d_topLevelSubstitutions
* that was pushed out to SAT.
* If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
- * then nothing has been pushed out yet. */
+ * then nothing has been pushed out yet.
+ */
context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPos;
static const bool d_doConstantProp = true;
@@ -254,6 +255,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
d_assertionList(NULL),
d_assignments(NULL),
d_logic(),
+ d_pendingPops(0),
d_fullyInited(false),
d_problemExtended(false),
d_queryMade(false),
@@ -377,6 +379,8 @@ void SmtEngine::shutdown() {
Dump("benchmark") << QuitCommand();
}
+ doPendingPops();
+
// check to see if a postsolve() is pending
if(d_needPostsolve) {
d_theoryEngine->postsolve();
@@ -392,8 +396,10 @@ SmtEngine::~SmtEngine() throw() {
SmtScope smts(this);
try {
+ doPendingPops();
+
while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
- internalPop();
+ internalPop(true);
}
shutdown();
@@ -1267,6 +1273,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
// returns false if simpflication led to "false"
bool SmtEnginePrivate::simplifyAssertions()
throw(TypeCheckingException, AssertionException) {
+ Assert(d_smt.d_pendingPops == 0);
try {
Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
@@ -1348,6 +1355,7 @@ bool SmtEnginePrivate::simplifyAssertions()
Result SmtEngine::check() {
Assert(d_fullyInited);
+ Assert(d_pendingPops == 0);
Trace("smt") << "SmtEngine::check()" << endl;
@@ -1399,6 +1407,7 @@ Result SmtEngine::quickCheck() {
void SmtEnginePrivate::processAssertions() {
Assert(d_smt.d_fullyInited);
+ Assert(d_smt.d_pendingPops == 0);
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
@@ -1572,6 +1581,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
@@ -1635,6 +1645,7 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
Trace("smt") << "SMT query(" << e << ")" << endl;
@@ -1690,6 +1701,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException)
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
ensureBoolean(e);
if(d_assertionList != NULL) {
@@ -1703,6 +1715,7 @@ Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) {
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
if( options::typeChecking() ) {
e.getType(true);// ensure expr is type-checked at this point
}
@@ -1766,6 +1779,7 @@ Expr SmtEngine::getValue(const Expr& e)
bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
Type type = e.getType(options::typeChecking());
// must be Boolean
CheckArgument( type.isBoolean(), e,
@@ -1857,6 +1871,7 @@ void SmtEngine::addToModelCommand( Command* c, int c_type ){
Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl;
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
if( options::produceModels() ) {
d_theoryEngine->getModel()->addCommand( c, c_type );
}
@@ -1866,6 +1881,12 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
+ finalOptionsAreSet();
+
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << GetModelCommand();
+ }
+
if(d_status.isNull() ||
d_status.asSatisfiabilityResult() == Result::UNSAT ||
d_problemExtended) {
@@ -1911,6 +1932,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
vector<Expr> SmtEngine::getAssertions()
throw(ModalException, AssertionException) {
+ finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssertionsCommand();
}
@@ -1926,15 +1948,10 @@ vector<Expr> SmtEngine::getAssertions()
return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
}
-size_t SmtEngine::getStackLevel() const {
- SmtScope smts(this);
- Trace("smt") << "SMT getStackLevel()" << endl;
- return d_context->getLevel();
-}
-
void SmtEngine::push() {
SmtScope smts(this);
finalOptionsAreSet();
+ doPendingPops();
Trace("smt") << "SMT push()" << endl;
d_private->processAssertions();
if(Dump.isOn("benchmark")) {
@@ -1978,7 +1995,7 @@ void SmtEngine::pop() {
AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
while (d_userLevels.back() < d_userContext->getLevel()) {
- internalPop();
+ internalPop(true);
}
d_userLevels.pop_back();
@@ -1996,6 +2013,7 @@ void SmtEngine::pop() {
void SmtEngine::internalPush() {
Assert(d_fullyInited);
Trace("smt") << "SmtEngine::internalPush()" << endl;
+ doPendingPops();
if(options::incrementalSolving()) {
d_private->processAssertions();
d_userContext->push();
@@ -2004,13 +2022,24 @@ void SmtEngine::internalPush() {
}
}
-void SmtEngine::internalPop() {
+void SmtEngine::internalPop(bool immediate) {
Assert(d_fullyInited);
Trace("smt") << "SmtEngine::internalPop()" << endl;
if(options::incrementalSolving()) {
+ ++d_pendingPops;
+ }
+ if(immediate) {
+ doPendingPops();
+ }
+}
+
+void SmtEngine::doPendingPops() {
+ Assert(d_pendingPops == 0 || options::incrementalSolving());
+ while(d_pendingPops > 0) {
d_propEngine->pop();
d_context->pop();
d_userContext->pop();
+ --d_pendingPops;
}
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 234814245..2c99bc7eb 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -135,6 +135,11 @@ class CVC4_PUBLIC SmtEngine {
LogicInfo d_logic;
/**
+ * Number of internal pops that have been deferred.
+ */
+ unsigned d_pendingPops;
+
+ /**
* Whether or not this SmtEngine has been fully initialized (that is,
* the ). This post-construction initialization is automatically
* triggered by the use of the SmtEngine; e.g. when setLogic() is
@@ -238,7 +243,9 @@ class CVC4_PUBLIC SmtEngine {
void internalPush();
- void internalPop();
+ void internalPop(bool immediate = false);
+
+ void doPendingPops();
/**
* Internally handle the setting of a logic. This function should always
@@ -415,11 +422,6 @@ public:
std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
/**
- * Get the current context level.
- */
- size_t getStackLevel() const;
-
- /**
* Push a user-level context.
*/
void push();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback