}
Node CnfStream::getNode(const SatLiteral& literal) {
- Node node;
NodeCache::iterator find = d_nodeCache.find(literal);
- if(find != d_nodeCache.end()) {
- node = find->second;
- }
- return node;
+ Assert(find != d_nodeCache.end());
+ return find->second;
}
SatLiteral CnfStream::convertAtom(TNode node) {
return lit;
}
-SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) {
+SatLiteral CnfStream::getLiteral(TNode node) {
TranslationCache::iterator find = d_translationCache.find(node);
- SatLiteral literal;
- if(create) {
- if(find == d_translationCache.end()) {
- literal = convertAtom(node);
- } else {
- literal = find->second;
- }
- } else {
- Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
- literal = find->second;
- }
- Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl;
+ Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+ SatLiteral literal = find->second;
+ Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
return literal;
}
* representation.
* @param node [Presumably there are some constraints on the kind of
* node? E.g., it needs to be a boolean? -Chris]
- * @param create Controls whether or not to create a new SAT literal
- * mapping for Node if it does not exist. This exists to break
- * circular dependencies, where an atom is converted and asserted to
- * the SAT solver, which propagates it immediately since it's a
- * unit, which can theory-propagate additional literals that don't
- * yet have a SAT literal mapping.
*/
- SatLiteral getLiteral(TNode node, bool create = false);
+ SatLiteral getLiteral(TNode node);
const TranslationCache& getTranslationCache() const {
return d_translationCache;
CRef Solver::reason(Var x) const {
- // If we already have a reaspon, just return it
+ // If we already have a reason, just return it
if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
// What's the literal we are trying to explain
// Get the explanation from the theory
SatClause explanation;
proxy->explainPropagation(l, explanation);
- assert(explanation[0] == l);
+ Assert(explanation[0] == l);
// We're actually changing the state, so we hack it into non-const
Solver* nonconst_this = const_cast<Solver*>(this);
void Solver::attachClause(CRef cr) {
const Clause& c = ca[cr];
- assert(c.size() > 1);
+ Assert(c.size() > 1);
watches[~c[0]].push(Watcher(cr, c[1]));
watches[~c[1]].push(Watcher(cr, c[0]));
if (c.learnt()) learnts_literals += c.size();
// The effort we will be using to theory check
CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
- CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD;
+ CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD;
// Keep running until we have checked everything, we
// have no conflict and no new literals have been asserted
proxy->theoryPropagate(propagatedLiterals);
const unsigned i_end = propagatedLiterals.size();
for (unsigned i = 0; i < i_end; ++ i) {
+ Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy);
}
proxy->clearPropagatedLiterals();
for (int i = 0; i < clause_size; ++i) {
int current_level = level(var(clause[i]));
Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(var(clause[i])) << " at level " << current_level << std::endl;
- Assert(assigns[var(clause[i])] != l_Undef, "Got an unassigned literal in conflict!");
+ Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!");
if (current_level > max_level) max_level = current_level;
}
// If smaller than the decision level then pop back so we can analyse
*j++ = w; continue; }
// Look for new watch:
+ Assert(c.size() >= 2);
for (int k = 2; k < c.size(); k++)
if (value(c[k]) != l_False){
c[1] = c[k]; c[k] = false_lit;
(int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
}
- // We have a conflict so, we are going back to standard checks
+ // We have a conflict so, we are going back to standard checks
check_type = CHECK_WITH_PROPAGATION_STANDARD;
}else{
// NO CONFLICT
- // If this was a final check, we are satisfiable
+ // If this was a final check, we are satisfiable
if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
return l_True;
for (int i = 0; i < trail.size(); i++){
Var v = var(trail[i]);
- if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
+ if (hasReason(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
ca.reloc(vardata[v].reason, to);
}
int decisionLevel () const; // Gives the current decisionlevel.
uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
CRef reason (Var x) const;
+ bool hasReason (Var x) const; // Does the variable have a reason
int level (Var x) const;
double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
bool withinBudget () const;
//=================================================================================================
// Implementation of inline methods:
+inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+
inline int Solver::level (Var x) const { return vardata[x].level; }
inline void Solver::insertVarOrder(Var x) {
const unsigned i_end = outputNodes.size();
for (unsigned i = 0; i < i_end; ++ i) {
Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl;
- // The second argument ("true") instructs the CNF stream to create
- // a new literal mapping if it doesn't exist. This can happen due
- // to a circular dependence, if a SAT literal "a" is asserted as a
- // unit to the SAT solver, a round of theory propagation can occur
- // before all Nodes have SAT variable mappings.
- SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true);
+ SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]);
output.push_back(l);
}
}
void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
Node literalNode = d_cnfStream->getNode(l);
Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
- // We can get null from the prop engine if the literal is useless (i.e.)
- // the expression is not in context anyomore
- if(!literalNode.isNull()) {
- d_theoryEngine->assertFact(literalNode);
- }
+ Assert(!literalNode.isNull());
+ d_theoryEngine->assertFact(literalNode);
}
void SatSolver::setCnfStream(CnfStream* cnfStream) {
AM_CPPFLAGS = \
-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" \
"-I@top_srcdir@/src" "-I@top_builddir@/src" \
+ "-I@top_srcdir@/src/prop/minisat" \
+ -D __STDC_LIMIT_MACROS \
+ -D __STDC_FORMAT_MACROS \
$(ANTLR_INCLUDES) $(TEST_CPPFLAGS)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(TEST_CXXFLAGS)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
projects / cvc5.git / commitdiff