Closed kjcjohnson closed 7 months ago
Fixes #113.
Adds three new "experimental" commands:
(define-intrinsic-fun <identifier> (<arg-sorts>) <return-sort>) (define-intrinsic-const <identifier> <sort>) (define-intrinsic-sort <identifier>)
These function symbols will be used during parsing, but will not be emitted as declare-function or define-function events.
declare-function
define-function
For example, to use cvc5's transcendental theory, one might do:
(define-intrinsic-const real.pi Real) (define-intrinsic-fun sin (Real) Real)
Fixes #113.
Adds three new "experimental" commands:
These function symbols will be used during parsing, but will not be emitted as
declare-functionordefine-functionevents.For example, to use cvc5's transcendental theory, one might do: