From 980fe7f0849e1923f8e302fc96bc9a43975aed9e Mon Sep 17 00:00:00 2001
From: Sven Verdoolaege <skimo@kotnet.org>
Date: Tue, 1 Aug 2006 17:47:30 +0200
Subject: [PATCH] occ: add interface to barvinok_lexsmaller_ev

---
 omega/count.cc | 25 +++++++++++++++++++++++++
 omega/count.h  |  1 +
 omega/parser.l |  1 +
 omega/parser.y | 25 +++++++++++++++++++++++--
 4 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/omega/count.cc b/omega/count.cc
index b820080..6ecbbbd 100644
--- a/omega/count.cc
+++ b/omega/count.cc
@@ -50,3 +50,28 @@ evalue *rank_relation(Relation& r)
     Domain_Free(D);
     return EP;
 }
+
+evalue *count_lexsmaller(Relation& r, Relation& domain)
+{
+    varvector P_vv;
+    varvector P_params;
+    varvector D_vv;
+    varvector D_params;
+    Polyhedron *P = relation2Domain(r, P_vv, P_params);
+    int P_dim = r.is_set() ? r.n_set() : r.n_inp() + r.n_out();
+    Polyhedron *D = relation2Domain(domain, D_vv, D_params);
+    int D_dim = r.is_set() ? r.n_set() : r.n_inp() + r.n_out();
+    assert(P_dim == D_dim);
+
+    evalue *EP = NULL;
+    if (P && D) {
+	assert(P->next == NULL);
+	assert(D->next == NULL);
+	Polyhedron *C = Universe_Polyhedron(D_params.size());
+	EP = barvinok_lexsmaller_ev(P, D, D_dim, C, MAXRAYS);
+	Polyhedron_Free(C);
+    }
+    Domain_Free(P);
+    Domain_Free(D);
+    return EP;
+}
diff --git a/omega/count.h b/omega/count.h
index ffff63d..6c1f5d2 100644
--- a/omega/count.h
+++ b/omega/count.h
@@ -3,3 +3,4 @@
 
 evalue *count_relation(Relation& r);
 evalue *rank_relation(Relation& r);
+evalue *count_lexsmaller(Relation& r, Relation& domain);
diff --git a/omega/parser.l b/omega/parser.l
index cbfada2..b97b91f 100644
--- a/omega/parser.l
+++ b/omega/parser.l
@@ -198,6 +198,7 @@ void includeFile(char *s) {
 "assert_unsatisfiable" 	{ BUFFER;  return ASSERT_UNSAT; }
 "card"     	{ BUFFER;  return CARD; }
 "ranking"     	{ BUFFER;  return RANKING; }
+"count_lexsmaller"     	{ BUFFER;  return COUNT_LEXSMALLER; }
 "/"		{ BUFFER;  return RESTRICT_RANGE; }
 "&"		{ BUFFER;  return AND; }
 "|"		{ BUFFER;  return OR; }
diff --git a/omega/parser.y b/omega/parser.y
index a881330..fd8e1f0 100644
--- a/omega/parser.y
+++ b/omega/parser.y
@@ -80,7 +80,7 @@ reachable_information *reachable_info;
 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
 %token ASSERT_UNSAT
-%token CARD RANKING
+%token CARD RANKING COUNT_LEXSMALLER
 
 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
 
@@ -98,7 +98,7 @@ reachable_information *reachable_info;
 %nonassoc GIVEN
 %left OMEGA_P9
 %left '('	OMEGA_P10
-%right CARD RANKING
+%right CARD RANKING COUNT_LEXSMALLER
 
 
 %type <INT_VALUE> effort 
@@ -483,6 +483,27 @@ printf("was substantially faster on the limited domain it handled.\n");
 	    }
 	    delete $2;
 	}
+	| COUNT_LEXSMALLER relation WITHIN relation ';' {
+	    evalue *EP = count_lexsmaller(*$2, *$4);
+	    if (EP) {
+		const Variable_ID_Tuple * globals = $4->global_decls();
+		int nvar = $4->n_set();
+		int n = nvar + globals->size();
+		const char **names = new (const char *)[n];
+		$4->setup_names();
+		for (int i = 0; i < nvar; ++i)
+		    names[i] = $4->set_var(i+1)->char_name();
+		for (int i = 0; i < globals->size(); ++i)
+		    names[nvar+i] = (*globals)[i+1]->char_name();
+		print_evalue(stdout, EP, (char**)names);
+		puts("");
+		delete [] names;
+		free_evalue_refs(EP); 
+		free(EP);
+	    }
+	    delete $2;
+	    delete $4;
+	}
 	;
 
 relTripList: relTripList ',' relation ':' relation ':' relation
-- 
2.11.4.GIT