diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node.h | 9 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 16 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 14 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 47 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 | ||||
-rw-r--r-- | src/theory/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 16 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 6 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 11 | ||||
-rw-r--r-- | src/theory/substitutions.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 | ||||
-rw-r--r-- | src/util/options.cpp | 18 | ||||
-rw-r--r-- | src/util/options.h | 8 |
15 files changed, 161 insertions, 12 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 4d39ec60f..3532116bc 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -451,6 +451,15 @@ public: } /** + * Returns true if this node represents a constant + * @return true if const + */ + inline bool isVar() const { + assertTNodeNotExpired(); + return getMetaKind() == kind::metakind::VARIABLE; + } + + /** * Returns the unique id of this node * @return the ud */ diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index ade887b23..b9db8dace 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -49,6 +49,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFNRA"] = QF_UFNRA; logicMap["QF_ABV"] = QF_ABV; logicMap["QF_AUFBV"] = QF_AUFBV; + logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA; + logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA; logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; @@ -219,6 +221,20 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case QF_AUFBVLIA: + addUf(); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_INTS); + break; + + case QF_AUFBVLRA: + addUf(); + addTheory(THEORY_ARRAYS_EX); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_REALS); + break; + case QF_AUFLIA: addTheory(THEORY_INT_ARRAYS_EX); addUf(); diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 1606d7bab..34ec624bc 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -42,6 +42,8 @@ public: LRA, QF_ABV, QF_AUFBV, + QF_AUFBVLIA, + QF_AUFBVLRA, QF_AUFLIA, QF_AUFLIRA, QF_AX, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index dc1b47bde..3fa00baae 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -166,6 +166,20 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_BITVECTORS); break; + case Smt::QF_AUFBVLIA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_INTS); + break; + + case Smt::QF_AUFBVLRA: + addOperator(kind::APPLY_UF); + addTheory(THEORY_ARRAYS); + addTheory(THEORY_BITVECTORS); + addTheory(THEORY_REALS); + break; + case Smt::QF_AUFLIA: addTheory(THEORY_ARRAYS); addOperator(kind::APPLY_UF); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 68485ca8a..14b3e3b42 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -159,6 +159,9 @@ class SmtEnginePrivate { // Simplify ITE structure void simpITE(); + // Simplify based on unconstrained values + void unconstrainedSimp(); + /** * Any variable in a assertion that is declared as a subtype type * (predicate subtype or integer subrange type) must be constrained @@ -255,6 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_staticLearningTime("smt::SmtEngine::staticLearningTime"), d_simpITETime("smt::SmtEngine::simpITETime"), + d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), @@ -268,6 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); StatisticsRegistry::registerStat(&d_staticLearningTime); StatisticsRegistry::registerStat(&d_simpITETime); + StatisticsRegistry::registerStat(&d_unconstrainedSimpTime); StatisticsRegistry::registerStat(&d_iteRemovalTime); StatisticsRegistry::registerStat(&d_theoryPreprocessTime); StatisticsRegistry::registerStat(&d_cnfConversionTime); @@ -373,6 +378,7 @@ SmtEngine::~SmtEngine() throw() { StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); StatisticsRegistry::unregisterStat(&d_staticLearningTime); StatisticsRegistry::unregisterStat(&d_simpITETime); + StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime); StatisticsRegistry::unregisterStat(&d_iteRemovalTime); StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime); StatisticsRegistry::unregisterStat(&d_cnfConversionTime); @@ -449,6 +455,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; } + // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode + if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) { + bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); + bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; + Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; + NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp; + } // Turn on arith rewrite equalities only for pure arithmetic if(! Options::current()->arithRewriteEqSetByUser) { bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified(); @@ -886,16 +899,24 @@ void SmtEnginePrivate::nonClausalSimplify() { d_nonClausalLearnedLiterals.resize(j); } + hash_set<TNode, TNodeHashFunction> s; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]))); + Node assertion = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); + s.insert(assertion); + d_assertionsToCheck.push_back(assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal preprocessed: " - << d_assertionsToCheck.back() << endl; + << assertion << endl; } d_assertionsToPreprocess.clear(); for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { - d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]))); + Node learned = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])); + if (s.find(learned) != s.end()) { + continue; + } + s.insert(learned); + d_assertionsToCheck.push_back(learned); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal learned : " << d_assertionsToCheck.back() << endl; @@ -916,6 +937,16 @@ void SmtEnginePrivate::simpITE() } } + +void SmtEnginePrivate::unconstrainedSimp() +{ + TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime); + + Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; + d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck); +} + + void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions) throw(AssertionException) { @@ -993,7 +1024,10 @@ void SmtEnginePrivate::simplifyAssertions() // Perform non-clausal simplification Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing non-clausal simplification" << endl; + // Abuse the user context to make sure circuit propagator gets backtracked + d_smt.d_userContext->push(); nonClausalSimplify(); + d_smt.d_userContext->pop(); } else { Assert(d_assertionsToCheck.empty()); d_assertionsToCheck.swap(d_assertionsToPreprocess); @@ -1004,9 +1038,16 @@ void SmtEnginePrivate::simplifyAssertions() simpITE(); } + if(Options::current()->unconstrainedSimp) { + unconstrainedSimp(); + } + if(Options::current()->repeatSimp) { d_assertionsToCheck.swap(d_assertionsToPreprocess); + // Abuse the user context to make sure circuit propagator gets backtracked + d_smt.d_userContext->push(); nonClausalSimplify(); + d_smt.d_userContext->pop(); } if(Options::current()->doStaticLearning) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 10a37b712..f07815e2e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -231,6 +231,8 @@ class CVC4_PUBLIC SmtEngine { TimerStat d_staticLearningTime; /** time spent in simplifying ITEs */ TimerStat d_simpITETime; + /** time spent in simplifying ITEs */ + TimerStat d_unconstrainedSimpTime; /** time spent removing ITEs */ TimerStat d_iteRemovalTime; /** time spent in theory preprocessing */ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 1341c048a..85d6fbdf8 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -31,7 +31,9 @@ libtheory_la_SOURCES = \ term_registration_visitor.h \ term_registration_visitor.cpp \ ite_simplifier.h \ - ite_simplifier.cpp + ite_simplifier.cpp \ + unconstrained_simplifier.h \ + unconstrained_simplifier.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f5e4f4630..60e48dba2 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -68,10 +68,6 @@ public: private: - /** Back edges from nodes to where they are used */ - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; - BackEdgesMap d_backEdges; - /** The propagation queue */ std::vector<TNode> d_propagationQueue; @@ -111,6 +107,15 @@ private: */ DataClearer< std::vector<Node> > d_learnedLiteralClearer; + /** Back edges from nodes to where they are used */ + typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; + + /** + * Similar data clearer for back edges. + */ + DataClearer<BackEdgesMap> d_backEdgesClearer; + /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far context::CDHashSet<TNode, TNodeHashFunction> d_seen; @@ -231,12 +236,13 @@ public: */ CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : - d_backEdges(), d_propagationQueue(), d_propagationQueueClearer(context, d_propagationQueue), d_conflict(context, false), d_learnedLiterals(outLearnedLiterals), d_learnedLiteralClearer(context, outLearnedLiterals), + d_backEdges(), + d_backEdgesClearer(context, d_backEdges), d_seen(context), d_state(context), d_forwardPropagation(enableForward), diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5be052947..197134b6a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -405,6 +405,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) { updateCoefMap(left[i], size, leftMap, leftConst); } } + else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) { + return utils::mkFalse(); + } else { updateCoefMap(left, size, leftMap, leftConst); } @@ -415,6 +418,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) { updateCoefMap(right[i], size, rightMap, rightConst); } } + else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) { + return utils::mkFalse(); + } else { updateCoefMap(right, size, rightMap, rightConst); } diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index caf7566b9..b7ad1d174 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -71,6 +71,10 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) } // Mark the substitution and continue Node result = builder; + find = substitutionCache.find(result); + if (find != substitutionCache.end()) { + result = find->second; + } Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl; substitutionCache[current] = result; toVisit.pop_back(); @@ -114,13 +118,16 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); } - // Put the new substitution in - d_substitutions[x] = t; + // Put the new substitution in, but apply existing substitutions to rhs first + d_substitutions[x] = apply(t); // Also invalidate the cache if (invalidateCache) { d_cacheInvalidated = true; } + else { + d_substitutionCache[x] = d_substitutions[x]; + } } static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 958f50276..711ff9b72 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -107,6 +107,12 @@ public: void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** + * Returns true iff x is in the substitution map + */ + bool hasSubstitution(TNode x) + { return d_substitutions.find(x) != d_substitutions.end(); } + + /** * Apply the substitutions to the node. */ Node apply(TNode t); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f72275cb2..4ed0bcb60 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -62,7 +62,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_inPreregister(false), d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms) + d_sharedTermsVisitor(d_sharedTerms), + d_unconstrainedSimp(context, logicInfo) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -1011,3 +1012,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion) result = Rewriter::rewrite(result); return result; } + + +void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) +{ + d_unconstrainedSimp.processAssertions(assertions); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 019818a5f..bc9f4c889 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,6 +42,7 @@ #include "util/hash.h" #include "util/cache.h" #include "theory/ite_simplifier.h" +#include "theory/unconstrained_simplifier.h" namespace CVC4 { @@ -734,8 +735,12 @@ private: /** For preprocessing pass simplifying ITEs */ ITESimplifier d_iteSimplifier; + /** For preprocessing pass simplifying unconstrained expressions */ + UnconstrainedSimplifier d_unconstrainedSimp; + public: Node ppSimpITE(TNode assertion); + void ppUnconstrainedSimp(std::vector<Node>& assertions); };/* class TheoryEngine */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 01b9648ff..e9ef7d959 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -85,6 +85,8 @@ Options::Options() : doStaticLearning(true), doITESimp(false), doITESimpSetByUser(false), + unconstrainedSimp(false), + unconstrainedSimpSetByUser(false), repeatSimp(false), repeatSimpSetByUser(false), interactive(false), @@ -189,6 +191,8 @@ Additional CVC4 options:\n\ --no-static-learning turn off static learning (e.g. diamond-breaking)\n\ --ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ --no-ite-simp turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\ + --unconstrained-simp turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\ + --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\ --repeat-simp make multiple passes with nonclausal simplifier\n\ --no-repeat-simp do not make multiple passes with nonclausal simplifier\n\ --replay=file replay decisions from file\n\ @@ -430,6 +434,8 @@ enum OptionValue { NO_STATIC_LEARNING, ITE_SIMP, NO_ITE_SIMP, + UNCONSTRAINED_SIMP, + NO_UNCONSTRAINED_SIMP, REPEAT_SIMP, NO_REPEAT_SIMP, INTERACTIVE, @@ -530,6 +536,8 @@ static struct option cmdlineOptions[] = { { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "ite-simp", no_argument, NULL, ITE_SIMP }, { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP }, + { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP }, + { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP }, { "repeat-simp", no_argument, NULL, REPEAT_SIMP }, { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP }, { "interactive", no_argument , NULL, INTERACTIVE }, @@ -855,6 +863,16 @@ throw(OptionException) { doITESimpSetByUser = true; break; + case UNCONSTRAINED_SIMP: + unconstrainedSimp = true; + unconstrainedSimpSetByUser = true; + break; + + case NO_UNCONSTRAINED_SIMP: + unconstrainedSimp = false; + unconstrainedSimpSetByUser = true; + break; + case REPEAT_SIMP: repeatSimp = true; repeatSimpSetByUser = true; diff --git a/src/util/options.h b/src/util/options.h index e6135dacb..f48b45b49 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options { */ bool doITESimpSetByUser; + /** Whether to do the unconstrained simplification pass */ + bool unconstrainedSimp; + + /** + * Whether the user explicitly requested unconstrained simplification + */ + bool unconstrainedSimpSetByUser; + /** Whether to do multiple rounds of nonclausal simplification */ bool repeatSimp; |