summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-02-06 20:54:41 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-02-06 20:54:41 -0800
commit542f84d2fb059a0779ee1878ee3c1cc2fdbad2df (patch)
tree41f3c34302e9c021d61d156ce69ba7163d02a14f
parent6ae1f35fae4eb7a8d569f88fe143faad8239c26c (diff)
downloadabc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.tar.gz
abc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.tar.bz2
abc-542f84d2fb059a0779ee1878ee3c1cc2fdbad2df.zip
Small changes to compile satoko on Windows.
-rw-r--r--abclib.dsp84
-rw-r--r--src/sat/satoko/act_clause.h4
-rw-r--r--src/sat/satoko/cnf_reader.c2
-rw-r--r--src/sat/satoko/solver.c2
4 files changed, 88 insertions, 4 deletions
diff --git a/abclib.dsp b/abclib.dsp
index d6b76966..12636df5 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1994,6 +1994,90 @@ SOURCE=.\src\sat\xsat\xsatUtils.h
SOURCE=.\src\sat\xsat\xsatWatchList.h
# End Source File
# End Group
+# Begin Group "satoko"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\act_clause.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\act_var.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\b_queue.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\cdb.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\clause.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\cnf_reader.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\heap.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\mem.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\misc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\satoko.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\solver.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\solver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\solver_api.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\sort.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\types.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\vec\vec_char.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\vec\vec_dble.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\vec\vec_int.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\utils\vec\vec_uint.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\satoko\watch_list.h
+# End Source File
+# End Group
# End Group
# Begin Group "opt"
diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h
index 5a2fda2b..2e80a1e6 100644
--- a/src/sat/satoko/act_clause.h
+++ b/src/sat/satoko/act_clause.h
@@ -26,9 +26,9 @@ static inline void clause_act_rescale(solver_t *s)
vec_uint_foreach(s->learnts, cref, i) {
clause = clause_read(s, cref);
- clause->data[clause->size].act *= 1e-20;
+ clause->data[clause->size].act *= (float)1e-20;
}
- s->clause_act_inc *= 1e-20;
+ s->clause_act_inc *= (float)1e-20;
}
/** Increment the activity value of one clause ('clause')
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index 5e4b92f9..9fbbda65 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -97,7 +97,7 @@ static void read_clause(char **token, vec_uint_t *lits)
break;
sign = (var > 0);
var = abs(var) - 1;
- vec_uint_push_back(lits, var2lit((unsigned) var, !sign));
+ vec_uint_push_back(lits, var2lit((unsigned) var, (char)!sign));
}
}
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 8c06bbe8..a4114e54 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -330,7 +330,7 @@ static inline int solver_rst(solver_t *s)
static inline int solver_block_rst(solver_t *s)
{
- return s->stats.n_conflicts > s->opts.fst_block_rst &&
+ return s->stats.n_conflicts > (int)s->opts.fst_block_rst &&
b_queue_is_valid(s->bq_lbd) &&
((long)vec_uint_size(s->trail) > (s->opts.b_rst * (long)b_queue_avg(s->bq_trail)));
}