Bug 227702

Summary: New port: math/cvc4, an SMT solver
Product: Ports & Packages Reporter: Val Packett <val>
Component: Individual Port(s)Assignee: Kurt Jaeger <pi>
Status: Closed FIXED    
Severity: Affects Only Me CC: pi
Priority: ---    
Version: Latest   
Hardware: Any   
OS: Any   
Attachments:
Description Flags
cvc4.patch
none
cvc4.patch none

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