CVC3: Solver studies #1

Installation

I followed the install directions from the website, after downloading the source distribution (cvc3-2.2.tar.gz)

Installation went fairly smoothly, I needed to apt-get bison and flex, and then I was ready to roll. I decided to run ./configure --enable-dynamic in order to make a .so for later use by python.

First Steps

First, I wanted to find out how to use the command line tool to do simple satisfaction problems. I had an initial problem where cvc3 wasn't giving me any output. Turns out you need to add the +int option to make it interactive.

As a first example, I entered the following into a test.cvc file:

x : BITVECTOR(5);
y : BITVECTOR(4);
z : BITVECTOR(5);

f : BOOLEAN =
z = BVPLUS(5, x, ~y);

ASSERT y /= 0bin1111;

CHECKSAT f;
WHERE;
COUNTERMODEL;

This yielded the following output

Satisfiable.
Current stack level is 0 (scope 4).
% Active assumptions:
ASSERT NOT (y = 0bin1111);
ASSERT NOT NOT (z = BVPLUS(5, x, (0bin0 @ (~(y))), 0bin00101));
ASSERT (BVPLUS(5, 0bin01100, z, (0bin0 @ y)) = x);
ASSERT NOT BOOLEXTRACT(y,0);

y : BITVECTOR(4);
z : BITVECTOR(5);
x : BITVECTOR(5);
% Current scope level is 4.
% Assertions which make the QUERY invalid:
ASSERT NOT (y = 0bin1111);
ASSERT (BVPLUS(5, 0bin01100, z, (0bin0 @ y)) = x);
ASSERT NOT BOOLEXTRACT(y,0);

Current scope level is 9.
%Satisfiable  Variable Assignment: %
ASSERT (x = 0bin11001);
ASSERT (y = 0bin1110);
ASSERT (z = 0bin11111)

Upcoming Steps:

Figure out how to read the COUNTEREXAMPLE output so that I can understand the sets described, formulate a clearer post on the subject later on.