Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Bugfix

  • Loading branch information...
commit ded3c5821cb2d21d7c579a6dbff7aef39fc53afe 1 parent d2fe0f1
@mwolf76 authored
View
12 src/enc/enc_mgr.cc
@@ -28,6 +28,8 @@
#include <enc.hh>
#include <enc_mgr.hh>
+// #define DEBUG_ENC
+
// static initialization
EncodingMgr_ptr EncodingMgr::f_instance = NULL;
@@ -47,23 +49,33 @@ IEncoding_ptr EncodingMgr::make_encoding(Type_ptr tp)
f_cudd.AutodynDisable();
if (NULL != (btype = dynamic_cast<BooleanType_ptr>(tp))) {
+ #ifdef DEBUG_ENC
DEBUG << "Encoding " << btype << endl;
+ #endif
res = new BooleanEncoding();
}
else if (NULL != (sa_type = dynamic_cast<SignedAlgebraicType_ptr>(tp))) {
+ #ifdef DEBUG_ENC
DEBUG << "Encoding " << sa_type << endl;
+ #endif
res = new AlgebraicEncoding(sa_type->width(), 0, true, sa_type->dds());
}
else if (NULL != (ua_type = dynamic_cast<UnsignedAlgebraicType_ptr>(tp))) {
+ #ifdef DEBUG_ENC
DEBUG << "Encoding " << ua_type << endl;
+ #endif
res = new AlgebraicEncoding(ua_type->width(), 0, false, ua_type->dds());
}
else if (NULL != (etype = dynamic_cast<EnumType_ptr>(tp))) {
+ #ifdef DEBUG_ENC
DEBUG << "Encoding " << etype << endl;
+ #endif
res = new EnumEncoding(etype->literals());
}
else if (NULL != (vtype = dynamic_cast<ArrayType_ptr>(tp))) {
+ #ifdef DEBUG_ENC
DEBUG << "Encoding " << vtype << endl;
+ #endif
Encodings encs;
assert( 0 == ( vtype->width() % vtype->of()->width()));
View
13 src/model/compiler/internals.cc
@@ -626,7 +626,6 @@ void Compiler::finalize_and_chains()
ACMap::iterator eye = f_chains.find(alpha);
assert( f_chains.end() != eye);
-
DDVector& Y ((*eye).second);
for (DDVector::iterator j = Y.begin(); Y.end() != j; ++ j) {
// a -> Y, that is: (!a v Y1) ^ (!a v Y2) ^ (!a v Y3) ^ ...
@@ -634,10 +633,16 @@ void Compiler::finalize_and_chains()
}
// !a -> !Y, that is: (a v !Y1 v !Y2 v !Y3 v ....)
- ADD tmp (alpha);
+ ADD bigOr = f_enc.zero();
for (DDVector::iterator j = Y.begin(); Y.end() != j; ++ j) {
- tmp = tmp.Or((*j).Cmpl());
+ BooleanEncoding_ptr be
+ = make_chain_encoding();
+
+ ADD av = be -> bits() [0];
+ bigOr = bigOr.Or( av);
+
+ PUSH_ADD( av.Cmpl(). Or( (*j). Cmpl()). Or( alpha));
}
- PUSH_ADD (tmp);
+ PUSH_ADD(bigOr);
}
}
View
2  src/sat/cnf_singlecut.cc
@@ -28,7 +28,7 @@
#include <dd_walker.hh>
-#define DEBUG_CNF
+// #define DEBUG_CNF
namespace Minisat {
/* internal, used only for CNF-ization */
Please sign in to comment.
Something went wrong with that request. Please try again.