Output tags ¶
cvc5 supports printing information about certain aspects of the solving process that is intended for regular users. This feature can be enabled using the output option.
The following output tags are currently supported:
inst ¶
With
-o
inst
, cvc5 prints information about quantifier instantions for individual quantifers.
$ bin/cvc5 -o inst ../test/regress/cli/regress1/quantifiers/qid-debug-inst.smt2
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
sygus ¶
With
-o
sygus
, cvc5 prints information about the internal SyGuS solver including enumerated terms and generated candidates.
$ bin/cvc5 -o sygus ../test/regress/cli/regress0/sygus/print-debug.sy
(sygus-enum 0)
(sygus-candidate (f 0))
(sygus-enum 1)
(sygus-candidate (f 1))
(
(define-fun f () Int 1)
)
sygus-grammar ¶
With
-o
sygus-grammar
, cvc5 prints the grammar it generates for a function-to-synthesize when no grammar was provided.
$ bin/cvc5 -o sygus-grammar ../test/regress/cli/regress0/sygus/print-grammar.sy
(sygus-grammar f
((f_Int Int) (f_Bool Bool) )
((f_Int Int ((Constant Int) x y 0 1 (+ f_Int f_Int) (- f_Int f_Int) (ite f_Bool f_Int f_Int) ))
(f_Bool Bool ((Constant Bool) true false (= f_Int f_Int) (<= f_Int f_Int) (not f_Bool) (and f_Bool f_Bool) (or f_Bool f_Bool) ))
))
(
(define-fun f ((x Int) (y Int)) Int 0)
)
trigger ¶
With
-o
trigger
, cvc5 prints the selected triggers when solving a quantified formula.
$ bin/cvc5 -o trigger ../test/regress/cli/regress1/quantifiers/qid-debug-inst.smt2
(trigger myQuant1 ((not (= (R x) false))))
(trigger myQuant1 ((not (= (P x) true))))
(trigger myQuant2 ((not (= (P x) false))))
(trigger myQuant2 ((not (= (Q x) true))))
unsat
raw-benchmark ¶
With
-o
raw-benchmark
, cvc5 prints the benchmark back just as it has been parsed.
$ bin/cvc5 -o raw-benchmark ../test/regress/cli/regress0/datatypes/datatype-dump.cvc.smt2
(set-logic ALL)
(declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
(declare-fun x () nat)
(check-sat-assuming ( (not (and (not ((_ is succ) x)) (not ((_ is zero) x)))) ))
sat
learned-lits ¶
With
-o
learned-lits
, cvc5 prints input literals that it has learned to hold globally.
$ bin/cvc5 -o learned-lits ../test/regress/cli/regress0/printer/learned-lit-output.smt2
(learned-lit (>= x 11) :preprocess)
(learned-lit (>= x 5))
(learned-lit (>= y 1))
sat
subs ¶
With
-o
subs
, cvc5 prints top-level substitutions learned during preprocessing.
$ bin/cvc5 -o subs ../test/regress/cli/regress0/printer/print_subs.smt2
(substitution (= a 3))
sat
post-asserts ¶
With
-o
post-asserts
, cvc5 prints a benchmark corresponding to the assertions of the input problem after preprocessing.
$ bin/cvc5 -o post-asserts ../test/regress/cli/regress0/printer/post-asserts-output.smt2
;; post-asserts start
(set-logic ALL)
(assert true)
(assert true)
(check-sat)
;; post-asserts end
sat
pre-asserts ¶
With
-o
pre-asserts
, cvc5 prints a benchmark corresponding to the assertions of the input problem before preprocessing.
deep-restart ¶
With
-o
deep-restart
, cvc5 prints when it performs a deep restart along with the literals it has learned.
$ bin/cvc5 -o deep-restart ../test/regress/cli/regress0/printer/deep-restart-output.smt2
sat
incomplete ¶
With
-o
incomplete
, cvc5 prints reason for why it answers unknown for any given check-sat query.
$ bin/cvc5 -o incomplete ../test/regress/cli/regress0/printer/incomplete.smt2
(incomplete INCOMPLETE QUANTIFIERS)
unknown