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

inst-strategy

With -o inst-strategy, cvc5 prints a summary of the instantiation techniques as they are run.

$ bin/cvc5 -o inst-strategy ../test/regress/cli/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2
(inst-strategy cbqi :inst 1 :time 0.000258)
(inst-strategy cbqi :inst 1 :time 0.002681)
(inst-strategy cbqi :inst 2 :time 0.00451)
(inst-strategy cbqi :time 0.003734)
(inst-strategy ematching :inst 183 :time 0.022799)
(inst-strategy cbqi :inst 1 :time 0.003798)
(inst-strategy cbqi :inst 1 :time 0.003595)
(inst-strategy cbqi :inst 1 :time 0.003572)
unsat

oracles

With -o oracles, cvc5 prints the I/O of calls made to external oracles.

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 ((A_Int Int) (A_Bool Bool) )((A_Int Int (x y 0 1 (+ A_Int A_Int) (- A_Int A_Int) (ite A_Bool A_Int A_Int)))(A_Bool Bool (false true (= A_Int A_Int) (<= A_Int A_Int) (not A_Bool) (and A_Bool A_Bool) (or A_Bool A_Bool)))))
(
(define-fun f ((x Int) (y Int)) Int 0)
)

sygus-enumerator

With -o sygus-enumerator, cvc5 prints enumerators generated by the sygus solver.

$ bin/cvc5 -o sygus-enumerator ../test/regress/cli/regress0/sygus/print-enumerator.sy
(sygus-enumerator :synth-fun f :role SINGLE_SOLUTION :type FAST)
(
(define-fun f ((x Int) (y Int)) Int x)
)

sygus-sol-gterm

With -o sygus-sol-gterm, cvc5 prints annotations for terms in sygus solutions that indicate the grammar used to generate them.

$ bin/cvc5 -o sygus-sol-gterm ../test/regress/cli/regress0/sygus/print-sygus-gterm.sy
(sygus-sol-gterm (f (! (+ (! 1 :gterm a) (! 1 :gterm b)) :gterm a)))
(
(define-fun f () Int (+ 1 1))
)

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) :input)
(learned-lit (>= y 1) :input)
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.

$ bin/cvc5 -o pre-asserts ../test/regress/cli/regress0/printer/pre-asserts-output.smt2
;; pre-asserts start
(set-logic ALL)
(declare-fun x () Int)
(assert (= x x))
(check-sat)
;; pre-asserts end
sat

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
(deep-restart ((= f k)))
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

lemmas

With -o lemmas, cvc5 prints lemmas as they are added to the SAT solver.

$ bin/cvc5 -o lemmas ../test/regress/cli/regress0/printer/print_sat_lemmas.smt2
(lemma (=> (forall ((x Int)) (P x)) (P 5)) :source QUANTIFIERS_INST_CBQI_CONFLICT)
unsat

trusted-proof-steps

With -o trusted-proof-steps, cvc5 prints formulas corresponding to trusted proof steps in final proofs.

$ bin/cvc5 -o trusted-proof-steps ../test/regress/cli/regress0/printer/print_trusted_proof_steps.smt2
unsat
(trusted-proof-step (=> true (= (= 0 1) false)))
(define @t1 () (= 0 1))
(assume @p1 @t1)
; WARNING: add trust step for MACRO_SR_EQ_INTRO
; trust MACRO_SR_EQ_INTRO
(step @p2 :rule trust :premises () :args ((= @t1 false)))
(step @p3 false :rule eq_resolve :premises (@p1 @p2))

timeout-core-benchmark

With -o timeout-core-benchmark, cvc5 prints the corresponding benchmark when it successfully computes a timeout core.

$ bin/cvc5 -o timeout-core-benchmark ../test/regress/cli/regress1/print_timeout_core.smt2
;; timeout core
(set-logic ALL)
(declare-fun x () Int)
(assert (= (* x x x) 564838384999))
(check-sat)
;; end timeout core
unknown
(
hard
)

unsat-core-benchmark

With -o unsat-core-benchmark, cvc5 prints the corresponding benchmark when it successfully computes an unsat core.

$ bin/cvc5 -o unsat-core-benchmark ../test/regress/cli/regress0/printer/print_unsat_core.smt2
unsat
;; unsat core
(set-logic ALL)
(declare-fun x () Int)
(assert (and (> x 2) (< x 0)))
(check-sat)
;; end unsat core
(
x20
)

unsat-core-lemmas-benchmark

With -o unsat-core-lemmas-benchmark, cvc5 prints the corresponding benchmark when it successfully computes an unsat core that includes the theory lemmas used.

$ bin/cvc5 -o unsat-core-lemmas-benchmark ../test/regress/cli/regress0/printer/print_unsat_core_lemmas.smt2
unsat
;; unsat core + lemmas
(set-logic ALL)
(declare-fun x () Int)
(assert (and (> x 2) (< x 0)))
(assert (or (not (>= x 3)) (>= x 0)))
(check-sat)
;; end unsat core + lemmas
(
(or (not (>= x 3)) (>= x 0))
)

portfolio

With -o portfolio, cvc5 prints the option strings tried in portfolio mode.

$ bin/cvc5 -o portfolio ../test/regress/cli/regress0/printer/portfolio-out.smt2 --use-portfolio
(portfolio "--simplification=none --enum-inst" :timeout 0.025)
(portfolio-success "--simplification=none --enum-inst")
unsat

block-model

With -o block-model, cvc5 prints the formulas used when block-model is run.

$ bin/cvc5 -o block-model ../test/regress/cli/regress0/printer/block_model_out.smt2
sat
(block-model (and (> y 0) (= x 4)))
sat
(block-model (and (> y 0) (= x 5)))

options-auto

With -o options-auto, cvc5 prints the options set during automatic configuration.

$ bin/cvc5 -o options-auto ../test/regress/cli/regress0/printer/print_options_auto.smt2
(options-auto bv-propagate false :reason "bitblast solver")
(options-auto arith-rewrite-equalities 1 :reason "logic")
(options-auto standard-effort-variable-order-pivots 200 :reason "logic")
(options-auto nl-rlv-assert-bounds 1 :reason "non-quantified logic")
(options-auto decision stoponly :reason "logic")
(options-auto quant-dsplit none :reason "non-datatypes logic")
sat