summaryrefslogtreecommitdiff
path: root/omega/omega_lib/src/pres_dnf.cc
diff options
context:
space:
mode:
Diffstat (limited to 'omega/omega_lib/src/pres_dnf.cc')
-rw-r--r--omega/omega_lib/src/pres_dnf.cc1416
1 files changed, 0 insertions, 1416 deletions
diff --git a/omega/omega_lib/src/pres_dnf.cc b/omega/omega_lib/src/pres_dnf.cc
deleted file mode 100644
index c9fd7e6..0000000
--- a/omega/omega_lib/src/pres_dnf.cc
+++ /dev/null
@@ -1,1416 +0,0 @@
-/*****************************************************************************
- Copyright (C) 1994-2000 the Omega Project Team
- Copyright (C) 2005-2011 Chun Chen
- All Rights Reserved.
-
- Purpose:
- Functions for disjunctive normal form.
-
- Notes:
-
- History:
-*****************************************************************************/
-
-#include <basic/Bag.h>
-#include <omega/pres_dnf.h>
-#include <omega/pres_conj.h>
-#include <omega/pres_tree.h> /* all DNFize functions are here */
-#include <omega/Relation.h>
-#include <omega/omega_i.h>
-
-namespace omega {
-
-void DNF::remap() {
- for(DNF_Iterator DI(this); DI.live(); DI.next()) {
- Conjunct *C = DI.curr();
- C->remap();
- }
-}
-
-
-//
-// DNF1 & DNF2 -> DNF.
-// Free arguments.
-//
-DNF* DNF_and_DNF(DNF* dnf1, DNF* dnf2) {
- DNF* new_dnf = new DNF;
- for(DNF_Iterator p(dnf2); p.live(); p.next()) {
- new_dnf->join_DNF(DNF_and_conj(dnf1, p.curr()));
- }
- delete dnf1;
- delete dnf2;
- if(new_dnf->length() > 1) {
- new_dnf->simplify();
- }
-
- if(pres_debug) {
- fprintf(DebugFile, "+++ DNF_and_DNF OUT +++\n");
- new_dnf->prefix_print(DebugFile);
- }
- return(new_dnf);
-}
-
-
-/*
- * Remove redundant conjuncts from given DNF.
- * If (C1 => C2), remove C1.
- * C1 => C2 is TRUE: when problem where C1 is Black and C2 is Red
- * Blk Red : has no red constraints.
- * It means that C1 is a subset of C2 and therefore C1 is redundant.
- *
- * Exception: C1 => UNKNOWN - leave them as they are
- */
-void DNF::rm_redundant_conjs(int effort) {
- if(is_definitely_false() || has_single_conjunct())
- return;
-
- use_ugly_names++;
- // skip_set_checks++;
-
- int count = 0;
- for(DNF_Iterator p(this); p.live(); p.next()) count++;
-
- if(pres_debug) {
- int i = 0;
- fprintf(DebugFile, "@@@ rm_redundant_conjs IN @@@[\n");
- prefix_print(DebugFile);
- for(DNF_Iterator p(this); p.live(); p.next())
- fprintf(DebugFile, "#%d = %p\n", ++i, p.curr());
- }
-
- DNF_Iterator pdnext;
- DNF_Iterator pdel(this);
- for(; pdel.live(); pdel=pdnext) {
- pdnext = pdel;
- pdnext.next();
- Conjunct *cdel = pdel.curr();
- int del_min_leading_zeros = cdel->query_guaranteed_leading_0s();
- int del_max_leading_zeros = cdel->query_possible_leading_0s();
-
- for(DNF_Iterator p(this); p.live(); p.next()) {
- Conjunct *c = p.curr();
- if(c != cdel) {
- int c_min_leading_zeros = cdel->query_guaranteed_leading_0s();
- int c_max_leading_zeros = cdel->query_possible_leading_0s();
- if(pres_debug)
- fprintf(DebugFile, "@@@ rm_redundant_conjs @%p => @%p[\n", cdel, c);
-
- if (c->is_inexact() && cdel->is_exact()) {
- if (pres_debug)
- fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ Exact Conj => Inexact Conj is not tested\n");
- }
- else if (del_min_leading_zeros >=0 && c_min_leading_zeros >= 0
- && c_max_leading_zeros >= 0 && del_max_leading_zeros >=0
- && (del_min_leading_zeros > c_max_leading_zeros
- || c_min_leading_zeros > del_max_leading_zeros)) {
- if (1 || pres_debug)
- fprintf(DebugFile, "]@@@ not redundant due to leading zero info\n");
- }
- else {
- Conjunct *cgist = merge_conjs(cdel, c, MERGE_GIST);
-
- if (!cgist->redSimplifyProblem(effort,0)) {
- if(pres_debug) {
- fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ IMPLICATION TRUE @%p\n", cdel);
- cdel->prefix_print (DebugFile);
- fprintf(DebugFile, "=>\n");
- c->prefix_print (DebugFile);
- }
- rm_conjunct(cdel);
- delete cdel;
- delete cgist;
- break;
- }
- else {
- if(pres_debug) {
- fprintf(DebugFile, "]@@@ rm_redundant_conjs @@@ IMPLICATION FALSE @%p\n", cdel);
- if(pres_debug > 1)
- cgist->prefix_print(DebugFile);
- }
- delete cgist;
- }
- }
- }
- }
- }
-
- if(pres_debug) {
- fprintf(DebugFile, "]@@@ rm_redundant_conjs OUT @@@\n");
- prefix_print(DebugFile);
- }
- // skip_set_checks--;
- use_ugly_names--;
-}
-
-
-/* Remove inexact conjuncts from given DNF if it contains UNKNOWN
- * conjunct
- */
-
-void DNF::rm_redundant_inexact_conjs() {
- if (is_definitely_false() || has_single_conjunct())
- return;
-
- bool has_unknown=false;
- bool has_inexact=false;
-
- Conjunct * c_unknown = 0; // make compiler shut up
- for (DNF_Iterator p(this); p.live(); p.next()) {
- assert (p.curr()->problem!=NULL);
- if (p.curr()->is_inexact()) {
- if (p.curr()->is_unknown()) {
- has_unknown=true;
- c_unknown = p.curr();
- }
- else
- has_inexact=true;
- }
- }
-
- if (! has_unknown || ! has_inexact)
- return;
-
- use_ugly_names++;
- // skip_set_checks++;
-
- DNF_Iterator pdnext;
- DNF_Iterator pdel(this);
-
- for (; pdel.live(); pdel=pdnext) {
- pdnext = pdel;
- pdnext.next();
- Conjunct * cdel=pdel.curr();
- if (cdel->is_inexact() && cdel!=c_unknown) {
- rm_conjunct(cdel);
- delete cdel;
- }
- }
-
- use_ugly_names--;
- // skip_set_checks--;
-}
-
-
-
-//
-// DNF properties.
-//
-bool DNF::is_definitely_false() const {
- return(conjList.empty());
-}
-
-bool DNF::is_definitely_true() const {
- return(has_single_conjunct() && single_conjunct()->is_true());
-}
-
-int DNF::length() const {
- return conjList.length();
-}
-
-Conjunct *DNF::single_conjunct() const {
- assert(conjList.length()==1);
- return(conjList.front());
-}
-
-bool DNF::has_single_conjunct() const {
- return (conjList.length()==1);
-}
-
-Conjunct *DNF::rm_first_conjunct() {
- if(conjList.empty()) {
- return NULL;
- }
- else {
- return conjList.remove_front();
- }
-}
-
-
-//
-// Convert DNF to Formula and add it root.
-// Free this DNF.
-//
-void DNF::DNF_to_formula(Formula* root) {
- Formula *new_or;
- if (conjList.length()!=1) {
- skip_finalization_check++;
- new_or = root->add_or();
- skip_finalization_check--;
- }
- else {
- new_or = root;
- }
- while(!conjList.empty()) {
- Conjunct *conj = conjList.remove_front();
- new_or->add_child(conj);
- }
- delete this;
-}
-
-
-//
-// DNF functions.
-//
-DNF::DNF() : conjList() {
-}
-
-DNF::~DNF() {
- // for(DNF_Iterator p(this); p.live(); p.next()) {
- // if(p.curr() != NULL)
- // delete p.curr();
- // }
- for(List_Iterator<Conjunct *> i(conjList); i.live(); i.next())
- delete *i;
-}
-
-//
-// Copy DNF
-//
-DNF* DNF::copy(Rel_Body *rel_body) {
- DNF *new_dnf = new DNF;
- for(DNF_Iterator pd(this); pd.live(); pd.next()) {
- Conjunct *conj = pd.curr();
- if(conj)
- new_dnf->add_conjunct(conj->copy_conj_diff_relation(rel_body,rel_body));
- }
- return(new_dnf);
-}
-
-//
-// Add Conjunct to DNF
-//
-void DNF::add_conjunct(Conjunct* conj) {
- conjList.append(conj);
-}
-
-//
-// Add DNF to DNF.
-// The second DNF is reused.
-//
-void DNF::join_DNF(DNF* dnf) {
- conjList.join(dnf->conjList);
- delete dnf;
-}
-
-//
-// Remove conjunct from DNF.
-// Conjunct itself is not deleted.
-//
-void DNF::rm_conjunct(Conjunct *c) {
- if(conjList.front() == c) {
- conjList.remove_front();
- }
- else {
- List_Iterator<Conjunct*> p, pp;
- for(p=List_Iterator<Conjunct*> (conjList); p; p++) {
- if((*p)==c) {
- conjList.del_after(pp);
- return;
- }
- pp = p;
- }
- assert(0 && "DNF::rm_conjunct: no such conjunct");
- }
-}
-
-
-// remove (but don't delete) all conjuncts
-
-void DNF::clear() {
- conjList.clear();
-}
-
-
-//
-// DNF & CONJ -> new DNF.
-// Don't touch arguments.
-//
-DNF* DNF_and_conj(DNF* dnf, Conjunct* conj) {
- DNF* new_dnf = new DNF;
- for(DNF_Iterator p(dnf); p.live(); p.next()) {
- Conjunct* new_conj = merge_conjs(p.curr(), conj, MERGE_REGULAR);
- new_dnf->add_conjunct(new_conj);
- }
- if(new_dnf->length() > 1) {
- new_dnf->simplify();
- }
- return(new_dnf);
-}
-
-//
-// Compute C0 and not (C1 or C2 or ... CN).
-// Reuse/delete its arguments.
-//
-DNF* conj_and_not_dnf(Conjunct *positive_conjunct, DNF *neg_conjs, bool weak) {
- DNF *ret_dnf = new DNF;
- int recursive = 0;
- use_ugly_names++;
-
- if(pres_debug) {
- fprintf(DebugFile, "conj_and_not_dnf [\n");
- fprintf(DebugFile, "positive_conjunct:\n");
- positive_conjunct->prefix_print(DebugFile);
- fprintf(DebugFile, "neg_conjs:\n");
- neg_conjs->prefix_print(DebugFile);
- fprintf(DebugFile, "\n\n");
- }
-
- if (simplify_conj(positive_conjunct, true, false, EQ_BLACK) == false) {
- positive_conjunct = NULL;
- goto ReturnDNF;
- }
-
- /* Compute gists of negative conjuncts given positive conjunct */
-
-
- int c0_updated;
- c0_updated = true;
- while(c0_updated) {
- c0_updated = false;
- for(DNF_Iterator p(neg_conjs); p.live(); p.next()) {
- Conjunct *neg_conj = p.curr();
- if(neg_conj==NULL) continue;
- if (!positive_conjunct->is_exact()
- && !neg_conj->is_exact()) {
- // C1 and unknown & ~(C2 and unknown) = C1 and unknown
- delete neg_conj;
- p.curr_set(NULL);
- continue;
- }
- Conjunct *cgist = merge_conjs(positive_conjunct, neg_conj, MERGE_GIST);
- if(simplify_conj(cgist, false, true, EQ_RED) == false) {
- // C1 & ~FALSE = C1
- delete neg_conj;
- p.curr_set(NULL);
- }
- else {
- cgist->rm_color_constrs();
- if(cgist->is_true()) {
- // C1 & ~TRUE = FALSE
- delete cgist;
- goto ReturnDNF;
- }
- else {
- if(cgist->cost()==1) { // single inequality
- DNF *neg_dnf = negate_conj(cgist);
- delete cgist;
- Conjunct *conj =
- merge_conjs(positive_conjunct, neg_dnf->single_conjunct(), MERGE_REGULAR);
- delete positive_conjunct;
- delete neg_dnf;
- positive_conjunct = conj;
- delete neg_conj;
- p.curr_set(NULL);
- if(!simplify_conj(positive_conjunct, false, false, EQ_BLACK)) {
- positive_conjunct = NULL;
- goto ReturnDNF;
- }
- c0_updated = true;
- }
- else {
- delete neg_conj;
- p.curr_set(cgist);
- }
- }
- }
- }
- }
-
- if(pres_debug) {
- fprintf(DebugFile, "--- conj_and_not_dnf positive_conjunct NEW:\n");
- positive_conjunct->prefix_print(DebugFile);
- fprintf(DebugFile, "--- conj_and_not_dnf neg_conjs GISTS:\n");
- neg_conjs->prefix_print(DebugFile);
- fprintf(DebugFile, "--- conj_and_not_dnf ---\n\n");
- }
-
- /* Find minimal negative conjunct */
- {
- Conjunct *min_conj = NULL;
- int min_cost = INT_MAX;
- DNF_Iterator min_p;
- int live_count = 0;
- for(DNF_Iterator q(neg_conjs); q.live(); q.next()) {
- Conjunct *neg_conj = q.curr();
- if(neg_conj!=NULL) {
- live_count++;
- if(neg_conj->cost() < min_cost) {
- min_conj = neg_conj;
- min_cost = neg_conj->cost();
- min_p = q;
- }
- }
- }
-
- /* Negate minimal conjunct, AND result with positive conjunct */
- if(weak || min_conj==NULL) {
- ret_dnf->add_conjunct(positive_conjunct);
- positive_conjunct = NULL;
- }
- else if (min_cost == CantBeNegated) {
- static int OMEGA_WHINGE = -1;
- if (OMEGA_WHINGE < 0) {
- OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0;
- }
- if (OMEGA_WHINGE) {
- fprintf(stderr, "Ignoring negative clause that can't be negated and generating inexact result\n");
- if (!pres_debug) fprintf(DebugFile, "Ignoring negative clause that can't be negated and generating inexact result\n");
- }
-
- positive_conjunct->make_inexact();
- ret_dnf->add_conjunct(positive_conjunct);
- positive_conjunct = NULL;
- if(pres_debug)
- fprintf(DebugFile, "Ignoring negative clause that can't be negated and generating inexact upper bound\n");
- }
- else {
- DNF *neg_dnf = negate_conj(min_conj);
- delete min_conj;
- min_p.curr_set(NULL);
- DNF *new_pos = DNF_and_conj(neg_dnf, positive_conjunct);
- delete neg_dnf;
- delete positive_conjunct;
- positive_conjunct = NULL;
- // new_dnf->rm_redundant_conjs(2);
- if(live_count>1) {
- recursive = 1;
- for(DNF_Iterator pd(new_pos); pd.live(); pd.next()) {
- Conjunct *conj = pd.curr();
- ret_dnf->join_DNF(conj_and_not_dnf(conj, neg_conjs->copy(conj->relation())));
- pd.curr_set(NULL);
- }
- delete new_pos;
- }
- else {
- ret_dnf->join_DNF(new_pos);
- }
- }
- }
-
-ReturnDNF:;
- delete positive_conjunct;
- delete neg_conjs;
-
- //if (recursive) ret_dnf->rm_redundant_conjs(1);
-
- if(pres_debug) {
- fprintf(DebugFile, "] conj_and_not_dnf RETURN:\n");
- ret_dnf->prefix_print(DebugFile);
- fprintf(DebugFile, "\n\n");
- }
- use_ugly_names--;
- return ret_dnf;
-}
-
-/* first some functions for manipulating oc "problems" */
-
-static void EqnnZero(eqn *e, int s) {
-// memset((char*)e, 0, (headerWords+1+s)*sizeof(int));
- e->key = 0;
- e->touched = 0;
- e->color = EQ_BLACK;
- e->essential = 0;
- e->varCount = 0;
- for (int i = 0; i <= s; i++)
- e->coef[i] = 0;
-}
-
-/*
- * Make a new black equation in a given problem
- */
-static int NewEquation(Problem *p) {
- int e = p->newEQ();
- EqnnZero(&p->EQs[e], p->nVars);
- return e;
-}
-
-/*
- * Make a new black inequality in a given problem
- */
-static int NewInequality(Problem *p) {
- int g = p->newGEQ();
- EqnnZero(&p->GEQs[g], p->nVars);
- return g;
-}
-
-//
-// ~CONJ -> DNF
-//
-DNF* negate_conj(Conjunct* conj) {
- if(pres_debug) {
- fprintf(DebugFile, "%%%%%% negate_conj IN %%%%%%\n");
- conj->prefix_print(DebugFile);
- fprintf(DebugFile, "\n");
- }
-
- DNF* new_dnf = new DNF;
- Problem *p = conj->problem;
- int i, j,k;
-
- if (!conj->is_exact()) new_dnf->add_conjunct(conj->copy_conj_same_relation());
-
- Conjunct* true_part = new Conjunct(NULL, conj->relation());
- Problem *tp = true_part->problem;
- copy_conj_header(true_part, conj);
- true_part->invalidate_leading_info();
- int *wildCard = new int[p->nGEQs];
- int *handleIt = new int[p->nVars+1];
- for(j=1; j<=p->nVars; j++) handleIt[j] = false;
-
- for(i=0; i<p->nGEQs; i++) {
- wildCard[i] = 0;
- for(j=1; j<=p->nVars; j++) {
- Variable_ID v = conj->mappedVars[j];
- if(v->kind()==Wildcard_Var && p->GEQs[i].coef[j]!=0) {
- assert(wildCard[i] == 0);
- handleIt[j] = true;
- if (p->GEQs[i].coef[j] > 0) wildCard[i] = j;
- else wildCard[i] = -j;
- }
- }
- }
-
- for(i=0; i<p->nGEQs; i++) if (wildCard[i] == 0) {
- /* ~(ax + by + c >= 0) = (-ax -by -c-1 >= 0) */
- Conjunct* new_conj = true_part->copy_conj_same_relation();
- Problem *np = new_conj->problem;
- new_conj->exact=true;
- int n_e = NewInequality(np);
- int t_e = NewInequality(tp);
- np->GEQs[n_e].coef[0] = -p->GEQs[i].coef[0]-1;
- tp->GEQs[t_e].coef[0] = p->GEQs[i].coef[0];
- for(j=1; j<=p->nVars; j++) {
- Variable_ID v = conj->mappedVars[j];
- if(v->kind()==Wildcard_Var && p->GEQs[i].coef[j]!=0) {
- assert(0 && "negate_conj: wildcard in inequality");
- }
- np->GEQs[n_e].coef[j] = -p->GEQs[i].coef[j];
- tp->GEQs[t_e].coef[j] = p->GEQs[i].coef[j];
-
- }
- assert(j-1 == p->nVars);
- assert(j-1 == conj->mappedVars.size());
- new_dnf->add_conjunct(new_conj);
- }
-
-
- for(i=0; i<p->nEQs; i++) {
- int wc_no = 0;
- int wc_j = 0; // make complier shut up
- for(j=1; j<=p->nVars; j++) {
- Variable_ID v = conj->mappedVars[j];
- if(v->kind()==Wildcard_Var && p->EQs[i].coef[j]!=0) {
- wc_no++;
- wc_j = j;
- }
- }
-
- if(wc_no!=0) {
-#if ! defined NDEBUG
- int i2;
- assert(!handleIt[wc_j]);
- for(i2=0; i2<p->nEQs; i2++)
- if(i != i2 && p->EQs[i2].coef[wc_j] != 0) break;
- assert(i2 >= p->nEQs);
-#endif
- assert(wc_no == 1 && "negate_conj: more than 1 wildcard in equality");
-
- // === Negating equality with a wildcard for K>0 ===
- // ~(exists v st expr + K v + C = 0) =
- // (exists v st 1 <= - expr - K v - C <= K-1)
-
- Conjunct *nc = true_part->copy_conj_same_relation();
- Problem *np = nc->problem;
- nc->exact=true;
-
- // -K alpha = expr <==> K alpha = expr
- if(p->EQs[i].coef[wc_j]<0)
- p->EQs[i].coef[wc_j] = -p->EQs[i].coef[wc_j];
-
- if(p->EQs[i].coef[wc_j]==2) {
- // ~(exists v st expr +2v +C = 0) =
- // (exists v st -expr -2v -C = 1)
- // That is (expr +2v +C+1 = 0)
- int e = NewEquation(np);
- np->EQs[e].coef[0] = p->EQs[i].coef[0] +1;
- for(j=1; j<=p->nVars; j++) {
- np->EQs[e].coef[j] = p->EQs[i].coef[j];
- }
- }
- else {
- // -expr -Kv -C-1 >= 0
- int e = NewInequality(np);
- np->GEQs[e].coef[0] = -p->EQs[i].coef[0] -1;
- for(j=1; j<=p->nVars; j++) {
- np->GEQs[e].coef[j] = -p->EQs[i].coef[j];
- }
-
- // +expr +Kv +C+K-1 >= 0
- e = NewInequality(np);
- np->GEQs[e].coef[0] = p->EQs[i].coef[0] +p->EQs[i].coef[wc_j] -1;
- for(j=1; j<=p->nVars; j++) {
- np->GEQs[e].coef[j] = p->EQs[i].coef[j];
- }
- }
-
- new_dnf->add_conjunct(nc);
-
- }
- else {
- /* ~(ax + by + c = 0) = (-ax -by -c-1 >= 0) Or (ax + by + c -1 >= 0) */
- Conjunct *nc1 = true_part->copy_conj_same_relation();
- Conjunct *nc2 = true_part->copy_conj_same_relation();
- Problem* np1 = nc1->problem;
- Problem* np2 = nc2->problem;
- nc1->invalidate_leading_info();
- nc2->invalidate_leading_info();
- nc1->exact=true;
- nc2->exact=true;
- int n_e1 = NewInequality(np1);
- int n_e2 = NewInequality(np2);
- np1->GEQs[n_e1].coef[0] = -p->EQs[i].coef[0]-1;
- np2->GEQs[n_e2].coef[0] = p->EQs[i].coef[0]-1;
- for(j=1; j<=p->nVars; j++) {
- coef_t coef = p->EQs[i].coef[j];
- np1->GEQs[n_e1].coef[j] = -coef;
- np2->GEQs[n_e2].coef[j] = coef;
- }
- new_dnf->add_conjunct(nc1);
- new_dnf->add_conjunct(nc2);
- }
- {
- int e = NewEquation(tp);
- tp->EQs[e].coef[0] = p->EQs[i].coef[0];
- for(j=1; j<=p->nVars; j++)
- tp->EQs[e].coef[j] = p->EQs[i].coef[j];
- }
- }
-
- for(j=1; j<=p->nVars; j++)
- if (handleIt[j]) {
- for(i=0; i<p->nGEQs; i++)
- if (wildCard[i] == j)
- for(k=0; k<p->nGEQs; k++) if (wildCard[k] == -j){
- // E_i <= c_i alpha
- // c_k alpha <= E_k
- // c_k E_i <= c_i c_k alpha <= c_i E_k
- // c_k E_i <= c_i c_k floor (c_i E_k / c_i c_k)
- // negating:
- // c_k E_i > c_i c_k floor (c_i E_k / c_i c_k)
- // c_k E_i > c_i c_k beta > c_i E_k - c_i c_k
- // c_k E_i - 1 >= c_i c_k beta >= c_i E_k - c_i c_k + 1
- Conjunct* new_conj = true_part->copy_conj_same_relation();
- Problem *np = new_conj->problem;
- coef_t c_k = - p->GEQs[k].coef[j];
- coef_t c_i = p->GEQs[i].coef[j];
- assert(c_k > 0);
- assert(c_i > 0);
- new_conj->exact=true;
- int n_e = NewInequality(np);
- // c_k E_i - 1 >= c_i c_k beta
- int v;
- for(v=0; v<=p->nVars; v++) {
- np->GEQs[n_e].coef[v] = - c_k * p->GEQs[i].coef[v];
- }
- np->GEQs[n_e].coef[j] = -c_i * c_k;
- np->GEQs[n_e].coef[0]--;
-
- n_e = NewInequality(np);
- // c_i c_k beta >= c_i E_k - c_i c_k + 1
- // c_i c_k beta + c_i c_k -1 >= c_i E_k
- for(v=0; v<=p->nVars; v++) {
- np->GEQs[n_e].coef[v] = - c_i * p->GEQs[k].coef[v];
- }
- np->GEQs[n_e].coef[j] = c_i * c_k;
- np->GEQs[n_e].coef[0] += c_i * c_k -1;
-
- new_dnf->add_conjunct(new_conj);
- }
- }
-
- if(pres_debug) {
- fprintf(DebugFile, "%%%%%% negate_conj OUT %%%%%%\n");
- new_dnf->prefix_print(DebugFile);
- }
- delete true_part;
- delete[] wildCard;
- delete[] handleIt;
- return(new_dnf);
-}
-
-
-
-
-///////////////////////////////////////////////////////
-// DNFize formula -- this is the real simplification //
-// It also destroys the formula it simplifies //
-///////////////////////////////////////////////////////
-
-
-
-//
-// Try to separate positive and negative clauses below the AND,
-// letting us use the techniques described in Pugh & Wonnacott:
-// "An Exact Method for Value-Based Dependence Analysis"
-//
-
-
-DNF* F_And::DNFize() {
- Conjunct *positive_conjunct = NULL;
- DNF *neg_conjs = new DNF;
- List<DNF*> pos_dnfs;
- List_Iterator<DNF*> pos_dnf_i;
- DNF *new_dnf = new DNF;
- int JustReturnDNF = 0;
-
- use_ugly_names++;
-
- if(pres_debug) {
- fprintf(DebugFile, "\nF_And:: DNFize [\n");
- prefix_print(DebugFile);
- }
-
- if(children().empty()) {
- Conjunct * c=new Conjunct(NULL, relation());
- new_dnf->add_conjunct(c);
- }
- else {
- while(!children().empty()) {
- Formula* carg = children().remove_front();
- if(carg->node_type()==Op_Not) {
- // DNF1 & ~DNF2 -> DNF
- DNF *dnf = carg->children().remove_front()->DNFize();
- delete carg;
- neg_conjs->join_DNF(dnf); // negative conjunct
- }
- else {
- // DNF1 & DNF2 -> DNF
- DNF *dnf = carg->DNFize();
- int dl = dnf->length();
- if(dl==0) {
- // DNF & false -> false
- delete this;
- JustReturnDNF = 1;
- break;
- }
- else if(dl==1) {
- // positive conjunct
- Conjunct *conj = dnf->rm_first_conjunct();
- delete dnf;
- if(positive_conjunct==NULL) {
- positive_conjunct = conj;
- }
- else {
- Conjunct *new_conj = merge_conjs(positive_conjunct, conj, MERGE_REGULAR);
- delete conj;
- delete positive_conjunct;
- positive_conjunct = new_conj;
- }
- }
- else {
- // positive DNF
- pos_dnfs.append(dnf);
- }
- }
- }
-
- if (!JustReturnDNF) {
- Rel_Body * my_relation = relation();
- delete this;
-
- // If we have a positive_conjunct, it can serve as the 1st arg to
- // conj_and_not_dnf. Otherwise, if pos_dnfs has one DNF,
- // use each conjunct there for this purpose.
- // Only pass "true" here if there is nothing else to try,
- // as long as TRY_TO_AVOID_TRUE_AND_NOT_DNF is set.
- //
- // Perhaps we should even try to and multiple DNF's?
-
- if (!positive_conjunct && pos_dnfs.length() == 1) {
- if(pres_debug) {
- fprintf(DebugFile, "--- F_AND::DNFize() Single pos_dnf:\n");
- pos_dnfs[1]->prefix_print(DebugFile);
- fprintf(DebugFile, "--- F_AND::DNFize() vs neg_conjs:\n");
- neg_conjs->prefix_print(DebugFile);
- }
-
- DNF *real_neg_conjs = new DNF;
- for (DNF_Iterator nc(neg_conjs); nc; nc++) {
- if (simplify_conj((*nc), true, false, EQ_BLACK) != false)
- real_neg_conjs->add_conjunct(*nc);
- (*nc) = 0;
- }
- delete neg_conjs;
- neg_conjs = real_neg_conjs;
-
- for(DNF_Iterator pc(pos_dnfs[1]); pc; pc++) {
- new_dnf->join_DNF(conj_and_not_dnf((*pc), neg_conjs->copy((*pc)->relation())));
- (*pc) = 0;
- }
- }
- else if(positive_conjunct==NULL && neg_conjs->is_definitely_false()) {
- pos_dnf_i = List_Iterator<DNF*>(pos_dnfs);
- delete new_dnf;
- new_dnf = *pos_dnf_i;
- *pos_dnf_i = NULL;
- pos_dnf_i++;
- for ( ; pos_dnf_i; pos_dnf_i++) {
- DNF *pos_dnf = *pos_dnf_i;
- new_dnf = DNF_and_DNF(new_dnf, pos_dnf);
- *pos_dnf_i = NULL;
- }
- }
- else {
- if(positive_conjunct==NULL) {
- static int OMEGA_WHINGE = -1;
- if (OMEGA_WHINGE < 0) {
- OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0;
- }
-
- if (pres_debug || OMEGA_WHINGE) {
- fprintf(DebugFile, "Uh-oh: F_AND::DNFize() resorting to TRUE and not DNF\n");
- fprintf(DebugFile, "--- F_AND::DNFize() neg_conjs\n");
- neg_conjs->prefix_print(DebugFile);
- fprintf(DebugFile, "--- F_AND::DNFize() pos_dnfs:\n");
- for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
- (*pos_dnf_i)->prefix_print(DebugFile);
- fprintf(DebugFile,"---- --\n");
- }
- }
- if (OMEGA_WHINGE) {
- fprintf(stderr, "Uh-oh: F_AND::DNFize() resorting to TRUE and not DNF\n");
- fprintf(stderr, "--- F_AND::DNFize() neg_conjs\n");
- neg_conjs->prefix_print(stderr);
- fprintf(stderr, "--- F_AND::DNFize() pos_dnfs:\n");
- for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
- (*pos_dnf_i)->prefix_print(stderr);
- fprintf(stderr,"---- --\n");
- }
- }
- positive_conjunct = new Conjunct(NULL, my_relation);
- }
-
- if(!neg_conjs->is_definitely_false()) {
- new_dnf->join_DNF(conj_and_not_dnf(positive_conjunct, neg_conjs));
- neg_conjs = NULL;
- }
- else {
- new_dnf->add_conjunct(positive_conjunct);
- }
- positive_conjunct = NULL;
-
- //
- // AND it with positive DNFs
- //
- if(pres_debug) {
- fprintf(DebugFile, "--- F_AND::DNFize() pos_dnfs:\n");
- for (pos_dnf_i=List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++)
- (*pos_dnf_i)->prefix_print(DebugFile);
- }
- for (pos_dnf_i = List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++) {
- DNF *pos_dnf = *pos_dnf_i;
- new_dnf = DNF_and_DNF(new_dnf, pos_dnf);
- *pos_dnf_i = NULL;
- }
- }
- }
- }
-
- delete positive_conjunct;
- delete neg_conjs;
- for (pos_dnf_i = List_Iterator<DNF*>(pos_dnfs); pos_dnf_i; pos_dnf_i++)
- delete *pos_dnf_i;
-
- if(pres_debug) {
- fprintf(DebugFile, "] F_AND::DNFize() OUT \n");
- new_dnf->prefix_print(DebugFile);
- }
-
- use_ugly_names--;
-
- return new_dnf;
-}
-
-//
-// ~ dnf = true ^ ~ dnf, so just call conj_and_not_dnf
-//
-
-DNF* F_Not::DNFize() {
- Conjunct *positive_conjunct = new Conjunct(NULL, relation());
- DNF *neg_conjs = children().remove_front()->DNFize();
- delete this;
- DNF *new_dnf = conj_and_not_dnf(positive_conjunct, neg_conjs);
-
- if(pres_debug) {
- fprintf(DebugFile, "=== F_NOT::DNFize() OUT ===\n");
- new_dnf->prefix_print(DebugFile);
- }
- return new_dnf;
-}
-
-
-//
-// or is almost in DNF already:
-//
-
-DNF* F_Or::DNFize() {
- DNF* new_dnf = new DNF;
- bool empty_or=true;
-
- while(!children().empty()) {
- DNF* c_dnf = children().remove_front()->DNFize();
- new_dnf->join_DNF(c_dnf);
- empty_or=false;
- }
-
-
- delete this;
-
- if(pres_debug) {
- fprintf(DebugFile, "=== F_OR::DNFize() OUT ===\n");
- new_dnf->prefix_print(DebugFile);
- }
- return(new_dnf);
-}
-
-
-//
-// exists x : (c1 v c2 v ...) --> (exists x : c1) v (exists x : c2) v ...
-//
-
-DNF* F_Exists::DNFize() {
- DNF *dnf = children().remove_front()->DNFize();
-
- for (DNF_Iterator pd(dnf); pd.live(); pd.next()) {
- Conjunct *conj = pd.curr();
-
- // can simply call localize_vars for DNF with a single conjunct
- Variable_ID_Tuple locals_copy(myLocals.size());
- copy_var_decls(locals_copy, myLocals);
- conj->push_exists(locals_copy);
- conj->remap();
- reset_remap_field(myLocals);
-
- conj->r_constrs = 0;
- conj->simplified = false; // who knows
- conj->cols_ordered = false;
- }
- delete this;
-
- if(pres_debug) {
- fprintf(DebugFile, "=== F_EXISTS::DNFize() OUT ===\n");
- dnf->prefix_print(DebugFile);
- }
- return(dnf);
-}
-
-
-//
-// Single conjunct is already in DNF.
-//
-
-DNF* Conjunct::DNFize() {
- assert(!is_compressed());
- DNF *results = new DNF;
-
- if (is_true()) {
- simplified = true;
- verified = true;
- results->add_conjunct(this);
- }
- else {
- results->add_conjunct(this);
- }
-
- return results;
-}
-
-
-//
-// Foralls should have been removed before we get to DNFize
-//
-
-DNF* F_Forall::DNFize() {
- assert(0);
- return(NULL);
-}
-
-void DNF::count_leading_0s() {
- if (conjList.empty())
- return;
-
- for (DNF_Iterator conj(this); conj; conj++) {
- (*conj)->count_leading_0s();
- }
-}
-
-
-// return x s.t. forall conjuncts c, c has >= x leading 0s
-// if set, always returns -1; arg tells you if it's a set or relation.
-
-int DNF::query_guaranteed_leading_0s(int what_to_return_for_empty_dnf) {
- count_leading_0s();
- int result = what_to_return_for_empty_dnf; // if set, -1; if rel, 0
- bool first = true;
-
- for (DNF_Iterator conj(this); conj; conj++) {
- int tmp = (*conj)->query_guaranteed_leading_0s();
- assert(tmp >= 0 || ((*conj)->relation()->is_set() && tmp == -1));
- if (first || tmp < result) result = tmp;
- first = false;
- }
-
- return result;
-}
-
-// return x s.t. forall conjuncts c, c has <= x leading 0s
-// if no conjuncts, return the argument
-
-int DNF::query_possible_leading_0s(int n_input_and_output) {
- count_leading_0s();
- int result = n_input_and_output;
- bool first = true;
-
- for (DNF_Iterator conj(this); conj; conj++) {
- int tmp = (*conj)->query_possible_leading_0s();
- assert(tmp >= 0 || (tmp == -1 && (*conj)->relation()->is_set()));
- if (first || tmp > result) result = tmp;
- first = false;
- }
-
- return result;
-}
-
-
-// return 0 if we don't know, or +-1 if we do
-
-int DNF::query_leading_dir() {
- count_leading_0s();
- int result = 0;
- bool first = true;
-
- for (DNF_Iterator conj(this); conj; conj++) {
- int glz = (*conj)->query_guaranteed_leading_0s();
- int plz = (*conj)->query_possible_leading_0s();
- int rlz = 0; // shut the compiler up
- if (glz != plz)
- return 0;
-
- if (first) {
- rlz = glz;
- result = (*conj)->query_leading_dir();
- first = false;
- }
- else
- if (glz != rlz || result != (*conj)->query_leading_dir())
- return 0;
- }
-
- return result;
-}
-
-void Conjunct::count_leading_0s() {
- Rel_Body *body = relation();
- int max_depth = min(body->n_inp(), body->n_out());
- if(body->is_set()) {
- assert(guaranteed_leading_0s == -1 && possible_leading_0s == -1);
-// guaranteed_leading_0s = possible_leading_0s = -1;
- leading_dir = 0;
- return;
- }
-
-
-#if ! defined NDEBUG
- assert_leading_info();
-#endif
- if (guaranteed_leading_0s < 0) {
- int L;
- for (L=1; L <= max_depth; L++) {
- Variable_ID in = body->input_var(L), out = body->output_var(L);
- coef_t min, max;
- bool guaranteed;
-
- query_difference(out, in, min, max, guaranteed);
- if (min < 0 || max > 0) {
- if (min > 0 || max < 0) { // we know guaranteed & possible
- guaranteed_leading_0s = possible_leading_0s = L-1;
- if (min > 0) // We know its 0,..,0,+
- leading_dir = 1;
- else // We know its 0,..,0,-
- leading_dir = -1;
- return;
- }
- break;
- }
- }
- guaranteed_leading_0s = L-1;
- for ( ; L <= max_depth; L++) {
- Variable_ID in = body->input_var(L),
- out = body->output_var(L);
- coef_t min, max;
- bool guaranteed;
-
- query_difference(out, in, min, max, guaranteed);
-
- if (min > 0 || max < 0) break;
- }
- possible_leading_0s = L-1;
- }
-#if ! defined NDEBUG
- assert_leading_info();
-#endif
-}
-
-//
-// add level-carried DNF form out to level "level"
-//
-
-
-void DNF::make_level_carried_to(int level) {
- count_leading_0s();
- Rel_Body *body = 0; // make compiler shut up
- if (length() > 0 && !(body = conjList.front()->relation())->is_set()) {
- // LCDNF makes no sense otherwise
- Relation tmp;
-#ifndef NDEBUG
- tmp = Relation(*body,42);
-#endif
-
- DNF *newstuff = new DNF;
- int shared_depth = min(body->n_inp(), body->n_out());
- int split_to = level >= 0 ? min(shared_depth,level) : shared_depth;
-
- skip_finalization_check++;
- EQ_Handle e;
-
- for (DNF_Iterator conj(this); conj; conj++) {
- assert(body = (*conj)->relation());
- int leading_eqs;
-
- bool is_guaranteed = (*conj)->verified;
-
- for (leading_eqs=1; leading_eqs <= split_to; leading_eqs++) {
- Variable_ID in = body->input_var(leading_eqs),
- out = body->output_var(leading_eqs);
- coef_t min, max;
- bool guaranteed;
-
- if (leading_eqs > (*conj)->possible_leading_0s &&
- (*conj)->leading_dir_valid_and_known()) {
- leading_eqs--;
- break;
- }
-
- if (leading_eqs > (*conj)->guaranteed_leading_0s) {
- (*conj)->query_difference(out, in, min, max, guaranteed);
- if (min > 0 || max < 0) guaranteed = true;
-// fprintf(DebugFile,"Make level carried, %d <= diff%d <= %d (%d):\n",
-// min,leading_eqs,max,guaranteed);
-// use_ugly_names++;
-// (*conj)->prefix_print(DebugFile);
-// use_ugly_names--;
- if (!guaranteed) is_guaranteed = false;
- bool generateLTClause = min < 0;
- bool generateGTClause = max > 0;
- bool retainEQClause = (leading_eqs <= (*conj)->possible_leading_0s &&
- min <= 0 && max >= 0);
- if (!(generateLTClause || generateGTClause || retainEQClause)) {
- // conjunct is infeasible
- if (pres_debug) {
- fprintf(DebugFile, "Conjunct discovered to be infeasible during make_level_carried_to(%d):\n", level);
- (*conj)->prefix_print(DebugFile);
- }
-#if ! defined NDEBUG
- Conjunct *cpy = (*conj)->copy_conj_same_relation();
- assert(!simplify_conj(cpy, true, 32767, 0));
-#endif
- }
-
- if (generateLTClause) {
- Conjunct *lt;
- if (!generateGTClause && !retainEQClause)
- lt = *conj;
- else
- lt = (*conj)->copy_conj_same_relation();
- if (max >= 0) {
- GEQ_Handle l = lt->add_GEQ(); // out<in ==> in-out-1>=0
- l.update_coef_during_simplify(in, 1);
- l.update_coef_during_simplify(out, -1);
- l.update_const_during_simplify(-1);
- }
- lt->guaranteed_leading_0s
- = lt->possible_leading_0s = leading_eqs-1;
- lt->leading_dir = -1;
- if (is_guaranteed) {
- /*
- fprintf(DebugFile,"Promising solutions to: %d <= diff%d <= %d (%d):\n",
- min,leading_eqs,max,guaranteed);
- use_ugly_names++;
- lt->prefix_print(DebugFile);
- use_ugly_names--;
- */
- lt->promise_that_ub_solutions_exist(tmp);
- }
- else if (0) {
- fprintf(DebugFile,"Can't guaranteed solutions to:\n");
- use_ugly_names++;
- lt->prefix_print(DebugFile);
- use_ugly_names--;
- }
- if (generateGTClause || retainEQClause)
- newstuff->add_conjunct(lt);
- }
-
- if (generateGTClause) {
- Conjunct *gt;
- if (retainEQClause) gt = (*conj)->copy_conj_same_relation();
- else gt = *conj;
- if (min <= 0) {
- GEQ_Handle g = gt->add_GEQ(); // out>in ==> out-in-1>=0
- g.update_coef_during_simplify(in, -1);
- g.update_coef_during_simplify(out, 1);
- g.update_const_during_simplify(-1);
- }
- gt->guaranteed_leading_0s =
- gt->possible_leading_0s = leading_eqs-1;
- gt->leading_dir = 1;
- if (is_guaranteed) {
- /*
- fprintf(DebugFile,"Promising solutions to: %d <= diff%d <= %d (%d):\n",
- min,leading_eqs,max,guaranteed);
- use_ugly_names++;
- gt->prefix_print(DebugFile);
- use_ugly_names--;
- */
- gt->promise_that_ub_solutions_exist(tmp);
- }
- else if (0) {
- fprintf(DebugFile,"Can't guaranteed solutions to:\n");
- use_ugly_names++;
- gt->prefix_print(DebugFile);
- use_ugly_names--;
- }
- if (retainEQClause) newstuff->add_conjunct(gt);
- }
-
- if (retainEQClause) {
- assert(min <= 0 && 0 <= max);
-
- if (min < 0 || max > 0) {
- e = (*conj)->add_EQ(1);
- e.update_coef_during_simplify(in, -1);
- e.update_coef_during_simplify(out, 1);
- }
-
- assert((*conj)->guaranteed_leading_0s == -1
- || leading_eqs > (*conj)->guaranteed_leading_0s);
- assert((*conj)->possible_leading_0s == -1
- || leading_eqs <= (*conj)->possible_leading_0s);
-
- (*conj)->guaranteed_leading_0s = leading_eqs;
- }
- else break;
- }
-
- {
- Set<Global_Var_ID> already_done;
- int remapped = 0;
-
- assert((*conj)->guaranteed_leading_0s == -1
- || leading_eqs <= (*conj)->guaranteed_leading_0s);
-
- for (Variable_ID_Iterator func(*body->global_decls()); func; func++) {
- Global_Var_ID f = (*func)->get_global_var();
- if (!already_done.contains(f) &&
- body->has_local(f, Input_Tuple) &&
- body->has_local(f, Output_Tuple) &&
- f->arity() == leading_eqs) {
- already_done.insert(f);
-
- // add f(in) = f(out), project one away
- e = (*conj)->add_EQ(1);
- Variable_ID f_in =body->get_local(f,Input_Tuple);
- Variable_ID f_out =body->get_local(f,Output_Tuple);
-
- e.update_coef_during_simplify(f_in, -1);
- e.update_coef_during_simplify(f_out, 1);
-
- f_out->remap = f_in;
- remapped = 1;
- is_guaranteed = false;
- }
- }
-
- if (remapped) {
- (*conj)->remap();
- (*conj)->combine_columns();
- reset_remap_field(*body->global_decls());
- remapped = 0;
- }
- }
- }
- if (is_guaranteed)
- (*conj)->promise_that_ub_solutions_exist(tmp);
- else if (0) {
- fprintf(DebugFile,"Can't guaranteed solutions to:\n");
- use_ugly_names++;
- (*conj)->prefix_print(DebugFile);
- use_ugly_names--;
- }
- }
-
- skip_finalization_check--;
- join_DNF(newstuff);
- }
-
-#if ! defined NDEBUG
- for (DNF_Iterator c(this); c; c++)
- (*c)->assert_leading_info();
-#endif
-
- simplify();
-}
-
-void DNF::remove_inexact_conj() {
- bool found_inexact=false;
-
- do {
- bool first=true;
- found_inexact=false;
- DNF_Iterator c_prev;
- for (DNF_Iterator c(this); c; c++) {
- if (!(*c)->is_exact()) { // remove it from the list
- found_inexact=true;
- delete (*c);
- if (first)
- conjList.del_front();
- else
- conjList.del_after(c_prev);
- break;
- }
- else {
- first=false;
- c_prev=c;
- }
- }
- }
- while (found_inexact);
-}
-
-
-int s_rdt_constrs;
-
-//
-// Simplify all conjuncts in a DNF
-//
-void DNF::simplify() {
- for (DNF_Iterator pd(this); pd.live(); ) {
- Conjunct *conj = pd.curr();
- pd.next();
- if(s_rdt_constrs >= 0 && !simplify_conj(conj, true, s_rdt_constrs, EQ_BLACK)) {
- rm_conjunct(conj);
- }
- }
-}
-
-} // namespace
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-02-09 01:48:04 +0000