search

dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
151 stars 32 forks source link

Support `define-fun` #225

Closed LeventErkok closed 4 years ago

LeventErkok commented 4 years ago

Another SMTLib2 nicety. The sequence:

(declare-fun s0 () Int)
(assert (= s0 1))

can be abbreviated to:

(define-fun s0 () Int 1)

This makes the benchmarks generated easier to read, and also can be taken advantage of internally by tools as they are essentially constants. (Easily discoverable by constant-folding, but helpful nonetheless.) But their main use case is to simplify generation of benchmarks, and reduce interprocess communication as it compresses two SMTLib commands into one.

Not an absolute must, but would be good to support this abbreviation. Almost all other solvers do.

soonho-tri commented 4 years ago

Please ignore the deleted comment, but try the following:

(set-logic QF_NRA)
(set-option :smtlib2_compliant true)
(define-fun s0 () Int 1)
(assert (= s0 1))
(check-sat)
(get-value (s0))
(exit)
LeventErkok commented 4 years ago

Quite right! I must've somehow confused myself to think it wasn't supported. Sorry about the noise!

soonho-tri commented 4 years ago

No problem. Thanks for checking things!