Index: configure.in =================================================================== --- configure.in (revision 27811) +++ configure.in (working copy) @@ -830,7 +830,6 @@ fi AC_SUBST(dftest_bin) - # Enable/disable randpkt AC_ARG_ENABLE(randpkt, Index: Makefile.common =================================================================== --- Makefile.common (revision 27811) +++ Makefile.common (working copy) @@ -221,7 +221,7 @@ dftest_SOURCES = \ dftest.c \ util.c - + # randpkt specifics randpkt_SOURCES = \ randpkt.c Index: epan/libwireshark.def =================================================================== --- epan/libwireshark.def (revision 27811) +++ epan/libwireshark.def (working copy) @@ -162,6 +162,12 @@ dfilter_macro_build_ftv_cache dfilter_macro_foreach dfilter_macro_get_uat +dcache_init +dcache_cleanup +dcache_start_satisfy_save +dcache_stop_satisfy_save +dcache_satisfy +dcache_save DisengageReason_vals DATA DisengageRejectReason_vals DATA display_epoch_time Index: epan/dfilter/drange.c =================================================================== --- epan/dfilter/drange.c (revision 27811) +++ epan/dfilter/drange.c (working copy) @@ -75,6 +75,16 @@ return drnode->ending; } +static gboolean +drange_node_equal(drange_node* drnode1, drange_node* drnode2) +{ + return + (drnode1->start_offset == drnode2->start_offset) && + (drnode1->length == drnode2->length) && + (drnode1->end_offset == drnode2->end_offset) && + (drnode1->ending == drnode2->ending); +} + /* drange_node mutators */ void drange_node_set_start_offset(drange_node* drnode, gint offset) @@ -205,3 +215,39 @@ { g_slist_foreach(dr->range_list,func,funcdata); } + + +gboolean +drange_equal(drange* dr1, drange* dr2) +{ + GSList *iter1; + GSList *iter2; + + if (drange_has_total_length(dr1) != drange_has_total_length(dr2)) + return FALSE; + + if (drange_get_total_length(dr1) != drange_get_total_length(dr2)) + return FALSE; + + if (drange_get_min_start_offset(dr1) != drange_get_min_start_offset(dr2)) + return FALSE; + + if (drange_get_max_start_offset(dr1) != drange_get_max_start_offset(dr2)) + return FALSE; + + if (g_slist_length(dr1->range_list) != g_slist_length(dr2->range_list)) + return FALSE; + + + for(iter1=dr1->range_list, iter2=dr2->range_list; + iter1 && iter2; + iter1=g_slist_next(iter1), iter2=g_slist_next(iter2)) { + drange_node *drnode1 = g_slist_nth_data(iter1, 0); + drange_node *drnode2 = g_slist_nth_data(iter2, 0); + + if (!drange_node_equal(drnode1, drnode2)) + return FALSE; + } + + return iter1 == iter2; +} Index: epan/dfilter/sttype-test.c =================================================================== --- epan/dfilter/sttype-test.c (revision 27811) +++ epan/dfilter/sttype-test.c (working copy) @@ -64,6 +64,44 @@ g_free(test); } +static gboolean +test_equal(gpointer n1, gpointer n2) +{ + test_t *t1 = n1; + test_t *t2 = n2; + + assert_magic(t1, TEST_MAGIC); + assert_magic(t2, TEST_MAGIC); + + if (t1->op != t2->op) + return FALSE; + + if (!stnode_equal(t1->val1, t2->val1)) + return FALSE; + + if (!stnode_equal(t1->val2, t2->val2)) + return FALSE; + + return TRUE; +} + +static gpointer +test_any(gpointer testp, STTypeAnyFuncVisitor fn, gpointer fn_arg) +{ + test_t *t = *(test_t **)testp; + gpointer node = NULL; + + assert_magic(t, TEST_MAGIC); + + if ( (node = stnode_any(&t->val1, fn, fn_arg)) != NULL) + return node; + + if ( (node = stnode_any(&t->val2, fn, fn_arg)) != NULL) + return node; + + return node; +} + static int num_operands(test_op_t op) { @@ -154,6 +192,8 @@ "TEST", test_new, test_free, + test_equal, + test_any, }; sttype_register(&test_type); Index: epan/dfilter/drange.h =================================================================== --- epan/dfilter/drange.h (revision 27811) +++ epan/dfilter/drange.h (working copy) @@ -99,4 +99,6 @@ void drange_prepend_drange_node(drange* dr, drange_node* drnode); void drange_foreach_drange_node(drange* dr, GFunc func, gpointer funcdata); +/* drange utilities */ +gboolean drange_equal(drange* dr1, drange* dr2); #endif /* ! __DRANGE_H__ */ Index: epan/dfilter/sttype-sat.c =================================================================== --- epan/dfilter/sttype-sat.c (revision 0) +++ epan/dfilter/sttype-sat.c (revision 0) @@ -0,0 +1,43 @@ +/* + * $Id$ + * + * Wireshark - Network traffic analyzer + * By Gerald Combs + * Copyright 2001 Gerald Combs + * + * + * This program is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif + +#include "ftypes/ftypes.h" +#include "syntax-tree.h" + +void sttype_register_sat(void) +{ + static sttype_t sat_type = { + STTYPE_SAT, + "SAT", + NULL, + NULL, + NULL, + NULL, + }; + + sttype_register(&sat_type); +} Index: epan/dfilter/sttype-integer.c =================================================================== --- epan/dfilter/sttype-integer.c (revision 27811) +++ epan/dfilter/sttype-integer.c (working copy) @@ -36,6 +36,8 @@ "INTEGER", NULL, NULL, + NULL, + NULL, }; sttype_register(&integer_type); Index: epan/dfilter/syntax-tree.c =================================================================== --- epan/dfilter/syntax-tree.c (revision 27811) +++ epan/dfilter/syntax-tree.c (working copy) @@ -42,6 +42,7 @@ sttype_register_range(); sttype_register_string(); sttype_register_test(); + sttype_register_sat(); } void @@ -93,7 +94,8 @@ node = g_new(stnode_t, 1); node->magic = STNODE_MAGIC; node->deprecated_token = NULL; - + node->value = 0; + if (type_id == STTYPE_UNINITIALIZED) { node->type = NULL; node->data = NULL; @@ -156,6 +158,52 @@ g_free(node); } +gboolean +stnode_equal(stnode_t *n1, stnode_t *n2) +{ + if (n1 == NULL && n2 == NULL) + return TRUE; + + if ( (n1 == NULL && n2 != NULL) || + (n1 != NULL && n2 == NULL) ) + return FALSE; + + if (n1->type != n2->type) + return FALSE; + + if (n1->value != n2->value) + return FALSE; + + if (n1->data == NULL && n2->data == NULL) + return TRUE; + + if ( (n1->data == NULL && n2->data != NULL) || + (n1->data != NULL && n2->data == NULL) ) + return FALSE; + + if (n1->type->func_equal == NULL) + return n1->data == n2->data; + + return n1->type->func_equal(n1->data, n2->data); +} + +gpointer +stnode_any(gpointer nodep, STTypeAnyFuncVisitor fn, gpointer fn_arg) +{ + stnode_t *node = *(stnode_t **)nodep; + + if (!node) + return NULL; + + if (fn(node, fn_arg)) + return nodep; + + if (node->type->func_any) + return node->type->func_any(&node->data, fn, fn_arg); + + return NULL; +} + const char* stnode_type_name(stnode_t *node) { Index: epan/dfilter/Makefile.nmake =================================================================== --- epan/dfilter/Makefile.nmake (revision 27811) +++ epan/dfilter/Makefile.nmake (working copy) @@ -64,6 +64,9 @@ $(MAKE) /$(MAKEFLAGS) -f makefile.nmake lemon cd ../epan/dfilter +wslimmat.obj : wslimmat.h wslimmat.c + $(CC) $(CVARSDLL) -DHAVE_CONFIG_H /I. $(GLIB_CFLAGS) -D_U_="" $(LOCAL_CFLAGS) -Fd.\ -c wslimmat.c + checkapi: $(PERL) ../../tools/checkAPIs.pl -g termoutput \ $(GENERATOR_FILES) \ Index: epan/dfilter/syntax-tree.h =================================================================== --- epan/dfilter/syntax-tree.h (revision 27811) +++ epan/dfilter/syntax-tree.h (working copy) @@ -36,19 +36,24 @@ STTYPE_INTEGER, STTYPE_RANGE, STTYPE_FUNCTION, + STTYPE_SAT, STTYPE_NUM_TYPES } sttype_id_t; typedef gpointer (*STTypeNewFunc)(gpointer); typedef void (*STTypeFreeFunc)(gpointer); +typedef gboolean (*STTypeEqualFunc)(gpointer, gpointer); - +typedef gboolean (*STTypeAnyFuncVisitor) (gpointer, gpointer); +typedef gpointer (*STTypeAnyFunc) (gpointer, STTypeAnyFuncVisitor, gpointer); /* Type information */ typedef struct { sttype_id_t id; const char *name; STTypeNewFunc func_new; STTypeFreeFunc func_free; + STTypeEqualFunc func_equal; + STTypeAnyFunc func_any; } sttype_t; /* Node (type instance) information */ @@ -70,6 +75,7 @@ void sttype_register_range(void); void sttype_register_string(void); void sttype_register_test(void); +void sttype_register_sat(void); void sttype_init(void); @@ -92,6 +98,9 @@ void stnode_free(stnode_t *node); +gboolean +stnode_equal(stnode_t *n1, stnode_t *n2); + const char* stnode_type_name(stnode_t *node); @@ -104,6 +113,9 @@ gint32 stnode_value(stnode_t *node); +gpointer +stnode_any(gpointer node, STTypeAnyFuncVisitor fn, gpointer fn_arg); + const char * stnode_deprecated(stnode_t *node); Index: epan/dfilter/dfilter.c =================================================================== --- epan/dfilter/dfilter.c (revision 27811) +++ epan/dfilter/dfilter.c (working copy) @@ -17,8 +17,7 @@ * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - */ + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ #ifdef HAVE_CONFIG_H #include "config.h" @@ -29,6 +28,7 @@ #include "dfilter-int.h" #include "syntax-tree.h" +#include "sttype-test.h" #include "gencode.h" #include "semcheck.h" #include "dfvm.h" @@ -37,6 +37,7 @@ #include "dfilter-macro.h" #include + #define DFILTER_TOKEN_ID_OFFSET 1 /* Global error message space for dfilter_compile errors */ @@ -51,6 +52,83 @@ /* Holds the singular instance of our Lemon parser object */ static void* ParserObj = NULL; +/* maximum number of cached syntax trees. It should be same number of + * bits as frame_data.dhistory. + */ +#define DCACHE_MAX_CACHE 64 + +/* maximum number of SAT variables. In other words, we will only match + * maximumly DCACHE_MAX_SATVAR syntax trees. */ +#define DCACHE_MAX_SATVAR 8 + +/* maximum number of SAT results. */ +#define DCACHE_MAX_SATRES (1<st_root = NULL; df->insns = NULL; df->deprecated = NULL; @@ -143,6 +222,10 @@ if (!df) return; + if (df->st_root) { + stnode_free(df->st_root); + } + if (df->insns) { free_insns(df->insns); } @@ -172,7 +255,7 @@ dfw = g_new(dfwork_t, 1); - dfw->st_root = NULL; + dfw->st_root = NULL; dfw->syntax_error = FALSE; dfw->insns = NULL; dfw->consts = NULL; @@ -188,10 +271,10 @@ static void dfwork_free(dfwork_t *dfw) { - if (dfw->st_root) { - stnode_free(dfw->st_root); - } - + if (dfw->st_root) { + stnode_free(dfw->st_root); + } + if (dfw->loaded_fields) { g_hash_table_destroy(dfw->loaded_fields); } @@ -295,7 +378,7 @@ failure = TRUE; /* Reset flex */ - df_scanner_cleanup(); + df_scanner_cleanup(); if (failure) goto FAILURE; @@ -322,8 +405,10 @@ /* Tuck away the bytecode in the dfilter_t */ dfilter = dfilter_new(); + dfilter->st_root = dfw->st_root; dfilter->insns = dfw->insns; dfilter->consts = dfw->consts; + dfw->st_root = NULL; dfw->insns = NULL; dfw->consts = NULL; dfilter->interesting_fields = dfw_interesting_fields(dfw, @@ -412,3 +497,611 @@ printf("\n"); } } + + + + +/* This is used for generating boolean expressions for SAT solver. */ +typedef struct satexp { + char *exp; /* the expression */ + int len; /* current length of exp without terminator */ + int max; /* the size of 'exp' buffer */ +} satexp; + + +/* write a string with format specified in 'format' to satexp 'e'. The + * only accepted SPEC in format is %v. For example, + * sat_print(e, "(%v)", 0); + * will add "(v0)" to e. + * + * Returns -1 if buffer in 'e' is not large enough. Otherwise returns + * number of bytes written to 'e'. + */ +static int +sat_print(satexp *e, char *format, ...) +{ + va_list va; + char *ch = format; + char *exp = e->exp; + char olen = e->len; + + va_start(va, format); + + while (*ch) { + if (e->len >= e->max - 1) + goto fail; + + if (*ch == '%') { + if (ch[1] == 'v') { + int nmax = e->max - e->len; + int nwritten = g_snprintf(&exp[e->len], nmax, "v%d", va_arg(va, int)); + + if (nwritten < 0 || nwritten >= nmax) + goto fail; + + e->len += nwritten; + } else { + goto fail; + } + + ch += 2; + } else { + exp[e->len] = *ch; + e->len += 1; + ch += 1; + } + } + + va_end(va); + + exp[e->len] = '\0'; + return e->len - olen; + +fail: + va_end(va); + + if (e->len >= e->max-1) + e->len = e->max-1; + + exp[e->len] = '\0'; + + return -1; +} + +static int +sat_print0(satexp *e) +{ + return sat_print(e, "(%v & !%v)", 0, 0); +} + +static int +sat_print1(satexp *e) +{ + return sat_print(e, "(%v | !%v)", 0, 0); +} + + +/* generate boolean expression from syntax tree. */ +static int +dcache_genexp_work(stnode_t *root, satexp *e) +{ +#define CHECK(EXP) do { \ + if ((EXP) == -1) \ + return -1; \ + } while (0) + + stnode_t *curr = root; + stnode_t *n1; + stnode_t *n2; + + test_op_t op; + + switch (curr->type->id) { + case STTYPE_TEST: + sttype_test_get(curr, &op, &n1, &n2); + + switch (op) { + case TEST_OP_EXISTS: + CHECK(sat_print(e, "%v", satvar)); + break; + case TEST_OP_NOT: + CHECK(sat_print(e, "(!")); + satvar++; CHECK(dcache_genexp_work(n1, e)); + CHECK(sat_print(e, ")")); + break; + case TEST_OP_AND: + CHECK(sat_print(e, "(")); + satvar++; CHECK(dcache_genexp_work(n1, e)); + CHECK(sat_print(e, "&")); + satvar++; CHECK(dcache_genexp_work(n2, e)); + CHECK(sat_print(e, ")")); + break; + case TEST_OP_OR: + CHECK(sat_print(e, "(")); + satvar++; CHECK(dcache_genexp_work(n1, e)); + CHECK(sat_print(e, "|")); + satvar++; CHECK(dcache_genexp_work(n2, e)); + CHECK(sat_print(e, ")")); + break; + + case TEST_OP_EQ: + case TEST_OP_NE: + case TEST_OP_GT: + case TEST_OP_GE: + case TEST_OP_LT: + case TEST_OP_LE: + case TEST_OP_BITWISE_AND: + case TEST_OP_CONTAINS: + case TEST_OP_MATCHES: + CHECK(sat_print(e, "%v", satvar)); + break; + default: + g_assert(0); + } + + break; + case STTYPE_SAT: + if (curr->value) { + CHECK(sat_print1(e)); + } else { + CHECK(sat_print0(e)); + } + break; + default: + g_assert(0); + } + + return 0; + +#undef CHECK +} + + +/* A simple wrapper for dcache_genexp_work for usability. */ +static int +dcache_genexp(stnode_t *root, char *exp, int size, int *len) +{ + satexp e; + int result; + + e.exp = exp; + e.max = size; + e.len = 0; + + /* satvar must start from 1, because 0 is reserved for generating + * TRUE and FALSE in boolean expressions. */ + satvar = 1; + result = dcache_genexp_work(root, &e); + + *len = e.len; + + return result; +} + +const char* dcache_info_satres_str(dcache_satres_t t) +{ + switch (t) { + case DS_1_UNSAT: + return "DS_1_UNSAT"; + break; + case DS_0_UNSAT: + return "DS_0_UNSAT"; + break; + case DS_UNKNOWN: + return "DS_UNKNOWN"; + break; + } + + return "ERROR"; +} + +/* To compute the SAT results for the boolean expression (EXP) for a + * syntax tree. Returns: + * DS_1_UNSAT if EXP can only be FALSE + * DS_0_UNSAT if !(EXP) can only be FALSE, i.e. EXP can only be TRUE + * DS_UNKNOWN if both EXP and !(EXP) can be TRUE. + */ +static dcache_satres_t +dcache_compute_satres(stnode_t* root) +{ + char exp[MAX_SAT_EXP] = {0}; + int len = 0; + int sat_result; + + if (dcache_genexp(root, &exp[2], MAX_SAT_EXP-3, &len) == -1) + return DS_UNKNOWN; + + sat_result = boolean_satisfy(&exp[2],strlen(&exp[2])); + + if (sat_result == -1) + return DS_UNKNOWN; + else if (sat_result == 0) + return DS_1_UNSAT; + + exp[0] = '!'; + exp[1] = '('; + exp[2+len] = ')'; + exp[2+len+1] = '\0'; + + sat_result = boolean_satisfy(exp,strlen(exp)); + + if (sat_result == -1) + return DS_UNKNOWN; + else if (sat_result == 0) + return DS_0_UNSAT; + + return DS_UNKNOWN; +} + +void +dcache_print() +{ + int icache; + char exp[MAX_SAT_EXP]; + int len; + + printf("\n"); + printf("********* dfilter cache (index %d)***********\n", dcache_current); + + for (icache = 0; icache < DCACHE_MAX_CACHE; icache++) { + if (dcache_cache[icache]) { + len = 0; + syntax_tree_print(dcache_cache[icache], 0); + dcache_genexp(dcache_cache[icache], exp, MAX_SAT_EXP-1, &len); + printf("cache %d: %s\n", icache, exp); + } + } + + printf("\n\n"); +} + +static void +print_indent(int indent) +{ + int i; + for (i = 0; itype->id) { + case STTYPE_TEST: + sttype_test_get(root, &op, &n1, &n2); + switch (op) { + case TEST_OP_EXISTS: + print_indent(indent); printf("- EXIST:%p\n", n1); + break; + case TEST_OP_NOT: + print_indent(indent); printf("- NOT:%p\n", n1); + syntax_tree_print(n1, indent+4); + break; + case TEST_OP_AND: + print_indent(indent); printf("- AND:%p && %p\n", n1, n2); + syntax_tree_print(n1, indent+4); + syntax_tree_print(n2, indent+4); + break; + case TEST_OP_OR: + print_indent(indent); printf("- OR:%p || %p\n", n1, n2); + syntax_tree_print(n1, indent+4); + syntax_tree_print(n2, indent+4); + break; + case TEST_OP_EQ: + print_indent(indent); printf("- EQ:%p == %p\n", n1, n2); + break; + case TEST_OP_NE: + print_indent(indent); printf("- NE:%p != %p\n", n1, n2); + break; + case TEST_OP_GT: + print_indent(indent); printf("- GT:%p > %p\n", n1, n2); + break; + case TEST_OP_GE: + print_indent(indent); printf("- GE:%p >= %p\n", n1, n2); + break; + case TEST_OP_LT: + print_indent(indent); printf("- LT:%p < %p\n", n1, n2); + break; + case TEST_OP_LE: + print_indent(indent); printf("- LE:%p <= %p\n", n1, n2); + break; + case TEST_OP_BITWISE_AND: + print_indent(indent); printf("- BA:%p & %p\n", n1, n2); + break; + case TEST_OP_CONTAINS: + print_indent(indent); printf("- CO:%p ]] %p\n", n1, n2); + break; + + default: + g_assert(0); + } + break; + case STTYPE_SAT: + print_indent(indent); printf("- SAT:%d\n", root->value); + break; + default: + g_assert(0); + } +} + +void +dfilter_tree_print(dfilter_t *df, const char* header) +{ + printf("\n%s\n", header); + syntax_tree_print(df->st_root, 0); +} + + +static gboolean +syntax_tree_equal(gpointer n1, gpointer n2) +{ + return stnode_equal(n1, n2); +} + +static stnode_t** +syntax_tree_match(stnode_t **target, stnode_t *pattern) +{ + return (stnode_t **) stnode_any(target, syntax_tree_equal, pattern); +} + +#define GET_BIT(MASK, POS) ((MASK>>POS) & 1) +#define SET_BIT(VAR, POS) ((VAR)|=(guint64) (1<<(POS))) +#define CLR_BIT(VAR, POS) ((VAR)&=(guint64)~(1<<(POS))) + + +static void +dcache_info_clear() +{ + int icache; + + dcache_info_nmatched = 0; + + for (icache=0; icache < DCACHE_MAX_CACHE; icache++) { + if (dcache_info[icache].varnode) { + stnode_free(dcache_info[icache].varnode); + } + + dcache_info[icache].varnode = NULL; + dcache_info[icache].oldnode = NULL; + dcache_info[icache].nodeptr = NULL; + } +} + +static void +dcache_info_restore() +{ + int icache; + + for (icache=0; icache= DCACHE_MAX_SATVAR) + return FALSE; + + dcache_info_nmatched++; + + dcache_info[icache].nodeptr = match_root; + dcache_info[icache].oldnode = *match_root; + dcache_info[icache].varnode = stnode_new(STTYPE_SAT, NULL); + *match_root = dcache_info[icache].varnode; + + return TRUE; +} + +/* Solve SAT for all possible value combinations of variable nodes. */ +static void +dcache_solve_sat(stnode_t* root) +{ + int icache; + int bit_pattern; + int bit_position; + + char exp[MAX_SAT_EXP]; + int len; + + dcache_genexp(root, exp, MAX_SAT_EXP-1, &len); + printf("dcache_solve_sat: %s\n", exp); + + for (bit_pattern=0; bit_pattern< (1<value = GET_BIT(bit_pattern, bit_position++); + } + } + + dcache_info_satres[bit_pattern] = dcache_compute_satres(root); + + printf("[dcache_solve_sat:%d] bit_pattern %x, dcache_info_satres %s\n", + __LINE__, + bit_pattern, dcache_info_satres_str(dcache_info_satres[bit_pattern])); + } +} + +void +dcache_init() +{ + int icache, isatres; + + dcache_is_saving = FALSE; + dcache_is_satisfying = FALSE; + dcache_current = 0; + + for (icache=0; icache < DCACHE_MAX_CACHE; icache++) { + if (dcache_info[icache].varnode) { + stnode_free(dcache_info[icache].varnode); + dcache_info[icache].varnode = NULL; + } + + if (dcache_cache[icache]) { + stnode_free(dcache_cache[icache]); + dcache_cache[icache] = NULL; + } + } + + for (isatres = 0; isatres < DCACHE_MAX_SATRES; isatres++) { + dcache_info_satres[isatres] = DS_UNKNOWN; + } +} + +void +dcache_cleanup() +{ + dcache_init(); +} + +/* Now we use dcache_start_satisfy_save and dcache_stop_satisfy_save + * to start/stop both 'satisfy'/'save' processes. + * + * So the individule start/stop routines are not public. + */ +static void +dcache_start_satisfy(dfilter_t *df) +{ + /* match_root is the address of the root the subtree matched in + * df->st_root. It might be &df->st_root, hence we MUST use + * df->st_root as the input of syntax_tree_match directly. */ + stnode_t **match_root; + int icache, n; + + dcache_is_satisfying = TRUE; + + g_assert(dcache_current >= 0 && dcache_current < DCACHE_MAX_CACHE); + + dcache_info_clear(); + + printf("------ tree before substitue -----\n"); + syntax_tree_print(df->st_root, 0); + + printf("\n------ cache before substitue -----\n"); + dcache_print(); + + + /* match and substitue the matched subtrees */ + for (icache=dcache_current, n=0; nst_root, dcache_cache[icache]); + + if (match_root) { + if (!dcache_info_save(icache, match_root)) + break; + } + } + + if (--icache < 0) + icache = DCACHE_MAX_CACHE - 1; + } + + printf("\n------ tree after substitue ------\n"); + syntax_tree_print(df->st_root, 0); + + dcache_solve_sat(df->st_root); + dcache_info_restore(); +} + +static void +dcache_stop_satisfy() +{ + dcache_is_satisfying = FALSE; +} + +dcache_satres_t +dcache_satisfy(guint64 dhistory) +{ + int icache; + int bit_pattern = 0; + + if (!dcache_is_satisfying || dcache_info_nmatched == 0) + return DS_UNKNOWN; + + /* least significant bit is at icache==0 */ + for (icache=DCACHE_MAX_CACHE-1; icache>=0; icache--) { + if (dcache_info[icache].varnode) { + bit_pattern <<= 1; + bit_pattern |= GET_BIT(dhistory, icache); + } + } + + return dcache_info_satres[bit_pattern]; +} + +/* Start saving process and save syntax tree in 'df' to dcache. */ +static void +dcache_start_save(dfilter_t *df) +{ + int icache; + stnode_t **match_root; + + dcache_is_saving = FALSE; + + if (!df->st_root) + return; + + /* Don't save syntax tree, if it is same as someone in dcache. */ + for (icache=0; icachest_root, dcache_cache[icache]); + + if (match_root == &df->st_root) + return; + } + } + + dcache_is_saving = TRUE; + + dcache_current++; + + if (dcache_current >= DCACHE_MAX_CACHE) { + dcache_current -= DCACHE_MAX_CACHE; + } + + if (dcache_cache[dcache_current]) { + stnode_free(dcache_cache[dcache_current]); + } + + dcache_cache[dcache_current] = df->st_root; + df->st_root = NULL; +} + +static void +dcache_stop_save() +{ + dcache_is_saving = FALSE; +} + +void +dcache_save(guint64 *dhistory, gboolean passed) +{ + if (!dcache_is_saving) + return; + + if (passed) + SET_BIT(*dhistory, dcache_current); + else + CLR_BIT(*dhistory, dcache_current); +} + +void +dcache_start_satisfy_save(dfilter_t *df) +{ + dcache_start_satisfy(df); + dcache_start_save(df); +} + +void +dcache_stop_satisfy_save() +{ + dcache_stop_satisfy(); + dcache_stop_save(); +} Index: epan/dfilter/sttype-string.c =================================================================== --- epan/dfilter/sttype-string.c (revision 27811) +++ epan/dfilter/sttype-string.c (working copy) @@ -35,6 +35,11 @@ g_free(value); } +static gboolean +string_equal(gpointer n1, gpointer n2) +{ + return g_strcmp0((const char *)n1, (const char *)n2) == 0; +} void sttype_register_string(void) @@ -44,6 +49,8 @@ "STRING", string_new, string_free, + string_equal, + NULL, }; static sttype_t unparsed_type = { @@ -51,6 +58,8 @@ "UNPARSED", string_new, string_free, + string_equal, + NULL, }; sttype_register(&string_type); Index: epan/dfilter/wslimmat.c =================================================================== --- epan/dfilter/wslimmat.c (revision 0) +++ epan/dfilter/wslimmat.c (revision 0) @@ -0,0 +1,7721 @@ +/*------------------------------------------------------------------------*\ +(C)2001-2002, Armin Biere, Computer Systems Institute, ETH Zurich. + +All rights reserved. Redistribution and use in source and binary forms, with +or without modification, are permitted provided that the following +conditions are met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + 3. All advertising materials mentioning features or use of this software + must display the following acknowledgement: + + This product includes software developed by Armin Biere, Computer + Systems Institute, ETH Zurich. + + 4. Neither the name of the University nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF +THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +\*------------------------------------------------------------------------*/ + +#define COPYRIGHT \ +"(C)2001-2002 Armin Biere, Computer Systems Institute, ETH Zurich" + +const char * +copyright_Limmat (void) +{ + return COPYRIGHT; +} + +/*------------------------------------------------------------------------*/ + +const char * +id_Limmat (void) +{ + return "$Id: limmat.c,v 1.98.2.41 2002/11/26 09:32:59 biere Exp $"; +} + +/*------------------------------------------------------------------------*/ + +#include +#include +#include +#include +#include + + +/*------------------------------------------------------------------------*/ + +#include "wslimmat.h" +#define LIMMAT_VERSION "1.3" +/*------------------------------------------------------------------------*/ + +const char * +version_Limmat (void) +{ + return LIMMAT_VERSION; +} + + +/*------------------------------------------------------------------------*/ +/* To add more dynamic checks to the program you should define + * 'CHECK_CONSISTENCY'. This results in a small increase in memory usage + * and a somewhat large time penalty. You may additionally also define + * 'EXPENSIVE_CHECKS' to enable thorough but expensive checks. + * +#define EXPENSIVE_CHECKS +#define CHECK_CONSISTENCY + */ + +/*------------------------------------------------------------------------*/ +/* You should not change anything in this section. + */ +#ifdef EXPENSIVE_CHECKS +#ifndef CHECK_CONSISTENCY +#define CHECK_CONSISTENCY +#endif +#warning "#define EXPENSIVE_CHECKS" +#endif +#ifdef CHECK_CONSISTENCY +#warning "#define CHECK_CONSISTENCY" +#endif +/*------------------------------------------------------------------------*/ +/* For easy debugging you may want to log the actions of the sat solving + * engine. This may produce a lot of output and should only be enabled for + * debugging purposes. + * +#define LOG_ASSIGNMENTS +#define LOG_BACKJUMP +#define LOG_BACKTRACK +#define LOG_CONFLICT +#define LOG_CONNECT +#define LOG_DECISION +#define LOG_LEARNED +#define LOG_PROPS +#define LOG_PUSH +#define LOG_RESCORE +#define LOG_RESTART +#define LOG_UIP +#define LOG_UNIT + */ + +/*------------------------------------------------------------------------*/ +#if defined(LOG_ASSIGNMENTS) || \ + defined(LOG_BACKTRACK) || \ + defined(LOG_CONFLICT) || \ + defined(LOG_DECISION) || \ + defined(LOG_LEARNED) || \ + defined(LOG_RESCORE) || \ + defined(LOG_RESTART) || \ + defined(LOG_UIP) || \ + defined(LOG_UNIT) +#warning "#define LOG_ ..." +#define LOGFILE(l) ((l)->log ? (l)->log : stdout) +#define LOG_SOMETHING +#endif +/*------------------------------------------------------------------------*/ +#if defined(NO_INLINE_KEYWORD) || !defined(NDEBUG) +#define inline +#endif +/*------------------------------------------------------------------------*/ +/* You may want to use different decision strategies. These strategies can + * still be set by environment variables. + */ +#define RESCORE 256 /* number of decisions before rescore */ +#define RESCOREFACTOR ((double)0.5) /* score factor multiplied in rescore */ +#define RESTART 10000 /* number of decisions before restart */ +#define STATISTICS 1 /* enable statistics */ + +/*------------------------------------------------------------------------*/ +/* The following section guarded by '!defined(EXTERNAL_DEFINES)' contains + * all the critical compile time options that control the speed of the + * solver. You may define 'EXTERNAL_DEFINES' by using './configure + * --external-defines', but then you have to compile the library manually + * and specify all these options on the comman line. + */ +#if !defined(EXTERNAL_DEFINES) +/*------------------------------------------------------------------------*/ +/* With a small runtime penalty and an additional restriction on the maximal + * size of a stack, actually the maximal count of elements on the stack, + * defining 'COMPACT_STACK' will use only two words for an inlined stack. + * This may decrease the size of a variable structure considerably. + * + */ +#define COMPACT_STACK + +/*------------------------------------------------------------------------*/ +/* Use the idea of Chaff to save the last search direction for each watched + * literal. + * + */ +#define OPTIMIZE_DIRECTION + +/*------------------------------------------------------------------------*/ +/* Enable early detection of conflict literals in BCP. + * + */ +#define EARLY_CONFLICT_DETECTION + +/*------------------------------------------------------------------------*/ +/* In case an already implied literal is again implied in BCP use the + * shorter clause as reason for the implication. + * + */ +#define SHORTEN_REASONS + +/*------------------------------------------------------------------------*/ +/* The Limmat data structure allows a constant lookup of the other watched + * literal in the clause. This may reduce the overall number of visits to + * literals, since the other watched literal is often assigned to 1 already. + * + */ +#define LOOK_AT_OTHER_WATCHED_LITERAL + +/*------------------------------------------------------------------------*/ +#else /* EXTERNAL DEFINES */ +#if !defined(RESCORE) || !defined(RESTART) || !defined(STATISTICS) +#error "EXTERNAL_DEFINES requires to define RESCORE, RESTART, STATISTICS" +#endif +#endif +/*------------------------------------------------------------------------*/ + +#define VARIABLE_ALIGNMENT sizeof(void*) +#define ALL_BUT_SIGN_BITS 0 +#define SIGN_BIT 1 + +typedef struct Clause *Occurence; + +/*------------------------------------------------------------------------*/ +/* Truth constants: By flipping their sign bit with 'not' they can be + * converted to each other respectively. + */ +#define FALSE ((Variable*)0) +#define TRUE ((Variable*)SIGN_BIT) + +/*------------------------------------------------------------------------*/ +/* We use the lowest bit of (Variable*) and (Clause*) pointers for negation + * and storing the link position respectively. This bit stuffing technique + * saves a lot of space but may be slower. To manipulate the lowest bit of + * pointers we have to cast a pointer to a machine word of the same size, + * since we need to cast it back again without loosing information. + * + * On most machines 'unsigned long' has the same number of bytes as pointer. + * This is checked in test case 'align0'. + */ +#define PTR_SIZED_WORD unsigned long + +/*------------------------------------------------------------------------*/ +/* Maximal size of a parse error string. + */ +#define ERROR_SIZE 200 + +/*------------------------------------------------------------------------*/ +/* Memory management related constants for checking consistency. + */ +#ifdef CHECK_CONSISTENCY +#define DATA_OFFSET (((char*) &(((Bucket*)0)->aligned_data)) - (char*)0) +#endif + +/*------------------------------------------------------------------------*/ + +typedef struct Arena Arena; +typedef struct Assignment Assignment; +typedef struct Clause Clause; +typedef struct Counter Counter; +typedef struct Frame Frame; +typedef struct Parser Parser; +typedef struct Stack Stack; +typedef struct Statistics Statistics; +typedef struct Variable Variable; + +/*------------------------------------------------------------------------*/ +#ifdef CHECK_CONSISTENCY +/*------------------------------------------------------------------------*/ + +typedef struct Bucket Bucket; + +/*------------------------------------------------------------------------*/ +/* A Bucket is a basic allocation unit. It is only used in consistency + * checking mode to save the allocation size together with allocated memory, + * in order to check that the size given as parameter to 'delete' actually + * is the same as the size given as parameter to 'new' or 'resize'. Note + * that aligning the data to 'double' may actually result on additional word + * being inserted by the compiler after the 'size' field. This may increase + * the actual memory used by two words per allocation, e.g. 64 bytes on a 32 + * bit machine with 8 byte aligned 'double' fields. If 'CHECK_CONSISTENCY' + * is disabled no additional memory is required. + */ +struct Bucket +{ + size_t size; + + union + { + double as_double; + void *as_pointer; + int as_number; + } + aligned_data; +}; + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* A generic stack implementation. The data elements to be pushed on the + * stack are generic 'void *' pointers. Stacks are resized automatically, + * but their size will never shrink during pop operations. Since the stack + * is implemented as contiguos area we provide a way to treat the stack + * contents as an array of pointers. + */ +struct Stack +{ +#ifdef COMPACT_STACK +#define LOG_LOG_MAX_STACK_SIZE 5 +#define LOG_MAX_STACK_COUNT (sizeof(unsigned) * 8 - LOG_LOG_MAX_STACK_SIZE) +#define LOG_MAX_STACK_SIZE (1 << LOG_LOG_MAX_STACK_SIZE) +#define MAX_STACK_COUNT (1 << LOG_MAX_STACK_COUNT) + unsigned internal_count:LOG_MAX_STACK_COUNT; + unsigned log_size:LOG_LOG_MAX_STACK_SIZE; +#else + int internal_count, internal_size; +#endif + + /* The stack is size optimized and avoids an additional heap allocation as + * long the size is <= 1. + */ + union + { + void **as_array; /* if size > 1 */ + void *as_pointer; /* size <= 1 */ + } + data; +}; + +/*------------------------------------------------------------------------*/ +/* An Arena is used for allocating aligned memory of aligned size. It is + * similar to a stack, since the new memory is always added to the end of + * the already allocated memory. Memory is kept contiguous thus that each + * allocation may trigger resizing and moving the already allocated data. + * This in turn requires that all pointers to allocated + * memory in an arena may have to be fixed. + */ +struct Arena +{ + int alignment; + char *mem_start, *mem_end, *data_start, *data_end; +}; + +/*------------------------------------------------------------------------*/ + +struct Variable +{ + Variable *assignment; /* TRUE, FALSE, or 'this' */ + Occurence reason; /* reason for the assignment */ + int decision_level; /* the decision level if assigned */ + Stack watched[2]; /* watched occurences of this variable */ + int ref[2]; /* number of occurrences */ + + int saved[2]; /* old score after last rescore */ + int score[2]; /* current score */ + int pos[2]; /* position in order */ + + int id; /* the external integer id of a variable */ + + /* We use this 'mark' bit for graph traversal purposes. + */ + unsigned mark:1; + + /* The 'sign_in_clause' is used to ensure that externally added clauses + * contain each variable only once. See 'unique_literals' for more + * details. + */ + unsigned sign_in_clause:1; + + /* If a variable is scheduled to be assigned, the position of the + * scheduled assignment in the assignment queue is stored with the + * variable. This allows early detection and generation of conflicts, in + * case a variable and its negation are both scheduled to be assigned to + * true. + */ + unsigned sign_on_queue:1; + int pos_on_queue; +}; + +/*------------------------------------------------------------------------*/ + +struct Clause +{ + unsigned learned:1; /* external or learned clause */ + int size:sizeof (unsigned) * 8 - 3; /* number of literals */ +#ifdef OPTIMIZE_DIRECTION + int direction:2; +#endif + int literals_idx; /* points into literal stack */ + int id; + int watched[2]; /* watched literals */ +}; + +/*------------------------------------------------------------------------*/ +/* The representation of a scheduled assignment is somewhat redundant, since + * the decision level and also the literal can be extracted from the + * reason, if 'reason' is non-zero. + */ +struct Assignment +{ + Variable *literal; + int decision_level; + Occurence reason; +}; + +/*------------------------------------------------------------------------*/ +/* The control stack contains frames. Each frame corresponds to a decision. + * Since we do not necessarily flip each decision made, but use conflict + * directed backtracking instead, there is no such notion as branches. + */ +struct Frame +{ + Variable *decision; /* the decisoin assignment made */ + int decision_level; + int trail_level; /* the old level of the trail */ +}; + +/*------------------------------------------------------------------------*/ +/* A counter, that counts up to a certain threshold, and then starts again + * with the threshold scaled by a certain factor. We use it to control + * rescore and restart operations and when to print a one line progress + * report. + */ +struct Counter +{ + int current, init, inc; + double factor, finished; +}; + +/*------------------------------------------------------------------------*/ + +struct Statistics +{ + double assignments, propagations, visits, uips, backjumps; + double swapped, compared, searched; + double learned_clauses, removed_clauses; + double learned_literals, removed_literals; + double rescored_variables, sum_assigned_in_decision, sum_score_in_decision; + int original_clauses, max_clauses; + int original_literals, max_literals; +}; + +/*------------------------------------------------------------------------*/ + +struct Limmat +{ + /* Control stack. + */ + int control_size, decision_level; + Frame *control; + Stack trail; /* assigned variables, ordered by decision level */ + + /* Scheduled assignments queue. + */ + int head_assignments, tail_assignments, size_assignments; + Assignment *assignments; + int inconsistent; /* position of first inconsistent assignment */ + + /* Variable manager. + */ + int max_id, num_literals, num_variables, current_max_score, max_score; + double added_literals; + Arena variables; + Stack order; /* order variables for choosing decisions */ + + /* Maintain interval in which we do not have to perform sorting of + * variables in the 'order' and also do not have to search for new + * assignments. + */ + int last_assigned_pos; /* position of last assigned variable */ + int first_zero_pos; /* position of first zero score variable */ + + /* Clause data base; + */ + int contains_empty_clause; + Stack clauses, units, literals; + + /* Necessary statistics. + */ + double num_decisions, num_conflicts, added_clauses; + int num_assigned, num_clauses; + + /* Additional statistics. + */ + Statistics *stats; + + /* Save literals for generating conflict clauses during conflict analysis + * on this stack. Keeping a global stack for this purpose around saves us + * some memory allocations. + */ + Stack clause; + + /* A multipurpose stack used in inner functions onlys. + */ + Stack stack; + + /* Logging. + */ + FILE *log; + + /* Counters. + */ + Counter report, restart, rescore; + + /* See 'RESCOREFACTOR'. + */ + double score_factor; + + char *error; + double time, timer; + + /* Memory manager. + */ + size_t bytes, max_bytes; + +#if defined(CHECK_CONSISTENCY) || defined(EXPENSIVE_CHECKS) + int check_counter; +#endif + +#ifdef EXPENSIVE_CHECKS + int inner_mode; /* no inner 'check_clause_is_implied' */ +#endif + +#ifdef LOG_SOMETHING + int dont_log; /* no internal logging */ +#endif +}; + +/*------------------------------------------------------------------------*/ + +struct Parser +{ + Limmat *limmat; + int num_specified_clauses, num_specified_max_id; + Stack literals; + FILE *file; + int close_file; /* do not close if 'file' was 'stdin' */ + int lineno; /* lineno */ + char *error; /* parse error occured */ + char *name; /* remember file name for error message */ +}; + +/*------------------------------------------------------------------------*/ +/* We want to keep 'align' as macro to be able to have the result of 'align' + * as compile time constant. One reason for this is to speed up the + * variable iterator. + */ +#define is_aligned(_n_,_alignment_) !((_n_) & ((_alignment_) - 1)) + +#define align(_n_,_alignment_) \ + (is_aligned(_n_,_alignment_) ? (_n_) : ((_n_)|((_alignment_) - 1)) + 1) + +/*------------------------------------------------------------------------*/ +/* Increment variable pointer during variable arena traversal. + */ +#define next_Variable(_v_) \ + ((Variable*)(align(sizeof(Variable), VARIABLE_ALIGNMENT) + (char*)(_v_))) + +/*------------------------------------------------------------------------*/ +/* Traverse all variables with non zero id. The 2nd and 3rd argument + * should be of type 'Variable*'. The helper variable '_end_of_variables_' + * is used for speeding up traversal. + * + * ATTENTION: These loops can not be nested. + */ +#define forall_variables(_limmat_,_pointer_to_variable_,_end_of_variables_) \ + for(_pointer_to_variable_ = start_of_Arena(&_limmat_->variables), \ + _end_of_variables_ = (Variable*) end_of_Arena(&_limmat_->variables); \ + _pointer_to_variable_ < (Variable*) _end_of_variables_; \ + _pointer_to_variable_ = next_Variable(_pointer_to_variable_)) \ + if(_pointer_to_variable_->id) + +/*------------------------------------------------------------------------*/ +/* Traverse the contents of a stack. Since 'p' actually points to the + * stack entries in the stack, you can use this loop for changing the + * contents of the stack as well. + * + * '_type_' the element type pushed on the stack + * '_ptr_in_stack_' a pointer to elements on the stack + * '_end_of_stack_' a helper variable to speed up the iterator + * + * Typical usage would be + * + * int * p, * end; + * Stack stack; + * init_Stack(limmat,&stack); + * push_Stack(limmat,&stack,(void*)0); // actually push an int + * push_Stack(limmat,&stack,(void*)1); // actually push an int + * push_Stack(limmat,&stack,(void*)2); // actually push an int + * ... + * s = 0; + * forall_Stack(&stack, int, p, end); + * s += (int) *p; + * + * ATTENTION: These loops can not be nested. In case you need to nest two + * loops simply use a static inlined function for the inner loop. + */ +#define forall_Stack(_stack_,_type_,_ptr_in_stack_,_end_of_stack_) \ + for(_ptr_in_stack_ = (_type_*) start_of_Stack(_stack_), \ + _end_of_stack_ = (_type_*) end_of_Stack(_stack_); \ + _ptr_in_stack_ < _end_of_stack_; \ + _ptr_in_stack_++) + +/*-----------------------------------------------------------------------*/ +/* Traverse all clauses. + * + * ATTENTION: These loops can not be nested. + */ +#define forall_clauses(_limmat_,_ptr_to_clause_,_end_of_clauses_) \ + forall_Stack(&(_limmat_)->clauses,Clause*,_ptr_to_clause_,_end_of_clauses_) + +/*------------------------------------------------------------------------*/ +/* Traverse the literals of a clause. + * + * ATTENTION: These loops can not be nested. + */ +#define forall_literals(_limmat_,_clause_,_ptol_,_eol_) \ + for(_ptol_ = clause2literals(_limmat_, _clause_), \ + _eol_ = (_clause_)->size + _ptol_; \ + _ptol_ < _eol_; \ + _ptol_++) + +/*------------------------------------------------------------------------*/ + +static int +min_int (int a, int b) +{ + return (a < b) ? a : b; +} + +/*------------------------------------------------------------------------*/ +#ifdef LIMMAT_WHITE +/*------------------------------------------------------------------------*/ + +inline static int +msnzb (int n) +{ + int res, i, tmp, mask; + + res = 0; + i = sizeof (int) * 4; + mask = (~0) << i; + + while (i) + { + tmp = n & mask; + if (tmp) + { + n = tmp >> i; + res += i; + } + i /= 2; + mask >>= i; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static int +log2ceil (int n) +{ + int res; + + assert (n > 0); + + res = msnzb (n); + if (n > (1 << res)) + res++; + + assert ((1 << res) >= n); + assert ((1 << res) / 2 < n); + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif /* LIMMAT_WHITE */ +/*------------------------------------------------------------------------*/ +/* Get the number of seconds spent in this process including system time. + */ +static double +get_time (void) +{ + double res = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ +/* To measure the time spent by a particular procedure, save the current + * process time with 'start_timer'. After the procedure has finished call + * 'stop_timer' with the previously saved time. The result is the time + * between both calls. + */ +static void +start_timer (double *timer) +{ + *timer = get_time (); +} + +/*------------------------------------------------------------------------*/ + +static double +stop_timer (double timer) +{ + double res; + + res = get_time () - timer; + if (res < 0) + res = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ +/* Combine both operations 'start_timer' and 'stop_timer'. The accumulated + * time is not added to the result for the previous time interval. + */ +static double +restart_timer (double *timer) +{ + double res; + + res = stop_timer (*timer); + start_timer (timer); + + return res; +} + +/*------------------------------------------------------------------------*/ + +void +adjust_timer_Limmat (Limmat * limmat) +{ + limmat->time += restart_timer (&limmat->timer); +} + +/*------------------------------------------------------------------------*/ + +static void +init_Counter (Counter * counter, int init, double factor, int increment) +{ + assert (init >= 0); + + counter->factor = factor; + counter->init = init; + counter->inc = increment; + counter->current = init; + counter->finished = 0; +} + +/*------------------------------------------------------------------------*/ + +static void +dec_Counter (Counter * counter) +{ + assert (counter->current >= 0); + if (counter->init && counter->current >= 0) + counter->current -= 1; +} + +/*------------------------------------------------------------------------*/ + +static int +done_Counter (Counter * counter) +{ + int res; + + if (counter->init) + { + if (counter->current) + res = 0; + else + { + counter->init = (int) (counter->init * counter->factor); + counter->init += counter->inc; + counter->current = counter->init; + counter->finished++; + res = 1; + } + } + else + res = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ +#ifdef CHECK_CONSISTENCY +/*------------------------------------------------------------------------*/ +/* This section contains some helper functions in case we want to check that + * allocated data is released with the correct size as argument to delete. + * Without this check we would not know whether our internal count for the + * used up memory is correct. + */ +/*------------------------------------------------------------------------*/ + +static int +bucketsize (size_t n) +{ + return n + DATA_OFFSET; +} + +/*------------------------------------------------------------------------*/ + +static Bucket * +ptr2bucket (void *ptr) +{ + Bucket *res; + + res = (Bucket *) (((char *) ptr) - DATA_OFFSET); + assert (ptr == (void *) &res->aligned_data); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void * +bucket2ptr (Bucket * bucket) +{ + return (void *) &bucket->aligned_data; +} + +/*------------------------------------------------------------------------*/ +#endif /* CHECK_CONSISTENCY */ +/*------------------------------------------------------------------------*/ + +static void * +new (Limmat * limmat, size_t size) +{ + size_t bytes; + void *res; + +#ifdef CHECK_CONSISTENCY + Bucket *bucket; + + bytes = bucketsize (size); + bucket = (Bucket *) malloc (bytes); + assert (bucket); + bucket->size = size; + res = bucket2ptr (bucket); +#else + bytes = size; + res = malloc (size); +#endif + + limmat->bytes += bytes; + if (limmat->max_bytes < limmat->bytes) + limmat->max_bytes = limmat->bytes; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +delete (Limmat * limmat, void *ptr, size_t size) +{ + size_t bytes; + +#ifdef CHECK_CONSISTENCY + Bucket *bucket; + + bucket = ptr2bucket (ptr); + assert (bucket->size == size); + bytes = bucketsize (bucket->size); + free (bucket); +#else + free (ptr); + bytes = size; +#endif + + assert (limmat->bytes >= bytes); + limmat->bytes -= bytes; +} + +/*------------------------------------------------------------------------*/ + +static void * +resize (Limmat * limmat, void *ptr, size_t new_size, size_t old_size) +{ + size_t old_bytes, new_bytes; + void *res; + +#ifdef CHECK_CONSISTENCY + Bucket *old_bucket, *new_bucket; + + old_bucket = ptr2bucket (ptr); + assert (old_bucket->size == old_size); + old_bytes = bucketsize (old_bucket->size); + new_bytes = bucketsize (new_size); + + new_bucket = (Bucket *) realloc (old_bucket, new_bytes); + assert (new_bucket); + new_bucket->size = new_size; + res = bucket2ptr (new_bucket); +#else + res = realloc (ptr, new_size); + assert (res); + old_bytes = old_size; + new_bytes = new_size; +#endif + + assert (limmat->bytes >= old_bytes); + + limmat->bytes -= old_bytes; + limmat->bytes += new_bytes; + + if (old_bytes > new_bytes && limmat->max_bytes < limmat->bytes) + limmat->max_bytes = limmat->bytes; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +count_Stack (Stack * stack) +{ + return stack->internal_count; +} + +/*------------------------------------------------------------------------*/ + +static void +reset_Stack (Limmat * limmat _U_, Stack * stack, int new_count) +{ + assert (new_count >= 0); + assert (new_count <= count_Stack (stack)); + + stack->internal_count = new_count; +} + +/*------------------------------------------------------------------------*/ + +static void +init_Stack (Limmat * limmat _U_, Stack * stack) +{ +#ifdef COMPACT_STACK + stack->log_size = 0; +#else + stack->internal_size = 1; +#endif + + stack->internal_count = 0; + stack->data.as_pointer = 0; +} + +/*------------------------------------------------------------------------*/ + +static int +size_Stack (Stack * stack) +{ + int res; + +#ifdef COMPACT_STACK + res = 1 << stack->log_size; +#else + res = stack->internal_size; +#endif + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +release_Stack (Limmat * limmat, Stack * stack) +{ + size_t bytes; + + if (size_Stack (stack) > 1) + { + bytes = size_Stack (stack) * sizeof (void *); + delete (limmat, stack->data.as_array, bytes); + } +} + +/*------------------------------------------------------------------------*/ + +static void +enlarge_Stack (Limmat * limmat, Stack * stack) +{ + size_t old_bytes, new_bytes; + int old_size, new_size; + void *data; + + old_size = size_Stack (stack); + new_size = old_size * 2; + new_bytes = new_size * sizeof (void *); + + if (old_size == 1) + { + data = stack->data.as_pointer; + stack->data.as_array = (void **) new (limmat, new_bytes); + stack->data.as_array[0] = data; + } + else + { + assert (old_size > 1); + old_bytes = old_size * sizeof (void *); + stack->data.as_array = (void **) + resize (limmat, stack->data.as_array, new_bytes, old_bytes); + } + +#ifdef COMPACT_STACK + if (stack->log_size + 1 >= LOG_MAX_STACK_SIZE) + abort (); + if (stack->internal_count + 1 >= MAX_STACK_COUNT) + abort (); + stack->log_size++; +#else + stack->internal_size = new_size; +#endif +} + +/*------------------------------------------------------------------------*/ + +inline static int +is_immediate_Stack (Stack * stack) +{ +#ifdef COMPACT_STACK + return stack->log_size == 0; +#else + return stack->internal_size <= 1; +#endif +} + +/*------------------------------------------------------------------------*/ + +inline static void * +pop (Stack * stack) +{ + void *res; + + assert (stack->internal_count); + + stack->internal_count -= 1; + + if (is_immediate_Stack (stack)) + res = stack->data.as_pointer; + else + res = stack->data.as_array[stack->internal_count]; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static int +is_full_Stack (Stack * stack) +{ + return stack->internal_count >= size_Stack (stack); +} + +/*------------------------------------------------------------------------*/ + +inline static void +push (Limmat * limmat, Stack * stack, void *data) +{ + if (is_full_Stack (stack)) + enlarge_Stack (limmat, stack); + + assert (stack->internal_count < size_Stack (stack)); + + if (is_immediate_Stack (stack)) + stack->data.as_pointer = data; + else + stack->data.as_array[stack->internal_count] = data; + + stack->internal_count += 1; +} + +/*------------------------------------------------------------------------*/ + +inline static void * +start_of_Stack (Stack * stack) +{ + void *res; + + switch (size_Stack (stack)) + { + case 0: + res = 0; + break; + + case 1: + res = &stack->data.as_pointer; + break; + + default: + res = stack->data.as_array; + break; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static void * +end_of_Stack (Stack * stack) +{ + void *res, **base; + + base = start_of_Stack (stack); + res = base + stack->internal_count; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static int * +intify_Stack (Stack * stack) +{ + void ** start; + + start = start_of_Stack (stack); + +#ifdef WIDE_POINTERS + { + void ** p, ** end; + int * q, tmp; + + end = end_of_Stack (stack); + + for(p = start, q = (int*) start ; p < end; p++, q++) + { + tmp = (int) (PTR_SIZED_WORD) *p; + *q = tmp; + } + } +#endif + + return (int*) start; +} + +/*------------------------------------------------------------------------*/ +#ifndef NDEBUG +/*------------------------------------------------------------------------*/ + +static int +is_valid_alignment (PTR_SIZED_WORD a) +{ + return a == 4 || a == 8 || a == 16 || a == 32 || a == 64; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +#if !defined(NDEBUG) || defined(LIMMAT_WHITE) +/*------------------------------------------------------------------------*/ + +static int +is_aligned_ptr (void *ptr, PTR_SIZED_WORD alignment) +{ + return is_aligned ((PTR_SIZED_WORD) ptr, alignment); +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +static void * +align_ptr (void *ptr, PTR_SIZED_WORD alignment) +{ + void *res; + + res = (void *) align ((PTR_SIZED_WORD) ptr, alignment); + assert (is_aligned_ptr (res, alignment)); + + return res; +} + +/*------------------------------------------------------------------------*/ +#if defined(CHECK_CONSISTENCY) || defined(EXPENSIVE_CHECKS) +/*------------------------------------------------------------------------*/ + +static int +check_it_now (Limmat * limmat) +{ + int res; + + assert (limmat->check_counter >= 0); + if (limmat->check_counter > 0) + limmat->check_counter--; + res = !limmat->check_counter; +#ifdef EXPENSIVE_CHECKS + if (res) + res = !limmat->inner_mode; +#endif + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +static void +invariant_Arena (Limmat * limmat _U_, Arena * arena) +{ +#ifndef NDEBUG + + assert (arena->mem_start <= arena->data_start); + assert (arena->data_start <= arena->data_end); + assert (arena->data_end <= arena->mem_end); + + assert (is_aligned_ptr (arena->data_start, arena->alignment)); + assert (is_aligned_ptr (arena->data_end, arena->alignment)); + +#ifdef EXPENSIVE_CHECKS + if (check_it_now (limmat)) + { + char *p; + for (p = arena->data_end; p < arena->mem_end; p++) + assert (!*p); + } +#endif +#endif +} + +/*------------------------------------------------------------------------*/ + +static void +init_Arena (Limmat * limmat _U_, Arena * arena, int alignment) +{ + assert (is_valid_alignment ((PTR_SIZED_WORD) alignment)); + + arena->alignment = alignment; + arena->mem_start = 0; + arena->mem_end = 0; + arena->data_start = 0; + arena->data_end = 0; +} + +/*------------------------------------------------------------------------*/ + +static void +release_Arena (Limmat * limmat, Arena * arena) +{ + size_t bytes; + + if (arena->mem_start) + { + bytes = arena->mem_end - arena->mem_start; + assert (bytes > 0); + delete (limmat, arena->mem_start, bytes); + } +} + +/*------------------------------------------------------------------------*/ + +static void +reset_Arena (Limmat * limmat _U_, Arena * arena) +{ + char *p; + for (p = arena->data_start; p < arena->data_end; p++) + *p = 0; + arena->data_end = arena->data_start; +} + +/*------------------------------------------------------------------------*/ + +static void +limmat_memcpy (char *dst, const char *src, size_t size) +{ + const char *p, *end; + char *q; + + if (src > dst) + { + p = src; + q = dst; + end = src + size; + while (p < end) + *q++ = *p++; + } + else if (src < dst) + { + p = src + size; + q = dst + size; + while (p > src) + *--q = *--p; + } +} + +/*------------------------------------------------------------------------*/ + +static void * +alloc_Arena (Limmat * limmat, Arena * arena, int size, size_t *delta_ptr) +{ + char *res, *new_data_start, *new_data_end, *new_mem_start, *p, *q; + size_t mem_delta, data_delta, old_bytes, new_bytes, required_bytes; + size_t old_alignment, new_alignment, delta_alignment; + + size = align (size, arena->alignment); + data_delta = 0; + + /* First adjust allocated memory to hold current data and at least + * additional 'size' bytes. + */ + if (arena->mem_start) + { + /* There has been a previous allocation. + */ + new_data_end = arena->data_end + size; + + if (new_data_end > arena->mem_end) + { + /* The allocated memory can not hold additional 'size' bytes. + */ +#ifdef EXPENSIVE_CHECKS + int len = arena->data_end - arena->data_start; + char *old_data = memmove (malloc (len), arena->data_start, len); +#endif + + old_bytes = arena->mem_end - arena->mem_start; + new_bytes = 2 * old_bytes; + required_bytes = old_bytes + size + arena->alignment; + while (new_bytes < required_bytes) + new_bytes *= 2; + + new_mem_start = (char *) + resize (limmat, arena->mem_start, new_bytes, old_bytes); + mem_delta = new_mem_start - arena->mem_start; + + if (mem_delta) + { + new_data_start = align_ptr (new_mem_start, arena->alignment); + data_delta = new_data_start - arena->data_start; + old_alignment = arena->data_start - arena->mem_start; + new_alignment = new_data_start - new_mem_start; + delta_alignment = new_alignment - old_alignment; + + if (delta_alignment) + { + new_data_end = arena->data_end + data_delta; + + /* Be carefull in case there is a clever 'realloc' and a + * reallocated block overlaps with the original block, and + * one block is aligned and the other not. In this case + * it is important to have a proper implementation of + * 'memcpy' that can handle overlapping source and + * destination data blocks. + */ + limmat_memcpy (new_data_start, + new_data_start - delta_alignment, + new_data_end - new_data_start); + } + } + else + { + new_data_start = arena->data_start; /* see assertion below */ + data_delta = 0; + } + + arena->mem_start = new_mem_start; + arena->mem_end = new_mem_start + new_bytes; + + arena->data_start += data_delta; + arena->data_end += data_delta; + + assert (arena->data_start == new_data_start); + + /* Clear all fresh allocated data. + */ + p = arena->data_end; + q = arena->mem_end; + while (p < q) + *p++ = 0; + +#ifdef EXPENSIVE_CHECKS + assert (!memcmp (old_data, arena->data_start, len)); + free (old_data); +#endif + } + } + else + { + /* No previous allocation. + */ + required_bytes = size + arena->alignment; + new_bytes = 16; + while (new_bytes < required_bytes) + new_bytes *= 2; + + new_mem_start = (char *) new (limmat, new_bytes); + new_data_start = align_ptr (new_mem_start, arena->alignment); + arena->mem_start = new_mem_start; + arena->mem_end = new_mem_start + new_bytes; + arena->data_start = new_data_start; + arena->data_end = new_data_start; + + /* Clear all allocated data. + */ + p = arena->mem_start; + q = arena->mem_end; + while (p < q) + *p++ = 0; + } + + res = arena->data_end; + arena->data_end += size; + + invariant_Arena (limmat, arena); + assert (is_aligned_ptr (res, arena->alignment)); + + *delta_ptr = data_delta; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void * +start_of_Arena (Arena * arena) +{ + return arena->data_start; +} + +/*------------------------------------------------------------------------*/ + +static void * +end_of_Arena (Arena * arena) +{ + return arena->data_end; +} + +/*------------------------------------------------------------------------*/ +#ifndef NDEBUG +/*------------------------------------------------------------------------*/ + +static int +is_array_Arena (Arena * arena, int element_size) +{ + int has_non_zero_rest; + size_t data_bytes; + + element_size = align (element_size, arena->alignment); + data_bytes = arena->data_end - arena->data_start; + has_non_zero_rest = data_bytes % element_size; + + return !has_non_zero_rest; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +#if 0 +/*------------------------------------------------------------------------*/ + +static void * +next_Arena (Arena * arena, void *ptr, int element_size) +{ + void *res; + + assert (is_array_Arena (arena, element_size)); + assert (is_aligned_ptr (ptr, arena->alignment)); + assert (arena->mem_start <= (char *) ptr); + assert (arena->mem_end > (char *) ptr); + + res = align (element_size, arena->alignment) + (char *) ptr; + + assert (is_aligned_ptr (res, arena->alignment)); + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* An Arena can be accessed as an array. + */ +static void * +access_Arena (Limmat * limmat, + Arena * arena, int index, int element_size, size_t *delta_ptr) +{ + int old_num_elements, new_num_elements, delta_num_elements; + size_t delta_bytes; + char *res; + + assert (index >= 0); + assert (element_size > 0); + assert (is_array_Arena (arena, element_size)); + + element_size = align (element_size, arena->alignment); + + old_num_elements = (arena->data_end - arena->data_start) / element_size; + new_num_elements = index + 1; + delta_num_elements = new_num_elements - old_num_elements; + + if (delta_num_elements > 0) + { + delta_bytes = delta_num_elements * element_size; + (void) alloc_Arena (limmat, arena, delta_bytes, delta_ptr); + assert (is_array_Arena (arena, element_size)); + } + else + *delta_ptr = 0; + + res = arena->data_start + element_size * index; + assert (res + element_size <= arena->data_end); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +getbit (void *v, PTR_SIZED_WORD bit) +{ + return (bit & (PTR_SIZED_WORD) v) != 0; +} + +/*------------------------------------------------------------------------*/ + +static void * +clrbit (void *v, PTR_SIZED_WORD bit) +{ + PTR_SIZED_WORD tmp; + void *res; + + tmp = (PTR_SIZED_WORD) v; + tmp &= ~bit; + res = (void *) tmp; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void * +toggle (void *v, PTR_SIZED_WORD bit) +{ + PTR_SIZED_WORD tmp; + void *res; + + tmp = (PTR_SIZED_WORD) v; + tmp ^= bit; + res = (void *) tmp; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +is_signed (void *v) +{ + return getbit (v, SIGN_BIT); +} +static void * +strip (void *v) +{ + return clrbit (v, SIGN_BIT); +} +static void * +not (void *v) +{ + return toggle (v, SIGN_BIT); +} + +/*------------------------------------------------------------------------*/ + +static void * +lit2var (void *v) +{ + return clrbit (v, ALL_BUT_SIGN_BITS); +} + +/*------------------------------------------------------------------------*/ + +static int +is_assigned (Variable * v) +{ + if (is_signed (v)) + v = not (v); + return v->assignment != v; +} + +/*------------------------------------------------------------------------*/ + +static Variable * +deref (Variable * v) +{ + Variable *res; + int sign; + + if ((sign = is_signed (v))) + v = not (v); + res = v->assignment; + if (sign) + res = not (res); + + return res; +} + +/*------------------------------------------------------------------------*/ +/* The assignments are stored in a cyclic queue. The 'head_assignments' + * index points to the next assignment to be dequeued, while the + * 'tail_assignments' index points to the next empty slot. Both keep on + * increasing starting from zero and wrap around at 'size_assignments'. + */ +static int +count_assignments (Limmat * limmat) +{ + int res; + + if (limmat->tail_assignments >= limmat->head_assignments) + { + res = limmat->tail_assignments - limmat->head_assignments; + } + else + { + res = limmat->size_assignments - limmat->head_assignments; + res += limmat->tail_assignments; + } + + assert (0 <= res); + assert (res < limmat->size_assignments); + + return res; +} + +/*------------------------------------------------------------------------*/ +/* Increase the size of the buffer allocated for the assignments queue by a + * factor of two. + */ +static void +resize_assignments (Limmat * limmat) +{ + int new_size, new_tail, new_bytes, old_size, old_bytes, i, old_pos; + Assignment *new_assignments, *old_assignments; + Variable *literal; + + old_size = limmat->size_assignments; + new_size = old_size * 2; + new_bytes = sizeof (Assignment) * new_size; + new_assignments = (Assignment *) new (limmat, new_bytes); + new_tail = count_assignments (limmat); + + assert (new_tail < new_size); + + old_assignments = limmat->assignments; + + /* We move the whole contents of the queue to the start of the new + * allocated buffer. Then we have to adjust the 'position' index of all + * variables of scheduled assignments. + */ + for (i = 0; i < new_tail; i++) + { + old_pos = i + limmat->head_assignments; + if (old_pos >= old_size) + old_pos -= old_size; + literal = strip (old_assignments[old_pos].literal); +#if defined(EARLY_CONFLICT_DETECTION) && defined(SHORTEN_REASONS) + assert (literal->pos_on_queue == old_pos); +#endif + new_assignments[i] = old_assignments[old_pos]; + literal->pos_on_queue = i; + } + + old_bytes = sizeof (Assignment) * old_size; + delete (limmat, old_assignments, old_bytes); + + limmat->assignments = new_assignments; + limmat->size_assignments = new_size; + limmat->tail_assignments = new_tail; + limmat->head_assignments = 0; +} + +/*------------------------------------------------------------------------*/ + +inline static void +fix_pointer (void *void_ptr_ptr, size_t delta) +{ + char **char_ptr_ptr, *new_value; + + char_ptr_ptr = (char **) void_ptr_ptr; + new_value = delta + *char_ptr_ptr; + *char_ptr_ptr = new_value; +} + +/*------------------------------------------------------------------------*/ + +static void +fix_variables (Limmat * limmat, size_t delta) +{ + Variable *v, *eov; + + forall_variables (limmat, v, eov) + if (v->assignment != TRUE && v->assignment != FALSE) + { + fix_pointer (&v->assignment, delta); + } +} + +/*------------------------------------------------------------------------*/ + +static void +fix_Stack (Stack * stack, size_t delta) +{ + void **o, **eoo; + + forall_Stack (stack, void *, o, eoo) fix_pointer (o, delta); +} + +/*------------------------------------------------------------------------*/ + +static Variable ** +clause2literals (Limmat * limmat, Clause * clause) +{ + Variable **res; + + res = start_of_Stack (&limmat->literals); + res += clause->literals_idx; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +fix_clauses (Limmat * limmat, size_t delta) +{ + Variable **q, **eol; + Clause **p, **eoc; + + forall_clauses (limmat, p, eoc) + forall_literals (limmat, *p, q, eol) fix_pointer (q, delta); +} + +/*------------------------------------------------------------------------*/ + +static void +fix_pointers_to_variables (Limmat * limmat, size_t delta) +{ + assert (limmat->decision_level < 0); + assert (!count_assignments (limmat)); + + fix_variables (limmat, delta); + fix_Stack (&limmat->order, delta); + fix_clauses (limmat, delta); +} + +/*------------------------------------------------------------------------*/ +#ifndef NDEBUG +/*------------------------------------------------------------------------*/ + +static void +check_valid_assignment_index (Limmat * limmat, int idx) +{ + assert (0 <= idx); + assert (idx <= limmat->size_assignments); + + if (limmat->head_assignments <= limmat->tail_assignments) + { + assert (idx >= limmat->head_assignments); + assert (idx < limmat->tail_assignments); + } + else + { + assert (idx >= limmat->head_assignments || + idx < limmat->tail_assignments); + } +} + +/*------------------------------------------------------------------------*/ + +static void +check_assignment_index (Limmat * limmat, Variable * literal) +{ + int sign; + + sign = is_signed (literal); + if (sign) + literal = not (literal); + check_valid_assignment_index (limmat, literal->pos_on_queue); + if (sign) + assert (literal->sign_on_queue); + else + assert (!literal->sign_on_queue); +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +#ifdef SHORTEN_REASONS +/*------------------------------------------------------------------------*/ +/* Compare assignments with respect to level and size of reasons. + */ +static int +cmp_assignment (Limmat * limmat _U_, Assignment * a, Assignment * b) +{ + int res, alevel, blevel, aid, bid; + Occurence areason, breason; + + alevel = a->decision_level; + blevel = b->decision_level; + + if (alevel < blevel) + res = -1; + else if (alevel > blevel) + res = 1; + else + { + areason = a->reason; + breason = b->reason; + + if (!areason) + { + if (breason) + res = -1; + else + res = 0; + } + else if (!breason) + res = 1; + else + { +/* Comment this out out to make comparison with indexed version easier. + */ +#if 1 + int asize, bsize; + + asize = areason->size; + bsize = breason->size; + + if (asize < bsize) + res = -1; + else if (asize > bsize) + res = 1; + else +#endif + { + aid = areason->id; + bid = breason->id; + res = 0; + if (aid < bid) + res = -1; + else if (aid > bid) + res = 1; + } + } + } + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Push a new assignment onto the assignment queue for later retrieval with + * 'pop_assignment'. The queue is a FIFO queue for implementing BFS. This + * should heuristically generate smaller conflict generating assignment + * sequences than DFS with potentially smaller conflict clauses. + */ +static void +push_assignment (Limmat * limmat, Assignment * assignment) +{ + Variable *literal, *stripped, *tmp; + int sign, tail, count; + +#ifdef SHORTEN_REASONS + Assignment *old_assignment; + int cmp; +#endif + +#ifdef LOG_PUSH + static int counter = 0; + static int var2int (Variable *); + fprintf (LOGFILE (limmat), "PUSH\t%d\t%d\t%d\n", + counter++, var2int (assignment->literal), + count_assignments (limmat)); +#endif + + if (limmat->inconsistent >= 0) + { + /* Just skip additional assignments after the assignment queue + * detected that two contradicting assignments have already been + * pushed in an earlier 'push_assignment' operation. + */ + return; + } + + literal = assignment->literal; + sign = is_signed (literal); + stripped = sign ? not (literal) : literal; + + tmp = deref (literal); + assert (tmp != FALSE); + +#ifndef NDEBUG + if (stripped->pos_on_queue >= 0) + { + if (!stripped->sign_on_queue) + check_assignment_index (limmat, stripped); + else + check_assignment_index (limmat, not (stripped)); + } +#endif + + if (tmp != TRUE) + { +#ifdef SHORTEN_REASONS + if (stripped->pos_on_queue >= 0 && /* var already scheduled */ + !sign == !stripped->sign_on_queue) /* with matching sign */ + { + /* In case the same assignment is already scheduled and it has + * a larger decision level than the current one, or it has the + * same decision level but the reason is smaller, then we are + * overwriting the old assignment with the current one. Otherwise + * we keep the old assignment and just skip this one. + */ + old_assignment = limmat->assignments + stripped->pos_on_queue; + assert (old_assignment->literal == assignment->literal); + + cmp = cmp_assignment (limmat, assignment, old_assignment); + if (!cmp) + assert (limmat->decision_level == -1); + + if (cmp < 0) + { + old_assignment->decision_level = assignment->decision_level; + old_assignment->reason = assignment->reason; + } + } + else +#endif + { + /* The variable of the assignment is not scheduled to be assigned + * or it was scheduled to be assigned with opposite value. In any + * case, we push a fresh assignment on the assignment queue making + * sure that there is enough space for scheduling the current + * assignment. In particular the queue can maximally hold + * 'limmat->size_assignments - 1' elements. + */ + count = count_assignments (limmat); + if (count + 1 >= limmat->size_assignments) + { + resize_assignments (limmat); + assert (count_assignments (limmat) == count); + } + + tail = limmat->tail_assignments; + +#ifdef EARLY_CONFLICT_DETECTION + if (stripped->pos_on_queue >= 0 && /* variable scheduled */ + !sign != !stripped->sign_on_queue) /* with opposite sign */ + { + /* The variable has been scheduled to be assigned to the + * opposite value already. We just set the 'inconsistent' + * flag to point to the position of this earlier assignment, + * such that 'propagate' will immediately use the old and this + * new assignment in sequence to generate a conflict as early + * as possible. + */ + assert (stripped->pos_on_queue >= 0); + limmat->inconsistent = stripped->pos_on_queue; + } + else +#endif + { + stripped->pos_on_queue = tail; + stripped->sign_on_queue = sign ? 1 : 0; + } + + /* Enqueue the current assignment at the tail of the assignment + * queue. The 'tail' is increased and may wrap back to '0' at the + * end of the buffer allocated for the queue. + */ + limmat->assignments[tail++] = *assignment; + if (tail >= limmat->size_assignments) + tail = 0; + limmat->tail_assignments = tail; + + assert (count_assignments (limmat) == count + 1); + } + } +} + +/*------------------------------------------------------------------------*/ +/* Pop a previously scheduled assignment from the the assignments queue. + */ +static void +pop_assignment (Limmat * limmat, Assignment * assignment) +{ + int pos, head, tail, size, inconsistent; + Assignment *assignments; + Variable *stripped; + +#ifndef NDEBUG + int count = count_assignments (limmat); + assert (count > 0); +#endif + + assignments = limmat->assignments; + head = limmat->head_assignments; + size = limmat->size_assignments; + inconsistent = limmat->inconsistent; + + if (inconsistent >= 0) + { + /* A previous 'push_assignment' detected two conflicting + * 'assignments'. The first can be found at position 'inconsistent' + * and the second is the last assignment at the tail of the queue. We + * first schedule the propagation of the first assignment at position + * 'inconsistent'. + */ + assert (inconsistent < size); + pos = inconsistent; + tail = limmat->tail_assignments - 1; + if (tail < 0) + tail = size - 1; + + assert (tail < limmat->size_assignments); + assert (limmat->inconsistent != tail); + assert (assignments[pos].literal == not (assignments[tail].literal)); + + /* Remember that we already propagated the first assignment and still + * need to propagate the last one. The queue itself is not changed. + * In particular its size is not decreased. + */ + limmat->inconsistent = tail; + } + else + { + pos = head++; + if (head >= size) + head = 0; + limmat->head_assignments = head; + + assert (count_assignments (limmat) + 1 == count); + } + + /* Do not forget to invalidate the 'position' for the variable. + */ + assert (0 <= pos); + assert (pos < limmat->size_assignments); + stripped = strip (assignments[pos].literal); + stripped->sign_on_queue = 0; + stripped->pos_on_queue = -1; + + *assignment = assignments[pos]; +} + +/*------------------------------------------------------------------------*/ +/* During backtrakcing, after a conflict has been generated, we have to + * reset the assignments queue. As with stack we never decrease the size of + * the allocated buffer itself. + */ +static void +reset_assignments (Limmat * limmat) +{ + int sign, pos, i, count, size, head; + Assignment *assignments; + Variable *literal; + + assignments = limmat->assignments; + count = count_assignments (limmat); + size = limmat->size_assignments; + head = limmat->head_assignments; + + for (i = 0; i < count; i++) + { + pos = i + head; + if (pos >= size) + pos -= size; + literal = assignments[pos].literal; + sign = is_signed (literal); + if (sign) + literal = not (literal); + +#ifndef NDEBUG + { + if (literal->pos_on_queue >= 0) + { +#if defined(EARLY_CONFLICT_DETECTION) && defined(SHORTEN_REASONS) + assert (literal->pos_on_queue == pos); + assert (!literal->sign_on_queue == !sign); +#endif + } + } +#endif + + literal->sign_on_queue = 0; + literal->pos_on_queue = -1; + } + + limmat->tail_assignments = 0; + limmat->head_assignments = 0; + limmat->inconsistent = -1; + + assert (count_assignments (limmat) == 0); +} + +/*------------------------------------------------------------------------*/ + +static Statistics * +new_Statistics (Limmat * limmat) +{ + Statistics *res; + + res = (Statistics *) new (limmat, sizeof (Statistics)); + + res->removed_clauses = 0; + res->removed_literals = 0; + + res->max_literals = 0; + res->learned_literals = 0; + res->original_literals = 0; + + res->original_clauses = 0; + res->learned_clauses = 0; + res->max_clauses = 0; + res->rescored_variables = 0; + res->sum_assigned_in_decision = 0; + res->sum_score_in_decision = 0; + + res->assignments = 0; + res->propagations = 0; + res->visits = 0; + res->uips = 0; + res->backjumps = 0; + + res->swapped = 0; + res->compared = 0; + res->searched = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +option (const char *name, int default_initialization) +{ + char *val; + int res; + + val = getenv (name); + if (val) + res = atoi (val); + else + res = default_initialization; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static double +foption (const char *name, double default_initialization) +{ + double res; + char *val; + + val = getenv (name); + if (val) + res = atof (val); + else + res = default_initialization; + + return res; +} + +/*------------------------------------------------------------------------*/ + +Limmat * +new_Limmat (FILE * log) +{ + Limmat *res; + int bytes; + + res = (Limmat *) malloc (sizeof (Limmat)); + res->bytes = 0; + res->max_bytes = 0; + + init_Stack (res, &res->clauses); + init_Stack (res, &res->units); + init_Stack (res, &res->literals); + res->contains_empty_clause = 0; + res->added_clauses = 0; + res->num_clauses = 0; + + res->max_id = 0; + res->added_literals = 0; + res->num_literals = 0; + res->num_variables = 0; + init_Arena (res, &res->variables, VARIABLE_ALIGNMENT); + + res->decision_level = -1; + res->control_size = 1; + bytes = sizeof (Frame) * res->control_size; + res->control = (Frame *) new (res, bytes); + + res->size_assignments = 1; + bytes = sizeof (Assignment) * res->size_assignments; + res->assignments = (Assignment *) new (res, bytes); + res->head_assignments = 0; + res->tail_assignments = 0; + + init_Stack (res, &res->stack); + init_Stack (res, &res->trail); + init_Stack (res, &res->clause); + init_Stack (res, &res->order); + res->last_assigned_pos = -1; + res->first_zero_pos = 0; + res->num_assigned = 0; + res->max_score = 0; + res->current_max_score = 0; + + res->inconsistent = -1; + + res->error = 0; + res->time = 0; + + res->log = log; + + init_Counter (&res->report, 99, 1.21, 0); + init_Counter (&res->restart, option ("RESTART", RESTART), 1.4142, 1); + init_Counter (&res->rescore, option ("RESCORE", RESCORE), 1, 0); + + res->score_factor = foption ("RESCOREFACTOR", RESCOREFACTOR); + + res->num_decisions = 0; + res->num_conflicts = 0; + + res->stats = 0; + if (option ("STATISTICS", STATISTICS)) + res->stats = new_Statistics (res); + +#if defined(CHECK_CONSISTENCY) || defined(EXPENSIVE_CHECKS) + res->check_counter = option ("CHECK", 0); +#endif + +#ifdef LOG_SOMETHING + res->dont_log = 0; +#endif + +#ifdef EXPENSIVE_CHECKS + res->inner_mode = 0; +#endif + + return res; +} + +/*------------------------------------------------------------------------*/ + +void +set_log_Limmat (Limmat * limmat, FILE * log) +{ + limmat->log = log; +} + +/*------------------------------------------------------------------------*/ + +static int +get_score (Variable * v) +{ + int res, sign; + + if ((sign = is_signed (v))) + v = not (v); + res = v->score[sign]; + + return res; +} + +/*------------------------------------------------------------------------*/ +/* We want to have a rather stable sorting criteria for variables. In + * particular the decision process should not depend on the permutation of + * clauses in the file. + */ +inline static int +cmp (Limmat * limmat, Variable * v0, Variable * v1) +{ + int score[2], id[2], res; + + assert (v0 != FALSE); + assert (v0 != TRUE); + assert (v1 != FALSE); + assert (v1 != TRUE); + + if (limmat && limmat->stats) + limmat->stats->compared++; + + if (v0 == v1) + res = 0; + else + { + score[0] = get_score (v0); + score[1] = get_score (v1); + + /* The first sorting criteria is the 'score'. + */ + if (score[0] < score[1]) + res = -1; + else if (score[0] > score[1]) + res = 1; + else if (v0 == not (v1)) + { + /* Unsigned variables with the same score and id are smaller. + */ + res = (v0 < v1) ? -1 : 1; + } + else + { + /* Now even the 'score' of the two variables is the same. Then use + * the 'id' of the variables as sorting criteria. Variables with + * smaller indices are supposed to be larger. Since the id of the + * two variables can not be same, because of the last and the + * first test, we can just forget about the sign. + */ + v0 = strip (v0); + v1 = strip (v1); + id[0] = v0->id; + id[1] = v1->id; + assert (id[0] != id[1]); + res = (id[0] < id[1]) ? 1 : -1; + } + } + + return res; +} + +/*------------------------------------------------------------------------*/ +#ifdef EXPENSIVE_CHECKS +/*------------------------------------------------------------------------*/ + +static Clause * +find_empty_clause (Limmat * limmat) +{ + Clause *clause, **p, **eoc, *res; + int i, num_literals, found; + + res = 0; + + forall_clauses (limmat, p, eoc) + { + clause = *p; + num_literals = clause->size; + found = 0; + + for (i = 0; !found && i < num_literals; i++) + found = + (deref (lit2var (clause2literals (limmat, clause)[i])) != FALSE); + + if (!found) + res = clause; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +check_no_empty_clause (Limmat * limmat) +{ +#if 0 +#warning "check_no_empty_clause disabled" +#else + Clause *clause; + + if (!check_it_now (limmat)) + return; + + clause = find_empty_clause (limmat); + assert (!clause); +#endif +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Unassign all variables assigned at 'decision_level' and higher. + */ +static void +untrail (Limmat * limmat, int decision_level) +{ + Variable **all, **start, **p, *src; + int lower_pos, new_trail_level; + Frame *frame; + + assert (decision_level <= limmat->decision_level); + + all = start_of_Stack (&limmat->trail); + p = all + count_Stack (&limmat->trail); + + if (decision_level >= 0) + { + frame = limmat->control + decision_level; + new_trail_level = frame->trail_level; + } + else + new_trail_level = 0; + + start = all + new_trail_level; + assert (p >= start); + + while (p > start) + { + src = *--p; + + assert (!is_signed (src)); + assert (is_assigned (src)); + assert (src->decision_level >= decision_level); + + src->assignment = src; + src->reason = 0; + src->decision_level = -1; + + assert (limmat->num_assigned > 0); + limmat->num_assigned--; + + lower_pos = min_int (src->pos[0], src->pos[1]); + if (lower_pos <= limmat->last_assigned_pos) + limmat->last_assigned_pos = lower_pos - 1; + } + + reset_Stack (limmat, &limmat->trail, new_trail_level); + +#ifdef EXPENSIVE_CHECKS + check_no_empty_clause (limmat); +#endif +} + +/*------------------------------------------------------------------------*/ + +static void +reset_control (Limmat * limmat) +{ + untrail (limmat, -1); + limmat->decision_level = -1; +} + +/*------------------------------------------------------------------------*/ + +static void +reset_clauses (Limmat * limmat) +{ + Clause *clause, **p, **eoc; + + forall_clauses (limmat, p, eoc) + { + clause = *p; + delete (limmat, clause, sizeof (Clause)); + } + + reset_Stack (limmat, &limmat->clauses, 0); + limmat->contains_empty_clause = 0; +} + +/*------------------------------------------------------------------------*/ + +static void +reset_variables (Limmat * limmat) +{ + Variable *v, *end; + + forall_variables (limmat, v, end) + { + release_Stack (limmat, &v->watched[0]); + release_Stack (limmat, &v->watched[1]); + } + + reset_Arena (limmat, &limmat->variables); +} + +/*------------------------------------------------------------------------*/ + +static void +reset_order (Limmat * limmat) +{ + reset_Stack (limmat, &limmat->order, 0); + limmat->last_assigned_pos = -1; + limmat->first_zero_pos = 0; +} + +/*------------------------------------------------------------------------*/ + +static void +reset_error (Limmat * limmat) +{ + if (limmat->error) + { + delete (limmat, limmat->error, strlen (limmat->error) + 1); + limmat->error = 0; + } +} + +/*------------------------------------------------------------------------*/ + +static void +reset_Limmat (Limmat * limmat) +{ + reset_assignments (limmat); + reset_Stack (limmat, &limmat->clause, 0); + reset_control (limmat); + reset_clauses (limmat); + reset_order (limmat); + reset_variables (limmat); + reset_error (limmat); +} + +/*------------------------------------------------------------------------*/ + +static void +release_assignments (Limmat * limmat) +{ + int bytes; + + bytes = sizeof (Assignment) * limmat->size_assignments; + delete (limmat, limmat->assignments, bytes); +} + +/*------------------------------------------------------------------------*/ + +static void +release_control (Limmat * limmat) +{ + int bytes; + + bytes = sizeof (Frame) * limmat->control_size; + delete (limmat, limmat->control, bytes); + + release_Stack (limmat, &limmat->trail); +} + +/*------------------------------------------------------------------------*/ + +static void +release_statistics (Limmat * limmat) +{ + if (limmat->stats) + delete (limmat, limmat->stats, sizeof (Statistics)); +} + +/*------------------------------------------------------------------------*/ + +static void +release_Limmat (Limmat * limmat) +{ + release_assignments (limmat); + release_Stack (limmat, &limmat->stack); + release_Stack (limmat, &limmat->clause); + release_control (limmat); + release_Stack (limmat, &limmat->clauses); + release_Stack (limmat, &limmat->units); + release_Stack (limmat, &limmat->literals); + release_Stack (limmat, &limmat->order); + release_Arena (limmat, &limmat->variables); + release_statistics (limmat); +} + +/*------------------------------------------------------------------------*/ + +static int +internal_delete_Limmat (Limmat * limmat) +{ + int res; + + reset_Limmat (limmat); + release_Limmat (limmat); + res = limmat->bytes; + free (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +void +delete_Limmat (Limmat * limmat) +{ + (void) internal_delete_Limmat (limmat); +} + +/*------------------------------------------------------------------------*/ + +static void +parse_error (Parser * parser, const char *str1, const char *str2) +{ + const char *p; + int i; + + if (parser->error) + delete (parser->limmat, parser->error, ERROR_SIZE); + parser->error = (char *) new (parser->limmat, ERROR_SIZE); + + i = 0; + + if (parser->name) + { + for (p = parser->name; *p && i < ERROR_SIZE - 2; i++, p++) + parser->error[i] = *p; + + parser->error[i++] = ':'; + } + + if (i < ERROR_SIZE - 30) + { + sprintf (parser->error + i, "%d: ", parser->lineno); + i = strlen (parser->error); + for (p = str1; *p && i < ERROR_SIZE - 1; i++, p++) + parser->error[i] = *p; + + if (str2) + { + for (p = str2; *p && i < ERROR_SIZE - 1; i++, p++) + parser->error[i] = *p; + } + } + + assert (i < ERROR_SIZE); + + parser->error[i] = 0; +} + +/*------------------------------------------------------------------------*/ + +static Parser * +new_Parser (Limmat * limmat, FILE * file, const char *input_name) +{ + const char *name; + Parser *res; + + res = (Parser *) new (limmat, sizeof (Parser)); + res->num_specified_clauses = -1; + res->num_specified_max_id = -1; + res->limmat = limmat; + init_Stack (limmat, &res->literals); + res->lineno = 0; + res->error = 0; + + if (input_name || file) + name = input_name; + else + name = ""; + + res->name = 0; + + if (name) + { + res->name = (char *) new (limmat, strlen (name) + 1); + strcpy (res->name, name); + } + + res->close_file = 0; + + if (file) + res->file = file; + else if (input_name) + { + res->file = fopen (name, "r"); + if (!res->file) + parse_error (res, "could not open file", 0); + else + res->close_file = 1; + } + else + res->file = stdin; + + res->lineno = 1; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +delete_Parser (Parser * parser) +{ + if (parser->close_file) + fclose (parser->file); + + if (parser->name) + delete (parser->limmat, parser->name, strlen (parser->name) + 1); + + if (parser->error) + delete (parser->limmat, parser->error, ERROR_SIZE); + + release_Stack (parser->limmat, &parser->literals); + delete (parser->limmat, parser, sizeof (Parser)); +} + +/*------------------------------------------------------------------------*/ + +static int +read_number (Parser * parser, int *literal) +{ + int res, tmp, ch; + + ch = getc (parser->file); + + if (isdigit (ch)) + { + tmp = ch - '0'; + res = 1; + + while (isdigit (ch = getc (parser->file))) + tmp = 10 * tmp + (ch - '0'); + + *literal = tmp; + if (ch != EOF) + ungetc (ch, parser->file); + } + else + { + parse_error (parser, "expected digit", 0); + res = 0; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +read_white_space (Parser * parser) +{ + int res, ch; + + ch = getc (parser->file); + if (isspace (ch)) + { + while (isspace (ch = getc (parser->file))) + ; + + if (ch != EOF) + ungetc (ch, parser->file); + + res = 1; + } + else + { + parse_error (parser, "expected white space", 0); + res = 0; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +read_clause (Parser * parser) +{ + int ch, literal, sign, res, found_zero; + + if (parser->error) + return 0; + + assert (parser->file); + + reset_Stack (parser->limmat, &parser->literals, 0); + found_zero = 0; + res = 1; + + do + { + while (isspace (ch = getc (parser->file))) + if (ch == '\n') + parser->lineno++; + + sign = 1; + + switch (ch) + { + case '-': + sign = -1; + /* FALL THROUGH */ + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': + if (ch != '-') + ungetc (ch, parser->file); + res = read_number (parser, &literal); + literal *= sign; + if (res) + { + if (!literal) + found_zero = 1; + else + push (parser->limmat, &parser->literals, + (void *) (PTR_SIZED_WORD) literal); + } + break; + + case 'c': + while ((ch = getc (parser->file)) != '\n' && ch != EOF) + ; + if (ch == '\n') + parser->lineno++; + break; + + case 'p': + if (parser->num_specified_clauses >= 0) + { + parse_error (parser, "found 'p' spec twice", 0); + res = 0; + } + else if (read_white_space (parser)) + { + if (getc (parser->file) != 'c' || + getc (parser->file) != 'n' || getc (parser->file) != 'f') + { + parse_error (parser, "expected 'cnf' after 'p'", 0); + res = 0; + } + else if (read_white_space (parser)) + { + if (read_number (parser, &parser->num_specified_max_id)) + { + if (read_white_space (parser)) + { + res = read_number (parser, + &parser->num_specified_clauses); + } + else + res = 0; + } + else + res = 0; + } + else + res = 0; + } + else + res = 0; + break; + + case EOF: + res = 0; + break; + + default: + parse_error (parser, "non valid character", 0); + res = 0; + break; + } + } + while (res && !found_zero && ch != EOF); + + if (ch == EOF) + { + if (!found_zero && count_Stack (&parser->literals)) + { + parse_error (parser, "expected '0' after clause", 0); + res = 0; + } + } + else if (!res) + assert (parser->error); + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static void +inc_ref (Limmat * limmat _U_, Variable * v) +{ + Variable *stripped; + int sign; + + stripped = (sign = is_signed (v)) ? not (v) : v; + stripped->ref[sign]++; +} + +/*------------------------------------------------------------------------*/ + +inline static int +var2int (Variable * v) +{ + int sign, res; + + if ((sign = is_signed (v))) + v = not (v); + res = v->id; + if (sign) + res = -res; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static void +init_Variable (Limmat * limmat, Variable * v, int id) +{ + int i; + + v->id = id; + v->decision_level = -1; + + for (i = 0; i < 2; i++) + { + v->score[i] = 0; + v->ref[i] = 0; + v->saved[i] = 0; + init_Stack (limmat, &v->watched[i]); + v->pos[i] = 0; + } + + v->assignment = v; + v->reason = 0; + + v->pos_on_queue = -1; + v->sign_on_queue = 0; + + v->sign_in_clause = 0; + v->mark = 0; +} + +/*------------------------------------------------------------------------*/ +#ifndef NDEBUG +/*------------------------------------------------------------------------*/ + +inline static int +get_pos (Variable * v) +{ + int sign, res; + + sign = is_signed (v); + if (sign) + v = not (v); + res = v->pos[sign]; + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +inline static void +set_pos (Variable * v, int pos) +{ + int sign; + + sign = is_signed (v); + if (sign) + v = not (v); + v->pos[sign] = pos; +} + +/*------------------------------------------------------------------------*/ + +inline static void +insert_order (Limmat * limmat, Variable * v) +{ + /* Since we assume that an unsigned variables is smaller than the same + * signed variable and the larger variables should occur before smaller in + * the order, we put 'not(v)' before 'v' in the order. + */ + assert (cmp (0, v, not (v)) < 0); + + set_pos (not (v), count_Stack (&limmat->order)); + push (limmat, &limmat->order, not (v)); + + set_pos (v, count_Stack (&limmat->order)); + push (limmat, &limmat->order, v); + + /* Otherwise we have to update 'limmat->first_zero_pos'. + */ + assert (!v->score[0]); + assert (!v->score[1]); +} + +/*------------------------------------------------------------------------*/ + +inline static Variable * +find (Limmat * l, int id) +{ + int sign, fresh; + Variable *res; + size_t delta; + + assert (id); + + sign = (id < 0); + if (sign) + id = -id; + + res = access_Arena (l, &l->variables, id, sizeof (Variable), &delta); + fresh = !res->id; + + if (fresh) + { + init_Variable (l, res, id); + if (delta) + fix_pointer (&res->assignment, (size_t)-delta); + l->num_variables++; + if (l->max_id < id) + l->max_id = id; + } + + if (delta) + fix_pointers_to_variables (l, delta); + if (fresh) + insert_order (l, res); + if (sign) + res = not (res); + + assert (is_aligned_ptr (strip (res), VARIABLE_ALIGNMENT)); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static Stack * +var2stack (Variable * v) +{ + Stack *res; + int sign; + + if ((sign = is_signed (v))) + v = not (v); + res = &v->watched[sign]; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int * +clause2watched (Clause * c) +{ + int *res, sign; + + sign = is_signed (c); + if (sign) + c = not (c); + + res = &c->watched[sign]; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static void +connect (Limmat * limmat, Clause * clause, int l) +{ + Variable *v, **literals; + Occurence occurrence; + Clause *stripped; + int vs; + + /* Get the corresponding variable and its sign at position 'l' in 'clause'. + */ + int *watched; + + stripped = strip (clause); + + assert (stripped->size > l); + literals = clause2literals (limmat, stripped); + v = lit2var (literals[l]); + if ((vs = is_signed (v))) + v = not (v); + + /* Mark this literal as watched in the clause. + */ + watched = clause2watched (clause); + assert (*watched < 0); /* is inwatched */ + *watched = l; + occurrence = clause; + + /* Finally enqueue this occurence to the variable. + */ + push (limmat, &v->watched[vs], occurrence); + +#ifdef LOG_CONNECT + fprintf (LOGFILE (limmat), + "CONNECT\t%d\t%u\n", + var2int (lit2var (literals[l])), count_Stack (&v->watched[vs])); +#endif +} + +/*------------------------------------------------------------------------*/ + +static void +partial_disconnect (Limmat * limmat, Clause * clause, int l) +{ + Variable **literals; + Clause *stripped; + int *watched; + + /* Mark the literal as watched in the clause. + */ + watched = clause2watched (clause); + assert (*watched == l); + stripped = strip (clause); + assert (stripped->size > l); + literals = clause2literals (limmat, stripped); + *watched = -1; +} + +/*------------------------------------------------------------------------*/ +#if defined(CHECK_CONSISTENCY) && defined(EXPENSIVE_CHECKS) && !defined(NDEBUG) +/*------------------------------------------------------------------------*/ + +static int +is_connected (Variable * v, Clause * clause) +{ + Clause **p, **end; + int res; + + res = 0; + + forall_Stack (var2stack (v), Clause *, p, end) if ((res = (*p == clause))) + break; + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +static void +invariant_clause (Limmat * limmat _U_, Clause * clause _U_) +{ +#ifdef CHECK_CONSISTENCY + Variable *v, **literals, *tmp, *l[2], *d[2], *s[2]; + int i, num_non_false, p[2]; + + assert (clause->size >= 1); + + if (!check_it_now (limmat)) + return; + + p[0] = clause->watched[0]; + p[1] = clause->watched[1]; + + literals = clause2literals (limmat, clause); + + if (clause->size > 1) + { + assert (p[0] >= 0); + assert (p[1] >= 0); + assert (p[0] < clause->size); + assert (p[1] < clause->size); + assert (p[0] != p[1]); + + num_non_false = 0; + for (i = 0; i < clause->size; i++) + { + v = lit2var (literals[i]); + tmp = deref (v); + if (tmp != FALSE) + num_non_false++; + } + + l[0] = lit2var (literals[p[0]]); + l[1] = lit2var (literals[p[1]]); + d[0] = deref (l[0]); + d[1] = deref (l[1]); + s[0] = strip (l[0]); + s[1] = strip (l[1]); + + if (num_non_false >= 2) + { + if (d[0] == FALSE) + { + assert (d[1] == TRUE); + assert (s[0]->decision_level >= s[1]->decision_level); + } + + if (d[1] == FALSE) + { + assert (d[0] == TRUE); + assert (s[1]->decision_level >= s[0]->decision_level); + } + +#ifdef EXPENSIVE_CHECKS + assert (is_connected (l[0], clause)); + assert (is_connected (l[1], not (clause))); +#endif + } + else if (num_non_false == 1) + { +#ifdef EXPENSIVE_CHECKS + assert (is_connected (l[0], clause)); +#endif + + assert ((d[0] == FALSE) + (d[1] == FALSE) == 1); + } + + for (i = 0; i < clause->size; i++) + { + v = strip (lit2var (literals[i])); + + if (i != p[0] && i != p[1]) + { + if (d[0] == FALSE && d[1] != TRUE) + assert (v->decision_level <= s[0]->decision_level); + + if (d[1] == FALSE && d[0] != TRUE) + assert (v->decision_level <= s[1]->decision_level); + } + } + } + else + { + assert (p[0] == 0); + assert (p[1] == -1); + } +#endif +} + +/*------------------------------------------------------------------------*/ + +static void +invariant (Limmat * limmat _U_) +{ +#ifdef EXPENSIVE_CHECKS + Variable *v, *eov, *u, **order; + Clause **p, **eoc, *clause; + int i, score, *watched; + + + if (!check_it_now (limmat)) + return; + + assert (limmat->current_max_score <= limmat->max_score); + + assert (limmat->num_assigned <= limmat->num_variables); + + forall_clauses (limmat, p, eoc) invariant_clause (limmat, *p); + + order = start_of_Stack (&limmat->order); + + forall_variables (limmat, v, eov) + { + for (i = 0; i < 2; i++) + { + u = (i ? not (v) : v); + + assert (order[get_pos (u)] == u); + + if (!is_assigned (u)) + assert (limmat->last_assigned_pos < get_pos (u)); + + score = get_score (u); + assert (score >= 0); + if (score) + assert (limmat->first_zero_pos > get_pos (u)); + + forall_Stack (&v->watched[i], Clause *, p, eoc) + { + watched = clause2watched (*p); + clause = strip (*p); + assert (lit2var (clause2literals (limmat, clause)[*watched]) == u); + } + } + } +#endif +} + +/*------------------------------------------------------------------------*/ +#if defined(EXPENSIVE_CHECKS) && !defined(NDEBUG) +/*------------------------------------------------------------------------*/ + +static int +is_unique_clause (Limmat * limmat, Clause * clause) +{ + Variable *u, *v; + int i, j, res; + + for (i = 0, res = 1; res && i < clause->size - 1; i++) + { + u = strip (lit2var (clause2literals (limmat, clause)[i])); + for (j = i + 1; res && j < clause->size; j++) + { + v = strip (lit2var (clause2literals (limmat, clause)[j])); + res = (u->id != v->id); + } + } + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Add a new clause to the clause data base. The pointers to the two + * watched literals in the clause have are set as well. In case + * 'conflict_driven_assignment' is non-zero generate a conflict driven + * assignment driven by this clause. + */ +static Clause * +add_clause (Limmat * limmat, + Variable ** variables, + int n, Assignment * conflict_driven_assignment) +{ + int i, watched[2], max[2], tmp, found_non_false[2], level; + Variable *v, *stripped_literal; + Statistics *stats; + Clause *clause; + + assert (n > 0); + + /* In the first part we just adjust the statistics. + */ + limmat->added_clauses++; + limmat->num_clauses++; + + stats = limmat->stats; + + if (stats) + { + if (stats->max_clauses < limmat->num_clauses) + stats->max_clauses = limmat->num_clauses; + } + + limmat->added_literals += n; + limmat->num_literals += n; + + if (stats) + { + if (stats->max_literals < limmat->num_literals) + stats->max_literals = limmat->num_literals; + } + + /* Then we allocate the clause and initialize some of its components. + */ + clause = (Clause *) new (limmat, sizeof (Clause)); + clause->id = count_Stack (&limmat->clauses); + push (limmat, &limmat->clauses, clause); + clause->learned = 0; + clause->size = n; + + clause->watched[0] = -1; + clause->watched[1] = -1; +#ifdef OPTIMIZE_DIRECTION + clause->direction = 1; +#endif + + clause->literals_idx = count_Stack (&limmat->literals); + + /* Push first literal of clause onto literals stack. + */ + v = variables[0]; + push (limmat, &limmat->literals, v); + + /* Push inner literals. + */ + for (i = 1; i < n - 1; i++) + { + v = variables[i]; + push (limmat, &limmat->literals, v); + } + + /* Push last literal. + */ + if (n > 1) + { + v = variables[n - 1]; + push (limmat, &limmat->literals, v); + } + + /* Finally we have to find two literals that are assigned at the largest + * decision level or are still unassigned. We start with the first + * literal. + */ + found_non_false[0] = 0; + watched[0] = -1; + max[0] = -2; /* unassigned decision_level is '-1' */ + + for (i = 0; !found_non_false[0] && i < n; i++) + { + v = variables[i]; + + if (deref (v) == FALSE) + { + tmp = ((Variable *) strip (v))->decision_level; + if (tmp > max[0]) + { + watched[0] = i; + max[0] = tmp; + } + } + else + { + found_non_false[0] = 1; + watched[0] = i; + } + } + + /* Connect the first pointer to the largest assigned or still unassigned + * literal. + */ + assert (watched[0] >= 0); + connect (limmat, clause, watched[0]); + + /* This previously choosen literal will necessarily be also the conflict + * driven assignment in case we want to generate one. + */ + if (conflict_driven_assignment) + { + conflict_driven_assignment->literal = variables[watched[0]]; + conflict_driven_assignment->reason = clause; + conflict_driven_assignment->decision_level = -1; + } + + /* The decision level of the conflict driven assignment still need to be + * calculated as the maximal level of all assigned variables beside the + * first found literal. + */ + level = -1; + + if (n > 1) + { + watched[1] = -1; + found_non_false[1] = 0; + max[1] = -2; /* unassigned decision_level is '-1' */ + + for (i = 0; !found_non_false[1] && i < n; i++) + { + if (i != watched[0]) /* skip the first watched literal */ + { + v = variables[i]; + + if (deref (v) == FALSE) + { + tmp = ((Variable *) strip (v))->decision_level; + if (tmp > max[1]) + { + watched[1] = i; + max[1] = tmp; + } + } + else + { + found_non_false[1] = 1; + watched[1] = i; + } + } + } + + /* Connect the second watched literal. + */ + assert (watched[1] >= 0); + connect (limmat, not (clause), watched[1]); + + if (conflict_driven_assignment) + { + /* The level of the conflict driven assignment is actually + * determined by the decision level of the second literal. + */ + assert (max[1] >= -1); + level = max[1]; + } + } + else + { + push (limmat, &limmat->units, clause); + +#ifdef LOG_UNIT + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "UNIT\t%d\n", var2int (variables[0])); +#endif + } + + if (conflict_driven_assignment) + { + conflict_driven_assignment->decision_level = level; + + if (stats && n > 1) + { + stripped_literal = strip (conflict_driven_assignment->literal); + + for (i = 0; i < n; i++) + { + v = strip (variables[i]); + + if (v != stripped_literal) + { + assert (v->decision_level <= level); + } + } + } + } + + for (i = 0; i < n; i++) + inc_ref (limmat, variables[i]); + + invariant_clause (limmat, clause); + +#ifdef EXPENSIVE_CHECKS + if (check_it_now (limmat)) + assert (is_unique_clause (limmat, clause)); +#endif + + return clause; +} + +/*------------------------------------------------------------------------*/ + +static void +print_clause (FILE * file, Limmat * limmat, Clause * clause) +{ + int i; + +#ifndef NDEBUG + if (!file) + file = stdout; +#endif + + for (i = 0; i < clause->size; i++) + fprintf (file, "%d ", + var2int (lit2var (clause2literals (limmat, clause)[i]))); + + fprintf (file, "0\n"); +} + +/*------------------------------------------------------------------------*/ + +static int +real_max_id (Limmat * limmat) +{ + Clause **eoc, **p, *clause; + int res, i, num_literals; + Variable *v; + + res = 0; + + forall_clauses (limmat, p, eoc) + { + clause = *p; + num_literals = clause->size; + + for (i = 0; i < num_literals; i++) + { + v = strip (lit2var (clause2literals (limmat, clause)[i])); + if (v->id > res) + res = v->id; + } + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +void +print_Limmat (Limmat * limmat, FILE * file) +{ + Clause **p, **eoc; + double delta; + + start_timer (&delta); + + if (!file) + file = stdout; + + if (limmat->error) + { + fprintf (file, "c %s\n", limmat->error); + } + else if (limmat->contains_empty_clause) + { + fprintf (file, "p cnf 0 1\n0\n"); + } + else + { + fprintf (file, "p cnf %d %d\n", + real_max_id (limmat), count_Stack (&limmat->clauses)); + + forall_clauses (limmat, p, eoc) print_clause (file, limmat, *p); + } + + limmat->time += stop_timer (delta); +} + +/*------------------------------------------------------------------------*/ +#if !defined(NDEBUG) || defined(LOG_SOMETHING) +/*------------------------------------------------------------------------*/ + +void +dump_clause_aux (FILE * file, + Limmat * limmat, + Clause * clause, + Variable * exception, + int negate_literals, + int print_level, int print_assignment, int print_connection) +{ + Variable *v, *tmp, *stripped, **literals, *l; + int i; + + if (!file) + file = stdout; + + if (clause) + { + literals = clause2literals (limmat, clause); + + for (i = 0; i < clause->size; i++) + { + l = literals[i]; + v = lit2var (l); + + if (v != exception) + { + if (negate_literals) + v = not (v); + + stripped = strip (v); + + if (print_connection) + { + if (clause->watched[0] == i || clause->watched[1] == i) + fputc ('>', file); + } + + fprintf (file, "%d", var2int (v)); + + if (print_level) + fprintf (file, "@%d", stripped->decision_level); + + if (print_assignment && is_assigned (v)) + { + tmp = deref (v); + fputs (tmp == FALSE ? "=0" : "=1", file); + } + + if (i < clause->size - 1) + fputc (' ', file); + } + } + } + + fputc ('\n', file); +} + +/*------------------------------------------------------------------------*/ + +void +dump_clause (Limmat * limmat, Clause * clause) +{ + dump_clause_aux (stdout, limmat, clause, 0, 0, 1, 1, 1); +} + +/*------------------------------------------------------------------------*/ + +void +dump (Limmat * limmat) +{ + Clause **p, **eoc; + + forall_clauses (limmat, p, eoc) dump_clause (limmat, *p); +} + +/*------------------------------------------------------------------------*/ + +static void +dump_frame (Frame * frame) +{ + int id; + + id = var2int (frame->decision); + printf ("decision level %d: %d\n", frame->decision_level, id); +} + +/*------------------------------------------------------------------------*/ + +void +dump_control (Limmat * limmat) +{ + Frame *frame; + int i; + + for (i = 0; i <= limmat->decision_level; i++) + { + frame = limmat->control + i; + dump_frame (frame); + } +} + +/*------------------------------------------------------------------------*/ + +#define ASSIGNED_MSG "------------------ assigned variables\n" +#define ZERO_MSG "------------------ zero score variables\n" + +/*------------------------------------------------------------------------*/ + +void +dump_order (Limmat * limmat) +{ + Variable **eoo, **p; + int i; + + i = 0; + + forall_Stack (&limmat->order, Variable *, p, eoo) + { + if (i - 1 == limmat->last_assigned_pos) + printf (ASSIGNED_MSG); + + printf ("%d %d %d\n", i++, var2int (*p), get_score (*p)); + + if (i == limmat->first_zero_pos) + printf (ZERO_MSG); + } +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Find number of unique literals and rearrange 'literals' to have the + * unique literals at the beginning of the array. In case a literal and its + * negation are found the result is negative to denote that the clause is + * trivial . + */ +static int +unique_literals (Variable ** literals, int n) +{ + Variable *u, *stripped; + int i, res, sign; + + for (i = 0, res = 0; res >= 0 && i < n; i++) + { + assert (res <= i); + + u = literals[i]; + sign = is_signed (u); + stripped = sign ? not (u) : u; + + if (stripped->mark) + { + /* The variable 'stripped' occurs again in the clause. If it + * occured with the opposite sign, the clause is trivial and '-1' + * is returned. Otherwise we can skip the second occurence. + */ + if (!sign != !stripped->sign_in_clause) + res = -1; + } + else + { + literals[res++] = u; + stripped->sign_in_clause = sign ? 1 : 0; + stripped->mark = 1; + } + } + + while (i > 0) + { + stripped = strip (literals[--i]); + stripped->sign_in_clause = 0; + stripped->mark = 0; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +void +add_Limmat (Limmat * limmat, const int *ivec) +{ + int i, n, max, tmp, old_literals_count; + Variable **vvec, *v; + + assert (ivec); + + old_literals_count = count_Stack (&limmat->clause); + + /* First find the the maximal id of a variable int the new clause. + */ + for (n = 0, max = 0; ivec[n]; n++) + { + tmp = ivec[n]; + if (tmp < 0) + tmp = -tmp; + if (tmp > max) + max = tmp; + } + + if (n) + { + /* Then access the variable with the largest index first, such that + * further access to variables in this clause do not require resizing + * the variables arena, which would result in invalidating the + * previously generated variable pointers. + */ + assert (max > 0); + (void) find (limmat, max); + + /* Now we can savely generate variable pointers in turn, since the + * variable arena should already be large enough to hold all variables + * of this clause and will not move. + */ + for (i = 0; i < n; i++) + { + v = find (limmat, ivec[i]); + push (limmat, &limmat->clause, v); + } + + vvec = (Variable **) start_of_Stack (&limmat->clause); + vvec += old_literals_count; + n = unique_literals (vvec, n); + assert (n != 0); + + if (n > 0) + add_clause (limmat, vvec, n, 0); + } + else + { + reset_Limmat (limmat); + limmat->contains_empty_clause = 1; + } + + reset_Stack (limmat, &limmat->clause, old_literals_count); +} + +/*------------------------------------------------------------------------*/ + +int +read_Limmat (Limmat * limmat, FILE * file, const char *name) +{ + int res, n, num_literals, num_clauses; + Parser *parser; + + start_timer (&limmat->timer); + parser = new_Parser (limmat, file, name); + + num_clauses = 0; + num_literals = 0; + + while (read_clause (parser) && !limmat->contains_empty_clause) + { + n = count_Stack (&parser->literals); + num_clauses++; + num_literals += n; + push (limmat, &parser->literals, (void *) (int) 0); + add_Limmat (limmat, intify_Stack (&parser->literals)); + } + + if (!parser->error && + !limmat->contains_empty_clause && parser->num_specified_clauses >= 0) + { + assert (parser->num_specified_max_id >= 0); + + if (parser->num_specified_clauses != num_clauses) + { + parse_error (parser, + "number of specified clauses does not match", 0); + } + else if (parser->num_specified_max_id < limmat->max_id) + { + parse_error (parser, "specified maximal variable exceeded", 0); + } + } + + if (parser->error) + { + reset_Limmat (limmat); + limmat->error = (char *) new (limmat, strlen (parser->error) + 1); + strcpy (limmat->error, parser->error); + res = 0; + } + else + { + if (limmat->stats) + { + limmat->stats->original_clauses += num_clauses; + limmat->stats->original_literals += num_literals; + } + + res = 1; + } + + delete_Parser (parser); + invariant (limmat); + limmat->time += stop_timer (limmat->timer); + + return res; +} + +/*------------------------------------------------------------------------*/ + +const char * +error_Limmat (Limmat * limmat) +{ + return limmat->error; +} + +/*------------------------------------------------------------------------*/ + +int +maxvar_Limmat (Limmat * limmat) +{ + return limmat->max_id; +} + +/*------------------------------------------------------------------------*/ + +int +literals_Limmat (Limmat * limmat) +{ + return limmat->num_literals; +} + +/*------------------------------------------------------------------------*/ + +int +clauses_Limmat (Limmat * limmat) +{ + return limmat->num_clauses; +} + +/*------------------------------------------------------------------------*/ + +double +time_Limmat (Limmat * limmat) +{ + return limmat->time; +} + +/*------------------------------------------------------------------------*/ + +size_t +bytes_Limmat (Limmat * limmat) +{ + return limmat->bytes; +} + +/*------------------------------------------------------------------------*/ + +static void +stats_performance (const char *description, + double absolute_value, double time, FILE * file) +{ + double performance; + + if (time) + performance = absolute_value / time; + else + performance = 0; + + fprintf (file, + LIMMAT_PREFIX + "%.0f %s (%.0f/sec)\n", absolute_value, description, performance); +} + +/*------------------------------------------------------------------------*/ + +void +stats_Limmat (Limmat * limmat, FILE * file) +{ + double avg_num, avg_original, avg_learned, avg_max, avg_added, avg_removed; + double avg_rescored_variables, avg_assigned_in_decision; + double bytes, H, M, S, MB, KB; + double avg_score_in_decision; + Statistics *stats; + int round; + + start_timer (&limmat->timer); + + stats = limmat->stats; + + S = limmat->time; + H = S / 3600; + round = H; + H = round; + M = (S - 3600 * H) / 60; + round = M; + M = round; + S = S - 60 * M; + + fprintf (file, + LIMMAT_PREFIX + "%.2f seconds in library (%.0f:%02.0f:%05.2f)\n", + limmat->time, H, M, S); + + bytes = limmat->max_bytes + sizeof (Limmat); + + fprintf (file, LIMMAT_PREFIX "%.0f bytes memory usage", bytes); + + KB = 1024; + MB = KB * KB; + + if (bytes >= KB / 10) + { + if (bytes >= MB / 10) + fprintf (file, " (%.1f MB)", bytes / MB); + else + fprintf (file, " (%.1f KB)", bytes / KB); + } + + fputc ('\n', file); + + if (!limmat->num_clauses) + avg_num = 0; + else + avg_num = limmat->num_literals / (double) limmat->num_clauses; + + if (stats) + { + fputs (LIMMAT_PREFIX "\n", file); + + stats_performance ("conflicts", limmat->num_conflicts, limmat->time, + file); + stats_performance ("decisions", limmat->num_decisions, limmat->time, + file); + stats_performance ("assignments", stats->assignments, limmat->time, + file); + stats_performance ("propagations", stats->propagations, limmat->time, + file); + stats_performance ("visits", stats->visits, limmat->time, file); + stats_performance ("compared", stats->compared, limmat->time, file); + stats_performance ("swapped", stats->swapped, limmat->time, file); + stats_performance ("searched", stats->searched, limmat->time, file); + + fputs (LIMMAT_PREFIX "\n", file); + + fprintf (file, + LIMMAT_PREFIX + "%.0f restarts, %.0f rescores\n", + limmat->restart.finished, limmat->rescore.finished); + + fprintf (file, + LIMMAT_PREFIX "%.0f uips, %.0f backjumps\n", + stats->uips, stats->backjumps); + + fputs (LIMMAT_PREFIX "\n", file); + + if (limmat->rescore.finished) + { + avg_rescored_variables = + stats->rescored_variables / limmat->rescore.finished; + } + else + avg_rescored_variables = 0; + + if (limmat->num_decisions) + { + avg_assigned_in_decision = + stats->sum_assigned_in_decision / limmat->num_decisions; + + avg_score_in_decision = + stats->sum_score_in_decision / limmat->num_decisions; + } + else + avg_score_in_decision = avg_assigned_in_decision = 0; + + fprintf (file, + LIMMAT_PREFIX + "average %.0f assigned variables per decision\n" + LIMMAT_PREFIX + "average %.1f variables rescored per decision\n" + LIMMAT_PREFIX + "average %.1f maximal score per decision\n" + LIMMAT_PREFIX + "maximal %d score\n", + avg_assigned_in_decision, + avg_rescored_variables, + avg_score_in_decision, limmat->max_score); + + fprintf (file, + LIMMAT_PREFIX + "\n" + LIMMAT_PREFIX + "%d clauses\n" + LIMMAT_PREFIX + "(%d orig, %.0f learned, %d max +%.0f -%.0f)\n", + limmat->num_clauses, + stats->original_clauses, + stats->learned_clauses, + stats->max_clauses, + limmat->added_clauses, stats->removed_clauses); + + fprintf (file, + LIMMAT_PREFIX + "\n" + LIMMAT_PREFIX + "%d literals\n" + LIMMAT_PREFIX + "(%d orig, %.0f learned, %d max +%.0f -%.0f)\n", + limmat->num_literals, + stats->original_literals, + stats->learned_literals, + stats->max_literals, + limmat->added_literals, stats->removed_literals); + + if (!stats->original_clauses) + avg_original = 0; + else + avg_original = + stats->original_literals / (double) stats->original_clauses; + + if (!stats->learned_clauses) + avg_learned = 0; + else + avg_learned = + stats->learned_literals / (double) stats->learned_clauses; + + if (!stats->max_clauses) + avg_max = 0; + else + avg_max = stats->max_literals / (double) stats->max_clauses; + + if (!limmat->added_clauses) + avg_added = 0; + else + avg_added = limmat->added_literals / (double) limmat->added_clauses; + + if (!stats->removed_clauses) + avg_removed = 0; + else + avg_removed = + stats->removed_literals / (double) stats->removed_clauses; + + fprintf (file, + LIMMAT_PREFIX + "\n" + LIMMAT_PREFIX + "%.1f literals/clause\n" + LIMMAT_PREFIX + "(%.1f orig, %.1f learned, %.1f max +%.1f -%.1f)\n", + avg_num, + avg_original, avg_learned, avg_max, avg_added, avg_removed); + } + else + { + fprintf (file, + LIMMAT_PREFIX + "%d literals, %d clauses, %.1f literals/clause\n", + limmat->num_literals, limmat->num_clauses, avg_num); + } + + if (stats) + fprintf (file, LIMMAT_PREFIX "\n"); + + fprintf (file, + LIMMAT_PREFIX + "%d variables with %d as maximal variable identifier\n", + limmat->num_variables, limmat->max_id); + + limmat->time += stop_timer (limmat->timer); +} + +/*------------------------------------------------------------------------*/ + +void +strategy_Limmat (Limmat * limmat, FILE * file) +{ + start_timer (&limmat->timer); + + if (!file) + file = stdout; + + fputs (LIMMAT_PREFIX +#ifdef NDEBUG + "-DEBUG " +#else + "+DEBUG " +#endif +#ifdef CHECK_CONSISTENCY + "+CHECK_CONSISTENCY " +#else + "-CHECK_CONSISTENCY " +#endif +#ifdef EXPENSIVE_CHECKS + "+EXPENSIVE_CHECKS" +#else + "-EXPENSIVE_CHECKS" +#endif + "\n", file); + + fputs (LIMMAT_PREFIX +#ifdef OPTIMIZE_DIRECTION + "+OPTIMIZE_DIRECTION " +#else + "-OPTIMIZE_DIRECTION " +#endif +#ifdef COMPACT_STACK + "+COMPACT_STACK" +#else + "-COMPACT_STACK" +#endif + "\n", file); + + fputs (LIMMAT_PREFIX +#ifdef EARLY_CONFLICT_DETECTION + "+EARLY_CONFLICT_DETECTION " +#else + "-EARLY_CONFLICT_DETECTION " +#endif +#ifdef SHORTEN_REASONS + "+SHORTEN_REASONS" +#else + "-SHORTEN_REASONS" +#endif + "\n", file); + + fputs (LIMMAT_PREFIX +#ifdef LOOK_AT_OTHER_WATCHED_LITERAL + "+LOOK_AT_OTHER_WATCHED_LITERAL" +#else + "-LOOK_AT_OTHER_WATCHED_LITERAL" +#endif + "\n", file); + + fprintf (file, + LIMMAT_PREFIX + "RESTART=%d " + "RESCORE=%d " + "RESCOREFACTOR=%f\n", + limmat->restart.init, limmat->rescore.init,limmat->score_factor); + + limmat->time += stop_timer (limmat->timer); +} + +/*------------------------------------------------------------------------*/ + +const char * +options_Limmat (void) +{ + return +#ifdef COMPACT_STACK + "1" +#else + "0" +#endif +#ifdef OPTIMIZE_DIRECTION + "1" +#else + "0" +#endif +#ifdef EARLY_CONFLICT_DETECTION + "1" +#else + "0" +#endif +#ifdef SHORTEN_REASONS + "1" +#else + "0" +#endif +#ifdef LOOK_AT_OTHER_WATCHED_LITERAL + "1" +#else + "0" +#endif + ; +} + +/*------------------------------------------------------------------------*/ +/* Push a new frame on the control stack. The stack is not modelled with an + * arena, since frames are of fixed size and do not need alignment. + */ +static void +push_frame (Limmat * limmat, Variable * assignment) +{ + int old_bytes, new_bytes; + Frame *frame; + + if (++limmat->decision_level >= limmat->control_size) + { + old_bytes = limmat->control_size * sizeof (Frame); + limmat->control_size *= 2; + new_bytes = limmat->control_size * sizeof (Frame); + + limmat->control = + (Frame *) resize (limmat, limmat->control, new_bytes, old_bytes); + } + + frame = limmat->control + limmat->decision_level; + frame->decision = assignment; + frame->decision_level = limmat->decision_level; + frame->trail_level = count_Stack (&limmat->trail); +} + +/*------------------------------------------------------------------------*/ +/* Actually perform an assignment. The 'assignment' field of the literal is + * overwritten, the reason and the decision level are updated. The + * assignment is recorded on the trail for later backtracking purposes. + */ +static void +assign (Limmat * limmat, Assignment * assignment) +{ + Variable *stripped, *literal; + int sign; + + if (limmat->stats) + limmat->stats->assignments++; + limmat->num_assigned++; + assert (limmat->num_assigned >= 0); + +#ifdef LOG_ASSIGNMENTS + if (!limmat->dont_log) + { + fprintf (LOGFILE (limmat), + "ASSIGN\t%d@%d", + var2int (assignment->literal), assignment->decision_level); + + if (assignment->reason && assignment->reason->size > 1) + { + fputs (" <= ", LOGFILE (limmat)); + + dump_clause_aux (LOGFILE (limmat), limmat, + assignment->reason, assignment->literal, 1, 1, 0, + 0); + } + else + fputc ('\n', LOGFILE (limmat)); + } +#endif + + literal = assignment->literal; + sign = is_signed (literal); + stripped = sign ? not (literal) : literal; + + stripped->assignment = (sign ? FALSE : TRUE); + stripped->decision_level = assignment->decision_level; + stripped->reason = assignment->reason; + + push (limmat, &limmat->trail, stripped); +} + +/*------------------------------------------------------------------------*/ + +static void +print_time_prefix (Limmat * limmat) +{ + assert (limmat->log); + + limmat->time += restart_timer (&limmat->timer); + fprintf (limmat->log, LIMMAT_PREFIX " %7.2f ", limmat->time); +} + +/*------------------------------------------------------------------------*/ + +static void +one_line_stats (Limmat * limmat) +{ + FILE *log; + Statistics *stats; + + stats = limmat->stats; + log = limmat->log; + + if (log) + { + if (limmat->report.finished == 1) + { + fprintf (log, LIMMAT_PREFIX "\n"); + if (stats) + fprintf (log, LIMMAT_PREFIX " "); + else + fprintf (log, LIMMAT_PREFIX " seconds "); + fprintf (log, "#decisions"); + + if (stats) + fprintf (log, + " #propagations\n" + LIMMAT_PREFIX + " seconds #assignments #visits"); + + fprintf (log, "\n" LIMMAT_PREFIX "\n"); + } + + print_time_prefix (limmat); + + fprintf (log, "%8.0f", limmat->num_decisions); + + if (stats) + { + fprintf (log, " %9.0f %10.0f %11.0f", + stats->assignments, stats->propagations, stats->visits); + } + + fputc ('\n', log); + fflush (log); + } +} + +/*------------------------------------------------------------------------*/ + +static Variable * +next_decision (Limmat * limmat) +{ + Variable *res, *tmp, **order; + Statistics *stats; + int pos, score; + + assert (limmat->num_assigned < limmat->num_variables); + + stats = limmat->stats; + pos = limmat->last_assigned_pos + 1; + order = (Variable **) start_of_Stack (&limmat->order); + + /* Find a still unassigned variable at 'pos' or above. + */ + res = 0; + while (pos < count_Stack (&limmat->order) && !res) + { + tmp = order[pos]; + if (is_assigned (tmp)) + { + pos++; + if (stats) + stats->searched++; + } + else + res = tmp; + } + + assert (res); + score = get_score (res); + limmat->current_max_score = score; + limmat->last_assigned_pos = pos - 1; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static void +swap (Limmat * limmat, Variable ** a, Variable ** b) +{ + Variable *tmp; + + if (limmat && limmat->stats) + limmat->stats->swapped++; + + tmp = *a; + *a = *b; + *b = tmp; +} + +/*------------------------------------------------------------------------*/ + +inline static void +cmpswap (Limmat * limmat, Variable ** a, Variable ** b) +{ + if (cmp (limmat, *a, *b) < 0) + swap (limmat, a, b); +} + +/*------------------------------------------------------------------------*/ + +inline static int +partition (Limmat * limmat, Variable ** a, int l, int r) +{ + Variable *v; + int i, j; + + i = l - 1; + j = r; + v = a[r]; + + for (;;) + { + while (cmp (limmat, a[++i], v) > 0) + ; + + while (cmp (limmat, v, a[--j]) > 0) + if (j == l) + break; + + if (i >= j) + break; + + swap (limmat, a + i, a + j); + } + + swap (limmat, a + i, a + r); + + return i; +} + +/*------------------------------------------------------------------------*/ + +inline static void +insertion (Limmat * limmat, Variable ** a, int l, int r) +{ + Variable *v; + int i, j; + + for (i = r; i > l; i--) + cmpswap (limmat, a + i - 1, a + i); + + for (i = l + 2; i <= r; i++) + { + j = i; + v = a[i]; + while (cmp (limmat, v, a[j - 1]) > 0) + { + a[j] = a[j - 1]; + j--; + } + a[j] = v; + } +} + +/*------------------------------------------------------------------------*/ + +#define ISORT_LIMIT 10 + +/*------------------------------------------------------------------------*/ + +inline static void +quicksort (Limmat * limmat, Variable ** a, int l, int r) +{ + int i, m, l_to_push, r_to_push; + Stack *stack; + +#if 1 + static int isort_limit = -1; + if (isort_limit < 0) + { + if (getenv ("ISORT")) + isort_limit = atoi (getenv ("ISORT")); + if (isort_limit < 0) + isort_limit = ISORT_LIMIT; + } +#undef ISORT_LIMIT +#define ISORT_LIMIT isort_limit +#endif + + assert (ISORT_LIMIT >= 3); + if (r - l <= ISORT_LIMIT) + return; + + stack = &limmat->stack; + reset_Stack (limmat, stack, 0); + + for (;;) + { +#if 0 + fprintf (stdout, "%d\n", r - l); +#endif + m = (l + r) / 2; + swap (limmat, a + m, a + r - 1); + cmpswap (limmat, a + l, a + r - 1); + cmpswap (limmat, a + l, a + r); + cmpswap (limmat, a + r - 1, a + r); + i = partition (limmat, a, l + 1, r - 1); + + if (i - l < r - i) + { + l_to_push = i + 1; + r_to_push = r; + r = i - 1; + } + else + { + l_to_push = l; + r_to_push = i - 1; + l = i + 1; + } + + if (r - l > ISORT_LIMIT) + { + assert (r_to_push - l_to_push > ISORT_LIMIT); + push (limmat, stack, (void *) (PTR_SIZED_WORD) l_to_push); + push (limmat, stack, (void *) (PTR_SIZED_WORD) r_to_push); + } + else if (r_to_push - l_to_push > ISORT_LIMIT) + { + l = l_to_push; + r = r_to_push; + } + else if (count_Stack (stack)) + { + r = (int) (PTR_SIZED_WORD) pop (stack); + l = (int) (PTR_SIZED_WORD) pop (stack); + } + else + break; + } +} + +/*------------------------------------------------------------------------*/ +/* This is the hyper sorting mechanism from the Sedgewick book. + */ +static void +hypersort (Limmat * limmat, Variable ** a, int l, int r) +{ + quicksort (limmat, a, l, r); + insertion (limmat, a, l, r); +} + +/*------------------------------------------------------------------------*/ + +static void +sort_order_aux (Limmat * limmat) +{ + Variable **base; + int end; + + base = start_of_Stack (&limmat->order); + end = limmat->first_zero_pos - 1; + hypersort (limmat, base, 0, end); +} + +/*------------------------------------------------------------------------*/ + +static void +adjust_search_interval (Limmat * limmat) +{ + int i, end, last_non_zero_pos, first_unassigned_pos; + Variable **variables, *v; + + variables = start_of_Stack (&limmat->order); + end = limmat->first_zero_pos - 1; + last_non_zero_pos = -1; + first_unassigned_pos = end + 1; + + for (i = 0; i <= end; i++) + { + v = variables[i]; + if (first_unassigned_pos > end && !is_assigned (v)) + first_unassigned_pos = i; + if (get_score (v)) + last_non_zero_pos = i; + set_pos (v, i); + } + + assert (last_non_zero_pos < limmat->first_zero_pos); + limmat->first_zero_pos = last_non_zero_pos + 1; + limmat->last_assigned_pos = first_unassigned_pos - 1; +} + +/*------------------------------------------------------------------------*/ +#if !defined(NDEBUG) || defined(LIMMAT_WHITE) +/*------------------------------------------------------------------------*/ + +static int +is_sorted (Limmat * limmat) +{ + Variable **order; + int i, end, res; + + order = start_of_Stack (&limmat->order); + end = limmat->first_zero_pos - 1; + + for (i = 0, res = 1; res && i < end; i++) + res = (cmp (0, order[i], order[i + 1]) > 0); + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Sort the array between from the start until 'limmat->first_zero_pos' (the + * latter excluded). We would like to start the sorting at + * 'limmat->last_assigned_pos+1' but we have to take into account that + * backtracking may actually unassign some variables with large positive + * score. Therefore those variables have to be sorted as well. + */ +static void +sort_order (Limmat * limmat) +{ + if (count_Stack (&limmat->order)) + { + sort_order_aux (limmat); + adjust_search_interval (limmat); + assert (is_sorted (limmat)); + invariant (limmat); + } +} + +/*------------------------------------------------------------------------*/ +/* Initialize the score of a literal that is used for sorting by the number + * of its occurences in clauses. Also adjust 'first_zero_pos'. + */ +static void +init_score (Limmat * limmat) +{ + int ref, i, last_non_zero_pos, pos; + Variable *v, *end; + + last_non_zero_pos = -1; + forall_variables (limmat, v, end) + { + for (i = 0; i < 2; i++) + { + ref = v->ref[i]; + assert (ref >= 0); + v->saved[i] = ref; + v->score[i] = ref; + if (ref > limmat->current_max_score) + { + limmat->current_max_score = ref; + if (ref > limmat->max_score) + limmat->max_score = ref; + } + + pos = v->pos[i]; + if (ref > 0 && pos > last_non_zero_pos) + last_non_zero_pos = pos; + } + } + limmat->first_zero_pos = last_non_zero_pos + 1; +} + +/*------------------------------------------------------------------------*/ + +static void +init_order (Limmat * limmat) +{ + init_score (limmat); + sort_order (limmat); +} + +/*------------------------------------------------------------------------*/ +/* First divide the score of all variables by a certain amount and add the + * delta of new references since the last rescore. Then sort the variables + * with respect to the new calculated score. + */ +static void +rescore (Limmat * limmat) +{ + int sign, ref, score, delta_ref, new_score, pos, end; + int max_new_score, last_non_zero_pos; + Variable *v, **variables; + +#ifdef LOG_RESCORE + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "RESCORE\t%.0f\n", limmat->rescore.finished); +#endif + + last_non_zero_pos = 0; + end = limmat->first_zero_pos - 1; + variables = start_of_Stack (&limmat->order); + assert (variables); + + max_new_score = -1; + + for (pos = 0; pos <= end; pos++) + { + v = variables[pos]; + + assert (get_pos (v) == pos); + sign = is_signed (v); + if (sign) + v = not (v); + + ref = v->ref[sign]; + delta_ref = ref - v->saved[sign]; + v->saved[sign] = ref; + score = v->score[sign]; + + if (score || delta_ref) + { + assert (delta_ref >= 0); + assert (score >= 0); + + new_score = score * (double) limmat->score_factor; + + if (delta_ref > 0) + { + if (limmat->stats) + limmat->stats->rescored_variables++; + new_score += delta_ref; + } + + if (new_score) + { + if (pos > last_non_zero_pos) + last_non_zero_pos = pos; + } + + if (new_score > max_new_score) + max_new_score = new_score; + + assert (new_score >= 0); + v->score[sign] = new_score; + } + } + + limmat->current_max_score = max_new_score; + if (max_new_score > limmat->max_score) + limmat->max_score = max_new_score; + + limmat->first_zero_pos = last_non_zero_pos + 1; + sort_order (limmat); +} + +/*------------------------------------------------------------------------*/ +/* Derive assignments from all unit clauses. + */ +static void +units2mark (Limmat * limmat) +{ + Clause **p, **eoc, *clause; + Assignment assignment; + + assignment.reason = 0; + assignment.decision_level = -1; + + forall_Stack (&limmat->units, Clause *, p, eoc) + { + clause = *p; + assert (clause->size == 1); + assignment.literal = lit2var (clause2literals (limmat, clause)[0]); + push_assignment (limmat, &assignment); + } +} + +/*------------------------------------------------------------------------*/ + +static void +restart (Limmat * limmat) +{ + assert (limmat->decision_level >= 0); + +#ifdef LOG_RESTART + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "RESTART\t%.0f\n", limmat->restart.finished); +#endif + + untrail (limmat, -1); + limmat->decision_level = -1; + init_order (limmat); + units2mark (limmat); + invariant (limmat); +} + +/*------------------------------------------------------------------------*/ + +static int +its_time_to_rescore (Limmat * limmat) +{ + int res; + + dec_Counter (&limmat->rescore); + res = done_Counter (&limmat->rescore); + + return res; +} + +/*------------------------------------------------------------------------*/ +/* Search for a still unassigned decision literal and push it on the + * assignment queue. + */ +static void +decide (Limmat * limmat) +{ + Assignment assignment; + Variable *decision; + Statistics *stats; + int score; + + if (its_time_to_rescore (limmat)) + rescore (limmat); + + decision = next_decision (limmat); + assert (decision); + + stats = limmat->stats; + + if (stats) + { + stats->sum_assigned_in_decision += limmat->num_assigned; + score = get_score (decision); + assert (score == limmat->current_max_score); + stats->sum_score_in_decision += score; + } + + limmat->num_decisions++; + push_frame (limmat, decision); + + assignment.decision_level = limmat->decision_level; + assignment.literal = decision; + assignment.reason = 0; + push_assignment (limmat, &assignment); + + if (limmat->log) + { + dec_Counter (&limmat->report); + if (done_Counter (&limmat->report)) + one_line_stats (limmat); + } + +#ifdef LOG_DECISION + if (!limmat->dont_log) + { + fprintf (LOGFILE (limmat), + "DECIDE\t%d@%d\n", var2int (decision), limmat->decision_level); + } +#endif +} + +/*------------------------------------------------------------------------*/ +#ifdef EXPENSIVE_CHECKS +/*------------------------------------------------------------------------*/ + +static void +check_clause_is_implied (Limmat * limmat, Clause * new_clause) +{ +#if 0 +#warning "check_clause_is_implied disabled" +#else + Clause *clause, **p, **eoc; + int i, id, n, res; + Variable *v; + Limmat *tmp; + + static int sat (Limmat *, int); + + if (!check_it_now (limmat)) + return; + + tmp = new_Limmat (0); +#ifdef LOG_SOMETHING + tmp->dont_log = 1; /* avoid logging in call to 'sat(tmp,...)' below */ +#endif + tmp->inner_mode = 1; + init_Counter (&tmp->restart, 0, 0, 0); + init_Counter (&tmp->rescore, 0, 0, 0); + + /* Avoid moving 'tmp->variables.data_start'. + */ + (void) find (tmp, limmat->max_id); + + forall_clauses (limmat, p, eoc) + { + clause = *p; + n = clause->size; + + if (clause == new_clause) + { + for (i = 0; i < n; i++) + { + id = + var2int (not (lit2var (clause2literals (limmat, clause)[i]))); + v = find (tmp, id); + add_clause (tmp, &v, 1, 0); + } + } + else + { + assert (!count_Stack (&tmp->stack)); + + for (i = 0; i < n; i++) + { + id = var2int (lit2var (clause2literals (limmat, clause)[i])); + v = find (tmp, id); + push (tmp, &tmp->stack, v); + } + + add_clause (tmp, (Variable **) start_of_Stack (&tmp->stack), n, 0); + reset_Stack (limmat, &tmp->stack, 0); + } + } + + res = sat (tmp, 0); /* unit resolution should show unsatisfiability */ + assert (!res); + delete_Limmat (tmp); +#endif +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ +/* Add all literals on the 'literals' stack as a clause to the clause data + * base and generate a conflict driven assignment. + */ +static void +add_literals (Limmat * limmat, Assignment * assignment) +{ + Variable **literals; + Clause *clause; + int count; + + count = count_Stack (&limmat->clause); + assert (count); + + if (limmat->stats) + limmat->stats->learned_clauses++; + if (limmat->stats) + limmat->stats->learned_literals += count; + + literals = (Variable **) start_of_Stack (&limmat->clause); + clause = add_clause (limmat, literals, count, assignment); + clause->learned = 1; + reset_Stack (limmat, &limmat->clause, 0); + +#ifdef LOG_LEARNED + if (!limmat->dont_log) + { + fprintf (LOGFILE (limmat), "LEARN\t"); + dump_clause_aux (LOGFILE (limmat), limmat, clause, 0, 0, 1, 0, 0); + } +#endif + +#ifdef EXPENSIVE_CHECKS + check_clause_is_implied (limmat, clause); +#endif +} + +/*------------------------------------------------------------------------*/ +#ifdef EXPENSIVE_CHECKS +/*------------------------------------------------------------------------*/ + +static void +check_all_variables_unmarked (Limmat * limmat) +{ + Variable *v, *eov; + + forall_variables (limmat, v, eov) assert (!v->mark); +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +inline static void +push_literal (Limmat * limmat, Variable * v) +{ + Variable *new_literal; + + assert (!is_signed (v)); + assert (is_assigned (v)); + + new_literal = ((v->assignment == TRUE) ? not (v) : v); + push (limmat, &limmat->clause, new_literal); +} + +/*------------------------------------------------------------------------*/ +/* One step in the breadth first backward search through the dependency + * graph of the assignments on the current decision level consists of + * pushing all unvisited variables onto to the 'visited' stack and updating + * the number of open paths from the conflict backward to this variable. + */ +inline static void +expand_open_paths (Limmat * limmat, Clause * clause, int *paths) +{ + Variable *v, **p, **eol; + + forall_literals (limmat, clause, p, eol) + { + v = strip (lit2var (*p)); + + if (v->decision_level >= 0 && !v->mark) + { + v->mark = 1; + + /* Restrict the search to variables on the current decision level. + * The rest of the dependency graph is masked out. + */ + if (v->decision_level == limmat->decision_level) + { + /* This is the first time we visit this variable. So we have + * to increase the number of paths back from the conflict by + * one. + */ + *paths += 1; + } + else + { + /* All variables with lower decision level become part of the + * conflict clause. + */ + assert (v->decision_level < limmat->decision_level); + push_literal (limmat, v); + } + } + } +} + +/*------------------------------------------------------------------------*/ +/* Reset all the marked bits of the literals in the clause in case they have + * a smaller decision level as the current decision level. These variables + * should have been marked, when they are pushed on the literals stack for + * generating the conflict clause. + */ +static void +unmark_clause_after_conflict_generation (Limmat * limmat, Clause * clause) +{ + Variable **p, **eol, *v; + + forall_literals (limmat, clause, p, eol) + { + v = strip (lit2var (*p)); + assert (v->decision_level <= limmat->decision_level); + if (v->decision_level >= 0) + if (v->decision_level < limmat->decision_level) + v->mark = 0; + } +} + +/*------------------------------------------------------------------------*/ +/* Reset the 'mark' bits of all variables traversed and marked in + * 'expand_open_paths'. Make sure to unmark the literals in the 'reason' + * for a variable assignment as well. + */ +static void +unmark_after_conflict_generation (Limmat * limmat, Variable * v) +{ + Clause *reason; + + assert (v->decision_level == limmat->decision_level); + + if (v->mark) + { + v->mark = 0; + reason = v->reason; + if (reason) + unmark_clause_after_conflict_generation (limmat, reason); + } +} + +/*------------------------------------------------------------------------*/ +/* A unique implication point (uip) is an assigned variable in the current + * decision level that occurs on all paths back from the conflict ignoring + * edges leading to variables with lower decision level. The decision + * variable of the current decision level acts as a sentinel to this search. + * The reverse order of the assigned variables on the trail is a topological + * order of the dependency graph. Thus we do not need a general graph + * algorithm to decompose a graph in its biconnected components. + */ +static void +generate_conflict_clause (Limmat * limmat, Clause * conflict) +{ + Variable **assigned, **last_assigned, **first_assigned, **p, *v; + Clause *reason; + Frame *frame; + int paths; + + assert (!count_Stack (&limmat->clause)); + assert (limmat->decision_level >= 0); + + frame = limmat->control + limmat->decision_level; + assigned = (Variable **) start_of_Stack (&limmat->trail); + first_assigned = assigned + frame->trail_level; + last_assigned = assigned + count_Stack (&limmat->trail) - 1; + +#ifdef NDEBUG + if (first_assigned > assigned) + assert (first_assigned[-1]->decision_level < limmat->decision_level); +#endif + + /* Traverse all assigned variables in the current decision level starting + * with the most recently assigned variable. Stop as soon as a unique + * implication point is found. During the traversal record the already + * visited variables by setting their 'mark' bit. Additionally count the + * number of open paths to detect unique implication points. In + * particular a unique implication point is found if all paths converged, + * thus the number of still open branches is zero. + */ + v = 0; + paths = 0; + expand_open_paths (limmat, conflict, &paths); + + for (p = last_assigned; paths; p--) + { + assert (p >= first_assigned); + + v = strip (*p); + assert (v->decision_level == limmat->decision_level); + + if (v->mark) + { + paths--; + reason = v->reason; + if (!reason) + assert (!paths); + + if (paths) + expand_open_paths (limmat, reason, &paths); + else + push_literal (limmat, v); + } + } + + assert (v); + + /* Reset the mark bit of all traversed variables. + */ + while (++p <= last_assigned) + unmark_after_conflict_generation (limmat, *p); + + /* And do not forget lower decision level variables referenced in the + * conflict clause only. + */ + unmark_clause_after_conflict_generation (limmat, conflict); + +#ifdef EXPENSIVE_CHECKS + check_all_variables_unmarked (limmat); +#endif + + if (v->reason) + { + if (limmat->stats) + limmat->stats->uips++; + +#ifdef LOG_UIP + if (!limmat->dont_log) + { + int sign; + + assert (is_assigned (v)); + sign = (v->assignment == FALSE) ? -1 : 1; + fprintf (LOGFILE (limmat), + "UIP\t%d@%d\n", sign * var2int (v), v->decision_level); + } +#endif + } +} + +/*------------------------------------------------------------------------*/ +/* Analyze the current conflict and deduce a conflict driven assignment. + * In case the empty clause is implied use 'FALSE' as 'literal' in the + * assignment. + */ +static void +analyze (Limmat * limmat, Clause * conflict, Assignment * assignment) +{ + assignment->literal = FALSE; + + if (limmat->decision_level >= 0) + { + generate_conflict_clause (limmat, conflict); + + if (count_Stack (&limmat->clause) > 0) + add_literals (limmat, assignment); + } +} + +/*------------------------------------------------------------------------*/ + +static int +backtrack (Limmat * limmat, Clause * conflict) +{ + Assignment assignment; + int res, delta; + + if (limmat->decision_level < 0) + return 0; + + assert (conflict); + + reset_assignments (limmat); + analyze (limmat, conflict, &assignment); + res = (assignment.literal != FALSE); + untrail (limmat, assignment.decision_level + 1); + delta = limmat->decision_level - assignment.decision_level; + assert (delta >= 0); + limmat->decision_level = assignment.decision_level; + + if (limmat->stats && delta > 1) + { + limmat->stats->backjumps += delta - 1; + +#ifdef LOG_BACKJUMP + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "JUMP\t%d\n", delta - 1); +#endif + } + + if (res) + { + push_assignment (limmat, &assignment); + +#ifdef LOG_BACKTRACK + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), + "BACK\t%d@%d\n", + var2int (assignment.literal), assignment.decision_level); +#endif + } + else + { +#ifdef LOG_BACKTRACK + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "BACK\ttop\n"); +#endif + } + + invariant (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ +#if !defined(NDEBUG) && defined(EXPENSIVE_CHECKS) +/*------------------------------------------------------------------------*/ + +static int +max_decision_level_clause (Limmat * limmat, Clause * clause) +{ + Variable *literal; + int i, res; + + for (res = -1, i = 0; i < clause->size; i++) + { + literal = strip (lit2var (clause2literals (limmat, clause)[i])); + if (literal->decision_level > res) + res = literal->decision_level; + } + + return res; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ + +inline static int +next_pos (int prev, + int *direction_ptr, int start, int num_literals, int *turned_ptr) +{ + int res, direction; + + direction = *direction_ptr; + res = prev + direction; + + if (res < 0 || res >= num_literals) + { + direction *= -1; + *direction_ptr = direction; + res = start + direction; + + if (res < 0 || res >= num_literals) + *turned_ptr = 2; + else + *turned_ptr += 1; + + } + + return res; +} + +/*------------------------------------------------------------------------*/ +/* This is the innermost propagation operation. It assumes that the watched + * occurence of the literal is assigned to false and the watched literals in + * the clause have to be adjusted accordingly. In this process we + * also detect unit clauses and conflicts. + */ +inline static Clause * +propagate_clause (Limmat * limmat, + Occurence signed_clause, int decision_level, int *remove) +{ + int sign, start, head, tail, i, num_literals, turned, direction; + Variable *tmp, **literals, *dereferenced_tail; + Variable *literal, *tail_literal; + Clause *conflict, *clause; + Assignment new_assignment; + + if (limmat->stats) + limmat->stats->propagations++; + +#ifdef LOG_PROPS + fprintf (LOGFILE (limmat), "PROPS\t%.0f\t", limmat->stats->propagations); + dump_clause (limmat, (Clause *) strip (signed_clause)); +#endif + + conflict = 0; + *remove = 0; + + sign = is_signed (signed_clause); + clause = sign ? not (signed_clause) : signed_clause; + + /* The tail 'watched' literal can be found by flipping the sign. + */ + tail = clause->watched[!sign]; + + if (tail < 0) + { + assert (clause->size == 1); + conflict = clause; + } + else + { + if (limmat->stats) + limmat->stats->visits++; + + literals = clause2literals (limmat, clause); +#ifndef LOOK_AT_OTHER_WATCHED_LITERAL + tail_literal = 0; + dereferenced_tail = FALSE; +#else + tail_literal = lit2var (literals[tail]); + dereferenced_tail = deref (tail_literal); + if (dereferenced_tail == FALSE) + conflict = clause; + else if (dereferenced_tail != TRUE) +#endif + { + head = clause->watched[sign]; + num_literals = clause->size; + + assert (num_literals >= 2); + assert (head >= 0); + assert (deref (lit2var (literals[head])) == FALSE); + + /* Now try to find an unassigned literal among the literals of the + * clause. Stop as soon a literal assigned to 'TRUE' is found or + * we wrap around and reach 'start' again. Prepare a new + * assignment, in case a unit clause has been found. + */ +#ifdef OPTIMIZE_DIRECTION + direction = clause->direction; +#else + direction = 1; +#endif + turned = 0; + start = head; + i = start; + + tmp = FALSE; + + while (tmp == FALSE && turned < 2) + { +#ifdef LOOK_AT_OTHER_WATCHED_LITERAL + /* Just skip the 'tail', since we already checked it. Also + * skip the 'head' since it should always be assigned to + * FALSE. + */ + if (i != tail) +#endif + if (i != head) + { + if (limmat->stats) + limmat->stats->visits++; + +#ifndef LOOK_AT_OTHER_WATCHED_LITERAL + if (i == tail) + { + tail_literal = lit2var (literals[i]); + dereferenced_tail = deref (tail_literal); + if (dereferenced_tail == TRUE) + break; + } + else +#endif + { + literal = lit2var (literals[i]); + tmp = deref (literal); + } + } + + if (tmp == FALSE) + i = next_pos (i, &direction, start, num_literals, &turned); + } + +#ifndef LOOK_AT_OTHER_WATCHED_LITERAL + if (tmp == FALSE && dereferenced_tail == FALSE) + conflict = clause; + else if (dereferenced_tail == TRUE) + { + /* nothing to be done */ + } + else +#endif + + if (turned >= 2) + { + /* We wrapped around without finding a non false assigned + * literal, except the tail literal. As a consequence assign + * the tail literal to true with the maximum level encountered + * while traversing the clause. Keep this occurence of the + * literal as watched. + */ + assert (tail_literal); + new_assignment.literal = tail_literal; + new_assignment.decision_level = decision_level; + new_assignment.reason = clause; + push_assignment (limmat, &new_assignment); + } + else + { + /* We found a non false literal which will become the new + * watched literal at 'sign'. This should be the standard + * case and we have to notify the calling function that this + * occurence can be removed. + */ + assert (i != tail); + partial_disconnect (limmat, signed_clause, start); + connect (limmat, signed_clause, i); + *remove = 1; +#ifdef OPTIMIZE_DIRECTION + clause->direction = direction; +#endif + } + } + } + + invariant_clause (limmat, clause); + + return conflict; +} + +/*------------------------------------------------------------------------*/ + +inline static Clause * +propagate_assignment (Limmat * limmat, Assignment * assignment) +{ + Occurence *occurrences; + int i, count, remove; + Clause *conflict; + Stack *stack; + +#ifdef EXPENSIVE_CHECKS + if (assignment->reason) + assert (max_decision_level_clause (limmat, assignment->reason) + <= assignment->decision_level); +#endif + + /* First actually assign the literal. + */ + assign (limmat, assignment); + + /* Traverse all occurrences that contain a watched negated literal of the + * assignment, as long no conflict has been found. + */ + stack = var2stack (not (assignment->literal)); + occurrences = start_of_Stack (stack); + count = count_Stack (stack); + conflict = 0; + i = 0; + + while (!conflict && i < count) + { + conflict = + propagate_clause (limmat, occurrences[i], assignment->decision_level, + &remove); + + /* To remove the occurence from the stack we just overwrite it with + * the last entry in the stack and pop the last Element of the stack. + * We do not want to reset the stack until the end, because we have to + * assume that stacks may shrink if their size is decreased. + */ + if (!conflict) + { + if (remove) + { + if (--count > 0) + occurrences[i] = occurrences[count]; + } + else + i++; + } + } + + reset_Stack (limmat, stack, count); + + return conflict; +} + +/*------------------------------------------------------------------------*/ +/* Propagate assignments until the assignments stack is empty or a conflict + * has been generated. + */ +static Clause * +propagate (Limmat * limmat) +{ + Variable *literal, *tmp; + Assignment assignment; + Clause *conflict; + + conflict = 0; + + while (!conflict && count_assignments (limmat) > 0) + { + /* Pop next assignment from mark stack. Each assignment is made of + * the literal that will be assigned to true, the level at which this + * assignment has been generated and finally the clause that triggered + * the assignment (0 if decision or toplevel unit). + */ + pop_assignment (limmat, &assignment); + + /* We dereference the literal. It should not be assigned to 'FALSE' + * since that would have triggered an earlier conflict. + */ + literal = assignment.literal; + tmp = deref (literal); +#ifdef SHORTEN_REASONS + assert (tmp != TRUE); +#else + if (tmp == TRUE) + continue; +#endif + if (tmp == FALSE) + conflict = assignment.reason; + else + conflict = propagate_assignment (limmat, &assignment); + } + +#ifdef LOG_CONFLICT + if (conflict && !limmat->dont_log) + { + fprintf (LOGFILE (limmat), "BOOM\t"); + dump_clause_aux (LOGFILE (limmat), limmat, conflict, 0, 1, 1, 0, 0); + } +#endif + + if (conflict) + limmat->num_conflicts++; + + return conflict; +} + +/*------------------------------------------------------------------------*/ + +static int +all_clauses_satisfied (Limmat * limmat) +{ + Variable **q, **eol; + Clause **p, **eoc; + int res, found; + + res = !limmat->contains_empty_clause; + + forall_clauses (limmat, p, eoc) + { + found = 0; + + forall_literals (limmat, *p, q, eol) + if ((found = (deref (lit2var (*q)) == TRUE))) + break; + + if (!(res = found)) + break; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +its_time_to_restart (Limmat * limmat) +{ + int res; + + if (limmat->decision_level >= 0) + { + dec_Counter (&limmat->restart); + res = done_Counter (&limmat->restart); + } + else + res = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +sat (Limmat * limmat, int max_decisions) +{ + int res, num_decisions; + Clause *conflict; + + if (limmat->contains_empty_clause) + res = 0; + else + { + init_order (limmat); + units2mark (limmat); + + num_decisions = 0; + res = -1; + + while (res < 0) + { + if (count_assignments (limmat)) + { + conflict = propagate (limmat); + if (conflict && !backtrack (limmat, conflict)) + res = 0; + } + else if (limmat->num_assigned < limmat->num_variables) + { + if (max_decisions >= 0) + { + if (num_decisions >= max_decisions) + break; + + num_decisions++; + } + + if (its_time_to_restart (limmat)) + restart (limmat); + else + decide (limmat); + } + else + { +#ifdef LOG_DECISION + if (!limmat->dont_log) + fprintf (LOGFILE (limmat), "NO MORE VARIABLES LEFT\n"); +#endif + + res = 1; + } + } + } + + if (limmat->log && limmat->report.finished > 0) + fprintf (limmat->log, LIMMAT_PREFIX "\n"); + + if (res == 1 && !all_clauses_satisfied (limmat)) + { + fprintf (stderr, "*** limmat internal error: inconsistent result\n"); + fflush (stderr); + abort (); + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +int +sat_Limmat (Limmat * limmat, int max_decisions) +{ + int res; + + start_timer (&limmat->timer); + res = sat (limmat, max_decisions); + limmat->time += stop_timer (limmat->timer); + + return res; +} + +/*------------------------------------------------------------------------*/ + +const int * +assignment_Limmat (Limmat * limmat) +{ + Variable *tmp, *v, *end; + int *res, literal; + + start_timer (&limmat->timer); + if (all_clauses_satisfied (limmat)) + { + reset_Stack (limmat, &limmat->clause, 0); + + forall_variables (limmat, v, end) + { + tmp = deref (v); + assert (tmp == FALSE || tmp == TRUE); + literal = v->id; + if (tmp == FALSE) + literal = -literal; + push (limmat, &limmat->clause, (void *) (PTR_SIZED_WORD) literal); + } + + push (limmat, &limmat->clause, (void *) (int) 0); + res = intify_Stack (&limmat->clause); + } + else + res = 0; + limmat->time += stop_timer (limmat->timer); + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define BUFFER_SIZE 100 + +/*------------------------------------------------------------------------*/ + +static int +intlen (int d) +{ + int sign, res; + + if (d) + { + if ((sign = (d < 0))) + d = -d; + + if (d < 10) + res = 1; + else if (d < 100) + res = 2; + else if (d < 1000) + res = 3; + else if (d < 10000) + res = 4; + else if (d < 100000) + res = 5; + else if (d < 1000000) + res = 6; + else if (d < 10000000) + res = 7; + else if (d < 100000000) + res = 8; + else if (d < 1000000000) + res = 9; + else + res = 10; /* fine for 32 bit machines */ + + if (sign) + res++; + } + else + res = 1; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline static int +insert_buffer (int val, int next, int pos, char *buffer) +{ + int l; + + if (pos) + assert (!buffer[pos]); + + if (pos) + buffer[pos++] = ' '; + sprintf (buffer + pos, "%d", val); + assert (intlen (val) == (int)strlen (buffer + pos)); + pos += intlen (val); + l = intlen (next); + + if (pos + l > 76) + { + assert (pos + 1 < BUFFER_SIZE); + buffer[pos] = 0; + pos = 0; + } + + return pos; +} + +/*------------------------------------------------------------------------*/ + +void +print_assignment_Limmat (const int *assignment, FILE * file) +{ + char buffer[BUFFER_SIZE]; + const int *p; + int pos; + + pos = 0; + buffer[pos] = 0; + + for (p = assignment; *p; p++) + { + pos = insert_buffer (p[0], p[1], pos, buffer); + if (!pos) + { +#ifdef SAT2002FMT + fputs ("v ", file); +#endif + fprintf (file, "%s\n", buffer); + } + } + + if (pos) + { +#ifdef SAT2002FMT + fputs ("v ", file); +#endif + fprintf (file, "%s\n", buffer); + } +} + +/*------------------------------------------------------------------------*/ +#ifdef LIMMAT_WHITE +/*------------------------------------------------------------------------*/ + +#include +#include +#include +#include + +/*------------------------------------------------------------------------*/ + +typedef struct Suite Suite; + +struct Suite +{ + int argc, ok, failed, backspaces; + char **argv; +}; + +/*------------------------------------------------------------------------*/ +/* Compare two files for differences. The result is '1' iff no differences + * were encountered and both files could be accessed. If one file could not + * be openend, then '0' is returned. + */ +static int +cmp_files (char *name0, char *name1) +{ + int res, ch; + FILE *f[2]; + + f[0] = fopen (name0, "r"); + if (f[0]) + { + f[1] = fopen (name1, "r"); + if (f[1]) + { + do + { + ch = fgetc (f[0]); + res = (fgetc (f[1]) == ch); + } + while (res && ch != EOF); + fclose (f[1]); + } + else + res = 0; + fclose (f[0]); + } + else + res = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +mem0 (void) +{ + Limmat limmat; + void *ptr; + int res; + + limmat.bytes = 0; + limmat.max_bytes = 0; + ptr = new (&limmat, 4711); + res = (limmat.bytes >= 4711); + delete (&limmat, ptr, 4711); + if (res) + res = !limmat.bytes; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_MEM1 1000 +#define M_MEM1 1000 + +static int +mem1 (void) +{ + void *ptr[N_MEM1]; + Limmat limmat; + int res, i; + + limmat.bytes = 0; + limmat.max_bytes = 0; + for (i = 0; i < N_MEM1; i++) + ptr[i] = new (&limmat, M_MEM1); + res = (limmat.bytes >= M_MEM1 * N_MEM1); + for (i = 0; i < N_MEM1; i++) + delete (&limmat, ptr[i], M_MEM1); + if (res) + res = !limmat.bytes; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +mem2 (void) +{ + void *ptr[5], *tmp; + Limmat limmat; + + limmat.bytes = 0; + limmat.max_bytes = 0; + ptr[0] = new (&limmat, 17); + ptr[1] = new (&limmat, 18); + ptr[2] = new (&limmat, 19); + ptr[3] = new (&limmat, 20); + ptr[4] = new (&limmat, 21); + tmp = malloc (17); + ptr[4] = resize (&limmat, ptr[4], 222, 21); + free (tmp); + ptr[0] = resize (&limmat, ptr[0], 5, 17); + ptr[2] = resize (&limmat, ptr[2], 18, 19); + ptr[3] = resize (&limmat, ptr[3], 20, 20); + delete (&limmat, ptr[1], 18); + delete (&limmat, ptr[3], 20); + delete (&limmat, ptr[4], 222); + delete (&limmat, ptr[2], 18); + delete (&limmat, ptr[0], 5); + + return 1; +} + +/*------------------------------------------------------------------------*/ + +static int +limmat0 (void) +{ + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +limmat1 (void) +{ + Limmat *limmat; + void *ptr; + int res; + + limmat = new_Limmat (0); + ptr = new (limmat, 4711); + res = (internal_delete_Limmat (limmat) >= 4711); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +limmat2 (void) +{ + Limmat *limmat; + FILE *log; + int res; + + limmat = new_Limmat (0); + (void) find (limmat, 1); + log = fopen ("log/limmat2.log", "w"); + if (log) + { + res = !error_Limmat (limmat); + stats_Limmat (limmat, log); + fclose (log); + } + else + res = 0; + delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +stack0 (void) +{ + int res, leaked; + Limmat *limmat; + Stack stack; + + limmat = new_Limmat (0); + init_Stack (limmat, &stack); + release_Stack (limmat, &stack); + leaked = internal_delete_Limmat (limmat); + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +stack1 (void) +{ + int res, leaked; + Limmat *limmat; + Stack stack; + + res = 1; + limmat = new_Limmat (0); + init_Stack (limmat, &stack); + push (limmat, &stack, (void *) 4711); + if (res) + res = (4711 == (int) (PTR_SIZED_WORD) pop (&stack)); + if (res) + res = !stack.internal_count; + push (limmat, &stack, (void *) (PTR_SIZED_WORD) 13); + if (res) + res = (13 == (int) (PTR_SIZED_WORD) pop (&stack)); + if (res) + res = !stack.internal_count; + push (limmat, &stack, (void *) (PTR_SIZED_WORD) 17); + push (limmat, &stack, (void *) (PTR_SIZED_WORD) 19); + if (res) + res = (19 == (int) (PTR_SIZED_WORD) pop (&stack)); + if (res) + res = (17 == (int) (PTR_SIZED_WORD) pop (&stack)); + if (res) + res = !stack.internal_count; + release_Stack (limmat, &stack); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_STACK1 10000 + +static int +stack2 (void) +{ + int res, leaked, i; + Limmat *limmat; + Stack stack; + + res = 1; + limmat = new_Limmat (0); + init_Stack (limmat, &stack); + for (i = 0; i < N_STACK1; i++) + push (limmat, &stack, (void *) (PTR_SIZED_WORD) i); + for (i = N_STACK1 - 1; res && i >= 0; i--) + res = (i == (int) (PTR_SIZED_WORD) pop (&stack)); + if (res) + res = !stack.internal_count; + release_Stack (limmat, &stack); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_STACK3 11 + +static int +stack3 (void) +{ + int * a, i, res, leaked; + Limmat * limmat; + Stack stack; + + res = 1; + limmat = new_Limmat (0); + init_Stack (limmat, &stack); + for(i = 0; i < N_STACK3; i++) + push (limmat, &stack, (void*)(PTR_SIZED_WORD)(int)i); + + a = intify_Stack(&stack); + + for(i = 0; res && i < N_STACK3; i++) + res = (a[i] == i); + + release_Stack (limmat, &stack); + leaked = internal_delete_Limmat (limmat); + if(res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +align0 (void) +{ + return sizeof (PTR_SIZED_WORD) == sizeof (void *); +} + +/*------------------------------------------------------------------------*/ + +static int +align1 (void) +{ + int res; + + res = 1; + if (res) + res = is_aligned (0, 4); + if (res) + res = is_aligned (0, 8); + if (res) + res = is_aligned (0, 16); + if (res) + res = !is_aligned (1, 4); + if (res) + res = !is_aligned (1, 8); + if (res) + res = !is_aligned (1, 16); + if (res) + res = !is_aligned (3, 4); + if (res) + res = !is_aligned (7, 8); + if (res) + res = !is_aligned (15, 16); + if (res) + res = is_aligned (32, 4); + if (res) + res = is_aligned (32, 8); + if (res) + res = is_aligned (32, 16); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +align2 (void) +{ + int res; + + res = 1; + if (res) + res = (align (0, 4) == 0); + if (res) + res = (align (0, 8) == 0); + if (res) + res = (align (0, 16) == 0); + if (res) + res = (align (1, 4) == 4); + if (res) + res = (align (1, 8) == 8); + if (res) + res = (align (1, 16) == 16); + if (res) + res = (align (3, 4) == 4); + if (res) + res = (align (7, 8) == 8); + if (res) + res = (align (15, 16) == 16); + if (res) + res = (align (4, 4) == 4); + if (res) + res = (align (8, 8) == 8); + if (res) + res = (align (16, 16) == 16); + if (res) + res = (align (32, 4) == 32); + if (res) + res = (align (32, 8) == 32); + if (res) + res = (align (32, 16) == 32); + if (res) + res = (align (33, 4) == 36); + if (res) + res = (align (33, 8) == 40); + if (res) + res = (align (33, 16) == 48); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +align3 (void) +{ + int res; + + res = 1; + + if (res) + res = !(ALL_BUT_SIGN_BITS & SIGN_BIT); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +align4 (void) +{ + FILE *log; + int res; + + log = fopen ("log/align4.log", "w"); + res = 0; + if (log) + { + res = is_aligned_ptr (next_Variable (0), VARIABLE_ALIGNMENT); + if (res) + res = (sizeof (Variable) <= (int) next_Variable (0)); + fprintf (log, "sizeof(Variable) = %d\n", (int) sizeof (Variable)); + fprintf (log, "next_Variable(0) = %d\n", (int) next_Variable (0)); + fclose (log); + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +log0 (void) +{ + int res; + + res = 1; + if (res) + res = (msnzb (0) == 0); + if (res) + res = (msnzb (1) == 0); + if (res) + res = (msnzb (2) == 1); + if (res) + res = (msnzb (3) == 1); + if (res) + res = (msnzb (4) == 2); + if (res) + res = (msnzb (5) == 2); + if (res) + res = (msnzb (6) == 2); + if (res) + res = (msnzb (7) == 2); + if (res) + res = (msnzb (8) == 3); + if (res) + res = (msnzb (15) == 3); + if (res) + res = (msnzb (16) == 4); + if (res) + res = (msnzb (32767) == 14); + if (res) + res = (msnzb (32768) == 15); + if (res) + res = (msnzb (65535) == 15); + if (res) + res = (msnzb (65536) == 16); + if (res) + res = (msnzb (1024 * 1024 - 1) == 19); + if (res) + res = (msnzb (1024 * 1024) == 20); + if (res) + res = (msnzb ((~0)) == sizeof (int) * 8 - 1); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +log1 (void) +{ + int res; + + res = 1; + if (res) + res = (log2ceil (1) == 0); + if (res) + res = (log2ceil (2) == 1); + if (res) + res = (log2ceil (3) == 2); + if (res) + res = (log2ceil (4) == 2); + if (res) + res = (log2ceil (5) == 3); + if (res) + res = (log2ceil (6) == 3); + if (res) + res = (log2ceil (7) == 3); + if (res) + res = (log2ceil (8) == 3); + if (res) + res = (log2ceil (9) == 4); + if (res) + res = (log2ceil (15) == 4); + if (res) + res = (log2ceil (16) == 4); + if (res) + res = (log2ceil (17) == 5); + if (res) + res = (log2ceil (32767) == 15); + if (res) + res = (log2ceil (32768) == 15); + if (res) + res = (log2ceil (32769) == 16); + if (res) + res = (log2ceil (65535) == 16); + if (res) + res = (log2ceil (65536) == 16); + if (res) + res = (log2ceil (65537) == 17); + if (res) + res = (log2ceil (1024 * 1024 - 1) == 20); + if (res) + res = (log2ceil (1024 * 1024) == 20); + if (res) + res = (log2ceil (1024 * 1024 + 1) == 21); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +arena0 (void) +{ + int res, leaked, alignment; + Limmat *limmat; + Arena arena; + + limmat = new_Limmat (0); + for (alignment = 4; alignment <= 16; alignment *= 2) + { + init_Arena (limmat, &arena, alignment); + release_Arena (limmat, &arena); + } + leaked = internal_delete_Limmat (limmat); + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_ARENA1 256 + +static int +arena1 (void) +{ + int res, leaked, alignment; + int *ptr[N_ARENA1], i, j; + Limmat *limmat; + size_t delta; + Arena arena; + + res = 1; + limmat = new_Limmat (0); + for (alignment = 4; res && alignment <= 16; alignment *= 2) + { + init_Arena (limmat, &arena, alignment); + for (i = 0; i < N_ARENA1; i++) + { + ptr[i] = access_Arena (limmat, &arena, i, sizeof (int), &delta); + if (delta) + for (j = 0; j < i; j++) + fix_pointer (ptr + j, delta); + } + + for (i = 0; res && i < N_ARENA1; i++) + { + res = + (ptr[i] == + access_Arena (limmat, &arena, i, sizeof (int), &delta)); + if (res) + res = !delta; + } + + release_Arena (limmat, &arena); + } + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var0 (void) +{ + return not (FALSE) == TRUE; +} + +/*------------------------------------------------------------------------*/ + +static int +var1 (void) +{ + return not (TRUE) == FALSE; +} + +/*------------------------------------------------------------------------*/ + +static int +var2 (void) +{ + return strip (TRUE) == FALSE; +} + +/*------------------------------------------------------------------------*/ + +static int +var3 (void) +{ + Variable v; + int res; + + v.assignment = &v; + res = !is_assigned (&v); + if (res) + res = (deref (&v) == &v); + if (res) + res = (deref (not (&v)) == not (&v)); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var4 (void) +{ + Variable v; + int res; + + v.assignment = FALSE; + res = is_assigned (&v); + if (res) + res = (deref (&v) == FALSE); + if (res) + res = (deref (not (&v)) == TRUE); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var5 (void) +{ + Variable v; + int res; + + v.assignment = TRUE; + res = is_assigned (&v); + if (res) + res = (deref (&v) == TRUE); + if (res) + res = (deref (not (&v)) == FALSE); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var6 (void) +{ + int res, leaked; + Limmat *limmat; + Variable *v; + + limmat = new_Limmat (0); + v = find (limmat, 1); + res = (v->id == 1); + if (res) + res = !is_assigned (v); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var7 (void) +{ + Variable *u, *v, *w; + int res, leaked; + Limmat *limmat; + + limmat = new_Limmat (0); + u = find (limmat, 1); + v = find (limmat, 1); + w = find (limmat, -1); + res = (u == v); + if (res) + res = (v == not (w)); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_VAR8 10 + +static int +var8 (void) +{ + int res, leaked, i, j; + Variable *u[N_VAR8]; + Limmat *limmat; + + limmat = new_Limmat (0); + for (i = 0; i < N_VAR8; i++) + u[i] = find (limmat, i + 1); + res = 1; + for (i = 0; res && i < N_VAR8 - 1; i++) + for (j = i + 1; res && j < N_VAR8; j++) + res = (u[i] != u[j]); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +var9 (void) +{ + Variable *u, *v; + int res, leaked; + Limmat *limmat; + + res = 1; + limmat = new_Limmat (0); + v = find (limmat, 4711); + u = find (limmat, -17); + if (res) + res = (var2int (u) == -17); + if (res) + res = (var2int (not (u)) == 17); + if (res) + res = (var2int (v) == 4711); + if (res) + res = (var2int (not (v)) == -4711); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +sort0 (void) +{ + int res, leaked; + Limmat *limmat; + + limmat = new_Limmat (0); + init_order (limmat); + res = is_sorted (limmat); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +#define N_SORT1 3 + +static int +sort1 (void) +{ + int c[3][2][2], i[3][2], j, k, s, id, res, leaked; + Limmat *limmat; + + for (s = 0; s < 2; s++) + for (j = 0; j < 3; j++) + { + id = j + 1; + c[j][s][0] = s ? -id : id; + c[j][s][1] = 0; + } + + res = 1; + for (i[0][0] = 0; i[0][0] < N_SORT1; i[0][0]++) + for (i[0][1] = 0; i[0][1] < N_SORT1; i[0][1]++) + for (i[1][0] = 0; i[1][0] < N_SORT1; i[1][0]++) + for (i[1][1] = 0; i[1][1] < N_SORT1; i[1][1]++) + for (i[2][0] = 0; i[2][0] < N_SORT1; i[2][0]++) + for (i[2][1] = 0; i[2][1] < N_SORT1; i[2][1]++) + { + limmat = new_Limmat (0); + + for (s = 0; res && s < 2; s++) + for (j = 0; res && j < 3; j++) + for (k = 0; k < i[j][s]; k++) + add_Limmat (limmat, c[j][s]); + + init_order (limmat); + if (res) + res = is_sorted (limmat); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser0 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "/dev/null"); + delete_Parser (parser); + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser1 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, 0); + delete_Parser (parser); + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser2 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, 0); + parse_error (parser, "this is a", " parse error"); + delete_Parser (parser); + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser3 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser3.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser4 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser4.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser5 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser5.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser6 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser6.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser7 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser7.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser8 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser8.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser9 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser9.in"); + res = !read_clause (parser); + if (res) + res = !parser->error; + if (res) + res = !parser->num_specified_max_id; + if (res) + res = !parser->num_specified_clauses; + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser10 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser10.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser11 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser11.in"); + res = read_clause (parser); + if (res) + res = (parser->num_specified_max_id == 2); + if (res) + res = (parser->num_specified_clauses == 2); + if (res) + res = (count_Stack (&parser->literals) == 2); + if (res) + res = (parser->literals.data.as_array[0] == (void *) 2); + if (res) + res = (parser->literals.data.as_array[1] == (void *) -1); + if (res) + res = read_clause (parser); + if (res) + res = (count_Stack (&parser->literals) == 2); + if (res) + res = (parser->literals.data.as_array[0] == (void *) -1); + if (res) + res = (parser->literals.data.as_array[1] == (void *) 2); + if (res) + res = !read_clause (parser); + if (res) + res = !parser->error; + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser12 (void) +{ + Parser *parser; + Limmat *limmat; + int res; + + limmat = new_Limmat (0); + parser = new_Parser (limmat, 0, "log/parser12.in"); + res = !read_clause (parser); + if (res) + res = (parser->error != 0); + delete_Parser (parser); + if (res) + res = !internal_delete_Limmat (limmat); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parse_and_print (int n, int expect_parse_error) +{ + char in_name[100], out_name[100], log_name[100]; + int res, leaked, ok; + Limmat *limmat; + FILE *log; + + sprintf (in_name, "log/parser%d.in", n); + sprintf (out_name, "log/parser%d.out", n); + sprintf (log_name, "log/parser%d.log", n); + + limmat = new_Limmat (0); + ok = read_Limmat (limmat, 0, in_name); + if (expect_parse_error) + res = !ok; + else + res = ok; + + log = fopen (log_name, "w"); + if (log) + { + print_Limmat (limmat, log); + fclose (log); + if (res) + res = cmp_files (log_name, out_name); + } + else + res = 0; + + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +parser13 (void) +{ + return parse_and_print (13, 0); +} +static int +parser14 (void) +{ + return parse_and_print (14, 0); +} +static int +parser15 (void) +{ + return parse_and_print (15, 0); +} +static int +parser16 (void) +{ + return parse_and_print (16, 1); +} +static int +parser17 (void) +{ + return parse_and_print (17, 1); +} +static int +parser18 (void) +{ + return parse_and_print (18, 0); +} +static int +parser19 (void) +{ + return parse_and_print (19, 1); +} +static int +parser20 (void) +{ + return parse_and_print (20, 0); +} +static int +parser21 (void) +{ + return parse_and_print (21, 1); +} +static int +parser22 (void) +{ + return parse_and_print (22, 0); +} + +/*------------------------------------------------------------------------*/ + +static int +check_sat (const char *prefix, int d, int satisfiable, int max_decisions) +{ + char in_name[100], log_name[100], out_name[100]; + int res, leaked; + const int *p; + Limmat *limmat; + FILE *log; + + limmat = new_Limmat (0); + sprintf (in_name, "log/%s%d.in", prefix, d); + sprintf (log_name, "log/%s%d.log", prefix, d); + sprintf (out_name, "log/%s%d.out", prefix, d); + res = read_Limmat (limmat, 0, in_name); + if (res) + { + res = (satisfiable == sat (limmat, max_decisions)); + if (satisfiable == 1) + { + p = assignment_Limmat (limmat); + if (p && (log = fopen (log_name, "w"))) + { + if (*p) + { + fprintf (log, "%d", *p++); + while (*p) + fprintf (log, " %d", *p++); + fputc ('\n', log); + } + + fclose (log); + res = cmp_files (out_name, log_name); + } + else + res = 0; + } + } + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +sat0 (void) +{ + return check_sat ("sat", 0, 1, -1); +} +static int +sat1 (void) +{ + return check_sat ("sat", 1, 0, -1); +} +static int +sat2 (void) +{ + return check_sat ("sat", 2, 1, -1); +} +static int +sat3 (void) +{ + return check_sat ("sat", 3, 0, -1); +} +static int +sat4 (void) +{ + return check_sat ("sat", 4, 1, -1); +} +static int +sat5 (void) +{ + return check_sat ("sat", 5, 1, -1); +} +static int +sat6 (void) +{ + return check_sat ("sat", 6, 1, -1); +} +static int +sat7 (void) +{ + return check_sat ("sat", 7, 0, -1); +} +static int +sat8 (void) +{ + return check_sat ("sat", 8, 1, -1); +} +static int +sat9 (void) +{ + return check_sat ("sat", 9, 1, -1); +} +static int +sat10 (void) +{ + return check_sat ("sat", 10, 1, -1); +} +static int +sat11 (void) +{ + return check_sat ("sat", 11, 1, -1); +} +static int +sat12 (void) +{ + return check_sat ("sat", 12, 1, -1); +} +static int +sat13 (void) +{ + return check_sat ("sat", 13, 1, -1); +} + +/*------------------------------------------------------------------------*/ + +static int +unit0 (void) +{ + return check_sat ("unit", 0, 0, 0); +} +static int +unit1 (void) +{ + return check_sat ("unit", 1, 0, 0); +} +static int +unit2 (void) +{ + return check_sat ("unit", 2, 1, 0); +} +static int +unit3 (void) +{ + return check_sat ("unit", 3, 1, 0); +} + +/*------------------------------------------------------------------------*/ + +static int +is_prime (int p) +{ + int i; + + for (i = 2; i * i <= p; i++) + if (!(p % i)) + return 0; + + return 1; +} + +/*------------------------------------------------------------------------*/ + +static int +check_prime (int p) +{ + return check_sat ("prime", p, !is_prime (p), -1); +} + +/*------------------------------------------------------------------------*/ + +static int +prime4 (void) +{ + return check_prime (4); +} +static int +prime9 (void) +{ + return check_prime (9); +} +static int +prime25 (void) +{ + return check_prime (25); +} +static int +prime49 (void) +{ + return check_prime (49); +} +static int +prime121 (void) +{ + return check_prime (121); +} +static int +prime169 (void) +{ + return check_prime (169); +} +static int +prime289 (void) +{ + return check_prime (289); +} +static int +prime361 (void) +{ + return check_prime (361); +} +static int +prime529 (void) +{ + return check_prime (529); +} +static int +prime841 (void) +{ + return check_prime (841); +} +static int +prime961 (void) +{ + return check_prime (961); +} +static int +prime1369 (void) +{ + return check_prime (1369); +} +static int +prime1681 (void) +{ + return check_prime (1681); +} +static int +prime1849 (void) +{ + return check_prime (1849); +} +static int +prime2209 (void) +{ + return check_prime (2209); +} + +/*------------------------------------------------------------------------*/ + +static int +add2 (void) +{ + return check_sat ("add", 2, 0, -1); +} +static int +add4 (void) +{ + return check_sat ("add", 4, 0, -1); +} +static int +add8 (void) +{ + return check_sat ("add", 8, 0, -1); +} +static int +add16 (void) +{ + return check_sat ("add", 16, 0, -1); +} + +/*------------------------------------------------------------------------*/ + +static int +api0 (void) +{ + Limmat *limmat; + int res, leaked; + + limmat = new_Limmat (0); + leaked = internal_delete_Limmat (limmat); + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +api1 (void) +{ + Limmat *limmat; + int res, leaked; + + limmat = new_Limmat (0); + res = (sat_Limmat (limmat, 0) == 1); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +api2 (void) +{ + int res, leaked, clause[1]; + Limmat *limmat; + + limmat = new_Limmat (0); + clause[0] = 0; + add_Limmat (limmat, clause); + res = (sat_Limmat (limmat, 0) == 0); + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +api3 (void) +{ + int res, leaked, clause[2]; + const int *assignment; + Limmat *limmat; + + limmat = new_Limmat (0); + clause[0] = 1; + clause[1] = 0; + add_Limmat (limmat, clause); + res = (sat_Limmat (limmat, 0) == 1); + if (res) + { + assignment = assignment_Limmat (limmat); + if (res) + res = (assignment != 0); + if (res) + res = (assignment[0] == 1); + if (res) + res = (assignment[1] == 0); + } + + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static int +api4 (void) +{ + int res, leaked, clause[3]; + const int *assignment; + Limmat *limmat; + + limmat = new_Limmat (0); + clause[0] = 1; + clause[1] = 2; + clause[2] = 0; + add_Limmat (limmat, clause); + res = (sat_Limmat (limmat, -1) == 1); + if (res) + { + assignment = assignment_Limmat (limmat); + if (res) + res = (assignment != 0); + if (res) + res = (assignment[0] && assignment[1] && !assignment[2]); + if (res) + res = (assignment[0] != assignment[1]); + if (res) + res = (assignment[0] == 1 || assignment[1] == 2); + } + + leaked = internal_delete_Limmat (limmat); + if (res) + res = !leaked; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +run (int (*tc) (void), Suite * suite, char *name, int n) +{ + int ok, skip, i, found_pattern; + char buffer[100]; + double timer; + + sprintf (buffer, "%s%d", name, n); + + for (i = 1, found_pattern = 0; !found_pattern && i < suite->argc; i++) + found_pattern = (suite->argv[i][0] != '-'); + + if (!found_pattern) + skip = 0; + else if (isdigit ((int) name[strlen (name) - 1])) + { + skip = 1; + for (i = 1; skip && i < suite->argc; i++) + skip = strcmp (suite->argv[i], name); + } + else + { + skip = 1; + for (i = 1; skip && i < suite->argc; i++) + skip = (strcmp (suite->argv[i], name) + && strcmp (suite->argv[i], buffer)); + } + + if (!skip) + { + start_timer (&timer); + + printf ("%-10s ...", buffer); + fflush (stdout); + + ok = tc (); + if (ok) + { + suite->ok++; + if (!suite->backspaces) + printf (" ok "); + } + else + { + suite->failed++; + printf (" failed "); + } + + if (ok && suite->backspaces) + { + for (i = 0; i < 14; i++) + fputc ('', stdout); + fflush (stdout); + } + else + printf ("in %.2f seconds\n", stop_timer (timer)); + } +} + +/*------------------------------------------------------------------------*/ +/* Fast test case. + */ +#define TF(name,n) do { run(name ## n, &suite, # name, n); } while(0) + +/*------------------------------------------------------------------------*/ +/* Slow test case. + */ +#define TS(name,n) \ +do { if(!only_fast) run(name ## n, &suite, # name, n); } while(0) + +/*------------------------------------------------------------------------*/ + +static void +line (void) +{ + printf ("-------------------------------------" + "------------------------------------\n"); +} + +/*------------------------------------------------------------------------*/ + +#define USAGE \ +"usage: white [-h|-f|-k] [ [] ... ]\n" \ +"\n" \ +" -h print command line option summary\n" \ +" -f run only fast test cases (usefull if checking is enabled)\n" \ +" -k print successful test cases (default in dumb terminals like emacs)\n" \ +"\n" \ +"The list of patterns specifies the test cases to run. If no pattern is\n" \ +"given all test cases are executed.\n" + +/*------------------------------------------------------------------------*/ + +int +main (int argc, char **argv) +{ + int i, only_fast; + double timer; + Suite suite; + + start_timer (&timer); + + only_fast = 0; + suite.backspaces = 0; + + if (isatty (1)) + { + /* Do not use backspace when running in an EMacs terminal. + */ + suite.backspaces = !getenv ("TERM") || strcmp (getenv ("TERM"), "dumb"); + } + + for (i = 1; i < argc; i++) + { + if (!strcmp (argv[i], "-h")) + { + printf (USAGE); + exit (0); + } + else if (!strcmp (argv[i], "-f")) + { + only_fast = 1; + } + else if (!strcmp (argv[i], "-k")) + { + suite.backspaces = 0; + } + else if (argv[i][0] == '-') + { + fprintf (stderr, + "*** white: unknown command line option '%s' (try '-h')\n", + argv[i]); + exit (1); + } + } + + suite.argc = argc; + suite.argv = argv; + suite.ok = 0; + suite.failed = 0; + + printf ("white box test cases for limmat %s\n", version_Limmat ()); + line (); + + TF (align, 0); + TF (align, 1); + TF (align, 2); + TF (align, 3); + TF (align, 4); + + TF (log, 0); + TF (log, 1); + + TF (stack, 0); + TF (stack, 1); + TF (stack, 2); + TF (stack, 3); + + TF (arena, 0); + TF (arena, 1); + + TF (mem, 0); + TF (mem, 1); + TF (mem, 2); + + TF (limmat, 0); + TF (limmat, 1); + TF (limmat, 2); + + TF (var, 0); + TF (var, 1); + TF (var, 2); + TF (var, 3); + TF (var, 4); + TF (var, 5); + TF (var, 6); + TF (var, 7); + TF (var, 8); + TF (var, 9); + + TF (sort, 0); + TF (sort, 1); + + TF (parser, 0); + TF (parser, 1); + TF (parser, 2); + TF (parser, 3); + TF (parser, 4); + TF (parser, 5); + TF (parser, 6); + TF (parser, 7); + TF (parser, 8); + TF (parser, 9); + TF (parser, 10); + TF (parser, 11); + TF (parser, 12); + TF (parser, 13); + TF (parser, 14); + TF (parser, 15); + TF (parser, 16); + TF (parser, 17); + TF (parser, 18); + TF (parser, 19); + TF (parser, 20); + TF (parser, 21); + TF (parser, 22); + + TF (sat, 0); + TF (sat, 1); + TF (sat, 2); + TF (sat, 3); + TF (sat, 4); + TF (sat, 5); + TF (sat, 6); + TF (sat, 7); + TF (sat, 8); + TF (sat, 9); + TF (sat, 10); + TF (sat, 11); + TF (sat, 12); + TF (sat, 13); + + TF (unit, 0); + TF (unit, 1); + TF (unit, 2); + TF (unit, 3); + + TF (prime, 4); + TF (prime, 9); + TF (prime, 25); + + TS (prime, 49); + TS (prime, 121); + TS (prime, 169); + TS (prime, 289); + TS (prime, 361); + TS (prime, 529); + TS (prime, 841); + TS (prime, 961); + TS (prime, 1369); + TS (prime, 1681); + TS (prime, 1849); + TS (prime, 2209); + + TF (add, 2); + TF (add, 4); + TS (add, 8); + TS (add, 16); + + TF (api, 0); + TF (api, 1); + TF (api, 2); + TF (api, 3); + TF (api, 4); + + if ((!suite.backspaces && suite.ok) || suite.failed) + line (); + + printf ("%d ok, %d failed, in %.2f seconds\n", + suite.ok, suite.failed, stop_timer (timer)); + + exit (0); + return 0; +} + +/*------------------------------------------------------------------------*/ +#endif +/*------------------------------------------------------------------------*/ Index: epan/dfilter/dfilter.h =================================================================== --- epan/dfilter/dfilter.h (revision 27811) +++ epan/dfilter/dfilter.h (working copy) @@ -91,4 +91,39 @@ void dfilter_dump(dfilter_t *df); +typedef enum { + /* display filter expression is unsatisfiable, i.e. the expression + * could only be FALSE. */ + DS_1_UNSAT, + + /* the NOT of display filter expression is unsatisfiable, i.e. the + * expression could only be TRUE. */ + DS_0_UNSAT, + + /* The expression could be either TRUE or FALSE. */ + DS_UNKNOWN, +} dcache_satres_t; + +/* Initialize and cleanup dcache. All previous dcaches are freed and + * dcache is set to empty. */ +void dcache_init(); +void dcache_cleanup(); + +/* Start 'dcache satisfy' and 'dcache save' processes so that + * dcache_save() and dcache_satisfy() will take effect. Without this + * call, these two routines will simply return. */ +void dcache_start_satisfy_save(dfilter_t *df); + +/* Stop 'dcache satisfy' and 'dcache save' processes. */ +void dcache_stop_satisfy_save(); + + +/* Return SAT results for current frame according to the info obtained + * in dcache and previous display results in dhistory. */ +dcache_satres_t dcache_satisfy(guint64 dhistory); + +/* Save 'passed' to nth bit of dhistory, n is current index of + * dcache. */ +void dcache_save(guint64 *dhistory, gboolean passed); + #endif Index: epan/dfilter/wslimmat.h =================================================================== --- epan/dfilter/wslimmat.h (revision 0) +++ epan/dfilter/wslimmat.h (revision 0) @@ -0,0 +1,121 @@ +#ifndef _limmat_h_INCLUDED +#define _limmat_h_INCLUDED + +/*------------------------------------------------------------------------*/ + +#include /* for 'FILE' */ +#include /* for 'size_t' */ + +/*------------------------------------------------------------------------*/ +/* In case the user program wants to print additional verbose output, it + * should use this prefix. + */ +#ifdef SAT2002FMT +#define LIMMAT_PREFIX "c " +#else +#define LIMMAT_PREFIX " " +#endif + +/*------------------------------------------------------------------------*/ + +typedef struct Limmat Limmat; + +/*------------------------------------------------------------------------*/ +/* Constructor and destructor for our SAT checker. If the 'log' is non zero + * we use it for logging status reports during satisfiability solving. + */ +Limmat *new_Limmat (FILE * log); +void delete_Limmat (Limmat *); +void set_log_Limmat (Limmat *, FILE * log); + +/*------------------------------------------------------------------------*/ + +const char *id_Limmat (void); /* RCS Id */ +const char *version_Limmat (void); +const char *copyright_Limmat (void); +const char *options_Limmat (void); + +/*------------------------------------------------------------------------*/ +/* After creation of a 'Limmat' you can read in a DIMACS file with + * 'read_Limmat'. The string given as third argument is supposed to be the + * name of the input file. It is used in error messages for parse errors. + * In case the FILE argument is zero, the library tries to open the file + * with this name. The name may be zero as well. In this case the file + * name is not included in the error message. The result is non zero if + * reading was succesfull. Otherwise '0' is returned and an error message + * is produced, that can be extracted with 'error_Limmat'. + */ +int read_Limmat (Limmat *, FILE *, const char *); +const char *error_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* Add a zero terminated list of literals to limmat. + */ +void add_Limmat (Limmat *, const int *clause); + +/*------------------------------------------------------------------------*/ +/* Print the current clause data base to the given file in DIMACS format. + */ +void print_Limmat (Limmat *, FILE *); + +/*------------------------------------------------------------------------*/ +/* Print some statistics. Call 'adjust_timer_Limmat' in case you want to + * include the time spent in an interrupted call. + */ +void stats_Limmat (Limmat *, FILE *); + +/*------------------------------------------------------------------------*/ +/* Print the setting of the parameters. They can all be controlled by + * environment variables. + */ +void strategy_Limmat (Limmat *, FILE *); + +/*------------------------------------------------------------------------*/ +/* Get the number of clauses and literals. + */ +int maxvar_Limmat (Limmat *); +int literals_Limmat (Limmat *); +int clauses_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* In a signal handler called by an interrupt you may want to adjust the + * time spent in the library before printing the statistics. Otherwise the + * time of the interrupted call is not included in the statistics. + */ +void adjust_timer_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* Get time spent in the library in seconds. Call 'adjust_timer_Limmat' in + * case you want to include the time spent in the library in an interrupted + * call. + */ +double time_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* Get number of currently allocated bytes in the library. + */ +size_t bytes_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* Determine satisfiability: 'sat_Limmat' returns '0' if the stored clauses + * are unsatisfiable. If a time out or space out occured a negative value + * is returned. Otherwise '1' is returned and a satisfying assignment has + * been found. The assignment can be extracted with 'assignment_Limmat' as + * a zero terminated list of literals. + * + * If 'max_decision' is less than 0, the number of decisions is unbounded. + * If 'max_decision' is zero, than only unit resolution on the toplevel is + * performed. In this case we still check whether all variables are already + * assigned without deriving a conflict. + */ +int sat_Limmat (Limmat *, int max_decisions); +const int *assignment_Limmat (Limmat *); + +/*------------------------------------------------------------------------*/ +/* Pretty print an assignment, a sequence of integers terminated by zero, by + * wrapping numbers at a 80 column margin. + */ +void print_assignment_Limmat (const int *, FILE *); + +/*------------------------------------------------------------------------*/ +#endif Index: epan/dfilter/sttype-pointer.c =================================================================== --- epan/dfilter/sttype-pointer.c (revision 27811) +++ epan/dfilter/sttype-pointer.c (working copy) @@ -27,7 +27,32 @@ #include "ftypes/ftypes.h" #include "syntax-tree.h" +#include +static gboolean +field_equal(gpointer f1, gpointer f2) +{ + header_field_info *hf1 = f1; + header_field_info *hf2 = f2; + + return g_strcmp0(hf1->abbrev, hf2->abbrev) == 0; +} + +static gboolean +fvalue_equal(gpointer f1, gpointer f2) +{ + fvalue_t *fv1 = f1; + fvalue_t *fv2 = f2; + + ftype_t *ft1 = fvalue_ftype(fv1); + ftype_t *ft2 = fvalue_ftype(fv2); + + if (ft1 != ft2) + return FALSE; + + return fvalue_eq(fv1, fv2); +} + void sttype_register_pointer(void) { @@ -36,12 +61,16 @@ "FIELD", NULL, NULL, + field_equal, + NULL, }; static sttype_t fvalue_type = { STTYPE_FVALUE, "FVALUE", NULL, NULL, + fvalue_equal, + NULL, }; sttype_register(&field_type); Index: epan/dfilter/sttype-function.c =================================================================== --- epan/dfilter/sttype-function.c (revision 27811) +++ epan/dfilter/sttype-function.c (working copy) @@ -73,7 +73,22 @@ g_free(stfuncrec); } +/* a conservative implementation. */ +static gboolean +function_equal(gpointer f1, gpointer f2) +{ + function_t *func1 = f1; + function_t *func2 = f2; + if (func1->funcdef != func2->funcdef) + return FALSE; + + if (func1->params != func2->params) + return FALSE; + + return TRUE; +} + /* Set the parameters for a function stnode_t. */ void sttype_function_set_params(stnode_t *node, GSList *params) @@ -118,6 +133,8 @@ "FUNCTION", function_new, function_free, + function_equal, + NULL, }; sttype_register(&function_type); Index: epan/dfilter/wslimboole.c =================================================================== --- epan/dfilter/wslimboole.c (revision 0) +++ epan/dfilter/wslimboole.c (revision 0) @@ -0,0 +1,1111 @@ +#include +#include +#include +#include +#include +#include + +/*------------------------------------------------------------------------*/ + +#include "wslimmat.h" + +/*------------------------------------------------------------------------*/ + +char *limboole_id = "$Id: limboole.c,v 1.15 2002/11/07 07:12:07 biere Exp $"; + +/*------------------------------------------------------------------------*/ +/* These are the node types we support. They are ordered in decreasing + * priority: if a parent with type t1 has a child with type t2 and t1 > t2, + * then pretty printing the parent requires parentheses. See 'pp_aux' for + * more details. + */ +enum Type +{ + VAR = 0, + LP = 1, + RP = 2, + NOT = 3, + AND = 4, + OR = 5, + IMPLIES = 6, + IFF = 7, + DONE = 8, + ERROR = 9, +}; + +/*------------------------------------------------------------------------*/ + +typedef enum Type Type; +typedef struct Node Node; +typedef union Data Data; + +/*------------------------------------------------------------------------*/ + +union Data +{ + char *as_name; /* variable data */ + Node *as_child[2]; /* operator data */ +}; + +/*------------------------------------------------------------------------*/ + +struct Node +{ + Type type; + int idx; /* tsetin index */ + Node *next; /* collision chain in hash table */ + Node *next_inserted; /* chronological list of hash table */ + Data data; +}; + +/*------------------------------------------------------------------------*/ + +typedef struct Mgr Mgr; + +struct Mgr +{ + unsigned nodes_size; + unsigned nodes_count; + int idx; + Node **nodes; + Node *first; + Node *last; + Node *root; + char *buffer; + char *name; + unsigned buffer_size; + unsigned buffer_count; + int saved_char; + int saved_char_is_valid; + int last_y; + int verbose; + unsigned x; + unsigned y; + Limmat *limmat; + const char *in; + int ngot; + int nchar; + FILE *log; + FILE *out; + int close_in; + int close_log; + int close_out; + Type token; + unsigned token_x; + unsigned token_y; + Node **idx2node; + int check_satisfiability; + int dump; +}; + +/*------------------------------------------------------------------------*/ + +static unsigned +hash_var (Mgr * mgr, const char *name) +{ + unsigned res, tmp; + const char *p; + + res = 0; + + for (p = name; *p; p++) + { + tmp = res & 0xf0000000; + res <<= 4; + res += *p; + if (tmp) + res ^= (tmp >> 28); + } + + res &= (mgr->nodes_size - 1); + assert (res < mgr->nodes_size); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static unsigned +hash_op (Mgr * mgr, Type type, Node * c0, Node * c1) +{ + unsigned res; + + res = (unsigned) type; + res += 4017271 * (unsigned) c0; + res += 70200511 * (unsigned) c1; + + res &= (mgr->nodes_size - 1); + assert (res < mgr->nodes_size); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static unsigned +hash (Mgr * mgr, Type type, void *c0, Node * c1) +{ + if (type == VAR) + return hash_var (mgr, (char *) c0); + else + return hash_op (mgr, type, c0, c1); +} + +/*------------------------------------------------------------------------*/ + +static int +eq_var (Node * n, const char *str) +{ + return n->type == VAR && !strcmp (n->data.as_name, str); +} + +/*------------------------------------------------------------------------*/ + +static int +eq_op (Node * n, Type type, Node * c0, Node * c1) +{ + return n->type == type && n->data.as_child[0] == c0 + && n->data.as_child[1] == c1; +} + +/*------------------------------------------------------------------------*/ + +static int +eq (Node * n, Type type, void *c0, Node * c1) +{ + if (type == VAR) + return eq_var (n, (char *) c0); + else + return eq_op (n, type, c0, c1); +} + +/*------------------------------------------------------------------------*/ + +static Node ** +find (Mgr * mgr, Type type, void *c0, Node * c1) +{ + Node **p, *n; + unsigned h; + + h = hash (mgr, type, c0, c1); + for (p = mgr->nodes + h; (n = *p); p = &n->next) + if (eq (n, type, c0, c1)) + break; + + return p; +} + +/*------------------------------------------------------------------------*/ + +static void +enlarge_nodes (Mgr * mgr) +{ + Node **old_nodes, *p, *next; + unsigned old_nodes_size, h, i; + + old_nodes = mgr->nodes; + old_nodes_size = mgr->nodes_size; + mgr->nodes_size *= 2; + mgr->nodes = (Node **) calloc (mgr->nodes_size, sizeof (Node *)); + + for (i = 0; i < old_nodes_size; i++) + { + for (p = old_nodes[i]; p; p = next) + { + next = p->next; + if (p->type == VAR) + h = hash_var (mgr, p->data.as_name); + else + h = + hash_op (mgr, p->type, p->data.as_child[0], + p->data.as_child[1]); + p->next = mgr->nodes[h]; + mgr->nodes[h] = p; + } + } + + free (old_nodes); +} + +/*------------------------------------------------------------------------*/ + +static void +insert (Mgr * mgr, Node * node) +{ + if (mgr->last) + mgr->last->next_inserted = node; + else + mgr->first = node; + mgr->last = node; + mgr->nodes_count++; +} + +/*------------------------------------------------------------------------*/ + +static Node * +var (Mgr * mgr, const char *str) +{ + Node **p, *n; + + if (mgr->nodes_size <= mgr->nodes_count) + enlarge_nodes (mgr); + + p = find (mgr, VAR, (void *) str, 0); + n = *p; + if (!n) + { + n = (Node *) malloc (sizeof (*n)); + memset (n, 0, sizeof (*n)); + n->type = VAR; + n->data.as_name = strdup (str); + + *p = n; + insert (mgr, n); + } + + return n; +} + +/*------------------------------------------------------------------------*/ + +static Node * +op (Mgr * mgr, Type type, Node * c0, Node * c1) +{ + Node **p, *n; + + if (mgr->nodes_size <= mgr->nodes_count) + enlarge_nodes (mgr); + + p = find (mgr, type, c0, c1); + n = *p; + if (!n) + { + n = (Node *) malloc (sizeof (*n)); + memset (n, 0, sizeof (*n)); + n->type = type; + n->data.as_child[0] = c0; + n->data.as_child[1] = c1; + + *p = n; + insert (mgr, n); + } + + return n; +} + +/*------------------------------------------------------------------------*/ + +static Mgr * +init (void) +{ + Mgr *res; + + res = (Mgr *) malloc (sizeof (*res)); + memset (res, 0, sizeof (*res)); + res->nodes_size = 2; + res->nodes = (Node **) calloc (res->nodes_size, sizeof (Node *)); + res->buffer_size = 2; + res->buffer = (char *) malloc (res->buffer_size); + res->in = NULL; + res->log = stderr; + res->out = stdout; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +connect_solver (Mgr * mgr) +{ + assert (!mgr->limmat); + mgr->limmat = new_Limmat (mgr->verbose ? mgr->log : 0); +} + +/*------------------------------------------------------------------------*/ + +static void +release (Mgr * mgr) +{ + Node *p, *next; + + if (mgr->limmat) + delete_Limmat (mgr->limmat); + + for (p = mgr->first; p; p = next) + { + next = p->next_inserted; + if (p->type == VAR) + free (p->data.as_name); + free (p); + } + + + if (mgr->close_out) + fclose (mgr->out); + if (mgr->close_log) + fclose (mgr->log); + + free (mgr->idx2node); + free (mgr->nodes); + free (mgr->buffer); + free (mgr); +} + +/*------------------------------------------------------------------------*/ + +static void +print_token (Mgr * mgr) +{ + switch (mgr->token) + { + case VAR: + fputs (mgr->buffer, mgr->log); + break; + case LP: + fputc ('(', mgr->log); + break; + case RP: + fputc (')', mgr->log); + break; + case NOT: + fputc ('!', mgr->log); + break; + case AND: + fputc ('&', mgr->log); + break; + case OR: + fputc ('|', mgr->log); + break; + case IMPLIES: + fputs ("->", mgr->log); + break; + case IFF: + fputs ("<->", mgr->log); + break; + default: + assert (mgr->token == DONE); + fputs ("EOF", mgr->log); + break; + } +} + +/*------------------------------------------------------------------------*/ + +static void +parse_error (Mgr * mgr, const char *fmt, ...) +{ + va_list ap; + char *name; + + name = mgr->name ? mgr->name : ""; + fprintf (mgr->log, "%s:%u:%u: ", name, mgr->token_x + 1, mgr->token_y); + if (mgr->token == ERROR) + fputs ("scan error: ", mgr->log); + else + { + fputs ("parse error at '", mgr->log); + print_token (mgr); + fputs ("' ", mgr->log); + } + va_start (ap, fmt); + vfprintf (mgr->log, fmt, ap); + va_end (ap); + fputc ('\n', mgr->log); +} + +/*------------------------------------------------------------------------*/ + +static int +is_var_letter (int ch) +{ + if (isalnum (ch)) + return 1; + + switch (ch) + { + case '-': + case '_': + case '.': + case '[': + case ']': + case '$': + case '@': + return 1; + + default: + return 0; + } +} + +/*------------------------------------------------------------------------*/ + +static void +enlarge_buffer (Mgr * mgr) +{ + mgr->buffer_size *= 2; + mgr->buffer = (char *) realloc (mgr->buffer, mgr->buffer_size); +} + +/*------------------------------------------------------------------------*/ +static int +get_char(Mgr * mgr) +{ + if (mgr->ngot >= mgr->nchar) + return EOF; + else + return mgr->in[mgr->ngot++]; +} + +static int +next_char (Mgr * mgr) +{ + int res; + + mgr->last_y = mgr->y; + + if (mgr->saved_char_is_valid) + { + mgr->saved_char_is_valid = 0; + res = mgr->saved_char; + } + else + res = get_char (mgr); + + if (res == '\n') + { + mgr->x++; + mgr->y = 0; + } + else + mgr->y++; + + return res; +} + +/*------------------------------------------------------------------------*/ + +static void +unget_char (Mgr * mgr, int ch) +{ + assert (!mgr->saved_char_is_valid); + + mgr->saved_char_is_valid = 1; + mgr->saved_char = ch; + + if (ch == '\n') + { + mgr->x--; + mgr->y = mgr->last_y; + } + else + mgr->y--; +} + +/*------------------------------------------------------------------------*/ + +static void +next_token (Mgr * mgr) +{ + int ch; + + mgr->token = ERROR; + ch = next_char (mgr); + +RESTART_NEXT_TOKEN: + + while (isspace ((int) ch)) + ch = next_char (mgr); + + if (ch == '%') + { + while ((ch = next_char (mgr)) != '\n' && ch != EOF) + ; + + goto RESTART_NEXT_TOKEN; + } + + mgr->token_x = mgr->x; + mgr->token_y = mgr->y; + + if (ch == EOF) + mgr->token = DONE; + else if (ch == '<') + { + if (next_char (mgr) != '-') + parse_error (mgr, "expected '-' after '<'"); + else if (next_char (mgr) != '>') + parse_error (mgr, "expected '>' after '-'"); + else + mgr->token = IFF; + } + else if (ch == '-') + { + if (next_char (mgr) != '>') + parse_error (mgr, "expected '>' after '-'"); + else + mgr->token = IMPLIES; + } + else if (ch == '&') + { + mgr->token = AND; + } + else if (ch == '|') + { + mgr->token = OR; + } + else if (ch == '!' || ch == '~') + { + mgr->token = NOT; + } + else if (ch == '(') + { + mgr->token = LP; + } + else if (ch == ')') + { + mgr->token = RP; + } + else if (is_var_letter (ch)) + { + mgr->buffer_count = 0; + + while (is_var_letter (ch)) + { + if (mgr->buffer_size <= mgr->buffer_count + 1) + enlarge_buffer (mgr); + + mgr->buffer[mgr->buffer_count++] = ch; + ch = next_char (mgr); + } + + unget_char (mgr, ch); + mgr->buffer[mgr->buffer_count] = 0; + + if (mgr->buffer[mgr->buffer_count - 1] == '-') + parse_error (mgr, "variable '%s' ends with '-'", mgr->buffer); + else + mgr->token = VAR; + } + else + parse_error (mgr, "invalid character '%c'", ch); +} + +/*------------------------------------------------------------------------*/ + +static Node *parse_expr (Mgr *); + +/*------------------------------------------------------------------------*/ + +static Node * +parse_basic (Mgr * mgr) +{ + Node *child; + Node *res; + + res = 0; + + if (mgr->token == LP) + { + next_token (mgr); + child = parse_expr (mgr); + if (mgr->token != RP) + { + if (mgr->token != ERROR) + parse_error (mgr, "expected ')'"); + } + else + res = child; + next_token (mgr); + } + else if (mgr->token == VAR) + { + res = var (mgr, mgr->buffer); + next_token (mgr); + } + else if (mgr->token != ERROR) + parse_error (mgr, "expected variable or '('"); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_not (Mgr * mgr) +{ + Node *child, *res; + + if (mgr->token == NOT) + { + next_token (mgr); + child = parse_not (mgr); + if (child) + res = op (mgr, NOT, child, 0); + else + res = 0; + } + else + res = parse_basic (mgr); + + return res; +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_associative_op (Mgr * mgr, Type type, Node * (*lower) (Mgr *)) +{ + Node *res, *child; + int done; + + res = 0; + done = 0; + + do + { + child = lower (mgr); + if (child) + { + res = res ? op (mgr, type, res, child) : child; + if (mgr->token == type) + next_token (mgr); + else + done = 1; + } + else + res = 0; + } + while (res && !done); + + return res; +} + + +/*------------------------------------------------------------------------*/ + +static Node * +parse_and (Mgr * mgr) +{ + return parse_associative_op (mgr, AND, parse_not); +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_or (Mgr * mgr) +{ + return parse_associative_op (mgr, OR, parse_and); +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_implies (Mgr * mgr) +{ + Node *l, *r; + + if (!(l = parse_or (mgr))) + return 0; + if (mgr->token != IMPLIES) + return l; + next_token (mgr); + if (!(r = parse_or (mgr))) + return 0; + + return op (mgr, IMPLIES, l, r); +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_iff (Mgr * mgr) +{ + return parse_associative_op (mgr, IFF, parse_implies); +} + +/*------------------------------------------------------------------------*/ + +static Node * +parse_expr (Mgr * mgr) +{ + return parse_iff (mgr); +} + +/*------------------------------------------------------------------------*/ + +static int +parse (Mgr * mgr) +{ + next_token (mgr); + + if (mgr->token == ERROR) + return 0; + + if (!(mgr->root = parse_expr (mgr))) + return 0; + + if (mgr->token == DONE) + return 1; + + if (mgr->token != ERROR) + parse_error (mgr, "expected operator or EOF"); + + return 0; +} + +/*------------------------------------------------------------------------*/ + +static void +unit_clause (Mgr * mgr, int a) +{ + int clause[2]; + + clause[0] = a; + clause[1] = 0; + + add_Limmat (mgr->limmat, clause); + + if (mgr->dump) + fprintf (mgr->out, "%d 0\n", a); +} + +/*------------------------------------------------------------------------*/ + +static void +binary_clause (Mgr * mgr, int a, int b) +{ + int clause[3]; + + clause[0] = a; + clause[1] = b; + clause[2] = 0; + + add_Limmat (mgr->limmat, clause); + + if (mgr->dump) + fprintf (mgr->out, "%d %d 0\n", a, b); +} + +/*------------------------------------------------------------------------*/ + +static void +ternary_clause (Mgr * mgr, int a, int b, int c) +{ + int clause[4]; + + clause[0] = a; + clause[1] = b; + clause[2] = c; + clause[3] = 0; + + add_Limmat (mgr->limmat, clause); + + if (mgr->dump) + fprintf (mgr->out, "%d %d %d 0\n", a, b, c); +} + +/*------------------------------------------------------------------------*/ + +static void +tsetin (Mgr * mgr) +{ + int num_clauses; + int sign; + Node *p; + + num_clauses = 0; + + for (p = mgr->first; p; p = p->next_inserted) + { + p->idx = ++mgr->idx; + + if (mgr->dump && p->type == VAR) + fprintf (mgr->out, "c %d %s\n", p->idx, p->data.as_name); + + switch (p->type) + { + case IFF: + num_clauses += 4; + break; + case OR: + case AND: + case IMPLIES: + num_clauses += 3; + break; + case NOT: + num_clauses += 2; + break; + default: + assert (p->type == VAR); + break; + } + } + + mgr->idx2node = (Node **) calloc (mgr->idx + 1, sizeof (Node *)); + for (p = mgr->first; p; p = p->next_inserted) + mgr->idx2node[p->idx] = p; + + if (mgr->dump) + fprintf (mgr->out, "p cnf %d %u\n", mgr->idx, num_clauses + 1); + + for (p = mgr->first; p; p = p->next_inserted) + { + switch (p->type) + { + case IFF: + ternary_clause (mgr, p->idx, + -p->data.as_child[0]->idx, + -p->data.as_child[1]->idx); + ternary_clause (mgr, p->idx, p->data.as_child[0]->idx, + p->data.as_child[1]->idx); + ternary_clause (mgr, -p->idx, -p->data.as_child[0]->idx, + p->data.as_child[1]->idx); + ternary_clause (mgr, -p->idx, p->data.as_child[0]->idx, + -p->data.as_child[1]->idx); + break; + case IMPLIES: + binary_clause (mgr, p->idx, p->data.as_child[0]->idx); + binary_clause (mgr, p->idx, -p->data.as_child[1]->idx); + ternary_clause (mgr, -p->idx, + -p->data.as_child[0]->idx, + p->data.as_child[1]->idx); + break; + case OR: + binary_clause (mgr, p->idx, -p->data.as_child[0]->idx); + binary_clause (mgr, p->idx, -p->data.as_child[1]->idx); + ternary_clause (mgr, -p->idx, + p->data.as_child[0]->idx, p->data.as_child[1]->idx); + break; + case AND: + binary_clause (mgr, -p->idx, p->data.as_child[0]->idx); + binary_clause (mgr, -p->idx, p->data.as_child[1]->idx); + ternary_clause (mgr, p->idx, + -p->data.as_child[0]->idx, + -p->data.as_child[1]->idx); + break; + case NOT: + binary_clause (mgr, p->idx, p->data.as_child[0]->idx); + binary_clause (mgr, -p->idx, -p->data.as_child[0]->idx); + break; + default: + assert (p->type == VAR); + break; + } + } + + assert (mgr->root); + + sign = (mgr->check_satisfiability) ? 1 : -1; + unit_clause (mgr, sign * mgr->root->idx); +} + +/*------------------------------------------------------------------------*/ + +static void +pp_aux (Mgr * mgr, Node * node, Type outer) +{ + int le, lt; + + le = outer <= node->type; + lt = outer < node->type; + + switch (node->type) + { + case NOT: + fputc ('!', mgr->out); + pp_aux (mgr, node->data.as_child[0], node->type); + break; + case IMPLIES: + case IFF: + if (le) + fputc ('(', mgr->out); + pp_aux (mgr, node->data.as_child[0], node->type); + fputs (node->type == IFF ? " <-> " : " -> ", mgr->out); + pp_aux (mgr, node->data.as_child[1], node->type); + if (le) + fputc (')', mgr->out); + break; + + case OR: + case AND: + if (lt) + fputc ('(', mgr->out); + pp_aux (mgr, node->data.as_child[0], node->type); + fputs (node->type == OR ? " | " : " & ", mgr->out); + pp_aux (mgr, node->data.as_child[1], node->type); + if (lt) + fputc (')', mgr->out); + break; + + default: + assert (node->type == VAR); + fprintf (mgr->out, "%s", node->data.as_name); + break; + } +} + +/*------------------------------------------------------------------------*/ + +static void +pp_and (Mgr * mgr, Node * node) +{ + if (node->type == AND) + { + pp_and (mgr, node->data.as_child[0]); + fprintf (mgr->out, "\n&\n"); + pp_and (mgr, node->data.as_child[1]); + } + else + pp_aux (mgr, node, AND); +} + +/*------------------------------------------------------------------------*/ + +static void +pp_or (Mgr * mgr, Node * node) +{ + if (node->type == OR) + { + pp_or (mgr, node->data.as_child[0]); + fprintf (mgr->out, "\n|\n"); + pp_or (mgr, node->data.as_child[1]); + } + else + pp_aux (mgr, node, OR); +} + +/*------------------------------------------------------------------------*/ + +static void +pp_and_or (Mgr * mgr, Node * node, Type outer) +{ + assert (outer > AND); + assert (outer > OR); + + if (node->type == AND) + pp_and (mgr, node); + else if (node->type == OR) + pp_or (mgr, node); + else + pp_aux (mgr, node, outer); +} + +/*------------------------------------------------------------------------*/ + +static void +pp_iff_implies (Mgr * mgr, Node * node, Type outer) +{ + if (node->type == IFF || node->type == IMPLIES) + { + pp_and_or (mgr, node->data.as_child[0], node->type); + fprintf (mgr->out, "\n%s\n", node->type == IFF ? "<->" : "->"); + pp_and_or (mgr, node->data.as_child[1], node->type); + } + else + pp_and_or (mgr, node, outer); +} + +/*------------------------------------------------------------------------*/ + +static void _U_ +pp (Mgr * mgr) +{ + assert (mgr->root); + pp_iff_implies (mgr, mgr->root, DONE); + fputc ('\n', mgr->out); +} + +/*------------------------------------------------------------------------*/ + +static void +print_assignment (Mgr * mgr, const int *assignment) +{ + const int *p; + Node *n; + int val; + int idx; + + for (p = assignment; *p; p++) + { + idx = *p; + if (idx < 0) + { + idx = -idx; + val = 0; + } + else + val = 1; + + assert (idx > 0); + assert (idx <= mgr->idx); + + n = mgr->idx2node[idx]; + if (n->type == VAR) + fprintf (mgr->out, "%s = %d\n", n->data.as_name, val); + } +} + +/*------------------------------------------------------------------------*/ +/* + * 0 - unsatisfiable + * 1 - satisfiable + * -1 - error input + */ + +int +boolean_satisfy (const char *exp, int len) +{ + const int *assignment; + int result = 0; + int satres = 0; + + Mgr *mgr = init (); + mgr->check_satisfiability = 1; + mgr->in = exp; + mgr->nchar = len; + + if (!parse (mgr)) + goto fail; + + connect_solver (mgr); + tsetin (mgr); + + satres = sat_Limmat (mgr->limmat, -1 /* max_decisions */); + + if (satres < 0) + { + goto fail; + } + else if (satres == 1) + { + assignment = assignment_Limmat (mgr->limmat); + print_assignment (mgr, assignment); + + result = 1; + } + else + { + result = 0; + } + + goto done; + +fail: + result = -1; +done: + release (mgr); + return result; +} + + +/* for test */ + +int limboole(int argc _U_ , char **argv _U_) +{ + const char exp3[] = "(v0 & !v0)"; + printf("result 3 is %d\n", boolean_satisfy(exp3, strlen(exp3))); + + return 0; +} + Index: epan/dfilter/grammar.lemon =================================================================== --- epan/dfilter/grammar.lemon (revision 27811) +++ epan/dfilter/grammar.lemon (working copy) @@ -103,6 +103,7 @@ case STTYPE_NUM_TYPES: case STTYPE_RANGE: case STTYPE_FVALUE: + case STTYPE_SAT: g_assert_not_reached(); break; } Index: epan/dfilter/semcheck.c =================================================================== --- epan/dfilter/semcheck.c (revision 27811) +++ epan/dfilter/semcheck.c (working copy) @@ -325,6 +325,7 @@ case STTYPE_INTEGER: case STTYPE_FVALUE: case STTYPE_NUM_TYPES: + case STTYPE_SAT: g_assert_not_reached(); } } Index: epan/dfilter/sttype-range.c =================================================================== --- epan/dfilter/sttype-range.c (revision 27811) +++ epan/dfilter/sttype-range.c (working copy) @@ -71,6 +71,38 @@ g_free(range); } +static gboolean +hfinfo_equal(header_field_info *hf1, header_field_info *hf2) +{ + if (hf1 == hf2) + return TRUE; + + if ((hf1 == NULL && hf2 != NULL) || + (hf1 != NULL && hf2 == NULL)) + return FALSE; + + return g_strcmp0(hf1->abbrev, hf2->abbrev) == 0; +} + +static gboolean +range_equal(gpointer n1, gpointer n2) +{ + range_t *r1 = n1; + range_t *r2 = n2; + + assert_magic(r1, RANGE_MAGIC); + assert_magic(r2, RANGE_MAGIC); + + + if (!hfinfo_equal(r1->hfinfo, r2->hfinfo)) + return FALSE; + + if (!drange_equal(r1->drange, r2->drange)) + return FALSE; + + return TRUE; +} + void sttype_range_remove_drange(stnode_t *node) { @@ -116,6 +148,8 @@ "RANGE", range_new, range_free, + range_equal, + NULL, }; sttype_register(&range_type); Index: epan/dfilter/Makefile.common =================================================================== --- epan/dfilter/Makefile.common (revision 27811) +++ epan/dfilter/Makefile.common (working copy) @@ -42,8 +42,11 @@ sttype-range.c \ sttype-string.c \ sttype-test.c \ - syntax-tree.c - + sttype-sat.c \ + syntax-tree.c \ + wslimmat.c \ + wslimboole.c + # Header files that are not generated from other files NONGENERATED_HEADER_FILES = \ dfilter.h \ @@ -57,7 +60,8 @@ sttype-function.h \ sttype-range.h \ sttype-test.h \ - syntax-tree.h + syntax-tree.h \ + wslimmat.h # Files that generate compileable files GENERATOR_FILES = \ Index: epan/dfilter/dfilter-int.h =================================================================== --- epan/dfilter/dfilter-int.h (revision 27811) +++ epan/dfilter/dfilter-int.h (working copy) @@ -31,6 +31,7 @@ /* Passed back to user */ struct _dfilter_t { + stnode_t *st_root; GPtrArray *insns; GPtrArray *consts; int num_registers; Index: epan/Makefile.am =================================================================== --- epan/Makefile.am (revision 27811) +++ epan/Makefile.am (working copy) @@ -137,7 +137,7 @@ libwireshark_asmopt.la crc/libcrc.la crypt/libairpdcap.la \ ftypes/libftypes.la dfilter/libdfilter.la dissectors/libdissectors.la \ dissectors/libdirtydissectors.la $(wslua_lib) \ - ${top_builddir}/wsutil/libwsutil.la + ${top_builddir}/wsutil/libwsutil.la #EXTRA_PROGRAMS = reassemble_test #reassemble_test_LDADD = $(GLIB_LIBS) Index: epan/frame_data.h =================================================================== --- epan/frame_data.h (revision 27811) +++ epan/frame_data.h (working copy) @@ -59,6 +59,7 @@ } flags; void *color_filter; /* Per-packet matching color_filter_t object */ col_expr_t col_expr; /* Column expressions & values */ + guint64 dhistory; /* display history, 1 for passed, 0 for not-passed. nth history is mapped to nth dcache. */ } frame_data; /* Index: file.c =================================================================== --- file.c (revision 27811) +++ file.c (working copy) @@ -415,7 +415,7 @@ volatile gint64 progbar_nextstep; volatile gint64 progbar_quantum; dfilter_t *dfcode; - + /* Compile the current display filter. * We assume this will not fail since cf->dfilter is only set in * cf_filter IFF the filter was valid. @@ -915,8 +915,9 @@ { gint row; gboolean create_proto_tree = FALSE; - epan_dissect_t *edt; - + epan_dissect_t *edt = NULL; + dcache_satres_t sattype; + /* just add some value here until we know if it is being displayed or not */ fdata->cum_bytes = cum_bytes + fdata->pkt_len; @@ -955,57 +956,77 @@ this packet. */ nstime_delta(&fdata->del_dis_ts, &fdata->abs_ts, &prev_dis_ts); - /* If either + sattype = dcache_satisfy(fdata->dhistory); - we have a display filter and are re-applying it; + if (sattype == DS_1_UNSAT && !fdata->flags.ref_time) { + /* sattype is DS_1_UNSAT, that is 'passed_filter == 1' can not + * be satisfied. And this frame is not marked as a time + * reference frame, therefore there's no need to dissect it. */ + fdata->flags.passed_dfilter = 0; + } else { + /* sattype is either + 1. DS_UNKNOWN, we need dissect and filter. + 2. DS_0_UNSAT, we need dissect only - we have a list of color filters; + or this frame is marked as a time reference frame. + */ + + /* If either - we have tap listeners; + we have a display filter and are re-applying it; - we have custom columns; + we have a list of color filters; - allocate a protocol tree root node, so that we'll construct - a protocol tree against which a filter expression can be - evaluated. */ - if ((dfcode != NULL && refilter) || color_filters_used() - || num_tap_filters != 0 || have_custom_cols(&cf->cinfo)) - create_proto_tree = TRUE; + we have tap listeners; - /* Dissect the frame. */ - edt = epan_dissect_new(create_proto_tree, FALSE); + we have custom columns; - if (dfcode != NULL && refilter) { - epan_dissect_prime_dfilter(edt, dfcode); - } - /* prepare color filters */ - if (color_filters_used()) { - color_filters_prime_edt(edt); - } + allocate a protocol tree root node, so that we'll construct + a protocol tree against which a filter expression can be + evaluated. */ - col_custom_prime_edt(edt, &cf->cinfo); + if ((dfcode != NULL && refilter) || color_filters_used() + || num_tap_filters != 0 || have_custom_cols(&cf->cinfo)) + create_proto_tree = TRUE; + + /* Dissect the frame. */ + edt = epan_dissect_new(create_proto_tree, FALSE); + + if (dfcode != NULL && refilter) { + epan_dissect_prime_dfilter(edt, dfcode); + } + /* prepare color filters */ + if (color_filters_used()) { + color_filters_prime_edt(edt); + } - tap_queue_init(edt); - epan_dissect_run(edt, pseudo_header, buf, fdata, &cf->cinfo); - tap_push_tapped_queue(edt); + col_custom_prime_edt(edt, &cf->cinfo); + + tap_queue_init(edt); + epan_dissect_run(edt, pseudo_header, buf, fdata, &cf->cinfo); + tap_push_tapped_queue(edt); - /* If we have a display filter, apply it if we're refiltering, otherwise - leave the "passed_dfilter" flag alone. + /* If we have a display filter, apply it if we're refiltering, otherwise + leave the "passed_dfilter" flag alone. - If we don't have a display filter, set "passed_dfilter" to 1. */ - if (dfcode != NULL) { - if (refilter) { - fdata->flags.passed_dfilter = dfilter_apply_edt(dfcode, edt) ? 1 : 0; - } - } else - fdata->flags.passed_dfilter = 1; - + If we don't have a display filter, set "passed_dfilter" to 1. */ + if (dfcode != NULL) { + if (refilter) { + if (sattype == DS_0_UNSAT) + fdata->flags.passed_dfilter = 1; + else + fdata->flags.passed_dfilter = dfilter_apply_edt(dfcode, edt) ? 1 : 0; + } + } else + fdata->flags.passed_dfilter = 1; + } + if( (fdata->flags.passed_dfilter) - || (edt->pi.fd->flags.ref_time) ){ + || (fdata->flags.ref_time) ){ /* This frame either passed the display filter list or is marked as a time reference frame. All time reference frames are displayed even if they dont pass the display filter */ - if(edt->pi.fd->flags.ref_time){ + if(fdata->flags.ref_time){ /* if this was a TIME REF frame we should reset the cul bytes field */ cum_bytes = fdata->pkt_len; fdata->cum_bytes = cum_bytes; @@ -1062,10 +1083,11 @@ * we do both to make sure that when a packet gets un-marked, the * color will be correctly set (fixes bug 2038) */ - fdata->color_filter = color_filters_colorize_packet(row, edt); - if (fdata->flags.marked) { - packet_list_set_colors(row, &prefs.gui_marked_fg, &prefs.gui_marked_bg); - } + fdata->color_filter = color_filters_colorize_packet(row, edt); + + if (fdata->flags.marked) { + packet_list_set_colors(row, &prefs.gui_marked_fg, &prefs.gui_marked_bg); + } /* Set the time of the previous displayed frame to the time of this frame. */ @@ -1077,7 +1099,12 @@ to the clist, and thus has no row. */ row = -1; } - epan_dissect_free(edt); + + if (edt) + epan_dissect_free(edt); + + dcache_save(&fdata->dhistory, fdata->flags.passed_dfilter); + return row; } @@ -1116,7 +1143,8 @@ fdata->abs_ts.secs = phdr->ts.secs; fdata->abs_ts.nsecs = phdr->ts.nsecs; - + fdata->dhistory = 0; + if (cf->plist_end != NULL) nstime_delta(&fdata->del_cap_ts, &fdata->abs_ts, &cf->plist_end->abs_ts); else @@ -1544,6 +1572,13 @@ init_dissection(); } + if (dfcode != NULL) { + if (redissect) + dcache_cleanup(); + + dcache_start_satisfy_save(dfcode); + } + /* Freeze the packet list while we redo it, so we don't get any screen updates while it happens. */ packet_list_freeze(); @@ -1648,6 +1683,8 @@ g_slist_free(fdata->pfd); fdata->pfd = NULL; } + + fdata->dhistory = 0; } if (!wtap_seek_read (cf->wth, fdata->file_off, &cf->pseudo_header, @@ -1768,6 +1805,7 @@ /* Cleanup and release all dfilter resources */ if (dfcode != NULL){ + dcache_stop_satisfy_save(); dfilter_free(dfcode); } }