summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.cpp4
-rw-r--r--src/prop/cnf_stream.cpp60
-rw-r--r--src/prop/prop_engine.cpp34
3 files changed, 86 insertions, 12 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 78c4f9186..cd61b257f 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -116,7 +116,7 @@ Node Node::xorExpr(const Node& right) const {
return NodeManager::currentNM()->mkNode(XOR, *this, right);
}
-void indent(ostream & o, int indent){
+static void indent(ostream & o, int indent){
for(int i=0; i < indent; i++)
o << ' ';
}
@@ -130,8 +130,10 @@ void Node::printAst(ostream & o, int ind) const{
}else if(getNumChildren() >= 1){
for(Node::iterator child = begin(); child != end(); ++child){
+ o << endl;
(*child).printAst(o, ind+1);
}
+ o << endl;
indent(o, ind);
}
o << ')';
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 17ae60313..e758301d4 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -18,6 +18,7 @@
#include "prop/prop_engine.h"
#include "expr/node.h"
#include "util/Assert.h"
+#include "util/output.h"
#include <queue>
@@ -27,6 +28,8 @@ using namespace std;
namespace CVC4 {
namespace prop {
+bool atomic(const Node & n);
+
CnfStream::CnfStream(PropEngine *pe) :
d_propEngine(pe) {
}
@@ -35,7 +38,25 @@ TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
CnfStream(pe) {
}
+static void printLit(ostream & out, Lit l) {
+ const char * s = (sign(l))?"~":" ";
+ out << s << var(l);
+
+}
+
+static void printClause(ostream & out, vec<Lit> & c) {
+ out << "clause :";
+ for(int i=0;i<c.size();i++){
+ out << " ";
+ printLit(out, c[i]) ;
+ }
+ out << ";" << endl;
+}
+
void CnfStream::insertClauseIntoStream(vec<Lit> & c) {
+ Debug("cnf") << "Inserting into stream ";
+ printClause(Debug("cnf"),c);
+
d_propEngine->assertClause(c);
}
@@ -64,15 +85,22 @@ bool CnfStream::isCached(const Node & n) const {
}
Lit CnfStream::lookupInCache(const Node & n) const {
- Assert(isCached(n));
+ Assert(isCached(n),
+ "Node is not in cnf translation cache");
return d_translationCache.find(n)->second;
}
void CnfStream::flushCache() {
+ Debug("cnf") << "flushing the translation cache" << endl;
d_translationCache.clear();
}
void CnfStream::registerMapping(const Node & node, Lit lit, bool atom) {
+
+ Debug("cnf") << "Mapping Node "<< node << " to ";
+ printLit(Debug("cnf"),lit);
+ Debug("cnf") << endl;
+
//Prop engine does not need to know this mapping
d_translationCache.insert(make_pair(node, lit));
if(atom)
@@ -96,6 +124,10 @@ Lit CnfStream::aquireAndRegister(const Node & node, bool atom) {
/***********************************************/
Lit TseitinCnfStream::handleAtom(const Node & n) {
+ Assert(atomic(n), "handleAtom(n) expects n to be an atom");
+
+ Debug("cnf") << "handling atom" << endl;
+
Lit l = aquireAndRegister(n, true);
switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
case TRUE:
@@ -131,7 +163,8 @@ Lit TseitinCnfStream::handleXor(const Node & n) {
*/
void TseitinCnfStream::mapRecTransformOverChildren(const Node& n,
vec<Lit> & target) {
- Assert(target.size() == n.getNumChildren());
+ Assert(target.size() == n.getNumChildren(),
+ "Size of the children must be the same the constructed clause");
int i = 0;
Node::iterator subExprIter = n.begin();
@@ -162,14 +195,15 @@ Lit TseitinCnfStream::handleOr(const Node& n) {
* : (e | ~a1) & (e |~a2) & (e & ~a3) & ...
*/
- vec<Lit> c;
- c.push(~e);
+ vec<Lit> c(1 + lits.size());
+
for(int index = 0; index < lits.size(); ++index) {
Lit a = lits[index];
- c.push(a);
+ c[index] = a;
insertClauseIntoStream(e, ~a);
}
+ c[lits.size()] = ~e;
insertClauseIntoStream(c);
return e;
@@ -226,13 +260,14 @@ Lit TseitinCnfStream::handleAnd(const Node& n) {
* : e | ~a1 | ~a2 | ~a3 | ...
*/
- vec<Lit> c;
- c.push(e);
+ vec<Lit> c(lits.size()+1);
for(int index = 0; index < lits.size(); ++index) {
Lit a = lits[index];
- c.push(~a);
+ c[index] = (~a);
insertClauseIntoStream(~e, a);
}
+ c[lits.size()] = e;
+
insertClauseIntoStream(c);
return e;
@@ -274,9 +309,11 @@ Lit TseitinCnfStream::handleNot(const Node & n) {
Node m = n[0];
Lit equivM = recTransform(m);
- registerMapping(n, ~equivM, false);
+ Lit equivN = ~equivM;
+
+ registerMapping(n, equivN, false);
- return equivM;
+ return equivN;
}
//FIXME: This function is a major hack! Should be changed ASAP
@@ -325,6 +362,7 @@ bool atomic(const Node & n) {
case XOR:
case ITE:
case IFF:
+ case IMPLIES:
case OR:
case AND:
return false;
@@ -353,6 +391,8 @@ Lit TseitinCnfStream::recTransform(const Node & n) {
return handleIte(n);
case IFF:
return handleIff(n);
+ case IMPLIES:
+ return handleImplies(n);
case OR:
return handleOr(n);
case AND:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3455b845e..8485a6e32 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -70,6 +70,11 @@ Lit PropEngine::requestFreshLit(){
}
void PropEngine::assertFormula(const Node& node) {
+
+ Debug("prop") << "Asserting ";
+ node.printAst(Debug("prop"));
+ Debug("prop") << endl;
+
d_cnfStream->convertAndAssert(node);
d_assertionList.push_back(node);
}
@@ -87,6 +92,12 @@ void PropEngine::restart(){
}
}
+static void printLit(ostream & out, Lit l) {
+ const char * s = (sign(l))?"~":" ";
+ out << s << var(l);
+
+}
+
Result PropEngine::solve() {
if(d_restartMayBeNeeded)
restart();
@@ -98,7 +109,28 @@ Result PropEngine::solve() {
d_restartMayBeNeeded = true;
}
- Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+ Message() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+
+ if(result){
+ for(map<Node,Lit>::iterator atomIter = d_atom2lit.begin();
+ atomIter != d_atom2lit.end();
+ ++atomIter){
+ Node n = (*atomIter).first;
+ Lit l = (*atomIter).second;
+
+ lbool lb = d_sat->modelValue(l);
+
+ Notice() << n << "->" << lb.toInt() << endl;
+ }
+ }else{
+ // unsat case
+ Notice() << "Conflict {";
+ for(int i=0; i< d_sat->conflict.size(); i++){
+ Notice() << endl << " ";
+ printLit(Notice(), d_sat->conflict[i]);
+ }
+ Notice() << endl << "}" << endl;
+ }
return Result(result ? Result::SAT : Result::UNSAT);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback