Bug 227702 - New port: math/cvc4, an SMT solver
Summary: New port: math/cvc4, an SMT solver
Status: Closed FIXED
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: --- Affects Only Me
Assignee: Kurt Jaeger
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2018-04-22 20:06 UTC by Val Packett
Modified: 2018-06-21 11:06 UTC (History)
1 user (show)

See Also:

Attachments
cvc4.patch (9.06 KB, patch)
2018-04-22 20:06 UTC, Val Packett 		no flags Details | Diff
cvc4.patch (9.02 KB, patch)
2018-04-29 11:07 UTC, Val Packett 		no flags Details | Diff
Show Obsolete (1) View All Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Val Packett 2018-04-22 20:06:38 UTC 
Created attachment 192734 [details]
cvc4.patch

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

https://cvc4.cs.stanford.edu/web/
Comment 1 Val Packett 2018-04-29 11:07:08 UTC 
Created attachment 192897 [details]
cvc4.patch

oops, not actually using gsed and gawk, don't need them as deps
Comment 2 Kurt Jaeger freebsd_committer freebsd_triage 2018-06-21 11:06:15 UTC 
Committed, thanks!
Comment 3 commit-hook freebsd_committer freebsd_triage 2018-06-21 11:06:36 UTC 
A commit references this bug:

Author: pi
Date: Thu Jun 21 11:06:12 UTC 2018
New revision: 472970
URL: https://svnweb.freebsd.org/changeset/ports/472970

Log:
  New port: math/cvc4

  An efficient open-source automatic theorem prover for satisfiability modulo
  theories (SMT) problems. It can be used to prove the validity (or, dually, the
  satisfiability) of first-order formulas in a large number of built-in logical
  theories and their combination.

  WWW: https://cvc4.cs.stanford.edu/web/

  PR:		227702
  Submitted by:	Greg V <greg@unrelenting.technology>

Changes:
  head/math/Makefile
  head/math/cvc4/
  head/math/cvc4/Makefile
  head/math/cvc4/distinfo
  head/math/cvc4/files/
  head/math/cvc4/files/patch-src_base_configuration.cpp
  head/math/cvc4/files/patch-src_main_portfolio.cpp
  head/math/cvc4/pkg-descr
  head/math/cvc4/pkg-plist