From 7730b9562b11d13236ce566f15ede0cb3416fe21 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 13 May 2010 05:30:20 +0000 Subject: [PATCH] Minor refactorings and corrections to comments --- src/expr/node_manager.h | 12 ++++-------- src/prop/cnf_stream.cpp | 26 +++++++++++++------------- src/prop/cnf_stream.h | 26 ++++++++++++++------------ 3 files changed, 31 insertions(+), 33 deletions(-) diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 53abdb703..fcfca5296 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -707,14 +707,10 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) { // assume it's atomic if its kind can be atomic, check children // to see if that is actually true bool atomic = kind::kindCanBeAtomic(nv->getKind()); - if(atomic) { - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - if(!(atomic = isAtomic(*i))) { - break; - } - } + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + atomic && i != nv->nv_end(); + ++i) { + atomic = isAtomic(*i); } setAttribute(nv, AtomicAttr(), atomic); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 611689c2b..25134b413 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -271,7 +271,7 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { SatLiteral TseitinCnfStream::handleNot(TNode notNode) { Assert(!isCached(notNode), "Atom already mapped!"); Assert(notNode.getKind() == NOT, "Expecting a NOT expression!"); - Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!"); + Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!"); SatLiteral notLit = ~toCNF(notNode[0]); @@ -341,29 +341,29 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) { void TseitinCnfStream::convertAndAssert(TNode node) { Debug("cnf") << "convertAndAssert(" << node << ")" << endl; - // If the node is a conjuntion, we handle each conjunct separatelu if(node.getKind() == AND) { - TNode::const_iterator conjunct = node.begin(); - TNode::const_iterator node_end = node.end(); - while(conjunct != node_end) { + // If the node is a conjunction, we handle each conjunct separately + for( TNode::const_iterator conjunct = node.begin(), + node_end = node.end(); + conjunct != node_end; + ++conjunct ) { convertAndAssert(*conjunct); - ++ conjunct; } - return; - } - // If the node is a disjunction, we construct a clause and assert it - if(node.getKind() == OR) { + } else if(node.getKind() == OR) { + // If the node is a disjunction, we construct a clause and assert it int nChildren = node.getNumChildren(); SatClause clause(nChildren); TNode::const_iterator disjunct = node.begin(); for(int i = 0; i < nChildren; ++ disjunct, ++ i) { + Assert( disjunct != node.end() ); clause[i] = toCNF(*disjunct); } + Assert( disjunct == node.end() ); assertClause(clause); - return; + } else { + // Otherwise, we just convert using the definitional transformation + assertClause(toCNF(node)); } - // Otherwise, we just convert using the definitional transformation - assertClause(toCNF(node)); } }/* CVC4::prop namespace */ diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 66cdaa730..9a63c26f9 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -11,12 +11,12 @@ ** information. ** ** This class takes a sequence of formulas. - ** It outputs a stream of clauses that is propositional - ** equisatisfiable with the conjunction of the formulas. + ** It outputs a stream of clauses that is propositionally + ** equi-satisfiable with the conjunction of the formulas. ** This stream is maintained in an online fashion. ** ** Unlike other parts of the system it is aware of the PropEngine's - ** internals such as the representation and translation of + ** internals such as the representation and translation of [??? -Chris] **/ #include "cvc4_private.h" @@ -35,7 +35,7 @@ namespace prop { class PropEngine; /** - * Comments for the behavior of the whole class... + * Comments for the behavior of the whole class... [??? -Chris] * @author Tim King */ class CnfStream { @@ -45,7 +45,7 @@ private: /** The SAT solver we will be using */ SatSolver *d_satSolver; - /** Cache of what literal have been registered to a node. */ + /** Cache of what literals have been registered to a node. */ typedef __gnu_cxx::hash_map TranslationCache; TranslationCache d_translationCache; @@ -139,15 +139,17 @@ public: virtual void convertAndAssert(TNode node) = 0; /** - * Returns a node the is represented by a give SatLiteral literal. + * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver * @return the actual node */ Node getNode(const SatLiteral& literal); /** - * Returns the literal the represents the given node in the SAT CNF - * representation. + * Returns the literal that represents the given node in the SAT CNF + * representation. [Presumably there are some constraints on the kind + * of node? E.g., it needs to be a boolean? -Chris] + * */ SatLiteral getLiteral(TNode node); @@ -156,12 +158,12 @@ public: /** * TseitinCnfStream is based on the following recursive algorithm * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf - * The general gist of the algorithm is to introduce a new literal that - * will be equivalent to each subexpression in the constructed equisatisfiable - * formula then substitute the new literal for the formula, and to do this + * The general idea is to introduce a new literal that + * will be equivalent to each subexpression in the constructed equi-satisfiable + * formula, then substitute the new literal for the formula, and so on, * recursively. * - * This implementation does this in a single recursive pass. + * This implementation does this in a single recursive pass. [??? -Chris] */ class TseitinCnfStream : public CnfStream { -- 2.30.2