11:50 Yuri Victorovich (yuri) 

math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5

Remove the PYTHON option - it will be made into a separate port.

    faf8043

15:20 fernape 

math/cvc4: update to 1.7

ChangeLog:

https://github.com/CVC4/CVC4/releases/tag/1.7

* New Features:
    Proofs:
        Support for bit-vector proofs with eager bitblasting
    Strings:
        Support for str.replaceall operator.
        New option --re-elim
    SyGuS:
        Support for abduction (--sygus-abduct)

* Improvements:
    Strings:
        Significantly better performance

* Changes:
    API change: Expr::iffExpr() is renamed to Expr::eqExpr()
    Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
    The CVC3 compatibility layer has been removed.
    The build system now uses CMake instead of Autotools

 

18:30 yuri 

math/cvc4: Update 1.5 -> 1.6

Port changes:
* Add dependency on cryptominisat, and the corresponding port option
* Add USES=autoreconf, the suplied configure fails, see
https://github.com/CVC4/CVC4/issues/2192
* Now build depends on python
* Force clang-60 to prevent build failures on 10

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

 

11:06 pi 

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>