ipasir interface for d

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "ipasir"]
+	path = ipasir
+	url = git@github.com:biotomas/ipasir.git

dub.json

@@ -0,0 +1,15 @@
+{
+	"authors": [
+		"Alexander Weigl"
+	],
+	"copyright": "Copyright © 2019, Alexander Weigl",
+	"description": "A minimal D application.",
+	"license": "proprietary",
+	"name": "ipasir-d",
+	"sourceFiles": ["source/app.d", 
+		"source/ipasirc.d", 
+		"source/ipasir.d", 
+		"ipasir/sat/minisat220/libipasirminisat220.a"
+	]
+
+}

source/app.d

@@ -0,0 +1,8 @@
+import std.stdio;
+import ipasir;
+//dmd -fPIC -L-lstdc++ ipasir/sat/minisat220/libipasirminisat220.a  source/app.d source/ipasirc.d source/ipasir.d
+void main()
+{
+	auto s = new Solver();
+	writeln(s.signature());
+}

source/ipasir.d

@@ -0,0 +1,66 @@
+import std.conv;
+import ipasirc;
+
+alias Literal = int;
+alias Clause = Literal[];
+
+class Solver {
+    private void* internalSolver;
+    private Literal maximum;
+
+    this() {
+        this.internalSolver = ipasir_init();
+    }
+
+    ~this() {
+        ipasir_release(internalSolver);
+    }
+
+    string signature() {
+        return to!string(ipasir_signature());
+    }
+
+    void add(in Clause clause){
+        if(clause.length>0) {
+            foreach(lit; clause)
+                ipasir_add(this.internalSolver, lit);
+            ipasir_add(this.internalSolver, 0);
+        }
+    }
+
+    void assume(in Literal lit) {
+        void ipasir_assume (void * solver, int lit);
+    }
+
+
+    void assume(in Clause clause) {
+        void ipasir_assume (void * solver, int lit);
+    }
+
+
+    int solve(){
+        return ipasir_solve(this.internalSolver);
+    }
+
+
+    int get_value(Literal l){
+        return ipasir_val(this.internalSolver, l);
+    }
+
+    int[] model(){
+        int[] model;
+        for(int i = 1; i <= maximum; i++ ){
+            model ~= get_value(i);
+        }
+        return model;
+    }
+
+    void set_terminate(S=void)(S* state, int function(void* state) terminate) {
+        ipasir_set_terminate(this.internalSolver, state, terminate);
+    }
+
+    void set_learn(S=void)(S* state, int max_length, void function(S* state, int* clause) callback){
+        ipasir_set_learn (this.internalSolver, cast(void*) state, max_length, callback);
+    }
+
+}

source/ipasirc.d

@@ -0,0 +1,126 @@
+extern (C) {
+/**
+ * Return the name and the version of the incremental SAT
+ * solving library.
+ */
+const(char*) ipasir_signature ();
+
+/**
+ * Construct a new solver and return a pointer to it.
+ * Use the returned pointer as the first parameter in each
+ * of the following functions.
+ *
+ * Required state: N/A
+ * State after: INPUT
+ */
+void* ipasir_init ();
+
+/**
+ * Release the solver, i.e., all its resoruces and
+ * allocated memory (destructor). The solver pointer
+ * cannot be used for any purposes after this call.
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: undefined
+ */
+void ipasir_release (void* solver);
+
+/**
+ * Add the given literal into the currently added clause
+ * or finalize the clause with a 0.  Clauses added this way
+ * cannot be removed. The addition of removable clauses
+ * can be simulated using activation literals and assumptions.
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: INPUT
+ *
+ * Literals are encoded as (non-zero) integers as in the
+ * DIMACS formats.  They have to be smaller or equal to
+ * INT_MAX and strictly larger than INT_MIN (to avoid
+ * negation overflow).  This applies to all the literal
+ * arguments in API functions.
+ */
+void ipasir_add (void * solver, int lit_or_zero);
+
+/**
+ * Add an assumption for the next SAT search (the next call
+ * of ipasir_solve). After calling ipasir_solve all the
+ * previously added assumptions are cleared.
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: INPUT
+ */
+void ipasir_assume (void * solver, int lit);
+
+/**
+ * Solve the formula with specified clauses under the specified assumptions.
+ * If the formula is satisfiable the function returns 10 and the state of the solver is changed to SAT.
+ * If the formula is unsatisfiable the function returns 20 and the state of the solver is changed to UNSAT.
+ * If the search is interrupted (see ipasir_set_terminate) the function returns 0 and the state of the solver remains INPUT.
+ * This function can be called in any defined state of the solver.
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: INPUT or SAT or UNSAT
+ */
+int ipasir_solve (void * solver);
+
+/**
+ * Get the truth value of the given literal in the found satisfying
+ * assignment. Return 'lit' if True, '-lit' if False, and 0 if not important.
+ * This function can only be used if ipasir_solve has returned 10
+ * and no 'ipasir_add' nor 'ipasir_assume' has been called
+ * since then, i.e., the state of the solver is SAT.
+ *
+ * Required state: SAT
+ * State after: SAT
+ */
+int ipasir_val (void * solver, int lit);
+
+/**
+ * Check if the given assumption literal was used to prove the
+ * unsatisfiability of the formula under the assumptions
+ * used for the last SAT search. Return 1 if so, 0 otherwise.
+ * This function can only be used if ipasir_solve has returned 20 and
+ * no ipasir_add or ipasir_assume has been called since then, i.e.,
+ * the state of the solver is UNSAT.
+ *
+ * Required state: UNSAT
+ * State after: UNSAT
+ */
+int ipasir_failed (void * solver, int lit);
+
+/**
+ * Set a callback function used to indicate a termination requirement to the
+ * solver. The solver will periodically call this function and check its return
+ * value during the search. The ipasir_set_terminate function can be called in any
+ * state of the solver, the state remains unchanged after the call.
+ * The callback function is of the form "int terminate(void * state)"
+ *   - it returns a non-zero value if the solver should terminate.
+ *   - the solver calls the callback function with the parameter "state"
+ *     having the value passed in the ipasir_set_terminate function (2nd parameter).
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: INPUT or SAT or UNSAT
+ */
+void ipasir_set_terminate (void * solver, void * state, 
+    //int (*terminate)(void * state));
+    int function(void* state) terminate);
+
+/**
+ * Set a callback function used to extract learned clauses up to a given length from the
+ * solver. The solver will call this function for each learned clause that satisfies
+ * the maximum length (literal count) condition. The ipasir_set_learn function can be called in any
+ * state of the solver, the state remains unchanged after the call.
+ * The callback function is of the form "void learn(void * state, int * clause)"
+ *   - the solver calls the callback function with the parameter "state"
+ *     having the value passed in the ipasir_set_learn function (2nd parameter).
+ *   - the argument "clause" is a pointer to a null terminated integer array containing the learned clause.
+ *     the solver can change the data at the memory location that "clause" points to after the function call.
+ *
+ * Required state: INPUT or SAT or UNSAT
+ * State after: INPUT or SAT or UNSAT
+ */
+void ipasir_set_learn (void * solver, void * state, int max_length, 
+    //void (*learn)(void * state, int * clause)
+    void function(void* state, int* clause) learn);
+}