Skip to content

Instantly share code, notes, and snippets.

@hiroto-takatoshi

hiroto-takatoshi/case2

Last active August 16, 2017 04:02
Show Gist options
  • Save hiroto-takatoshi/232a9924c30fc217dac4632d30582a1c to your computer and use it in GitHub Desktop.
Save hiroto-takatoshi/232a9924c30fc217dac4632d30582a1c to your computer and use it in GitHub Desktop.
Download ZIP
cc
Raw
case2
myKB.tgds = {
TGD ( { Atom ( "U" , { "x" , "y" , "z" } ) } , { Atom ( "T" , { "x" , "y" , "z" } ) } ),
TGD ( { Atom ( "R" , { "x" , "y" } ) , Atom ( "S" , { "x" , "z" , "w" } ) } , { Atom ( "T" , { "x", "y", "z" } ) , Atom ( "V" , { "w", "x" } ) } )
};
myKB.src.localI = {
Tuple ( "R", { Cell(CONST, "1") , Cell(CONST, "1") } ),
Tuple ( "R", { Cell(CONST, "3") , Cell(CONST, "2") } ),
Tuple ( "S", { Cell(CONST, "1") , Cell(CONST, "1") , Cell(CONST, "4") } ),
Tuple ( "S", { Cell(CONST, "1") , Cell(CONST, "2") , Cell(CONST, "4") } ),
Tuple ( "U", { Cell(CONST, "3") , Cell(CONST, "2") , Cell(CONST, "3") } )
};
myKB.tga.localI = {
Tuple ( "V", { Cell(CONST, "5") , Cell(CONST, "3") } )
};
Raw
my1.cc
#include <iostream>
#include <vector>
#include <string>
#include <map>
#include <utility>
#include <iterator>
#include <cassert>
#include <type_traits>
#include <algorithm>
using namespace std;
enum cellType { VAR, CONST, NONE };
struct Cell {
enum cellType t;
string v;
Cell():t(NONE){}
Cell(enum cellType t_,string v_):t(t_),v(v_){}
bool isEmpty() { return t==NONE; }
bool isVar() { return t==VAR; }
bool isCon() { return t==CONST; }
bool mapsTo(Cell &c) {
if(isCon()) {
return equalTo(c);
}
else {
if(c.isCon()) return true;
else return equalTo(c);
}
}
bool equalTo(Cell &c) {
if(t==NONE || c.t==NONE) return true;
return t==c.t && v==c.v;
}
void operator = (const Cell &c) {
t = c.t;
v = c.v;
}
void show () {
cout<<v<<" ";
}
};
struct Atom {
string name;
vector<string> attr;
Atom(){}
Atom(string n_,vector<string>a_):name(n_),attr(a_){}
};
typedef vector<Atom> Term;
struct TGD {
Term lhs, rhs;
vector<string> joinAttr, refAttr, skolemAttr;
map<string, vector<string> > lFather, rFather;
map<pair<string,string>, int> lPos, rPos;
TGD(){}
TGD(Term l,Term r):lhs(l),rhs(r){
for(auto it : lhs) {
int len = it.attr.size();
for(int i = 0; i < len; ++i) {
string jt = it.attr[i];
lFather[jt].push_back(it.name);
lPos[make_pair(it.name, jt)] = i;
}
}
for(auto it : rhs) {
int len = it.attr.size();
for(int i = 0; i < len; ++i) {
string jt = it.attr[i];
rFather[jt].push_back(it.name);
rPos[make_pair(it.name, jt)] = i;
}
}
for(auto const &it : lFather)
if(it.second.size() > 1)
joinAttr.push_back(it.first);
for(auto const &it : rFather)
if(lFather.count(it.first) > 0)
refAttr.push_back(it.first);
else
skolemAttr.push_back(it.first);
}
TGD inverse() {
return TGD(rhs, lhs);
}
bool valid() {
return !lhs.empty() && !rhs.empty();
}
};
struct Tuple {
string name;
vector<Cell> cs;
Tuple(){}
Tuple(string n_,vector<Cell>cs_):name(n_),cs(cs_){}
Tuple(string n_,int x):name(n_) {
for(int i = 0; i < x; ++i) cs.push_back(Cell());
}
bool isPlaceHolder () {
bool ret = false;
for (auto i : cs)
ret |= i.isEmpty();
return ret;
}
bool operator == (Tuple & t) {
bool ret = (name == t.name) && (t.cs.size() == cs.size());
for(int i = 0, l = cs.size(); ret && i < l; ++i)
ret &= (cs[i].equalTo(t.cs[i]));
return ret;
}
void show () {
cout << name << ":";
for (auto i : cs) i.show();
cout << endl;
}
};
typedef vector<Tuple> Tuples;
struct Peers {
Tuples staged, localI, localD;
};
typedef Tuples Images;
struct KB { // Knowledge Base
Peers src, tga;
Images srci, tgai;
vector<TGD> tgds, tgdsi;
int nullCounter;
void stage() {
src.staged.clear();
tga.staged.clear();
src.staged = srci;
tga.staged = tgai;
clearImg();
}
void clearImg() {
srci.clear();
tgai.clear();
}
void clearUnstaged() {
src.localD.clear();
src.localI.clear();
tga.localD.clear();
tga.localI.clear();
}
void init() {
nullCounter = 0;
for(auto i : tgds)
tgdsi.push_back(i.inverse());
}
};
bool isSubset(Tuples xx, Tuples yy) {
// x sub of y, for certain sequence on a tgd rhs
if(xx.size()!=yy.size()) return false;
int len = xx.size();
for(int i = 0; i < len; ++i) {
Tuple x = xx[i], y = yy[i];
if(x.name!=y.name) return false; // should not happen
if(x.isPlaceHolder()) continue;
else if(!x.isPlaceHolder()&&y.isPlaceHolder()) return false;
else {
if(!(x==y)) return false;
}
}
return true;
}
vector<Tuples> chaseBeta (Images &si, Images &ti, TGD &tgd, Term &term, Term::iterator it, Tuples lt, Tuples rt) {
// hit; no hit is okay
// hit once is okay
// 0 - no hit; 1 - hit; (wrong)
// return vec of tuples for consistency in skl
bool ret = false;
if (it == term.end()) { // check rhs
// refs on rhs shall be the same
for (auto i : tgd.refAttr) {
Cell c;
for (auto j : tgd.rFather[i]) {
int pos = tgd.rPos[make_pair(j,i)];
for (auto k : rt) {
if (k.name == j) {
Cell cc = k.cs[pos];
if(c.isEmpty()) {
c = cc;
}
else if (!c.equalTo(cc)) {
//cout << "failrefsame" << endl;
return vector<Tuples>();
}
}
}
}
}
// also skolems
for (auto i : tgd.skolemAttr) {
Cell c;
for (auto j : tgd.rFather[i]) {
int pos = tgd.rPos[make_pair(j,i)];
for (auto k : rt) {
if (k.name == j) {
Cell cc = k.cs[pos];
if(c.isEmpty()) {
c = cc;
}
else if (!c.equalTo(cc)) {
//cout << "failsklsame" << endl;
return vector<Tuples>();
}
}
}
}
}
// finally refs shall equal on l&r
for (auto i : tgd.refAttr) {
Cell c;
for (auto j : tgd.rFather[i]) {
int pos = tgd.rPos[make_pair(j,i)];
for (auto k : rt) {
if (k.name == j) {
Cell cc = k.cs[pos];
if(c.isEmpty()) {
c = cc;
goto out1;
}
}
}
}
out1:
//cout << "theref" << endl;
//c.show();
for (auto j : tgd.lFather[i]) {
int pos = tgd.lPos[make_pair(j,i)];
for (auto k : lt) {
if (k.name == j) {
Cell cc = k.cs[pos];
//cout << j << endl << "pos " << pos << endl;
//cout << "cc" << endl;
//cc.show();
if(!c.equalTo(cc)) {
//cout << "failrefconsistency" << endl;
return vector<Tuples>();
}
goto out2;
}
}
}
out2:;
}
// print some hit info
//cout << "hit" << endl;
return {rt};
}
else { // enum rhs
vector <Tuples> ret;
ret.clear();
for (auto i : ti)
if((*it).name == i.name) {
Tuples t_ = rt;
t_.push_back(i);
vector<Tuples> vec = chaseBeta(si,ti,tgd,term,next(it),lt,t_);
if(vec.size()) ret.insert(ret.end(), vec.begin(), vec.end());
}
Tuples t_ = rt;
t_.push_back( Tuple((*it).name,(*it).attr.size()) );
vector<Tuples> vec = chaseBeta(si,ti,tgd,term,next(it),lt,t_);
if(vec.size()) ret.insert(ret.end(), vec.begin(), vec.end());
return ret;
}
assert(0);
}
bool chaseAlpha (Images &si, Images &ti, int &np, TGD &tgd, Term &term, Term::iterator it, Tuples now) {
bool done = false;
//cout << "ALpha" << endl;
//for (auto i : now) i.show();
//cout << endl;
if(it == term.end()) {
// judge
bool ok = true;
for (auto i : tgd.joinAttr) {
Cell c;
for (auto j : tgd.lFather[i]) {
for (auto k : now) {
if (k.name == j) {
int pos = tgd.lPos[make_pair(j,i)];
Cell cc = k.cs[pos];
if(c.isEmpty()) {
c = cc;
}
else {
if(!c.equalTo(cc)) {
ok = false;
goto failPoint;
}
}
}
}
}
}
failPoint:;
if(ok) {
// return the current vector in stack
// query & insert, O(n^beta)
vector<Tuples> vt = chaseBeta(si,ti,tgd,tgd.rhs,tgd.rhs.begin(),now,Tuples());
bool cont = true;
//cout << vt.size() << endl;
//char ch = getchar();
do {
vector<bool> vbool;
for(vector<Tuples>::iterator it = vt.begin(); it != vt.end(); ++it)
vbool.push_back(false);
cont = false;
int len = vt.size();
for(int i = 0; i < len; ++i)
for(int j = 0; j < len; ++j)
if(j==i || vbool[i] || vbool[j]) continue;
else if (isSubset(vt[j], vt[i])) vbool[j]=true;
vector<Tuples>::iterator it = vt.begin();
for(int i = 0; i < len; ++i,++it)
if(vbool[i]) vt.erase(it);
} while(cont);
//cout << vt.size() << endl;
//ch = getchar();
// if lhs tuples are nothing but nulls, do no insertion
bool allNull = true;
for (auto i : now) {
for (auto j : i.cs)
allNull &= j.isVar();
}
// insert a set of fresh labelled nulls to, ti
bool added = false;
for (auto vec : vt) {
// for every possible rhs pattern
bool allHit = true;
for (auto i : vec)
allHit &= !i.isPlaceHolder();
if(allHit) continue;
Tuples ts_ = Tuples();
Tuple t;
for (auto i : vec) {
if(i.isPlaceHolder()) {
ts_.push_back(Tuple(i.name,i.cs.size()));
}
}
for (auto i : tgd.skolemAttr) {
Cell c;
for (auto j : tgd.rFather[i]) {
for (auto &k : vec) {
if (k.name == j && !k.isPlaceHolder()) {
c = k.cs[tgd.rPos[make_pair(j,i)]];
}
}
}
if(c.isEmpty()) {
int sknum = ++np;
c = Cell(VAR, "_" + to_string(sknum));
}
for (auto j : tgd.rFather[i]) {
for (auto &k : ts_) {
if (k.name == j) {
k.cs[tgd.rPos[make_pair(j,i)]] = c;
}
}
}
}
for (auto i : tgd.refAttr) {
int pos = tgd.lPos[make_pair(tgd.lFather[i][0], i)];
Cell c;
//cout << "tell me how many times?" << endl;
for (auto k : now) {
if (k.name == tgd.lFather[i][0]) {
c = k.cs[pos];
break;
}
}
//cout<<"see1"<<endl,assert(!c.isEmpty()),cout<<"see"<<endl;
for (auto j : tgd.rFather[i]) {
for (auto &k : ts_) {
if (k.name == j) {
//cout << "ha?" << endl;
k.cs[tgd.rPos[make_pair(j, i)]] = c;
//k.show();
}
}
}
}
added = true;
cout << "inserted:" << endl;
for(auto i : ts_)
i.show();
char ch = getchar();
ti.insert(ti.end(), ts_.begin(), ts_.end());
}
return added;
}
else {
// fail added
return false;
}
}
else {
// enum, O(n^alpha)
bool ret = false;
for(auto i: si) {
if((*it).name == i.name) {
Tuples t_ = now;
t_.push_back(i);
ret |= chaseAlpha(si,ti,np,tgd,term,next(it),t_);
//break;
}
}
return ret;
}
}
bool checkDuplicate (Images &img, Tuple &t) {
vector <Tuple> :: iterator it = img.begin();
for(;it!=img.end()&&!(*it==t);++it);
return it!=img.end();
}
Images genImage(Peers &base) {
Images rimg;
rimg = base.staged;
for (auto i : base.localI)
if (!checkDuplicate(rimg, i))
rimg.push_back(i);
for (auto i : base.localD) {
vector <Tuple> :: iterator it = rimg.begin();
for(;it!=rimg.end()&&!(*it==i);++it);
if (it != rimg.end()) {
// should raise exception
rimg.erase(it);
}
}
return rimg;
}
int checkViolation(Peers &base, Images &img) {
// can add more, can't add deleted, can't delete existing
// true = violate
// shall raise exception
Images baseimg = genImage(base);
for (auto i : img) {
if(checkDuplicate(base.localD, i)) {
cout << "violation on local deletion" << endl;
i.show();
return 2;
}
}
for (auto i : baseimg) {
if(!checkDuplicate(img, i)) {
cout << "violation on local insertion" << endl;
i.show();
return 3;
}
}
return 0;
}
int chase(KB &kb) {
// for every possible firing situation, first do a query,
// if no tuples even with labelled nulls satisfy the query, insert a set of fresh nulls.
// on either direction, it's not ok to delete what's been inserted, vice versa.
// chase returns 1 for successful propagation, returns 0 for no new modification,
// returns 2 on invalid insertion and 3 on invalid deletion
// chase : iterate pattern, query, maybe insert
bool done (false);
int err (0);
//cout << "chase" << endl;
for(auto t : kb.tgds) {
// for every TGD
done |= chaseAlpha(kb.srci,kb.tgai,kb.nullCounter,t,t.lhs,t.lhs.begin(),Tuples());
if (err = checkViolation(kb.tga, kb.tgai)) {
cout << "wrong" << endl;
goto failPoint1;
}
else {
cout << kb.srci.size() << " " << kb.tgai.size() << endl;
char ch = getchar();
}
}
for(auto t : kb.tgdsi) {
done |= chaseAlpha(kb.tgai,kb.srci,kb.nullCounter,t,t.lhs,t.lhs.begin(),Tuples());
if (err = checkViolation(kb.src, kb.srci)) {
goto failPoint1;
}
else {
cout << kb.srci.size() << " " << kb.tgai.size() << endl;
char ch = getchar();
}
}
if(!done) return 0;
return 1; // success
failPoint1:
return err;
}
void doChaseLoop(KB &kb) {
// init
kb.clearImg();
kb.srci = genImage(kb.src);
kb.tgai = genImage(kb.tga);
// while
int err(0);
do {
err = chase(kb);
if(err > 1) {
// cout<<"saiyaku"<<endl,assert(0);
cerr << "end on case of violation" << endl;
kb.clearImg();
kb.clearUnstaged();
return;
}
//cout << err << endl;
} while(err);
// stage
kb.stage();
// show some info
}
KB theKB;
void do0() {
}
void do1() {
}
void do2() {
}
void do3() {
}
void do4() {
}
void do5() {
}
void do6() {
// TODO
}
void do7() {
exit(0);
}
void showHelp() {
cout << "-----------------------------------" << endl
<< "| 0. Clean all data. |" << endl
<< "| 1. Show Constraints. |" << endl
<< "| 2. Show data (staged and local).|" << endl
<< "| 3. Perform sync. |" << endl
<< "| 4. Perform local insertion. |" << endl
<< "| 5. Perform local deletion. |" << endl
<< "| 6. Perform local merge. |" << endl
// Merge is like del 2 and ins 1
// (possibly wrong) we are assigning some nulls to others, need to check consistency
<< "| 7. Quit. |" << endl
<< "-----------------------------------" << endl;
}
void handle(int o) {
void (*func[])() = {do0, do1, do2, do3, do4, do5, do6, do7};
(*func[o])();
cout<<"donehandle"<<endl;
}
// temp
int main1() {
// temp definitions here
KB myKB;
//myKB.tgds = { TGD ( { Atom ( "T" , { "x" , "y" } ) } , { Atom ( "U" , { "x", "y", "z" } ) } ) };
//myKB.src.localI = { Tuple ( "T", { Cell(CONST, "1") , Cell(CONST, "2") } ) };
myKB.tgds = {
TGD ( { Atom ( "U" , { "x" , "y" , "z" } ) } , { Atom ( "T" , { "x" , "y" , "z" } ) } ),
TGD ( { Atom ( "R" , { "x" , "y" } ) , Atom ( "S" , { "x" , "z" , "w" } ) } , { Atom ( "T" , { "x", "y", "z" } ) , Atom ( "V" , { "w", "x" } ) } )
};
myKB.src.localI = {
Tuple ( "R", { Cell(CONST, "1") , Cell(CONST, "1") } ),
Tuple ( "R", { Cell(CONST, "3") , Cell(CONST, "2") } ),
Tuple ( "S", { Cell(CONST, "1") , Cell(CONST, "1") , Cell(CONST, "4") } ),
Tuple ( "S", { Cell(CONST, "1") , Cell(CONST, "2") , Cell(CONST, "4") } ),
Tuple ( "U", { Cell(CONST, "3") , Cell(CONST, "2") , Cell(CONST, "3") } )
};
myKB.tga.localI = {
Tuple ( "V", { Cell(CONST, "5") , Cell(CONST, "3") } )
};
myKB.tga.localD = {
Tuple ( "T", { Cell(CONST, "3") , Cell(CONST, "2") , Cell(CONST, "3") } ),
Tuple ( "T", { Cell(CONST, "1") , Cell(CONST, "1") , Cell(CONST, "1") } )
};
myKB.init();
doChaseLoop(myKB);
exit(0);
}
int main() {
main1();
while(true) {
showHelp();
int o;
cin >> o;
if(cin.fail()) showHelp();
if(!o) return 0;
if(o > 0 && o < 8) handle(o);
//else showHelp();
}
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment