edits

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 935aff95af7dd1b7ca2aaa1c0e6c85192920df6f..43113ffa1d54eacbd4bd114de89a21aea462d8ce 100644 (file)
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -172,10 +172,24 @@ void killSolver(IncrementalSolver * This) {
                waitpid(This->solver_pid, &status, 0);
        }
 }
+bool first=true;
 
 void flushBufferSolver(IncrementalSolver * This) {
        ssize_t bytestowrite=sizeof(int)*This->offset;
        ssize_t byteswritten=0;
+       for(uint i=0;i<This->offset;i++) {
+               if (first)
+                       printf("(");
+               if (This->buffer[i]==0) {
+                       printf(")\n");
+                       first=true;
+               } else {
+                       if (!first)
+                               printf(" + ");
+                       first=false;
+                       printf("%d", This->buffer[i]);
+               }
+       }
        do {
                ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
                if (n == -1) {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 5c41571db2ed888bcd1c33af05619e374ee538d9..8d943c4f4b769754cab5e46ae1416057892c2ea8 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -70,6 +70,7 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
                Boolean *constraint=getVectorBoolean(constraints, i);
                Edge c= encodeConstraintSATEncoder(This, constraint);
                printCNF(c);
+               printf("\n");
                addConstraint(This->cnf, c);
        }
 }

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 81f01b3988c38deac8bbd87ed16560bfeb2c5f70..23d943c7344137bb068dbe3ff5344bad4a97dcb8 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -14,7 +14,7 @@ int main(int numargs, char ** argv) {
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
        addBoolean(solver, oc);
-       
+       /*      
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
        Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
@@ -38,6 +38,7 @@ int main(int numargs, char ** argv) {
        Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addBoolean(solver, pred);
+       */
        startEncoding(solver);
        deleteSolver(solver);
 }