diff --git a/primitives/cnf.in b/primitives/cnf.in new file mode 100644 index 0000000..c108c38 --- /dev/null +++ b/primitives/cnf.in @@ -0,0 +1,5 @@ +p cnf 4 3 +-1 2 0 +-2 -3 0 +3 -4 0 +0 diff --git a/primitives/include/sat_api.h b/primitives/include/sat_api.h index f36efc1..b3f588d 100644 --- a/primitives/include/sat_api.h +++ b/primitives/include/sat_api.h @@ -51,13 +51,10 @@ typedef double c2dWmc; //for (weighted) model count ******************************************************************************/ typedef struct var { - - // ... TO DO ... - //c2dSize index; variable index (you can change the variable name as you wish) - - BOOLEAN mark; //THIS FIELD MUST STAY AS IS + c2dSize index; + BOOLEAN mark; //THIS FIELD MUST STAY AS IS } Var; /****************************************************************************** @@ -69,11 +66,11 @@ typedef struct var { ******************************************************************************/ typedef struct literal { - - // ... TO DO ... - //c2dLiteral index; literal index (you can change the variable name as you wish) + c2dLiteral index; + c2dLiteral decision_level; + Var* var; } Lit; /****************************************************************************** @@ -87,12 +84,15 @@ typedef struct literal { ******************************************************************************/ typedef struct clause { - - // ... TO DO ... - //c2dSize index; clause index (you can change the variable name as you wish) + c2dSize index; + //Lit** literals; literal array (you can change the variable name as you wish) - + Lit** literals; + + // size of literals + c2dSize size; + BOOLEAN mark; //THIS FIELD MUST STAY AS IS } Clause; @@ -104,8 +104,10 @@ typedef struct clause { ******************************************************************************/ typedef struct sat_state_t { + c2dSize num_vars; + c2dSize num_clauses; - // ... TO DO ... + c2dSize cur_level; } SatState; diff --git a/primitives/src/sat_api.c b/primitives/src/sat_api.c index ceab82d..3e7f5d4 100644 --- a/primitives/src/sat_api.c +++ b/primitives/src/sat_api.c @@ -17,43 +17,28 @@ //returns a variable structure for the corresponding index Var* sat_index2var(c2dSize index, const SatState* sat_state) { - - // ... TO DO ... - - return NULL; //dummy valued + return NULL; } //returns the index of a variable c2dSize sat_var_index(const Var* var) { - - // ... TO DO ... - - return 0; //dummy valued + return 0; } //returns the variable of a literal Var* sat_literal_var(const Lit* lit) { - - // ... TO DO ... - - return NULL; //dummy valued + return NULL; } //returns 1 if the variable is instantiated, 0 otherwise //a variable is instantiated either by decision or implication (by unit resolution) BOOLEAN sat_instantiated_var(const Var* var) { - - // ... TO DO ... - - return 0; //dummy valued + return 0; } //returns 1 if all the clauses mentioning the variable are subsumed, 0 otherwise BOOLEAN sat_irrelevant_var(const Var* var) { - - // ... TO DO ... - - return 0; //dummy valued + return 0; } //returns the number of variables in the cnf of sat state @@ -67,10 +52,7 @@ c2dSize sat_var_count(const SatState* sat_state) { //returns the number of clauses mentioning a variable //a variable is mentioned by a clause if one of its literals appears in the clause c2dSize sat_var_occurences(const Var* var) { - - // ... TO DO .. - - return 0; //dummy valued + return 0; } //returns the index^th clause that mentions a variable @@ -97,10 +79,7 @@ Lit* sat_index2literal(c2dLiteral index, const SatState* sat_state) { //returns the index of a literal c2dLiteral sat_literal_index(const Lit* lit) { - - // ... TO DO ... - - return 0; //dummy valued + return 0; } //returns the positive literal of a variable @@ -246,15 +225,18 @@ Clause* sat_assert_clause(Clause* clause, SatState* sat_state) { //constructs a SatState from an input cnf file SatState* sat_state_new(const char* file_name) { - // ... TO DO ... - + // FILE *file = fopen(file_name, "r") + + // SatState* state = malloc(sizeof(SatState)); + + // fclose(file); + printf("gcc test.c -std=c99 -O2 -Wall -Iinclude -Llib -lsat -o test\n"); + return NULL; //dummy valued } //frees the SatState void sat_state_free(SatState* sat_state) { - - // ... TO DO ... return; //dummy valued } diff --git a/primitives/test.c b/primitives/test.c new file mode 100644 index 0000000..893a0c6 --- /dev/null +++ b/primitives/test.c @@ -0,0 +1,11 @@ +#include "sat_api.h" + +void TEST_READ_FILE() { + printf("CAO\n"); + sat_state_new("cnf.in"); +} + +int main() { + TEST_READ_FILE(); + return 0; +} diff --git a/primitives/test.sh b/primitives/test.sh new file mode 100755 index 0000000..d9b8e6b --- /dev/null +++ b/primitives/test.sh @@ -0,0 +1,6 @@ +make clean +make +cp libsat.a ./lib + +gcc test.c -std=c99 -O2 -Wall -Iinclude -Llib -lsat -o test +./test