CODEWITHSUNDEEP
z3
user2972285
user2972285

Reputation: 21

I want to know whether Z3 supports that a input file includes an another file

I have two files, one is variable definition file, the other is formula file. Could you tell me how to insert the variable definition file into formula file. In yices, we can use "(include "file")" to do it.

Upvotes: 2

Views: 150

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Z3 does not have an include command. However, you can use cat and pipes for doing what you want. For example, suppose you have the files def.smt2 and form.smt2. Then, you can use the following command for concatenating and then invoking Z3.

  cat def.smt2 form.smt2 | z3 -in -smt2

The option -in tells z3 to use the standard input, and -smt2 that the input is in SMT 2.0 format.

Upvotes: 2

Related Questions