{"action":"created","issue":{"url":"https://api.github.com/repos/eigengo/lift/issues/89","labels_url":"https://api.github.com/repos/eigengo/lift/issues/89/labels{/name}","comments_url":"https://api.github.com/repos/eigengo/lift/issues/89/comments","events_url":"https://api.github.com/repos/eigengo/lift/issues/89/events","html_url":"https://github.com/eigengo/lift/pull/89","id":57725128,"number":89,"title":"CVC4 Support for Lift","user":{"login":"carlpulley","id":176421,"avatar_url":"https://avatars.githubusercontent.com/u/176421?v=3","gravatar_id":"","url":"https://api.github.com/users/carlpulley","html_url":"https://github.com/carlpulley","followers_url":"https://api.github.com/users/carlpulley/followers","following_url":"https://api.github.com/users/carlpulley/following{/other_user}","gists_url":"https://api.github.com/users/carlpulley/gists{/gist_id}","starred_url":"https://api.github.com/users/carlpulley/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/carlpulley/subscriptions","organizations_url":"https://api.github.com/users/carlpulley/orgs","repos_url":"https://api.github.com/users/carlpulley/repos","events_url":"https://api.github.com/users/carlpulley/events{/privacy}","received_events_url":"https://api.github.com/users/carlpulley/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":36,"created_at":"2015-02-15T10:05:32Z","updated_at":"2015-02-24T17:27:01Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/eigengo/lift/pulls/89","html_url":"https://github.com/eigengo/lift/pull/89","diff_url":"https://github.com/eigengo/lift/pull/89.diff","patch_url":"https://github.com/eigengo/lift/pull/89.patch"},"body":"* [x] added in CVC4 JNI jar file as unmanaged dependency\r\n* [x] defined CVC4 satisfiability function\r\n* [x] unit testing for CVC4 simplify, satisfiability and validity functions\r\n* [ ] integration testing of `ExerciseModel.evaluate` function\r\n* [x] `main` dockerfile updated to build CVC4 shared libraries\r\n* [x] defined `Vagrantfile` for building development environment\r\n* [ ] `sbt test`\r\n* [ ] ready for review/merge\r\n\r\n---\r\nIssue [LIFT-36](https://cakesolutions.jira.com/browse/LIFT-36) tracks this PR.\r\n\r\nThis PR builds on ~~https://github.com/eigengo/lift/pull/58~~ by introducing an implementation of the `SMTInterface` based on the [CVC4](http://cvc4.cs.nyu.edu/web/) theorem prover.\r\n\r\nA future PR will investigate possible viable implementations for the `SMTInterface.simplify` function via the CVC4 SMT function `simplify: Expr -> Expr` (for now, no rewriting occurs).\r\n\r\n---\r\n **[Historical]** CVC4 Install Instructions (for OS X with brew 'support'):\r\n```bash\r\nwget http://cvc4.cs.nyu.edu/builds/src/cvc4-1.4.tar.gz\r\ntar -xzvf cvc4-1.4.tar.gz\r\ncd cvc4-1.4\r\nbrew install libantlr3c swig\r\n./configure --prefix=/usr/local/Cellar/cvc4/1.4 --enable-language-bindings=java JAVA_CPPFLAGS=-I/System/Library/Frameworks/JavaVM.framework/Headers && make && make install && brew link cvc4\r\n```\r\nWe expect the JNI shared library to be located at `/usr/local/Cellar/cvc4/1.4/lib/jni/libcvc4jni.dylib`\r\n\r\n**Note:** the above instructions worked for myself on 1 machine - for the other two they failed!!\r\n\r\n---\r\n**[Default]** Instructions for building/testing within a vagrant environment (this is essentially our Docker container environment):\r\n```bash\r\ncd $LIFT_SERVER_ROOT\r\nvagrant up\r\nvagrant ssh\r\nsbt test:compile # <== if akka-persistence-cassandra fails to download, simply run again!\r\nsbt test\r\n```"},"comment":{"url":"https://api.github.com/repos/eigengo/lift/issues/comments/75802164","html_url":"https://github.com/eigengo/lift/pull/89#issuecomment-75802164","issue_url":"https://api.github.com/repos/eigengo/lift/issues/89","id":75802164,"user":{"login":"cake-demo","id":11073979,"avatar_url":"https://avatars.githubusercontent.com/u/11073979?v=3","gravatar_id":"","url":"https://api.github.com/users/cake-demo","html_url":"https://github.com/cake-demo","followers_url":"https://api.github.com/users/cake-demo/followers","following_url":"https://api.github.com/users/cake-demo/following{/other_user}","gists_url":"https://api.github.com/users/cake-demo/gists{/gist_id}","starred_url":"https://api.github.com/users/cake-demo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cake-demo/subscriptions","organizations_url":"https://api.github.com/users/cake-demo/orgs","repos_url":"https://api.github.com/users/cake-demo/repos","events_url":"https://api.github.com/users/cake-demo/events{/privacy}","received_events_url":"https://api.github.com/users/cake-demo/received_events","type":"User","site_admin":false},"created_at":"2015-02-24T17:27:01Z","updated_at":"2015-02-24T17:27:01Z","body":"\nRefer to this link for build results (access rights to CI server needed): \nhttp://jenkins.cakedemo.eigengo.io//job/dev.build.lift-scala-short-pr/3/\nshort:test  SUCCESS! Nothing less expected!"}}