About Vine-1.0

[nicko]

Hi, everyone

Can Vine-1.0 generate files for the STP in a format different from the CVC?

He also uses the CVC format, do I understand correctly?

[Alex Bazhanyuk]

vine can generated stp code from IL code.

vine cannot transform formats of solver.

--
 
---
You received this message because you are subscribed to the Google Groups "BitBlaze User Discussion group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bitblaze-user...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

--
Thanks,
Alex

[Stephen McCamant]

>>>>> "N" == nicko <ochir...@gmail.com> writes:

N> Hi, everyone
N> Can Vine-1.0 generate files for the STP in a format different from
N> the CVC? He also uses the CVC format, do I understand correctly?

The historically native format of STP is a subset of the format
accepted by the older tool CVC, which they now refer to as "CVC
format". The Vine code and libraries usually just refer to this as
"STP format" (e.g. ocaml/stp.ml), and this is the best supported
output format for formulas from Vine.

The Vine 1.0 release also contains some code for converting Vine
expressions into SMT-LIB format, which is a common interchange format
supported by a number of other SMT solvers along with STP; this is in
the file "ocaml/smt-lib.ml". From the age, and since it doesn't
specify a version, I'm guessing this predates SMT-LIB 2, though the
versions are relatively similar. However this code hasn't been as well
tested as the STP code paths, and for instance it's not supported by
command-line options in the wrapper tools like appreplay and wputil.

Another possibility you can explore if you want to convert Vine's
formula outputs into other formats is that STP has the capability of
translating any formula it can read into any of its supported input
formats, via the --print-back-CVC, --print-back-SMTLIB1, and
--print-back-SMTLIB2 options. So for instance you could also get
SMT-LIB 2 output by getting CVC-format output out of Vine and then
translating it via STP.

Hope this helps,

-- Stephen

[nicko]

Thank you, Stephen and Alex.

I did not understand how to use this option

I write the following:

        

                 ./stp/stp-print-back-SMTLIB2 five.stp

        Output:

                 Invalid.

                 ASSERT( INPUT_1001_0000_61  = 0hex35  );

                 ASSERT( INPUT_1001_0000_61  = 0hex35  );

Could you give an example of using this option, please?

вторник, 12 марта 2013 г., 13:41:36 UTC+3 пользователь nicko написал:

[Stephen McCamant]

>>>>> "N" == nicko <ochir...@gmail.com> writes:

N> Thank you, Stephen and Alex.
N> I did not understand how to use this option
N> I write the following:

N> ./stp/stp-print-back-SMTLIB2 five.stp
N> Output:
N> Invalid.
N> ASSERT( INPUT_1001_0000_61 = 0hex35 );
N> ASSERT( INPUT_1001_0000_61 = 0hex35 );

N> Could you give an example of using this option, please?

The option in question being "--print-back-SMTLIB2", I presume?

The sample execution you quote above seems strangely confused. Like a
usual option for a Unix program, you pass "--print-back-SMTLIB2" as a
separate command-line argument, so there should be a space between the
name of the program and the option. In the command you quoted above,
there's no space between "stp" and the option, so your system would
look for a program named "stp-print-back-SMTLIB2". That wouldn't work
unless you had renamed your binary to that.

Perhaps your real problem is that you are attempting to use this
option with an STP binary distributed with Vine 1.0? Those binaries
are too old to include this functionality. You can tell that's the
problem if STP prints a usage message that includes other options but
not that one. You'll need to compile yourself a new STP binary, see:

https://sites.google.com/site/stpfastprover/

Once you have an appropriate STP binary, the option is
"--print-back-SMTLIB2" with two "-"s at the front; it will cause STP
to print the rewritten formula to standard output rather than solving
it. So a command to use it would look like:

% ,.stp --print-back-SMTLIB2 /tmp/five.stp >/tmp/five.smt2

[nicko]

Thank you, Stephen!
Again copy-paste failed me( I typed space between "stp" and option )

I don't know that Vine's distribution of STP so old.
Hope this helps!

вторник, 12 марта 2013 г., 13:41:36 UTC+3 пользователь nicko написал:

Hi, everyone