Permalink
Browse files

Bugfix. Added alternative implementation for !=, additional debug out…

…put for cnf
  • Loading branch information...
1 parent 76c16ae commit d2fe0f16ed87ff9c2ba1770007894d4fee218c59 @mwolf76 committed Dec 31, 2013
@@ -760,6 +760,7 @@ extern DdNode * Cudd_addBWXor (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addBWXnor (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addNotEquals (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addLT (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addLEQ (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
@@ -898,6 +898,38 @@ Cudd_addEquals(
} /* end of Cudd_addEquals */
+/**Function********************************************************************
+
+ Synopsis [Inequality of two ADDs.]
+
+ Description [Equality of two ADDs. Returns NULL if not a terminal
+ case; f != g otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addNotEquals(
+ DdManager * dd,
+ DdNode ** f,
+ DdNode ** g)
+{
+ DdNode *F, *G;
+
+ F = *f; G = *g;
+ if (cuddIsConstant(F) && cuddIsConstant(G)) {
+ if (cuddV(F) != cuddV(G)) {
+ return DD_ONE(dd);
+ } else {
+ return DD_ZERO(dd);
+ }
+ }
+ return(NULL);
+
+} /* end of Cudd_addLT */
+
/**Function********************************************************************
Synopsis [Integer LT (<).]
@@ -2626,6 +2626,17 @@ ADD::Equals(
} // ADD::Equals
+ADD
+ADD::NotEquals(
+ const ADD& g) const
+{
+ DdManager *mgr = checkSameManager(g);
+ DdNode *result = Cudd_addApply(mgr, Cudd_addNotEquals, node, g.node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::Equals
+
ADD
ADD::LT(
const ADD& g) const
@@ -406,6 +406,7 @@ public:
ADD Xnor(const ADD& g) const;
ADD BWXnor(const ADD& g) const;
ADD Equals(const ADD& g) const;
+ ADD NotEquals(const ADD& g) const;
ADD LT(const ADD& g) const;
ADD LEQ(const ADD& g) const;
ADD Log() const;
@@ -622,6 +622,23 @@ void Compiler::algebraic_equals(const Expr_ptr expr)
void Compiler::algebraic_not_equals(const Expr_ptr expr)
{
+#if 1
+ /* new implementation, does not perform rewriting on Equals */
+ assert( is_binary_algebraic(expr) );
+ unsigned width = algebrize_binary_relational();
+
+ POP_ALGEBRAIC(rhs, width);
+ POP_ALGEBRAIC(lhs, width);
+
+ ADD tmp = f_enc.zero();
+ for (unsigned i = 0; i < width; ++ i) {
+ unsigned ndx = width - 1 -i;
+ tmp = tmp.Or( lhs[ndx].NotEquals(rhs[ndx]));
+ }
+
+ PUSH_ADD( tmp);
+#else
+ /* old implementation, performs rewriting on Equals */
ExprMgr& em = f_owner.em();
assert( is_binary_algebraic(expr) );
@@ -631,6 +648,7 @@ void Compiler::algebraic_not_equals(const Expr_ptr expr)
(*this)(em.make_not(em.make_eq(expr->lhs(),
expr->rhs())));
+#endif
}
void Compiler::algebraic_gt(const Expr_ptr expr)
@@ -621,15 +621,23 @@ void Compiler::finalize_and_chains()
{
// Conjunct booked AND chains into result stack
for (DDVector::iterator i = f_roots.begin(); f_roots.end() != i; ++ i) {
- ADD a (*i);
+ ADD alpha (*i); ADD not_alpha = alpha.Cmpl();
- ACMap::iterator eye = f_chains.find(a);
+ ACMap::iterator eye = f_chains.find(alpha);
assert( f_chains.end() != eye);
- // a -> Y, that is: (!a v Y1) ^ (!a v Y2) ^ (!a v Y3) ^ ...
+
DDVector& Y ((*eye).second);
for (DDVector::iterator j = Y.begin(); Y.end() != j; ++ j) {
- PUSH_ADD( a.Cmpl().Or( *j));
+ // a -> Y, that is: (!a v Y1) ^ (!a v Y2) ^ (!a v Y3) ^ ...
+ PUSH_ADD (not_alpha.Or(*j));
+ }
+
+ // !a -> !Y, that is: (a v !Y1 v !Y2 v !Y3 v ....)
+ ADD tmp (alpha);
+ for (DDVector::iterator j = Y.begin(); Y.end() != j; ++ j) {
+ tmp = tmp.Or((*j).Cmpl());
}
+ PUSH_ADD (tmp);
}
}
View
@@ -28,6 +28,7 @@
#include <dd_walker.hh>
+#define DEBUG_CNF
namespace Minisat {
/* internal, used only for CNF-ization */
@@ -113,7 +114,9 @@ namespace Minisat {
ps.push( mkLit( x, px ));
- //DRIVEL << ps << endl;
+ #ifdef DEBUG_CNF
+ DRIVEL << ps << endl;
+ #endif
f_sat.f_solver.addClause_(ps, f_color);
}
@@ -126,7 +129,9 @@ namespace Minisat {
ps.push( mkLit( x, px ));
ps.push( mkLit( y, py ));
- //DRIVEL << ps << endl;
+ #ifdef DEBUG_CNF
+ DRIVEL << ps << endl;
+ #endif
f_sat.f_solver.addClause_(ps, f_color);
}
@@ -140,7 +145,9 @@ namespace Minisat {
ps.push( mkLit( y, py ));
ps.push( mkLit( w, pw ));
- //DRIVEL << ps << endl;
+ #ifdef DEBUG_CNF
+ DRIVEL << ps << endl;
+ #endif
f_sat.f_solver.addClause_(ps, f_color);
}
View
@@ -107,7 +107,7 @@ Witness::Witness(string name, step_t j)
DEBUG
<< "Created new witness: "
<< f_id
- << ", starting at time"
+ << ", starting at time "
<< f_j
<< endl;
}

0 comments on commit d2fe0f1

Please sign in to comment.