test process

primitives/cnf.in

@@ -0,0 +1,5 @@
+p cnf 4 3
+-1 2 0
+-2 -3 0
+3 -4 0
+0

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;
 

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
 }

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;
+}

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