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) {
Boolean *constraint=getVectorBoolean(constraints, i);
Edge c= encodeConstraintSATEncoder(This, constraint);
printCNF(c);
+ printf("\n");
addConstraint(This->cnf, c);
}
}
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);
Element* inputs2 [] = {e4, e3};
Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
addBoolean(solver, pred);
+ */
startEncoding(solver);
deleteSolver(solver);
}