<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: HOWTO Write a Decision Procedure</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li class="current"><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div>
<div class="header">
<div class="headertitle">
<div class="title">HOWTO Write a Decision Procedure </div> </div>
</div>
<div class="contents">
<div class="textblock"><p>Note: This document is under construction. Some newer aspects of adding a decision procedure are not yet documented here. Please let us know if you have a question that is not answered here.</p>
<h2><a class="anchor" id="theory_api_contents"></a>
Contents</h2>
<ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_prelim">Preliminaries and Coding Guidelines</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_files">Directory Structure and Files</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_naming">Naming Convensions</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_general">General Guidelines</a> </li>
</ul>
</li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_addnew">Adding New Theory</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_start">Before You Start...</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_config">Configure and Makefiles</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_header">Header File: theory_foo.h</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_expr">Kinds, Expressions, and Types</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_kind_decl">Kind Declaration</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_kind_reg">Kind Registration</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_expr_subclass">New Expression Subclasses</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_methods">Constructor and API Methods</a> </li>
</ul>
</li>
</ul>
</li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_invars">Theory API: The Very Important Invariants</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_flow">High-Level Information Flow</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_backtrack">Backtracking Data Structures</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_ileaves">Variables and Foreign Terms (i-Leaves)</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_inputs">Methods Reimplemented in a Subclass</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_assertFact">assertFact()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_checkSat">checkSat(bool fullEffort)</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_setup">setup()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_update">update()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_addSharedTerm">addSharedTerm()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_rewrite">rewrite(Expr e)</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_solve">solve(Theorem e)</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_computeType">computeType()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_computeTCC">computeTCC()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_notifyInconsistent">notifyInconsistent()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_print">print()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_parseExprOp">parseExprOp()</a> </li>
</ul>
</li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_outputs">Methods Provided by Theory API</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_enqueueFact">enqueueFact()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_setInconsistent">setInconsistent()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_simplifyThm">simplifyThm() and simplify()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_enqueueEquality">enqueueEquality()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_inconsistentThm">inconsistentThm() and inconsistent()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_isTerm">isTerm()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_isLiteral">isLiteral()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_isAtomic">isAtomic()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_updateHelper">updateHelper()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_getType">getType()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_getTCC">getTCC()</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_parseExpr">parseExpr()</a> </li>
</ul>
</li>
</ul>
</li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_proofs">Proof Rules: The Trusted Core</a> <ul>
<li>
<a class="el" href="theory_api_howto.html#theory_api_proof_classes">Hierarchy of Classes</a> </li>
<li>
<a class="el" href="theory_api_howto.html#theory_api_proof_rule">Implementing a Proof Rule</a> </li>
</ul>
</li>
</ul>
<h2><a class="anchor" id="theory_api_prelim"></a>
Preliminaries and Coding Guidelines</h2>
<h3><a class="anchor" id="theory_api_files"></a>
Directory Structure and Files</h3>
<p>Each theory (a.k.a. decision procedure, or DP) must reside in a directory <code>src/theory_foo</code> (where <code>foo</code> is the theory name). All the sounce files and <code>Makefile.in</code> must be in that directory, except for some shared header files, which must reside in the common directory <code>src/include</code>. In particular, <code>theory_foo.h</code> must be placed in <code>src/include</code>.</p>
<p>The master source file for a theory should be called <code>theory_foo.cpp</code>. Typically, a new theory needs its own set of proof rules, which are implemented as three files: <code>foo_proof_rules.h</code>, <code>foo_theorem_producer.h</code>, and <code>foo_theorem_producer.cpp</code>. The first one is the abstract interface to the rules, which the untrusted DP code can <code>#include</code>. The other two files implement this abstract API, and comprise the trusted part of the code. All these files should be placed in <code>src/theory_foo</code>.</p>
<h3><a class="anchor" id="theory_api_naming"></a>
Naming Convensions</h3>
<p>Each individual theory is a subclass of a Theory class, and therefore, its name should be <code>class TheoryFoo</code>.</p>
<p>A theory may define several methods for creating expressions in <code>theory_foo.h</code>. Typically, they are named as <code>barExpr()</code>, <code>bazExpr()</code>, etc. For instance, <code><a class="el" href="theory__arith_8h.html">theory_arith.h</a></code> defines <a class="el" href="namespaceCVC3.html#accd3d7d38b0e04136afbc3e5191bc8bb">plusExpr()</a>, <a class="el" href="namespaceCVC3.html#a9ba326c305c5aeb61de515009aaa61f8">minusExpr()</a>, etc. These functions are most useful if they are declared as non-member functions (not part of the class <code>TheoryFoo</code>), since then they can be called directly by the <a class="el" href="namespaceCVC3.html">CVC3</a> library users.</p>
<p>It is also convenient to define testers like <code>isBar()</code> and <code>isBaz()</code>, which return true for the corresponding expressions. For example, <code><a class="el" href="theory__arith_8h.html">theory_arith.h</a></code> defines <code><a class="el" href="namespaceCVC3.html#afb0f7d15ddbd87f9abb128108101f557">isPlus()</a></code>, <code><a class="el" href="namespaceCVC3.html#ae89ac977fe1032189f00bccb1bb94b92">isMinus()</a></code>, etc.</p>
<p>Of course, the rest of the code should follow our general naming and coding guidelines described at length in the project FAQ: <a href="http://verify.stanford.edu/savannah/faq/?group_id=1&question=How_Do_I_Become_A_CVC3_Developer.txt">http://verify.stanford.edu/savannah/faq/?group_id=1&question=How_Do_I_Become_A_CVC3_Developer.txt</a> .</p>
<h3><a class="anchor" id="theory_api_general"></a>
General Guidelines</h3>
<p>The Theory API is designed to minimize the changes in the central (core) files when adding a new theory. Ideally, only <code><a class="el" href="vcl_8cpp.html">src/vcl/vcl.cpp</a></code> file needs to be modified to add a constructor call to the new theory. Everything else --- kinds, special expression subclasses, types, etc. --- can (and should) be defined locally in the theory-specific files.</p>
<p>There are several important guidelines for writing proof rules specific to your theory:</p>
<ul>
<li>
<p class="startli">Each proof rule must be mathematically sound.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">It is a mortal sin to introduce a proof rule without a proper doxygen comment concisely and clearly describing what it does.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">The code must contain enough <code>CHECK_SOUND</code> checks to guarantee that all the premises are of the right form, and all the side conditions of the rule are satisfied. That is, if these soundness checks pass, then the rule application is guaranteed to be sound mathematically.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">Keep the code in each rule as clean and simple as possible, so that the correctness of the implementation w.r.t. the mathematical formulation can be easily checked by manual inspection. That is, many simple and independent rules are strongly preferred to a few big mega-rules.</p>
<p class="endli"></p>
</li>
<li>
<p class="startli">Avoid calling other proof rules from within a proof rule. Rule of thumb: if your rule has to use other rules, most likely, it is a <em>strategy</em> (a derived rule), and should be implemented in the untrusted part of the code (e.g. in <code>theory_foo.cpp</code>).</p>
<p class="endli"></p>
</li>
</ul>
<p>More details are given in the separate <a class="el" href="theory_api_howto.html#theory_api_proofs">section on proof rules</a>.</p>
<p>Finally, and <em>most importantly</em>: <b>document your code!!</b></p>
<p>Every method, variable, class, or type should have a doxygen-style comment with <em>at least</em> a brief description:</p>
<div class="fragment"><pre class="fragment">
//! Convert Blah expression to Baz value
Baz Blah2Baz(const Blah& b);
</pre></div><p>Imagine telling such a description to your colleague who has very faint idea of what you are coding. If a brief description does not make sense to him/her, or the function does something non-trivial or non-obvious, add a longer description:</p>
<div class="fragment"><pre class="fragment">
//! Convert Blah expression to Baz value
/*!
* Recursively descend into Blah, collect every Foo-leaf, order them in
* the descending order of Baz-ability, and wrap into the Baz expression.
*
* \param b is a non-trivial Blah value (otherwise we assert-fail).
*/
Baz Blah2Baz(const Blah& b);
</pre></div><p>Often it is convenient to keep the brief description in the <code>*.h</code> file, and the long description in the corresponding <code>*.cpp</code> file.</p>
<p>The only exceptions are the <a class="el" href="group__Theory__API.html#theory_api">Theory API methods</a>, for which no documentation is necessary, since these are already documented in <code><a class="el" href="theory_8h.html" title="Generic API for Theories plus methods commonly used by theories.">theory.h</a></code>.</p>
<h2><a class="anchor" id="theory_api_addnew"></a>
Adding New Theory</h2>
<h3><a class="anchor" id="theory_api_start"></a>
Before You Start...</h3>
<p>...Make sure you have a very good idea about what your new decision procedure is supposed to do, why it is useful, and what exactly it decides.</p>
<p>Next, write down all the definitions mathematically and phrase the scope of the new theory in terms of a logic with a particular signature (the set of predefined interpreted and uninterpreted symbols that belong to this theory). Make sure this signature is disjoint from all the other theories (this is <b>very important</b>, since <a class="el" href="namespaceCVC3.html">CVC3</a> is based on Nelson-Oppen combination result, and requires signatures to be disjoint).</p>
<p>Your decision procedure should decide inconsistency of a set of formulas in the above logic. Make sure you actually know an algorithm for that. While it is possible to add undecidable or incomplete theories to <a class="el" href="namespaceCVC3.html">CVC3</a> (and we already have some), those should only be used for a very good reason. Otherwise, make sure you know that your algorithm is sound, complete, and terminating.</p>
<p>Take the above algorithm and make it an <em>online</em> one. That is, your algorithm should be able to accept a new formula at any point in time, and perform some incremental computation to take that formula into account. This is usually the most complicated step as far as the math is concerned. I will explain this step in detail in section <a class="el" href="theory_api_howto.html#theory_api_invars">Theory API</a> below.</p>
<p>If you are adding your theory to the official <a class="el" href="namespaceCVC3.html">CVC3</a> code base, <b>discuss your ideas on the mailing list!</b> Yes, <b>do</b> it, I mean it. If you do not, we will notice your sneaky additions right away, and will ask many difficult questions in public. So, you may as well just announce it yourself.</p>
<h3><a class="anchor" id="theory_api_config"></a>
Configure and Makefiles</h3>
<p>Now you are ready to begin. Pick a name for your new theory, say, <em>Foo</em>, and do the following steps.</p>
<ul>
<li>Create a new CVS branch. You already know how to do this, right? If not, read the FAQ: <a href="http://verify.stanford.edu/savannah/faq/?group=vergrp">http://verify.stanford.edu/savannah/faq/?group=vergrp</a> . Read it <b>NOW</b>.</li>
</ul>
<ul>
<li>Create a directory <code>src/theory_foo</code>, add it to CVS</li>
</ul>
<ul>
<li>Create the following files (either empty or copy them from an existing theory), and add them <b>to your new CVS branch</b>: <dl>
<dt>In <code>src/include/</code> </dt>
<dd><code>theory_foo.h</code> </dd>
<dt>In <code>src/theory_foo/</code> </dt>
<dd><code>theory_foo.cpp</code><br/>
<code>Makefile.in</code> </dd>
</dl>
If your new theory needs to create new custom proof rules, also create <dl>
<dt>in <code>src/theory_foo/</code> </dt>
<dd><code>foo_proof_rules.h</code><br/>
<code>foo_theorem_producer.h</code><br/>
<code>foo_theorem_producer.cpp</code> </dd>
</dl>
While you at it, add the <b>required header comment</b> to each source file (*.h and *.cpp), with the appropriately modified file name, author, date, and an optional description <em>after</em> the license excerpt. Look at any existing source file for a template.</li>
<li>Edit <code>src/theory_foo/Makefile.in</code> appropriately (look for a template from some other theory, for example, <code>theory_array</code>). You need to modify the values of:<ul>
<li><code>LIBRARY</code></li>
<li><code>LOCAL_OBJ_DIR</code> and <code>LOCAL_SRC_DIR</code></li>
<li><code>SRC</code></li>
<li><code>HEADERS</code> (if you created any *.h files in <code>src/theory_foo/</code>, such as <code>foo_proof_rules.h</code>).</li>
</ul>
</li>
<li>Edit <code>src/Makefile.in</code> (it is a common Makefile for all theories):<ul>
<li>Add <code>theory_foo.h</code> to <code>HEADER_NAMES</code></li>
<li>Add <code>cd theory_foo && $(MAKE) $(TARGET)</code> to <code>build:</code> target</li>
<li>Add <code>theory_foo</code> entry to <code>CVC_LIB_NAMES</code></li>
</ul>
</li>
<li>Edit <code>configure.in</code>:<ul>
<li>Add an entry <code>$CVC_SRC_SUBDIR/theory_foo/Makefile</code> to <code>CVC_OUTPUT_FILES</code> variable</li>
</ul>
</li>
<li>Run <code>autoheader</code>, <code>autoconf</code>, <code>./configure</code>.</li>
<li>Edit <code><a class="el" href="vcl_8cpp.html">src/vcl/vcl.cpp</a></code> to add a call to your theory's constructor:<ul>
<li>Add <code>#include "theory_foo.h"</code> at the top;</li>
<li>Add <code>d_theories.push_back(new TheoryFoo(this));</code> to the end of VCL::VCL() constructor.</li>
</ul>
</li>
</ul>
<p>File <code><a class="el" href="vcl_8cpp.html">src/vcl/vcl.cpp</a></code> is <b>the only source file</b> in the core of <a class="el" href="namespaceCVC3.html">CVC3</a> that you really need to touch in order to add a new theory. If you have to do something else, you are either doing it wrong, or there better be a very good reason for it.</p>
<p>Now you are all set for compiling your new code, except that there is no code to compile yet...</p>
<h3><a class="anchor" id="theory_api_header"></a>
Header File: theory_foo.h</h3>
<p>The easiest way to start is to use an existing <code>theory_whatever.h</code> file as a template. This header file should declare the following elements:</p>
<ul>
<li>
<code>class TheoryFoo</code> as a subclass of <code>Theory</code>; </li>
<li>
Non-member (global) functions for creating expressions in your theory, and possibly, testers for those expressions; for instance: <code><a class="el" href="namespaceCVC3.html#accd3d7d38b0e04136afbc3e5191bc8bb">plusExpr()</a></code>, <code><a class="el" href="namespaceCVC3.html#adb35e0739f86730543924dbc8211a778">multExpr()</a></code>, ..., <code><a class="el" href="namespaceCVC3.html#afb0f7d15ddbd87f9abb128108101f557">isPlus()</a></code>, <code><a class="el" href="namespaceCVC3.html#a28ae8672047db708e99602ebaca89777">isMult()</a></code>, ... </li>
<li>
Optionally, declaration of new kinds (an <code>enum</code> type) used in the above expressions. </li>
</ul>
<p>Declaration of <code>TheoryFoo</code> class is required. Kinds and functions for creating new expressions are only needed if you want the end-user of the <a class="el" href="namespaceCVC3.html">CVC3</a> library to be able to create expressions from your theory and/or refer to their kinds directly. This is not always desirable. For instance, you may want to generate special terms or predicates that only make sense as temporary storage of information for <em>your</em> theory. The <code>DARK_SHADOW</code> and <code>GRAY_SHADOW</code> operators are good examples from the arithmetic theory. You have no clue what I'm talking about? That's right, you get it.</p>
<h3><a class="anchor" id="theory_api_expr"></a>
Kinds, Expressions, and Types</h3>
<p>The purpose of a new theory (or a <em>decision procedure</em>) is to extend the existing logic of <a class="el" href="namespaceCVC3.html">CVC3</a> with new interpreted, and sometimes uninterpreted, operators and symbols. These new symbols comprise a <em>signature</em> of the theory, and it must be disjoint from the signatures of the other theories.</p>
<p>In code, the new symbols and operators translate into new kinds of expressions. That is, new <em>kinds</em> and new values of the <code>Expr</code> class.</p>
<p>A <em>kind</em> is a natural number which uniquely determines what sort of expression it is (variable, uninterpreted function symbol, specific operator like plus, minus, a type expression, etc.). Kinds are also used to define your <em>theory's signature</em>, and hence, they must be unique to your theory.</p>
<p>In the simplest case, a kind represents the entire expression or type. Examples are simple types (like <code>REAL</code> and <code>INT</code>) and some constants (e.g. <code>TRUE</code> and <code>FALSE</code>).</p>
<p>More typically, however, a kind represents an operator (<code>PLUS</code>, <code>MINUS</code>, ...), and children of an expression of that kind are the arguments of that operator.</p>
<p>Finally, some kinds are used by more complex expressions with additional non-term attributes. For example, <code>REC_LITERAL</code> is used by record expressions { f1=e1, f2=e2, ... } whose children are the values of the fields (e1, e2, ...), and an additional attribute is the vector of field names: (f1, f2, ...). Other examples are quantifiers and lambda-terms. Such expressions require not only a new kind declaration, but also a special subclass of <code>ExprValue</code> (see below).</p>
<h3><a class="anchor" id="theory_api_kind_decl"></a>
Kind Declaration</h3>
<p>Kinds are declared as elements of an <code>enum</code> type (with doxygen comments):</p>
<div class="fragment"><pre class="fragment">
//! Local kinds of TheoryFoo
typedef enum {
FOO_TYPE = 3500, //!< Type FOO for the elements of this theory
BAR, //!< The binary (x | y) operator, where x,y: FOO
BAZ, //!< Unary buzz(x) predicate
BLEAH //!< An internal auxiliary term
} FooKind;
</pre></div><p>Notice, that the numbering in this example starts from 3500. This can be any integer which ensures that the new kinds do not clash with the existing kinds in other theories. Pick a random one, see if your kinds don't clash with others. You can check this either by inspecting <code><a class="el" href="kinds_8h.html">src/include/kinds.h</a></code> (the cental declaration of core kinds) and all the other theories, or compile and run <code>cvc3</code> to see if you get an error message about kinds registered twice.</p>
<p>The above type declaration of <code>FooKind</code> can be either in <code>src/include/theory_foo.h</code> (usually the best place), or in some header file in <code>src/theory_foo/</code> directory, depending on whether you want to expose your kinds to the end library user or not. In the latter case, do not forget to add that header file to the <code>HEADERS</code> variable in your <code>Makefile.in</code> (see the <a class="el" href="theory_api_howto.html#theory_api_config">previous section</a>).</p>
<h3><a class="anchor" id="theory_api_kind_reg"></a>
Kind Registration</h3>
<p>New kinds must be registered with the expression manager, which is done in your theory's constructor (see the <a class="el" href="theory_api_howto.html#theory_api_methods">next section</a>). Registration is done by calling <code>newKind()</code> method of <code>ExprManager</code> for each kind:</p>
<div class="fragment"><pre class="fragment">
getEM()->newKind(FOO_TYPE, "FOO");
getEM()->newKind(BAR, "||");
....
</pre></div><p>The string in the second argument is for printing the kind by the pretty-printer, and also for parsing, that is, turning a string back into a number (the kind).</p>
<h3><a class="anchor" id="theory_api_expr_subclass"></a>
New Expression Subclasses</h3>
<p>Sometimes an expression has a more complicated structure than a fixed operator with arguments, and more sophisticated data structures are necessary to represent it. <a class="el" href="namespaceCVC3.html">CVC3</a> has an API for declaring and registering a new <em>expression subclass</em> just for that purpose.</p>
<p>An expression subclass is a subclass of <a class="el" href="classCVC3_1_1ExprValue.html#ExprValue">ExprValue</a>. You can declare it where appropriate in your theory files, using the same judgement as for the kinds. The new subclass needs to be registered with <code>ExprManager</code> by calling <code>registerSubclass()</code> method.</p>
<p>A subclass of <code>ExprValue</code> <b>must</b> implement the following methods:</p>
<div class="fragment"><pre class="fragment">
size_t computeHash() const;
size_t getMMIndex() const;
int isGeneric() const { return getMMIndex(); }
bool isGeneric(int idx) const { return (idx == getMMIndex()); }
// Syntactic equality of two expressions
bool operator==(const ExprValue& ev2) const;
// Make a clean copy of itself using the given memory manager
ExprValue* copy(MemoryManager* mm, ExprIndex idx = 0);
</pre></div><p>Also, each subclass must overload <code>new()</code> and <code>delete()</code> as follows:</p>
<div class="fragment"><pre class="fragment">
void* operator new(size_t, MemoryManager* mm) {
return mm->newData();
}
void operator delete(void*) { }
</pre></div><p>Subclasses may overload other virtual methods of <code>ExprValue</code> as needed. For instance, <code>arity()</code>, <code>getKids()</code>, <code>ExprValueGenericAttr "getXXXAttr"()</code>, etc. Some standard attribute access functions can also be overloaded, e.g. <code>getString()</code>, <code>getRational()</code>.</p>
<p>However, you should <b>not</b> overload testers such as <code>isRecord()</code>, <code>isVar()</code> and such (unless you really know what you are doing), since the core relies on specific properties of the corresponding subclasses.</p>
<p>For example, let us say that the auxiliary term <code>BLEAH</code> in <code>TheoryFoo</code> needs a string attribute, which is a part of expression, but is not a child (and not even a term in the logic), and an integer attribute which is not part of the expression (e.g. it is needed for marking expressions during the algorithm run). An example of a new subclass for this expression is the following:</p>
<div class="fragment"><pre class="fragment">
class BleahExpr: public ExprValue {
private:
string d_str; //!< Data field; defines the value of expression
int d_int; //!< An attribute
size_t d_MMIndex; //!< The registration index for ExprManager
public:
//! Constructor
BleahExpr(ExprManager* em, const string& str,
size_t mmIndex, ExprIndex idx = 0)
: ExprValue(em, ARRAY_VAR, idx), d_str(str),
d_int(0), d_MMIndex(mmIndex) { }
//! String attribute (part of expression)
const std::string& getString() const { return d_str; }
//! Integer attribute (not part of expression)
int& getIntAttr(int idx) { return d_int; }
size_t getIntAttrSize() const { return 1; }
ExprValue* copy(MemoryManager* mm, ExprIndex idx = 0) const {
return new(mm) BleahExpr(d_em, d_str, d_MMIndex, idx);
}
size_t computeHash() const {
return PRIME*ExprValue::hash(BLEAH)+s_charHash(d_str.c_str());
}
size_t getMMIndex() const { return d_MMIndex; }
size_t isGeneric() const { return getMMIndex(); }
bool isGeneric(size_t idx) const { return (idx == getMMIndex()); }
// Only compare the string, not the integer attribute
bool operator==(const ExprValue& ev2) const {
if(ev2.getMMIndex() != d_MMIndex) return false;
return (d_str == ev2.getString());
}
void* operator new(size_t, MemoryManager* mm) {
return mm->newData();
}
void operator delete(void*) { }
};
</pre></div><p>Registration of this subclass generates a memory manager index, which must be stored somewhere, usually in a class variable of <code>TheoryFoo</code>, say <code>d_bleahIdx</code> of type size_t. Registration in this case should be done in the constructor of <code>TheoryFoo</code>:</p>
<div class="fragment"><pre class="fragment">
d_bleahIndex = getEM()->registerSubclass(sizeof(BleahExpr));
</pre></div><p>The approved and recommended way of <b>creating expressions</b> of <code>BLEAH</code> kind is the following:</p>
<div class="fragment"><pre class="fragment">
Expr bleahExpr(const string& s) {
BleahExpr av(d_em, s, d_BleahIndex);
return newExpr(&av);
}
</pre></div><p>Using the new expression is now very easy:</p>
<div class="fragment"><pre class="fragment">
Expr bleah = bleahExpr("cow moo"), b2 = bleahExpr("asdfqwerty");
bleah.getIntAttr(0) = 42;
if(bleah != b2)
cout << bleah.getString() << b2.getIntAttr(0) << endl;
</pre></div><p>Note that it is impossible to define a non-member expression creation function for <code>BleahExpr</code>, since the memory manager index is stored in the class-local variable of <code>TheoryFoo</code>. And <b>don't even think</b> of using a static variable to work around this limitation.</p>
<p>In general, you should <b>NEVER</b> store anything in a static variable, since it may violate thread-safety of the library. Before you ever think of using a static variable for anything, think what happens if someone creates two copies of the system (with two different sets of expression and memory managers). Is it safe to share this variable among several system instances? In the case of the memory manager index, the answer is <em>definitely not</em>.</p>
<p>One possible fix for this problem is to bind the memory manager to the kind(s) that the subclass uses. Let us know if you really need this feature, and it will be implemented.</p>
<h3><a class="anchor" id="theory_api_methods"></a>
Constructor and API Methods</h3>
<p>The only constructor for your new theory should have the following declaration:</p>
<div class="fragment"><pre class="fragment">
TheoryFoo(VCL* vcl);
</pre></div><p>The constructor has to:</p>
<ul>
<li>Initialize the base class,</li>
<li>Register new kinds and expression subclasses (if any) with <code>ExprManager</code>,</li>
<li>Collect the kinds which belong to the new theory in a vector, and register the theory (method <code>registerTheory()</code>) with these kinds,</li>
<li>Initialize theory-specific data structures, if needed.</li>
</ul>
<p>Here is a typical example of the constructor implementation:</p>
<div class="fragment"><pre class="fragment">
TheoryFoo::TheoryFoo(VCL *vcl): Theory(vcl, "Foo") {
d_rules = createProofRules(vcl); // instantiate our own rules
// Register new local kinds with ExprManager
getEM()->newKind(FOO_TYPE, "FOO");
getEM()->newKind(BAR, "||");
getEM()->newKind(BAZ, "BAZ");
getEM()->newKind(BLEAH, "BLEAH");
// Register our expression subclass
d_bleahIndex = getEM()->registerSubclass(sizeof(BleahExpr));
vector<int> kinds;
kinds.push_back(FOO_TYPE);
kinds.push_back(BAR);
kinds.push_back(BAZ);
kinds.push_back(BLEAH);
registerTheory(this, kinds);
}
</pre></div><p>The following <a class="el" href="group__Theory__API.html#theory_api">Theory API methods</a> are <b>required</b> in the subclass:</p>
<div class="fragment"><pre class="fragment">
void assertFact(const Theorem& e);
void checkSat(bool fullEffort);
void computeType(const Expr& e);
</pre></div><p>Other methods are <b>optional</b>, but often needed:</p>
<div class="fragment"><pre class="fragment">
Theorem rewrite(const Expr& e);
void setup(const Expr& e);
void update(const Theorem& e, const Expr& d);
ExprStream& print(ExprStream& os, const Expr& e);
Expr parseExprOp(const Expr& e);
</pre></div><p>Finally, a few other methods are rarely needed in practice:</p>
<div class="fragment"><pre class="fragment">
void addSharedTerm(const Expr& e);
Theorem solve(const Theorem& e);
void notifyInconsistent(const Theorem& thm);
Expr computeTCC(const Expr& e);
</pre></div><p>The next section describes these API methods in more detail. You are also strongly encouraged to <a class="el" href="group__Theory__API.html#theory_api">read the documentation</a> on each of these methods.</p>
<h2><a class="anchor" id="theory_api_invars"></a>
Theory API: The Very Important Invariants</h2>
<h3><a class="anchor" id="theory_api_flow"></a>
High-Level Information Flow</h3>
<p>Every decision procedure communicates with the <a class="el" href="namespaceCVC3.html">CVC3</a> Core interactively through several methods, most of which belong to the Theory class. Generally, those methods that your theory class re-implements carry information <em>from</em> the core, and others add new information generated in the DP <em>to</em> the core. Some methods (like <code>rewrite()</code> and <code>solve()</code>) return information through their return values.</p>
<p>The chart below shows the flow of information to and from the decision procedure, and which parts of the core are responsible for collecting and generating it. Thick lines represent the most important methods, and dashed lines represent methods used only for very special occasions.</p>
<div class="image">
<img src="theory_api_flow.jpg" alt="theory_api_flow.jpg"/>
</div>
<p>The most straightforward path of information, once it gets to the core through the external user input, is the following. First, all the relevant terms are typechecked (<code>computeType()</code> method). This method implements a step in the recursive typechecking algorithm, where the current expression is typechecked based on its structure and the types of its children. Typechecking of children is done by calling <code>getType()</code> or <code>getBaseType()</code>. The latter computes the largest supertype of the expression; for instance, the exact type of <code>x</code> may be a subrange <code>0..5</code>, which is a subtype of <code>INT</code>, but its base type is <code>REAL</code>. Exact and base types are cached on expressions, and are computed on demand.</p>
<p>An important property of <code>computeType()</code> is that it must not only compute the exact type of the expression, but also verify that all subexpressions are type-correct, <em>relative to their base types</em>. For instance, <code>x = y</code> has type <code>BOOLEAN</code>, and it is only type-correct if <code>getBaseType(x) == getBaseType(y)</code>. If this property is violated, <code>TypecheckException</code> must be thrown with the appropriate message. Note, that the exact types of <code>x</code> and <code>y</code> may be different, and even disjoint.</p>
<p>After the type checking, <em>Type Correctness Conditions</em> (TCCs) are generated and checked. TCC is a formula which is true if and only if any partial function in the original formula is used safely according to the Kleene semantics. That is, every partial function is either applied only to the arguments in its domain, or its value does not influence the value of the formula.</p>
<p>TCCs are computed recursively by <code>computeTCC()</code> and <code>getTCC()</code> methods, very similar to computing the types. If your theory does not introduce partial functions explicitly (like division in arithmetic), then you do not need to re-implement <code>computeTCC()</code> in your theory; the default implementation will do the job.</p>
<p>TCCs have a nice property that if they are true in the current context, then the corresponding user formulas can be safely interpreted by the total 2-valued models. Hence, <code>computeTCC()</code> is <b>the only</b> Theory API method that deals with partiality. All other methods consider any formula to be total (no partial functions) and 2-valued (only <code>TRUE</code> or <code>FALSE</code>, no undefined values.</p>
<p>Once TCC has been proven valid in the current context, the new fact (formula) goes to the <a class="el" href="namespaceSAT.html">SAT</a> solver, and if it is a literal (atomic formula or its negation), it is submitted to the decision procedure through <code>assertFact()</code>. The decision procedure processes this fact, updates its internal data structures, and possibly reports a contradiction (<code>setInconsistent()</code>) or new facts (<code>enqueueFact()</code>, and in special cases, <code>enqueueEquality()</code>). This completes the main loop of information flow.</p>
<p>Note, that both <code>enqueueFact()</code> and <code>setInconsistent()</code> deliver information to the same place in the core, except that reporting the conflict bypasses the queue, and is taken care of immediately, rather than after all the previously enqueued facts are processed. This is the primary reason for having these two functions separated (as opposed to having only <code>enqueueFact()</code>).</p>
<p>Inside this main loop, <code>rewrite()</code> and <code>solve()</code> are called to transform (or simplify) the facts before they reach the rest of the core. Normally, these functions do not have side-effects (except for caching results), and return new (simplified) facts through their return values.</p>
<p>When the <a class="el" href="namespaceSAT.html">SAT</a> solver runs out of facts, and the context is still satisfiable, it calls <code>checkSat()</code> with <code>fullEffort==true</code>. At this point, the decision procedure must determine whether all the information it has seen so far makes the context satisfiable or not w.r.t. its theory. Just like in the case of <code>assertFact()</code>, it may either report a contradiction, or enqueue a new fact. If any new fact is enqueued, it starts the main loop again. If <code>checkSat()</code> does not generate any new facts and does not find a contradiction, the core stops and reports the context to be satisfiable.</p>
<p>Method <code>checkSat()</code> is also called every time the fact queue becomes empty, before the <a class="el" href="namespaceSAT.html">SAT</a> solver asserts a new splitter. In this case, the <code>fullEffort</code> argument is set to <code>false</code>, and the decision procedure is not required to do anything. Many DPs, however, choose to perform some relatively inexpensive checks to detect inconsistencies and/or new facts, which increases performance. Similarly, if a new fact is enqueued, the main loop continues (without the <a class="el" href="namespaceSAT.html">SAT</a> solver asserting new splitters) until the queue is empty.</p>
<p>In <a class="el" href="namespaceCVC3.html">CVC3</a>, every term (non-formula expression) has a <em>canonical representative</em> in the union-find database. This database represents the equivalence classes of terms w.r.t. logical equality. All the terms in the formulas passing through the core are <em>simplified</em> by replacing them with their canonical representatives.</p>
<p>Often, a decision procedure wants to be notified when a subexpression changes its canonical representative. For instance, if the DP has seen an term <code>2*x+3*y</code>, and <code>x</code> has changed its representative to <code>y+2</code>, then it is important to conclude that <code>2*x+3*y == 2*(y+2) + 3*y == 5*y+4</code>. For this purpose, the core maintains the <em>notify list</em> data structure, which is interfaced through <code>setup()</code> and <code>update()</code> methods.</p>
<p>Every term in the core must be <em>setup</em>, and as a part of that process, the method <code>setup()</code> of the appropriate DP is called. Here the decision procedure has a chance to register notification requests related to the given expression. These requests are added to the <em>notify lists</em> of the relevant expressions using <code>Expr::addToNotify()</code> member method.</p>
<p>Normally, a DP wants to be notified when immediate children of the expression change. For instance, for an expression <code>2*x</code>, if the variable <code>x</code> changes, the arithmetic DP wants to be notified about it. Therefore, in the <code>setup(2*x)</code> call, it adds <code>2*x</code> to the notify list of <code>x</code> by calling <code>x.addToNotify(this, 2*x)</code>. The first argument (<code>this</code>) is the reference to the current Theory subclass.</p>
<p>Later, when <code>x</code> changes its canonical representative, say, to <code>y+2</code>, its notify list is consulted, and the <code>update(x==y+2, 2*x)</code> call is made. The first argument is a directed equality informing the DP of what has changed, and the second is the expression for which this change is relevant. In this particular example, <code>update()</code> will enqueue a new fact: <code>2*x==2*y+4</code>.</p>
<p>Similarly, when <code>2*x+3*y</code> is being setup, its immediate children (<code>2*x</code> and <code>3*y</code>) get the entire expression added to their notify lists. Later, when <code>2*x</code> changes its canonical representative to <code>2*y+4</code> due to the previous <code>update()</code> call, another <code>update()</code> call is made with <code>2*x==2*y+4</code> for <code>2*x+3*y</code>, and a new fact is enqueued: <code>2*x+3*y==5*y+4</code>, and so on.</p>
<p>Note, that the notify list mechanism is not restricted to only immediate children. For instance, for high-degree monomials in non-linear arithmetics (e.g. <code>x^2*y</code>) it makes sense to register them with all factors (in this case, <code>x</code>, <code>x^2</code>, <code>y</code>, and <code>x*y</code>) which are not necessarily subexpressions of the original monomial (<code>x^2*y</code>).</p>
<p>Finally, sometimes a decision procedure may want to know that the current context has become inconsistent, and this what <code>notifyInconsistent()</code> call is for. To date, only the quantifier theory uses it to find out which instantiations were useful in producing a conflict. Most likely, you do not need it.</p>
<h3><a class="anchor" id="theory_api_backtrack"></a>
Backtracking Data Structures</h3>
<p>Up to this point, the description assumed that new facts are always <em>added</em> to the current logical context, and <em>never removed</em>. This, of course, is not true in reality, since when a conflict is found, the <a class="el" href="namespaceSAT.html">SAT</a> solver will <em>backtrack</em>, and <em>restore the context</em> to what it was before the assertion of a splitter. In particular, this means that each decision procedure needs to restore all its internal state to the same point. You may have noticed that there is no Theory API call to signal such backtracking. How the heck can a DP restore the state if it does not know when the core backtracks?</p>
<p>The trick used in <a class="el" href="namespaceCVC3.html">CVC3</a> is actually quite simple and elegant: DP <em>does not have to know about backtracking</em>, it indeed works under the assumption that facts can only be added to the context. However, all of its internal state must be stored in <em>backtracking data structures</em>, which backtrack automatically with the core.</p>
<p>Such backtracking data structures are called <em>context-dependent objects</em> (CDO). There are currently three pre-defined context-dependent data structures: <em>CDO</em> (context-dependent object, <code><a class="el" href="cdo_8h.html">cdo.h</a></code>), <em>CDList</em> (backtracking stack, <code><a class="el" href="cdlist_8h.html">cdlist.h</a></code>), and <em>CDMap</em> (backtracking map, similar to STL map, <code><a class="el" href="cdmap_8h.html">cdmap.h</a></code>).</p>
<p>Class CDO is a templated class for any C++ class which can be cleanly copied with <code>operator=()</code> and copy constructor, and which have the default constructor (this is how these objects are saved and restored on backtracking). CDO is best suited for individual variables (array indices, <code>Expr</code> or <code>Theorem</code> variables, etc.).</p>
<p>Class CDList is a backtracking stack, and its API is very similar to that of STL vector. You can <code>push_back()</code> elements onto the stack, check the <code>size()</code> of the stack, and look up individual elements with <code>operator[]</code>. You <em>cannot</em>, however, modify or remove elements from the list. Keep in mind, that the size of the list may change between the API method calls, which means, you should keep any persistent indices to the list in backtracking variables (CDO).</p>
<p>Class CDMap is a templated class very similar to STL <code>map</code>. You can add new key-value pairs to it, you can modify the value under a key, but you cannot remove a pair from the map.</p>
<p>Let me repeat this again: <b>all persistent data in a decision procedure MUST be stored in backtracking data structures!</b> There are some rare exceptions to the rule (like storing the <code>Expr</code> representing the value "0" to avoid re-building it), but generally, you do not even want to know about backtracking. It is all done under the hood, and you should not care.</p>
<h3><a class="anchor" id="theory_api_ileaves"></a>
Variables and Foreign Terms (i-Leaves)</h3>
<p>Any subterm that your decision procedure cannot recognize must be treated as a variable. This is a very important point, and it may cause a long-lasting confusion for the beginning developers if not understood from the start. Read it carefully, several times, until you are sure you never forget it, even if I wake you up in the middle of the night.</p>
<p>What <a class="el" href="namespaceCVC3.html">CVC3</a> knows as a "variable" has nothing to do with what a decision procedure considers a "variable." These two are not very much related.</p>
<p>A variable (or an <em>i-leaf</em>) from the DP point of view is either a <a class="el" href="namespaceCVC3.html">CVC3</a> variable, or a <em>shared term</em> from some other theory. For instance, in <code>2*arr[idx]-3*y</code>, the subterm <code>arr[idx]</code> belongs to the theory of arrays, and therefore, is a variable (an i-leaf) as far as the theory of arithmetic is concerned. Similarly, <code>y</code> is a variable in the theory of arithmetic, because it is also a <a class="el" href="namespaceCVC3.html">CVC3</a> variable.</p>
<p>Such a definition does not provide a direct test for an i-leaf. Instead, you have to check whether this term is one of "yours" (one that your theory knows about), which is usually determined by the expression kind. If not, then it is a variable, as far as your theory is concerned.</p>
<p>But never make any assumptions about an i-leaf; it can be any expression whatsoever, and <code>Expr::isVar()</code> tester will <em>not</em> necessarily return <code>true</code> for it. In other words, <em>there is no such thing as a variable</em> in your theory. There are only terms you cannot recognize, which you treat as variables.</p>
<h3><a class="anchor" id="theory_api_inputs"></a>
Methods Reimplemented in a Subclass</h3>
<h3><a class="anchor" id="theory_api_assertFact"></a>
assertFact()</h3>
<p>There are no tricky invariants for this method. The only important property is that all the facts that are submitted to the DP through this call become part of the logical context which the DP must check for satisfiability.</p>
<p>Mathematically, the asserted fact <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is added to the logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>, and the job of the decision procedure is to check whether <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> is satisfiable or not; in other words, we are solving the problem <img class="formulaInl" alt="$\Gamma\models\bot$" src="form_2.png"/>.</p>
<p>When the decision procedure receives a new fact <img class="formulaInl" alt="$\phi$" src="form_0.png"/>, it may either save this fact in its internal database for later processing, or may immediately process it, and possibly derive new facts <img class="formulaInl" alt="$\{\psi_1,\ldots,\psi_k\}$" src="form_3.png"/> from <img class="formulaInl" alt="$\phi$" src="form_0.png"/> and submit them back to the core (<code>enqueueFact()</code>).</p>
<p>In the case when the set of derived facts is equisatisfiable with the original fact <img class="formulaInl" alt="$\phi$" src="form_0.png"/>, the decision procedure does not need to keep <img class="formulaInl" alt="$\phi$" src="form_0.png"/> in its database; the completeness will still be preserved.</p>
<p>For instance, if the DP receives <code>r1=r2</code>, where <code>r1</code> and <code>r2</code> are records with fields <code>f1</code> and <code>f2</code>, then the two facts <code>r1.f1=r2.f1</code> and <code>r1.f2=r2.f2</code> (equalities of the individual fields) together are logically equivalent to the original fact <code>r1=r2</code>, and therefore, enqueuing them is sufficient for preserving completeness. The original fact need not be saved.</p>
<h3><a class="anchor" id="theory_api_checkSat"></a>
checkSat(bool fullEffort)</h3>
<p>The most important invariant (for completeness) is that when <code>fullEffort</code> is <code>true</code>, the DP must do all the work that it has postponed to find out if the current context is indeed satisfiable. In particular, if satisfiability can be achieved by making some of the shared terms equal, it must be done at this time (see <a class="el" href="theory_api_howto.html#theory_api_addSharedTerm">addSharedTerm()</a> for more info on shared terms).</p>
<p>This call is your last warning: if you do not act now, the whole system will stop and notify the user. However, the worst that can happen is that <a class="el" href="namespaceCVC3.html">CVC3</a> becomes incomplete (it may report <code>InValid</code> when the query is actually valid). It still remains sound, however. That is, the <code>Valid</code> answer will still be correct.</p>
<p>When <code>fullEffort</code> is <code>false</code>, the DP may choose to do as much or as little work as it wants.</p>
<h3><a class="anchor" id="theory_api_setup"></a>
setup()</h3>
<p>Add the given expression <code>e</code> to the notify list of all the expressions <code>t<sub>1</sub>...t<sub>n</sub></code> whose change would affect the value of <code>e</code>. Normally, such expressions are the immediate children of <code>e</code>.</p>
<p>Whenever the canonical representative of any <code>t<sub>i</sub></code> changes in the union-find database, a corresponding call to <code>update()</code> will be made, and the DP will have a chance to re-process the expression <code>e</code> to keep it up-to-date.</p>
<h3><a class="anchor" id="theory_api_update"></a>
update()</h3>
<p>The property of this call is similar to <code>assertFact()</code>: the new fact becomes part of the logical context. However, the facts it receives do not necessarily belong to your theory, and are only reported because you asked the core to do so in <code>setup()</code>.</p>
<p>Also, the new equalities that <code>update()</code> derives must be submitted through <code>enqueueEquality()</code> call. This also means that the right-hand side of the submitted equalities must be fully simplified. See <code><a class="el" href="theory_api_howto.html#theory_api_enqueueEquality">enqueueEquality()</a></code> for more information.</p>
<h3><a class="anchor" id="theory_api_addSharedTerm"></a>
addSharedTerm()</h3>
<p>A term is called <em>shared</em> if it belongs to theory X, and appears as an i-leaf in a term from theory Y (that is, it's a Y-leaf). In this case, the term is shared by theories X and Y. For example, in <code>2*arr[idx]-3</code> the subterm <code>arr[idx]</code> belongs to the theory of arrays, but the entire term is an arithmetic expression; hence, <code>arr[idx]</code> is a shared term.</p>
<p>When such a term appears in the system, the core notifies both theories about the term.</p>
<p>Completeness of the <a class="el" href="namespaceCVC3.html">CVC3</a> framework relies on the invariant that decision procedures propagate all the equalities between shared terms that can be derived in the current logical context.</p>
<p>Often, the algorithms in DPs are designed to propagate all the equalities automatically (over all terms, including shared). In this case, <code>addSharedTerm()</code> need not be re-implemented.</p>
<p>In some cases, however, the DP has to take extra effort to satisfy the above invariant, and it is more efficient to restrict this extra effort only to the set of shared terms. In this case, <code>addSharedTerm()</code> needs to collect the set of shared terms in a database (which, of course, has to be <a class="el" href="theory_api_howto.html#theory_api_backtrack">backtrackable</a>), and use it in the <code>checkSat()</code> call.</p>
<h3><a class="anchor" id="theory_api_rewrite"></a>
rewrite(Expr e)</h3>
<p>This function must return a <em>rewrite Theorem</em> of the form <code>e==e1</code> (or <code>e<=>e1</code> if <code>e</code> is a formula), where <code>e1</code> is a logically equivalent term or formula.</p>
<p>This function can assume that all the immediate children of <code>e</code> are already completely simplified and rewritten. The same property must hold for the result of the rewrite.</p>
<p>Another invariant that <code>rewrite()</code> has to preserve is that if the result of a rewrite is an equality (you return <code>e<=>(e1==e2)</code>), then in the resulting equality <code>e1 >= e2</code> w.r.t. <code>operator>=(Expr, Expr)</code>, the fixed total ordering on all expressions given by the expression manager. This invariant is important for termination of the simplifier, since equalities in <a class="el" href="namespaceCVC3.html">CVC3</a> are used as (directed) rewrite rules, replacing the left-hand side (<code>e1</code>) with the right-hand side (<code>e2</code>).</p>
<p>The core will call the <code>rewrite()</code> function iteratively on the right-hand side of the result, until the expression does not change. However, if the rewriting algorithm can guarantee that in a particular case no further rewrites from this theory will change the expression, the result can be flagged as a <em>normal rewrite</em>. In this case, the core will not call <code>rewrite()</code> again, resulting in better performance. The property that the expression indeed does not change with further rewrites is checked in the "debug" build, and any violation triggers assertion failures with ``<em>Simplify Error 1</em>'' and ``<em>Simplify Error 2</em>'' messages.</p>
<p>It is important to understand that the iterative call to <code>rewrite()</code> only applies to the top-level node, and <em>not</em> to subexpressions. That is, if <code>rewrite()</code> changes the subexpressions (and not only the top-level operator), then it may violate another invariant that all the children of the result are completely rewritten and simplified. If this invariant cannot be guaranteed, then <code>rewrite()</code> needs to call <code>simplifyThm()</code> method explicitly.</p>
<p>Here is an example of a rewrite function:</p>
<div class="fragment"><pre class="fragment">
Theorem TheoryFoo::rewrite(const Expr& e) {
Theorem res;
if(isBar(e)) {
res = reflexivityRule(e);
res.getRHS().setRewriteNormal(); // No more rewrites needed
} else {
// May need to rewrite several times
res = < do real work >
}
return res;
}
</pre></div><h3><a class="anchor" id="theory_api_solve"></a>
solve(Theorem e)</h3>
<p>This method takes an equality <code>e</code> (as a <code>Theorem</code> object) and turns it into a logically equivalent <em>solved form</em>: a conjunction of fully simplified equalities, possibly existentially quantified. The terms on the left-hand sides cannot appear on any of the right-hand side terms, and every free variable in the solved form is also a free variable of <code>e</code>. (New variables in the solved form must be existentially quantified).</p>
<p>According to Clark Barrett's Ph.D. thesis, only one theory is allowed to have a solver. In <a class="el" href="namespaceCVC3.html">CVC3</a>, such theory is the theory of arithmetic. The restriction to a single solver in <a class="el" href="namespaceCVC3.html">CVC3</a> is somewhat relaxed, and several theories can have their own solvers, provided that the solved form that such a secondary solver generates is also a solved form w.r.t. the theory of arithmetic. This is the only asymmetric and non-local invariant in the core of Theory API.</p>
<h3><a class="anchor" id="theory_api_computeType"></a>
computeType()</h3>
<p>The basic <a class="el" href="namespaceCVC3.html">CVC3</a> type checking mechanism is a simple recursive descent into the term structure, and it is implemented as a <code>getType()</code> method in the base <code>Theory</code> class.</p>
<p>When computing a type of an expression <code>e</code>, this method determines which DP owns the expression, and calls the appropriate <code>computeType()</code> method, which is expected to check the expression for type consistency, and return the exact type of the expression. The return type is then cached as an attribute on the expression <code>e</code> for a fast look-up in the subsequent calls to <code>getType()</code>.</p>
<p>Each decision procedure must implement <code>computeType()</code> method for all of its operators. For example, the theory of records has an operator for constructing record literals, for extracting a field of a record, and for updating a field of a record. This means that <code>computeType()</code> needs to be able to compute the types for these three operators, and verify that all subexpressions are of expected types.</p>
<p>Since subtypes in <a class="el" href="namespaceCVC3.html">CVC3</a> are handled by TCCs, type consistency at this stage is only checked with respect to the <em>base types</em>, which is returned by <code>getBaseType()</code> method provided by the base <code>Theory</code> class. For example, if a record expression <code>e</code> has a field <code>foo</code> of type <code>INT</code>, and the expression is a record update <code>e WITH .foo := t</code>, where <code>t</code> is of type <code>REAL</code>, then this expression is considered well-typed, since the base types of both <code>INT</code> and <code>REAL</code> is <code>REAL</code>.</p>
<p>An important property of <code>computeType()</code> is that it must not only compute the exact type of the expression, but also verify that all subexpressions are type-correct, <em>relative to their base types</em>. For instance, <code>x = y</code> has type <code>BOOLEAN</code>, and it is only type-correct if <code>getBaseType(x) == getBaseType(y)</code>. If this property is violated, <code>TypecheckException</code> must be thrown with the appropriate message. Note, that the exact types of <code>x</code> and <code>y</code> may be different, and even disjoint.</p>
<h3><a class="anchor" id="theory_api_computeTCC"></a>
computeTCC()</h3>
<p>Type Correctness Condition (TCC) for an expression <em>e</em> (which can be either a term or a formula) is a formula <em>D<sub>e</sub></em> such that <em>D<sub>e</sub></em> is true if and only if <em>e</em> is defined (or <em>denoting</em>) in the current logical context.</p>
<p>For example, an expression <code>x/y</code> is undefined when <code>y=0</code>, and is defined otherwise. Therefore, <img class="formulaInl" alt="$D_{x/y}\equiv y\ne 0$" src="form_4.png"/>.</p>
<h3><a class="anchor" id="theory_api_notifyInconsistent"></a>
notifyInconsistent()</h3>
<h3><a class="anchor" id="theory_api_print"></a>
print()</h3>
<p>The most important property of this method is that the printed expressions have to be parsable by the appropriate <a class="el" href="namespaceCVC3.html">CVC3</a> parser. That is, <a class="el" href="namespaceCVC3.html">CVC3</a> must be able to read what it prints.</p>
<p>The recursive call to the global pretty-printer is implemented through the overloaded <code>operator<<</code> for <code>ExprStream</code>. Read the documentation on <code>ExprStream</code> class before coding.</p>
<p>Once coded, <b>test your printer code!</b> Print all the kinds of expressions from your theory, make the expressions large and complex, interspersed with terms from other theories, etc. Make sure it both looks good, and <a class="el" href="namespaceCVC3.html">CVC3</a> can read every term it prints.</p>
<p>Here's an example of the <code>print()</code> method:</p>
<div class="fragment"><pre class="fragment">
ExprStream&
TheoryFoo::print(ExprStream& os, const Expr& e) {
switch(os.lang()) {
case PRESENTATION_LANG:
switch(e.getKind()) {
case ARROW:
os << "[" << push << e[0] << space << "-> " << e[1] << push << "]";
break;
case EQ:
os << "(" << push << e[0] << space << "= " << e[1] << push << ")";
break;
case NOT: os << "NOT " << e[0]; break;
.................
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.print(os);
}
break; // end of case PRESENTATION_LANGUAGE
case INTERNAL_LANG:
..................
break; // end of case INTERNAL_LANG
default:
// Print the top node in the default LISP format, continue with
// pretty-printing for children.
e.print(os);
}
return os;
}
</pre></div><h3><a class="anchor" id="theory_api_parseExprOp"></a>
parseExprOp()</h3>
<p>This method is not used yet, and is likely to change in the near future.</p>
<h3><a class="anchor" id="theory_api_outputs"></a>
Methods Provided by Theory API</h3>
<p>The Theory API consists not only of methods to re-implement in the subclass, but it also provides convenient methods in the base class which subclasses can readily use. These methods subdivide into the following categories:</p>
<ul>
<li>
Methods for sending information to the core from a theory (a decision procedure), </li>
<li>
<a class="el" href="classCVC3_1_1Theory.html#theory_api_core_proof_rules">Common proof rules</a>, </li>
<li>
Other convenient methods. </li>
</ul>
<h3><a class="anchor" id="theory_api_enqueueFact"></a>
enqueueFact()</h3>
<p>Normally, a decision procedure should use this <em>and only this</em> method for reporting newly derived facts back to the core. The only exception is a contradiction (a <code>FALSE</code> Theorem), which should be reported through <code>setInconsistent()</code> method for efficiency.</p>
<p>Other exceptions include facts derived by the <code>update()</code> function, which may be reported through <code><a class="el" href="theory_api_howto.html#theory_api_enqueueEquality">enqueueEquality()</a></code>.</p>
<h3><a class="anchor" id="theory_api_setInconsistent"></a>
setInconsistent()</h3>
<p>Similar to <code><a class="el" href="theory_api_howto.html#theory_api_enqueueFact">enqueueFact()</a></code>, except that it requires the new Theorem to be <code>FALSE</code> (a contradiction).</p>
<p>This method is used for more efficient processing of the derived contradiction, bypassing the fact queue.</p>
<h3><a class="anchor" id="theory_api_simplifyThm"></a>
simplifyThm() and simplify()</h3>
<p>In rare cases, a decision procedure may want to simplify a given expression w.r.t. the current context, and this is the function to call.</p>
<p><b>Be careful!</b> This method may call your own <code><a class="el" href="theory_api_howto.html#theory_api_rewrite">rewrite(Expr e)</a></code> method recursively.</p>
<p>It is also a relatively expensive function to call, so avoid it if possible.</p>
<h3><a class="anchor" id="theory_api_enqueueEquality"></a>
enqueueEquality()</h3>
<p>This function can be used in <code><a class="el" href="theory_api_howto.html#theory_api_update">update()</a></code> to propagate the equalities induced by the given equality <code>e1==e2</code> as the argument to <code>update()</code>.</p>
<p>In <a class="el" href="namespaceCVC3.html">CVC3</a>, equalities are treated as <em>directional</em>, meaning that left-hand side is always being replaced by the right-hand side. This means that if in the expression <code>d</code> there is a subexpression <code>e1</code>, then it must be replaced by <code>e2</code>. It also means that the resulting expression <code>d2</code> must be reported to be equal to the original one as <code>d==d2</code>, and <em>not</em> the other way around.</p>
<p>Since the core may occasionally swap equalities submitted through <code><a class="el" href="theory_api_howto.html#theory_api_enqueueFact">enqueueFact()</a></code> (for termination reasons), it is important to submit the above equality by-passing the swapping engine. This is where <code>enqueueEquality()</code> is useful.</p>
<p><b>Invariant:</b> <code>enqueueEquality()</code> expects the argument to be a Theorem of the form <code>e1==e2</code>, where <code>e2</code> is a <em>fully simplified expression</em> in the current context. That is, <code>e2 == simplify(e2)</code>. You are responsible for maintaining this invariant in your decision procedure.</p>
<h3><a class="anchor" id="theory_api_inconsistentThm"></a>
inconsistentThm() and inconsistent()</h3>
<p>If the context is inconsistent, the <code>inconsistent()</code> method returns <code>true</code>, and <code>inconsistentThm()</code> returns the Theorem of <code>FALSE</code> (a proof of the contradiction).</p>
<h3><a class="anchor" id="theory_api_isTerm"></a>
isTerm()</h3>
<p>Tests whether the given expression is a term (as opposed to a formula).</p>
<h3><a class="anchor" id="theory_api_isLiteral"></a>
isLiteral()</h3>
<p>Tests whether the given formula is a literal (is an atomic formula or its negation).</p>
<h3><a class="anchor" id="theory_api_isAtomic"></a>
isAtomic()</h3>
<p>Tests whether the given term or formula is atomic. In <a class="el" href="namespaceCVC3.html">CVC3</a> it means that the expression does not contain formulas as subexpressions (for instance, as conditions in the <code>IF-THEN-ELSE</code> operator).</p>
<p>This method is relatively expensive when called for the first time, but it caches the result in the Expr attributes, so the amortized complexity tends to be rather low.</p>
<h3><a class="anchor" id="theory_api_updateHelper"></a>
updateHelper()</h3>
<p>This method replaces all the immediate children of the given expression by their canonical representatives w.r.t. the union-find database, and returns the corresponding Theorem <code>e==e1</code>.</p>
<p>This function is convenient to use inside <code><a class="el" href="theory_api_howto.html#theory_api_update">update()</a></code> for rewriting <code>d</code>, the expression being updated. However, it only works when the changed subexpression in <code>d</code> is its immediate child.</p>
<h3><a class="anchor" id="theory_api_getType"></a>
getType()</h3>
<h3><a class="anchor" id="theory_api_getTCC"></a>
getTCC()</h3>
<h3><a class="anchor" id="theory_api_parseExpr"></a>
parseExpr()</h3>
<h2><a class="anchor" id="theory_api_proofs"></a>
Proof Rules: The Trusted Core</h2>
<p>Every proven formula (or <em>fact</em>) in <a class="el" href="namespaceCVC3.html">CVC3</a> appears in the form of a <code>Theorem</code>. Values of type <code>Theorem</code> have a special property: they cannot be constructed in any way but through the <em>proof rules</em>. This is implemented by making all the constructors of this class private. The only exception is the default constructor, which creates a null theorem, and it can only be used to create uninitialized variables of type <code>Theorem</code>, and assign them later.</p>
<p>A proof rule is a function which takes <em>premises</em> (previously generated theorems) and other parameters, and generates a new theorem. The implementation of proof rules comprises the <em>trusted core</em> of <a class="el" href="namespaceCVC3.html">CVC3</a>, and the soundness of the tool relies entirely on the soundness of this core. In other words, no matter what the bulk of the code does, if <a class="el" href="namespaceCVC3.html">CVC3</a> derives the validity of a particular fact, it is guaranteed that that theorem is indeed valid, provided the trusted implementation is correct and sound.</p>
<p>For this reason, it is prudent to keep the trusted core reasonably small, and more importantly, keep each proof rule clean and simple, so that the correctness of the rule itself (mathematically) and its implementation can be easily verified by manual inspection.</p>
<p>For the same reason, <b>every rule must be thoroughly documented</b>. It's a very good idea to include a LaTeX formula for the proof rule that a function implements. Keep in mind that reverse-engineering the mathematical meaning of a proof rule is a daunting task, especially if the code is rather long and complex.</p>
<p>Check out <code><a class="el" href="common__proof__rules_8h.html">src/include/common_proof_rules.h</a></code> for examples.</p>
<h3><a class="anchor" id="theory_api_proof_classes"></a>
Hierarchy of Classes</h3>
<p>Like anything else in <a class="el" href="namespaceCVC3.html">CVC3</a>, there is an API for implementing proof rules defined by the class <code>TheoremProducer</code>. This class provides two protected methods, <code>newTheorem()</code> and <code>newRWTheorem()</code>, to its subclasses, which can create arbitrary <code>Theorem</code> values. Therefore, a part of the code is considered <em>trusted</em> whenever the file contains <code>#include "theorem_producer.h"</code> statement in it. To enforce this, <code><a class="el" href="theorem__producer_8h.html">theorem_producer.h</a></code> requires a macro symbol <code>_CVC3_TRUSTED_</code> to be defined (otherwise, a compiler warning is generated).</p>
<p><b>Important:</b> the <code>_CVC3_TRUSTED_</code> symbol must be defined only in *.cpp files, and <b>never</b> in *.h, to prevent accidental inclusion of <code><a class="el" href="theorem__producer_8h.html">theorem_producer.h</a></code>, and thus, inadvertently making large portions of code trusted.</p>
<p>Exporting the proof rules to the untrusted code (class <code>TheoryFoo</code>) is implemented through the custom API in <code>foo_proof_rules.h</code> (abstract class <code>FooProofRules</code>), whose pure methods are the proof rules. This header file does not include <code><a class="el" href="theorem__producer_8h.html">theorem_producer.h</a></code>, and therefore, is suitable for inclusion by untrusted code.</p>
<p>The implementation of <code>FooProofRules</code> consists of the implementation API: <code>foo_theorem_producer.h</code> (class <code>FooTheoremProducer</code>, inherits from <code>FooProofRules</code> and <code>TheoremProducer</code>), and the implementation proper in <code>foo_theorem_producer.cpp</code>.</p>
<p>Normally, <code><a class="el" href="theorem__producer_8h.html">theorem_producer.h</a></code> is included from <code>foo_theorem_producer.h</code> (to declare <code>FooTheoremProducer</code> as a subclass of <code>TheoremProducer</code>), and <code>foo_theorem_producer.h</code> is included from <code>foo_theorem_producer.cpp</code>:</p>
<div class="fragment"><pre class="fragment">
// File foo_proof_rules.h
class FooProofRules {
....
};
</pre></div><div class="fragment"><pre class="fragment">
// File foo_theorem_producer.h
#include "theorem_producer.h"
class FooTheoremProducer: public FooProofRules, public TheoremProducer {
....
};
</pre></div><div class="fragment"><pre class="fragment">
// File foo_theorem_producer.cpp
#define _CVC3_TRUSTED_
#include "foo_theorem_producer.h"
....
</pre></div><p>In order for the theory code to use the proof rules, a pointer to <code>FooProofRules</code> is declared in the <code>TheoryFoo</code> class:</p>
<div class="fragment"><pre class="fragment">
// File theory_foo.h
class FooProofRules;
class TheoryFoo: public Theory {
......
FooProofRules* d_rules;
//! Create an instance of FooProofRules class
FooProofRules* createProofRules(VCL* vcl);
.....
};
</pre></div><p>Since instantiating <code>FooProofRules</code> requires creating a new object of class <code>FooTheoremProducer</code>, which belongs to trusted part of the code, the implementation of <code>createProofRules()</code> method needs to be in <code>foo_theorem_producer.cpp</code>, rather than in <code>theory_foo.cpp</code>. This is the only exception to the rule that everything declared in a <code>X.h</code> file must be implemented in the corresponding <code>X.cpp</code> file in <a class="el" href="namespaceCVC3.html">CVC3</a>.</p>
<div class="fragment"><pre class="fragment">
// File foo_theorem_producer.cpp
......
FooProofRules* TheoryFoo::createProofRules(VCL* vcl) {
return new FooTheoremProducer(vcl);
}
.....
</pre></div><p>In the <code>TheoryFoo()</code> constructor, the class variable <code>d_rules</code> is initialized by calling <code>createProofRules()</code>:</p>
<div class="fragment"><pre class="fragment">
// File theory_foo.cpp
.....
TheoryFoo::TheoryFoo(VCL* vcl): Theory(vcl, "Foo") {
.....
d_rules = createProofRules(vcl);
.....
}
// Destructor: destroy the proof rules class
TheoryFoo::~TheoryFoo() { delete d_rules; }
.....
</pre></div><h3><a class="anchor" id="theory_api_proof_rule"></a>
Implementing a Proof Rule</h3>
<p>Each function implementing a proof rule has several components:</p>
<ul>
<li>
Soundness check(s), </li>
<li>
The actual computation of the result, </li>
<li>
Building assumptions, </li>
<li>
Building a proof, </li>
<li>
Constructing a new <code>Theorem</code> object. </li>
</ul>
<p>There is a special macro <code><a class="el" href="theorem__producer_8h.html#a03dbe872f723d32fd975528f811d646e">CHECK_SOUND(cond, message)</a></code> for checking the soundness conditions. If the condition <code>cond</code> does not evaluate to <code>true</code>, then a <code>SoundException</code> is thrown with the <code>message</code> string.</p>
<p>For efficiency, the user may decide to skip the soundness checks. In order to honor this decision, all soundness checks must be supressed when the <code>CHECK_PROOFS</code> macro evaluates to <code>false</code>:</p>
<div class="fragment"><pre class="fragment">
if(CHECK_PROOFS) {
CHECK_SOUND(denominator != 0,
"TheoryArith: Division rule: denominator == 0");
}
</pre></div><p>Soundness checks play <b>the most important role</b> in making <a class="el" href="namespaceCVC3.html">CVC3</a> sound. Your implementation must guarantee that if all soundness checks pass, then the rule is indeed sound to apply, and the theorem you generate at the end is indeed a theorem. Soundness checks include verifying that the premises (Theorems given as arguments) are of the expected format, and all the additional parameters satisfy all the side conditions of the proof rule.</p>
<p>Soundness checks <b>must be complete and self-sufficient</b> (bullet-proof) within the rule; that is, no matter how the rule is called and with which arguments, there should be no way for the rule to generate an invalid theorem. Even if the untrusted code which calls the rule does all the necessary checks, you have to do them again inside the rule. This is the whole point of the code being trusted: <em>it cannot go wrong, no matter what happens outside</em>. In case of <a class="el" href="namespaceCVC3.html">CVC3</a>, this means that <em>any non-null</em> <code>Theorem</code> <em>object represents a valid theorem</em>, no matter how this theorem was generated.</p>
<p>The main component of a <code>Theorem</code> object is a formula (returned by <code>Theorem::getExpr()</code>), which is valid in the appropriate <em>logical context</em>. The logical context is defined by the set of <em>assumptions</em> carried along in the <code>Theorem</code> object. Mathematically, a theorem object represents a <em>sequent</em> <img class="formulaInl" alt="$\Gamma\vdash\phi$" src="form_5.png"/>, where <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> is the set of assumptions (formulas assumed to be true), and <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is the theorem itself, the formula which logically follows from <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>.</p>
<p>Typically, an inference rule has the following format: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash\phi_1\quad\cdots\quad\Gamma_n\vdash\phi_n} {\Gamma_1,\ldots,\Gamma_n\vdash\psi}\]" src="form_6.png"/>
</p>
<p> where the assumptions of the conclusion are the union of all the assumptions from the premises.</p>
<p>The easiest way to compute the set of assumptions for the conclusion is to use the overloaded method <code>merge()</code> provided by the <code><a class="el" href="theorem_8h.html">theorem.h</a></code> API. This way you do not have to bother about the internal representation of assumptions. Keep in mind, that <a class="el" href="namespaceCVC3.html">CVC3</a> may be running in the mode without assumptions (for efficiency), which can be queried by <code>withAssumptions()</code> method:</p>
<div class="fragment"><pre class="fragment">
Theorem fooRule(const Theorem& prem1, const Theorem& prem2) {
.....
Assumptions a;
if(withAssumptions())
a = merge(prem1, prem2);
....
}
</pre></div><p>If the rule accepts more than two premises, you can merge assumptions by passing the vector of all premises to the <code>merge()</code> method.</p>
<p>When there is only one premis, the simplest way is to make a clean copy of the assumptions from the premis:</p>
<div class="fragment"><pre class="fragment">
if(withAssumptions())
a = premis.getAssumptionsCopy();
</pre></div><p>Occasionally, one needs to remove assumptions from the set, as in the following rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash\alpha\quad \Gamma_2, \alpha\vdash\phi} {\Gamma_1, \Gamma_2\vdash\phi}\mbox{Cut}\]" src="form_7.png"/>
</p>
<p>In this case, you can use the overloaded <code><a class="el" href="namespaceCVC3.html#aacf567dce1c762f957267427472bd959">operator-()</a></code> for class <code>Assumptions</code>:</p>
<div class="fragment"><pre class="fragment">
Theorem cutRule(const Theorem& alpha, const Theorem& phi) {
.....
Assumptions a;
if(withAssumptions())
a = (phi.getAssumptions() - alpha.getExpr()) + alpha.getAssumptions();
....
}
</pre></div><p>Remember, however, that due to the internal representation used in <a class="el" href="namespaceCVC3.html">CVC3</a>, removing an assumption is quite expensive, while merging is very cheap.</p>
<p>Also, if the soundness of your rule relies on the presence (or absence) of certain assumptions in premises, the first thing you need to check for is that <code>withAssumptions()</code> returns <code>true</code> (otherwise there is no way to determine the soundness of the rule, so it should not be called in the mode without assumptions).</p>
<p>In the above rule, if the assumption <img class="formulaInl" alt="$\alpha$" src="form_8.png"/> were required to be present for soundness of the rule, one could check it as follows:</p>
<div class="fragment"><pre class="fragment">
const Expr& alphaExpr = alpha.getExpr();
const Assumptions& phiAssump = phi.getAssumptionsRef();
if(CHECK_PROOFS) {
CHECK_SOUND(withAssumptions(),
"TheoryFoo::cutRule: called without assumptions!");
CHECK_SOUND(!phiAssump[alphaExpr].isNull(),
"TheoryFoo::cutRule: alpha is not an assumption of phi");
}
</pre></div><p>It is <b>extremely important</b> that assumptions are computed correctly when <code>withAssumptions()</code> returns <code>true</code>, since assumptions are used by the <a class="el" href="namespaceSAT.html">SAT</a> solver in the core framework, and are absolutely crucial for the results to be correct (or <em>sound</em>). Remember, that assumptions represent the logical context where the theorem is true, and if they are not computed properly, the entire theorem may become invalid.</p>
<p>Each <code>Theorem</code> object carries a <em>proof</em> of itself in the form of a <code>Proof</code> object.</p>
<p>Proofs are relatively expensive to generate (they take up extra space and somewhat slow down the rule execution), and therefore, it is the user's privilege to turn them off. For this reason, all proof generation code must be guarded by the method <code>withProof()</code>, similarly to <code>withAssumptions()</code>.</p>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> uses a version of Natural Deduction as its logical basis, and exploits the idea of Curry-Howard isomorphism to represent proofs as terms over function symbols representing proof rules. A ``<em>type</em>'' of a proof term is the formula (theorem) derived by the corresponding proof. The correctness of a proof in this framework corresponds to the proof term being ``well-typed.''</p>
<p>The <code>TheoremProducer</code> API provides an overloaded method <code>newPf()</code> for building proof terms. The first argument of (almost) any <code>newPf()</code> version is the name of the proof rule (<code>string</code>), and the rest are the arguments (parameters as <code>Expr</code> values, and the proofs of the rule's premises).</p>
<p>The key idea in building a proof term for the rule is to provide enough information in the proof term to be able to re-run the rule again with exactly the same arguments.</p>
<p>For instance, a proof term for the following rule: </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\frac{\Gamma_1\vdash x < y \quad \Gamma_2\vdash y < z} {\Gamma_1, \Gamma_2\vdash x < z}\mbox{project} \]" src="form_9.png"/>
</p>
<p> can be constructed as follows:</p>
<div class="fragment"><pre class="fragment">
Theorem projectRule(const Theorem& xLTy, const Theorem& yLTz) {
.....
Proof pf;
if(withProof()) {
vector<Expr> exprs;
vector<Proof> pfs;
exprs.push_back(xLTy.getExpr()); exprs.push_back(yLTz.getExpr());
pfs.push_back(xLTy.getProof()); pfs.push_back(yLTz.getProof());
pf = newPf("project", exprs, pfs);
}
.....
}
</pre></div><p>It is a very good idea to describe the proof object arguments in the proof rule documentation (doxygen comments) in <code>foo_proof_rules.h</code> file.</p>
<p>Note, that the proof object does <em>not</em> carry around any information about the assumptions. This is because all the assumptions are present implicitly as ``types'' of bound proof variables in LAMBDA-terms. I skip the description of this issue in the current version of this document, as it is rather subtle, and there is a 99% chance that you do not need to know that for your DP.</p>
<p>Finally, creating the resulting theorem in the proof rule is usually done by calling <code>newTheorem(conclusionExpr, a, pf)</code>, where <code>a</code> is the <code>Assumptions</code> variable, and <code>pf</code> is the proof term.</p>
<p>There is a special class of proof rules called <em>rewrite rules</em> in <a class="el" href="namespaceCVC3.html">CVC3</a>. These are proof rules without premises (<em>axioms</em>) whose conclusion is of the form <code>expr1 = expr2</code> or <code>frm1 <=> frm2</code>. These rules are so ubiquitous in the system that there is a special optimized constructor for the corresponding theorems: <code>newRWTheorem(expr1, expr2, a, pf)</code>.</p>
<p><b>Note:</b> the <code>Theorem</code> object constructed by the rewrite rule has a different internal representation from the "normal" <code>Theorem</code> object. Therefore, constructing a rewrite theorem with <code>newTheorem(expr1.eqExpr(expr2), a, pf)</code> will result in a run-time error. Make sure that if your theorem is a rewrite theorem (an equality <code>=</code> or equivalence <code><=></code>), then it must be constructed using the <code>newRWTheorem()</code> method.</p>
<p>I did not mention anything about computing the expression for the conclusion of the rule, but it should be fairly obvious how to do this. Remember, that each proof rule should be coded as concisely and as cleanly as possible, to ensure the effectiveness of manual inspection. Remember, this is a trusted part of the code. <b>K</b>eep <b>I</b>t <b>S</b>imple, <b>S</b>tupid. :-)</p>
<p><em>Sergey Berezin / berezin AT stanford DOT edu</em> </p>
</div></div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
