return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
}
}
-
+
return createNode(cnf, NodeType_AND, lowindex, edges);
}
n->intAnnot[polarity]=1;
for (uint i=0;i<n->numEdges;i++) {
Edge succ=n->edges[i];
- succ=constraintNegateIf(succ, polarity);
if(!edgeIsVarConst(succ)) {
+ succ=constraintNegateIf(succ, polarity);
pushVectorEdge(stack, succ);
}
}
if (exp->litSize == 1) {
Literal l = getLiteralLitVector(&exp->singletons, 0);
deleteCNFExpr(exp);
- n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+ n->ptrAnnot[sign] = (void*) ((((intptr_t) l) << 1) | 1);
} else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
introProxy(cnf, e, exp, sign);
} else {
for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
Literal l=getLiteralLitVector(&expr->singletons,i);
Literal clause[] = {-lcond, l};
- addArrayClauseLiteral(cnf->solver, 1, clause);
+ addArrayClauseLiteral(cnf->solver, 2, clause);
}
for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
LitVector *lv=getVectorLitVector(&expr->clauses,i);
Node *n=getNodePtrFromEdge(e);
int i = n->numEdges;
while (i != 0) {
- Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+ Edge arg = n->edges[--i];
+ arg=constraintNegateIf(arg, isNeg);
Node * narg = getNodePtrFromEdge(arg);
if (edgeIsVarConst(arg)) {
Edge largestEdge;
CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
- if (accum == NULL) accum = allocCNFExprBool(true);
+ if (accum == NULL)
+ accum = allocCNFExprBool(true);
int i = getSizeVectorEdge(&cnf->args);
while (i != 0) {
conjoinCNFLit(accum, getProxy(argExp));
} else {
conjoinCNFExpr(accum, argExp, destroy);
- if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+ if (destroy)
+ narg->ptrAnnot[isNegEdge(arg)] = NULL;
}
}
}
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);
}
Edge v1=constraintNewVar(cnf);
Edge v2=constraintNewVar(cnf);
Edge v3=constraintNewVar(cnf);
+ Edge v4=constraintNewVar(cnf);
+ Edge v5=constraintNewVar(cnf);
+
Edge nv1=constraintNegate(v1);
- printCNF(nv1);
- printf("\n");
Edge nv2=constraintNegate(v2);
Edge nv3=constraintNegate(v3);
- Edge iff1=constraintIFF(cnf, nv1, v2);
- printCNF(iff1);
- printf("\n");
-
- Edge iff2=constraintOR2(cnf, constraintAND2(cnf, v2, v3), constraintAND2(cnf, nv2, nv3));
- printCNF(iff2);
- printf("\n");
- Edge iff3=constraintIFF(cnf, v3, nv1);
- Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+ Edge nv4=constraintNegate(v4);
- printCNF(cand);
+ Edge c1=constraintAND2(cnf, v1, nv2);
+ Edge c2=constraintAND2(cnf, v3, nv4);
+ Edge c3=constraintAND2(cnf, nv1, v2);
+ Edge c4=constraintAND2(cnf, nv3, v4);
+ Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+ printCNF(cor);
printf("\n");
- addConstraint(cnf, cand);
+ addConstraint(cnf, cor);
int value=solveCNF(cnf);
if (value==1) {
bool v1v=getValueCNF(cnf, v1);
bool v2v=getValueCNF(cnf, v2);
bool v3v=getValueCNF(cnf, v3);
- printf("%d %u %u %u\n", value, v1v, v2v, v3v);
+ bool v4v=getValueCNF(cnf, v4);
+ printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
} else
printf("%d\n",value);
deleteCNF(cnf);