summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp129
1 files changed, 120 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 21f2d9209..2cc606fa9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -52,6 +52,7 @@
#include "util/node_visitor.h"
#include "util/configuration.h"
#include "util/exception.h"
+#include "util/nary_builder.h"
#include "smt/command_list.h"
#include "smt/boolean_terms.h"
#include "smt/options.h"
@@ -90,6 +91,19 @@ namespace CVC4 {
namespace smt {
+/** Useful for counting the number of recursive calls. */
+class ScopeCounter {
+private:
+ unsigned& d_depth;
+public:
+ ScopeCounter(unsigned& d) : d_depth(d) {
+ ++d_depth;
+ }
+ ~ScopeCounter(){
+ --d_depth;
+ }
+};
+
/**
* Representation of a defined function. We keep these around in
* SmtEngine to permit expanding definitions late (and lazily), to
@@ -150,6 +164,9 @@ struct SmtEngineStatistics {
/** time spent in processAssertions() */
TimerStat d_processAssertionsTime;
+ /** Has something simplified to false? */
+ IntStat d_simplifiedToFalse;
+
SmtEngineStatistics() :
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
@@ -168,7 +185,10 @@ struct SmtEngineStatistics {
d_checkModelTime("smt::SmtEngine::checkModelTime"),
d_solveTime("smt::SmtEngine::solveTime"),
d_pushPopTime("smt::SmtEngine::pushPopTime"),
- d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") {
+ d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+ d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
+
+ {
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
@@ -188,6 +208,7 @@ struct SmtEngineStatistics {
StatisticsRegistry::registerStat(&d_solveTime);
StatisticsRegistry::registerStat(&d_pushPopTime);
StatisticsRegistry::registerStat(&d_processAssertionsTime);
+ StatisticsRegistry::registerStat(&d_simplifiedToFalse);
}
~SmtEngineStatistics() {
@@ -209,6 +230,7 @@ struct SmtEngineStatistics {
StatisticsRegistry::unregisterStat(&d_solveTime);
StatisticsRegistry::unregisterStat(&d_pushPopTime);
StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
+ StatisticsRegistry::unregisterStat(&d_simplifiedToFalse);
}
};/* struct SmtEngineStatistics */
@@ -305,6 +327,10 @@ class SmtEnginePrivate : public NodeManagerListener {
*/
Node d_modZero;
+ /** Number of calls of simplify assertions active.
+ */
+ unsigned d_simplifyAssertionsDepth;
+
public:
/**
* Map from skolem variables to index in d_assertionsToCheck containing
@@ -353,11 +379,15 @@ private:
void bvToBool();
// Simplify ITE structure
- void simpITE();
+ bool simpITE();
// Simplify based on unconstrained values
void unconstrainedSimp();
+ // Ensures the assertions asserted after before now
+ // effectively come before d_realAssertionsEnd
+ void compressBeforeRealAssertions(size_t before);
+
/**
* Any variable in an assertion that is declared as a subtype type
* (predicate subtype or integer subrange type) must be constrained
@@ -402,6 +432,7 @@ public:
d_divByZero(),
d_intDivByZero(),
d_modZero(),
+ d_simplifyAssertionsDepth(0),
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
d_topLevelSubstitutions(smt.d_userContext)
@@ -869,12 +900,41 @@ void SmtEngine::setLogicInternal() throw() {
}
// Turn on ite simplification for QF_LIA and QF_AUFBV
if(! options::doITESimp.wasSetByUser()) {
- bool iteSimp = !d_logic.isQuantified() &&
- ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) ||
- (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
+ bool qf_aufbv = !d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV);
+ bool qf_lia = !d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) &&
+ d_logic.isLinear() &&
+ !d_logic.isDifferenceLogic() &&
+ !d_logic.areRealsUsed();
+
+ bool iteSimp = (qf_aufbv || qf_lia);
Trace("smt") << "setting ite simplification to " << iteSimp << endl;
options::doITESimp.set(iteSimp);
}
+ if(! options::compressItes.wasSetByUser() ){
+ bool qf_lia = !d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) &&
+ d_logic.isLinear() &&
+ !d_logic.isDifferenceLogic() &&
+ !d_logic.areRealsUsed();
+
+ bool compressIte = qf_lia;
+ Trace("smt") << "setting ite compression to " << compressIte << endl;
+ options::compressItes.set(compressIte);
+ }
+ if(! options::simplifyWithCareEnabled.wasSetByUser() ){
+ bool qf_aufbv = !d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV);
+
+ bool withCare = qf_aufbv;
+ Trace("smt") << "setting ite simplify with care to " << withCare << endl;
+ options::simplifyWithCareEnabled.set(withCare);
+ }
// Turn off array eager index splitting for QF_AUFLIA
if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
if (not d_logic.isQuantified() &&
@@ -2031,16 +2091,56 @@ void SmtEnginePrivate::bvToBool() {
}
}
-void SmtEnginePrivate::simpITE() {
+bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
+ unsigned numAssertionOnEntry = d_assertionsToCheck.size();
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+ Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+ d_assertionsToCheck[i] = result;
+ if(result.isConst() && !result.getConst<bool>()){
+ return false;
+ }
}
+ bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
+ if(numAssertionOnEntry < d_assertionsToCheck.size()){
+ compressBeforeRealAssertions(numAssertionOnEntry);
+ }
+ return result;
}
+void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
+ size_t curr = d_assertionsToCheck.size();
+ if(before >= curr ||
+ d_realAssertionsEnd <= 0 ||
+ d_realAssertionsEnd >= curr){
+ return;
+ }
+
+ // assertions
+ // original: [0 ... d_realAssertionsEnd)
+ // can be modified
+ // ites skolems [d_realAssertionsEnd, before)
+ // cannot be moved
+ // added [before, curr)
+ // can be modified
+ Assert(0 < d_realAssertionsEnd);
+ Assert(d_realAssertionsEnd <= before);
+ Assert(before < curr);
+
+ std::vector<Node> intoConjunction;
+ for(size_t i = before; i<curr; ++i){
+ intoConjunction.push_back(d_assertionsToCheck[i]);
+ }
+ d_assertionsToCheck.resize(before);
+ size_t lastBeforeItes = d_realAssertionsEnd - 1;
+ intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+ Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+ d_assertionsToCheck[lastBeforeItes] = newLast;
+ Assert(d_assertionsToCheck.size() == before);
+}
void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
@@ -2490,11 +2590,13 @@ void SmtEnginePrivate::doMiplibTrick() {
d_realAssertionsEnd = d_assertionsToCheck.size();
}
+
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
throw(TypeCheckingException, LogicException) {
Assert(d_smt.d_pendingPops == 0);
try {
+ ScopeCounter depth(d_simplifyAssertionsDepth);
Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
@@ -2560,9 +2662,14 @@ bool SmtEnginePrivate::simplifyAssertions()
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
// ITE simplification
- if(options::doITESimp()) {
+ if(options::doITESimp() &&
+ (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
Chat() << "...doing ITE simplification..." << endl;
- simpITE();
+ bool noConflict = simpITE();
+ if(!noConflict){
+ Chat() << "...ITE simplification found unsat..." << endl;
+ return false;
+ }
}
dumpAssertions("post-itesimp", d_assertionsToCheck);
@@ -2916,6 +3023,9 @@ void SmtEnginePrivate::processAssertions() {
dumpAssertions("pre-simplify", d_assertionsToPreprocess);
Chat() << "simplifying assertions..." << endl;
bool noConflict = simplifyAssertions();
+ if(!noConflict){
+ ++(d_smt.d_stats->d_simplifiedToFalse);
+ }
dumpAssertions("post-simplify", d_assertionsToCheck);
dumpAssertions("pre-static-learning", d_assertionsToCheck);
@@ -2954,6 +3064,7 @@ void SmtEnginePrivate::processAssertions() {
if(options::repeatSimp()) {
d_assertionsToCheck.swap(d_assertionsToPreprocess);
Chat() << "re-simplifying assertions..." << endl;
+ ScopeCounter depth(d_simplifyAssertionsDepth);
noConflict &= simplifyAssertions();
if (noConflict) {
// Need to fix up assertion list to maintain invariants:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback