{"action":"created","issue":{"url":"https://api.github.com/repos/tracer-x/klee/issues/43","repository_url":"https://api.github.com/repos/tracer-x/klee","labels_url":"https://api.github.com/repos/tracer-x/klee/issues/43/labels{/name}","comments_url":"https://api.github.com/repos/tracer-x/klee/issues/43/comments","events_url":"https://api.github.com/repos/tracer-x/klee/issues/43/events","html_url":"https://github.com/tracer-x/klee/pull/43","id":142587496,"number":43,"title":"The implementation of Fourier Motzkin Elimination algorithm","user":{"login":"feliciahalim","id":11381494,"avatar_url":"https://avatars.githubusercontent.com/u/11381494?v=3","gravatar_id":"","url":"https://api.github.com/users/feliciahalim","html_url":"https://github.com/feliciahalim","followers_url":"https://api.github.com/users/feliciahalim/followers","following_url":"https://api.github.com/users/feliciahalim/following{/other_user}","gists_url":"https://api.github.com/users/feliciahalim/gists{/gist_id}","starred_url":"https://api.github.com/users/feliciahalim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/feliciahalim/subscriptions","organizations_url":"https://api.github.com/users/feliciahalim/orgs","repos_url":"https://api.github.com/users/feliciahalim/repos","events_url":"https://api.github.com/users/feliciahalim/events{/privacy}","received_events_url":"https://api.github.com/users/feliciahalim/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":9,"created_at":"2016-03-22T09:04:39Z","updated_at":"2016-04-25T01:47:46Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/tracer-x/klee/pulls/43","html_url":"https://github.com/tracer-x/klee/pull/43","diff_url":"https://github.com/tracer-x/klee/pull/43.diff","patch_url":"https://github.com/tracer-x/klee/pull/43.patch"},"body":"Hi Andrew, I have pushed the implementation of Fourier Motzkin Elimination algorithm. It currently able to make subsumption for all addition_safe example in https://github.com/feliciahalim/klee-examples/tree/master/basic . \r\n\r\nHowever, there are still limitations in the current version such as it works only for addition and subtraction operation. This version also has not handle strict inequality. I will continue to work on it by enable more operation and also handling strict inequality. "},"comment":{"url":"https://api.github.com/repos/tracer-x/klee/issues/comments/214090101","html_url":"https://github.com/tracer-x/klee/pull/43#issuecomment-214090101","issue_url":"https://api.github.com/repos/tracer-x/klee/issues/43","id":214090101,"user":{"login":"domainexpert","id":696558,"avatar_url":"https://avatars.githubusercontent.com/u/696558?v=3","gravatar_id":"","url":"https://api.github.com/users/domainexpert","html_url":"https://github.com/domainexpert","followers_url":"https://api.github.com/users/domainexpert/followers","following_url":"https://api.github.com/users/domainexpert/following{/other_user}","gists_url":"https://api.github.com/users/domainexpert/gists{/gist_id}","starred_url":"https://api.github.com/users/domainexpert/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/domainexpert/subscriptions","organizations_url":"https://api.github.com/users/domainexpert/orgs","repos_url":"https://api.github.com/users/domainexpert/repos","events_url":"https://api.github.com/users/domainexpert/events{/privacy}","received_events_url":"https://api.github.com/users/domainexpert/received_events","type":"User","site_admin":false},"created_at":"2016-04-25T01:47:46Z","updated_at":"2016-04-25T01:47:46Z","body":"@feliciahalim Correction: The normalization procedure is O(n . log n). Still, replacing it with O(n) procedure would be good. When matrices are used, no normalization needs to be done at each step, and matching is done in O(n) steps. Here, the columns are for the variables used in each term, and the rows are for the inequalities. The matching procedure is done by traversing the terms in two matching inequalities in the same order, while subtracting the coefficients of the corresponding terms with the same variables in both inequalities. "}}