MISTRAL
mistral.png

Introduction

Mistral is an SMT solver which decides satisfiability of formulas in the theory of linear arithmetic over integers and theory of equality with uninterpreted functions. Mistral is written in C++ and can be used both through a graphical user interface as well as a C++ library. In addition to deciding satisfiability, Mistral consists of the following modules:

Requirements and Installation

You can obtain the source code of Mistral from http://www.cs.utexas.edu/~tdillig/mistral-1.1.tar.gz

Mistral has been tested to compile on Ubuntu 12.04. First, to compile Mistral, you need to have cmake installed on your system as well as a set of other required libraries. On a recent Ubuntu/Kubuntu system, the following command will install everything you need: 

sudo apt-get install libc6-dev-i386 gettext gawk flex libmpfr-dev cmake  \
kdelibs5-dev libgtkmm-2.4-dev libboost-thread-dev libboost-serialization-dev \
libglademm-2.4-dev graphviz doxygen g++ libgmp-dev build-essential flex bison  \
binutils-gold

Once you have cmake installed, go to the mistral folder and type the following commands 

mkdir build
cd build
cmake ..
make

Once you type these commands, you can use Mistral either through a graphical user interface or as a library. For using Mistral from the GUI, type the following commands:

cd ui
../build/ui/mistral_ui

You can only start the Mistral GUI from the /mistral/ui folder

If you want to use Mistral as a library, see the Section Getting Started.

Getting Started

Logical formulas are represented in Mistral using the Constraint type. For example, you can construct boolean constants true and false in the following way: 

Constraint t(true);
Constraint f(false);

Here "t" represents the boolean constant "true" and "f" represents the boolean constant false. More complicated formulas are constructed using Term. Terms can be ConstantTerm (such as 0), VariableTerm (such as x), ArithmeticTerm (such as 3x + 2y), or FunctionTerm (such as f(g(x, 0), a)). Here is an example illustrating creation of various kinds of terms. 

   Term* t1 = VariableTerm::make("a");
   Term* t2 = VariableTerm::make("b");

   map<Term*, long int> elems;
   elems[t1] = 3;
   elems[t2] = 7;
   Term* t3 = ArithmeticTerm::make(elems, 2);

   vector<Term*> args;
   args.push_back(t1);
   Term* t4 = FunctionTerm::make("f", args);

Here, term t3 represents the arithmetic term 3a + 7b + 2, and term t4 represents the function term f(a).

Now, using these terms, we can create more interesting constraints. For example, the following code snippet shows how to create the constraint f(a) <= b & 3a + 7b + 2 = 4:

Constraint c1(t4, t2, ATOM_LEQ);
Constraint c2(t3, ConstantTerm::make(4), ATOM_EQ);
Constraint c3 = c1 & c2;

In this example, c1 corresponds to the formula f(a) <= b, c2 represents the formula 3a + 7b + 2 =4, and c3 represents the conjunction of c1 and c2. Mistral overloads the C++ operators &, |, ! for performing conjunction, disjunction, and negation of formulas respectively. For example, in the following code snippet:

Constraint c4 = !c1;
Constraint c5 = c4 | c2;

c4 represents the formula f(a) > b and c5 represents the disjunction of f(a) > b and 3a + 7b + 2 = 4.

Checking Satisfiability and Validity

Now that we can construct constraints, we can use Mistral to decide their satisfiability and validity:

bool res1 = c5.sat_discard();
bool res2 = c3.valid_discard();
bool res3 = c5.equivalent(c3);

Here res1 is true if and only if the formula represented by c5 is satisfiable, and res2 is true if and only if the formula represented by c3 is valid. The equivalent method of Constraint is used to check equivalence. Therefore, res3 is true if and only if c2 and c5 are equivalent.

There is also another way to check satisfiability and validity in Mistral using the sat() and valid() methods rather than sat_discard() and valid_discard(). The difference between these is that sat() and valid() also simplify the formula, as described in this publication . Therefore, the methods sat and valid are more expensive than sat_discard and valid_discard and should only be used if you want the formula to get simplified after performing a satisfiability or validity query. The section Simplify describes this in more detail.

Given a satisfiable constraint, Mistral also provides a way for obtaining satisfying assignments as follows:

map<Term*, SatValue> assignment;
bool res = c5.get_assignment(assignment);
for(auto it = assignment.begin(); it!= assignment.end(); it++)
{
    Term* t = it->first;
    SatValue sv = it->second;
    cout << " Term: " << t->to_string() << " satisfying assignment: " << sv.to_string() << endl;
}

The code snippet above shows how to obtain and print the satisfying assignment for formula represented by c5. In this code snippet, res indicates whether c5 is satisfiable, and, if res is true, "assignment" is a full satisfying assignment from each term in the formula to a satisfying value.

Other Functionalities

In addition to checking satisfiability and validity, Mistral can be used for performing abductive inference, simplifying constraints, performing quantifier elimination, and computing minimum satisfying assignments. For tutorials on using these functionalities, please refer to the Explain, Simplify, Cooper, and MSAFinder pages.

People

Mistral is developed and maintained by:

Other people who have contributed to some of the ideas implemented in Mistral include:

Publications

The techniques described in the following publications are incorporated in Mistral:

Acknowledgments

We are grateful to the developers of the MiniSAT SAT solver, which forms the SAT solving engine of Mistral. We also thank the developers of the GNU MP Bignum Library .

License and Support

Mistral is freely available for research purposes under the GPL license .

Generated on Thu Dec 13 2012 19:09:06 by   doxygen 1.7.6.1