* OVERVIEW
This file discusses the differences between the description on the FMSD
paper and the actual signature for the QF_IDL logic (as supported by the
clsat 1.1). The signature can be found in the clsat 1.1 distribution.

 Note: Please read separate readme files about how to use clsat and lfsc
       in their source distributions.


* DIFFERENCES FROM THE FMSD PAPER IN THE LFSC LANGUAGE
- Comments
Any line starts with the semicolon ";" in LFSC file (we use ".plf"
filename extension) is a comment.

- Integer Values
Any non-negative numbers are integers (mpz type in LFSC). Negative
numbers can be expressed using the unary "~" operator. For example,
(~ 1) for -1. Note that the "~" operator is only for values, not
general expressions. LFSC has a separate integer negation function
(explained below).

- Built-in Side Condition Programs
"markvar" built-in program has variations like "markvar2", "markvar3",
and so on up to "markvar31".

On the paper, "ifneg" command was explained. In the actual syntax,
it is "mp_ifneg". The "mp_" prefix stands for "multi-precision".
"mp_ifneg" is overloaded for values of mpz type (integer) and mpq type
(rational). More "mp_" functions are listed below:

mp_add : addition
mp_mult : multiplication
mp_neg : arithmetic negation

- Side Condition Declaration
The declaration of side conditions in the actual syntax is slightly
different. On the paper, we have an example as below:

(declare eq_zero (! t term (^ (normalize t) 0) (holds (= t 0))))

That is actually written as

(declare eq_zero (! t term (! r (^ (normalize t) 0) (holds (= t 0)))))

Our LFSC implementation currently requires an implicit function argument
(the "r" argument, above) for every side condition. The formal argument
r does not have a value and cannot be used in anywhere. And it also does
not take an actual argument to apply, either.

- Fresh State for Each Side Condition
The typing rule for a side condition tells that each execution is run
from an empty (fresh) state. However, the current LFSC implementation
reuses the previous state without cleaning up. Instead, we made sure our
side condition code cleans up the context before finishing. This
behavior is for a performance reason. The state (variable marks) is
scattered across LFSC variable objects in memory. Scanning and cleaning
up every variable will take a long time (or tracking changes). Cleaning
up can be done more efficiently in the side condition program because it
knows what to clean. But, it requires to verify all side conditions
indeed clean up the state.


* SIGNATURE FILES
The QF_IDL signature consists of several files for the convenience of
development and understanding. Those files are located in the
"proof-rules" subdirectory of the clsat distribution. Here's a brief
overview of the signature files.

sat.plf      : Propositional clause syntax/judgement, the resolution rule
smt.plf      : SMT formula syntax/judgement
cnf_conv.plf : CNF conversion rules and propositional abstraction rules
th_base.plf  : Basic theory reasoning skeleton (theory hypothesis)
               Some common rules (equality related)
th_idl.plf   : IDL specific rules (including normalization rules)

Note that sat.plf (by itself) is suffice to check propositional proofs
from SAT benchmarks. Also, this signature can be extended for other
logics by adding more theories.


* PROPOSITIONAL REASONING
The signature for clsat 1.1 uses the deferred resolution as explained on
the FMSD paper. And we reuse the name "R", instead of "DR" shown on the
paper, and we simply don't use the original resolution. From the user's
point of view, the deferred resolution changes the number of input
arguments (the number of holes because their actuall values can be all
inferred). In addition to the "R" rule, sat.plf defines the "Q" rule. Q
rule is basically same as R rule, however, Q rule expect its inputs (the
two premises) in the opposite order. R rule expects (pos v) in the
clause of the first proof p1 and (neg v) in the clause of the second
proof p2. On the other hand, Q rule expects (neg v) in the first clause,
and so on. For example,

(R _ _ p1 p2 v)

is same as

(Q _ _ p2 p1 v)


* PROPOSITIONAL LEMMA
The "satlem" rule simplifies and the deferred resolution terms and
declares lemmas to be used for later.

(declare satlem (! c1 clause
                (! c2 clause
                (! c3 clause
                (! u1 (holds c1)
                (! r (^ (simplify_clause c1) c2)
                (! u2 (! x (holds c2) (holds c3))
                   (holds c3))))))))

It takes a proof of c1 and clears up the deferred resolutions (storing
the result to c2). Also, it takes a proof of c3 under the assumption of
c2. Finally, it justifies c3 without the assumption. The assumption (x
above) acts as a new lemma, which can be used to derive c3. This satlem
rule subsumes the S rule shown on the paper, which simplifies deferred
resolution terms. S is shown on the paper for demonstration purposes and
not present in the actual signature.


* PROOF STRUCTURE
The output from an UNSAT benchmark by clsat contains a "check" LFSC
command, which tells LFSC to check the following expression is well
formed, and LFSC variables declarations (with their types representing
the input formula), and an ascription expression "(: Type term)" to
check if the type of given term (representing the proof) is the one
representing the empty clause (or false). Consider this formula:

  (p1 or p2) and (~p1 or p2) and (p1 or ~p2) and (~p1 or ~p2)

Here is an example LFSC proof for that formula:

(check 
(% v1 var 
(% v2 var 
(% x0 (holds (clc (pos v1) (clc (pos v2) cln)))
(% x1 (holds (clc (neg v1) (clc (pos v2) cln)))
(% x2 (holds (clc (pos v1) (clc (neg v2) cln)))
(% x3 (holds (clc (neg v1) (clc (neg v2) cln)))
(: (holds cln)
(satlem _ _ _ (R _ _ x0 x2 v2)
(\ m0
(satlem _ _ _ (R _ _ m0 (R _ _ x1 x3 v2) v1)
(\ @done @done
))))		; closing the satlem applications
))))))))

The declarations of function arguments from v1 up x3 represent the input
formula. The input formula consists of the variable declarations (v1 and
v2) and the hypotheses of CNF clauses (x1, x2, x3). The first argument
of the ascription expression ":" is the type declaration representing
the formula being proved. The second argument is a term representing the
actual "proof" (with the rest being decorations).
Logically, a proof is a sequence of lemmas. However, due to the way
satlem is defined, satlem takes a proof the lemma and the rest of
proof as the second argument. This makes a proof very deeply nested.
But, such a term is right-associative and LFSC is optimized to
perform tail-recursions for such cases.

Note that the last satlem is necessary to simplify the proof of the
empty clause with the deferred resolution term into the pure empty
clause, which is names as "@done". Then, the proof simply concluded the
"@done". Also, note the closing parentheses at the end of the proof.
Currently, the proof generator has to count how many number of
parentheses need to be closed at the end. That's one thing you would not
want to care. Hopefully, this will be improved for later (using a closure
symbol or else).


* SMT SYNTAX
Our signature supports most Boolean connectives and let/flet bindings and
the term/predicate if-then-else expressions.

- SMT Sorts
We declared "sort" type to represent the SMT sorts like integer, real,
array, and so on. For SMT predicates, we declared the "Bool" sort. It is
to avoid to declare two separate congruence rule for terms and
predicates. The Qf_IDL logic would only need the integer and Bool sorts,
though. Here the symbols "Bool", "Int", "Real" are just constants of the
sort type. The "term" type family represent the types of SMT predicates
and terms. For example, "(term Bool)" is the type for predicates and
"(term Int)" is the type for integers. The reason we defined "term" with
sorts is because SMT has some rules that are indeed polymorphic. For
example, the congruence rule is applicable to all SMT sorts and
predicates. We use a function "p_app" to cast (term Bool) into formula.
Suppose p is a variable of (term Bool), (p_app p) is a formula, now. For
a similar reason, integer numerals in LFSC, which are of the mpz type,
need the "an_int" function to be casted as an SMT integer of the (term
Int) type. On the paper, we used "int" for (term Int) for clarity, and
"as_int" for "an_int".

- Functions and Predicates with Arguments
Functions and predicates with arguments can be defined using the "arrow"
function. For example, "(arrow (term Int) (term Int))" represets
functions of Int -> Int type. Note that (term Bool) is distinct from
formula. To apply functions and predicates, use the "apply" function.
Note that they are not necessary for the QF_IDL logic.


* A SIMPLE EXAMPLE PROOF
Following is an SMT proof, but only with propositional reasoning, to
demonstrate how CNF conversion is processed using the partial clause
rules. The variables in the proof are annotated with their supposedly
computed types.

(check
(% p (term Bool)
(% @f (th_holds (and (p_app p) (not (p_app p))))
(: (holds cln)
(start _ @f
(\ @f0  ; (pc_holds (pcc (and (p_app p) (not (p_app p))) pc_nil) cln)
(dist_pos _ _ _ _ @f0
(\ @f1  ; (pc_holds (pcc (p_app p) pc_nil) cln)
(\ @f2  ; (pc_holds (pcc (not (p_app p)) pc_nil) cln)
(decl_atom_pos _ _ _ @f1
(\ @v0  ; var
(\ @a0  ; (atom v0 (p_app p))
(\ @f3  ; (pc_holds pc_nil (clc (pos v0) cln))
(clausify _ @f3
(\ @x0  ; (holds (clc (pos v0) cln))
(subst_atom_neg _ _ _ _ @f2 @a0
(\ @f4  ; (pc_holds pc_nil (clc (neg v0) cln))
(clausify _ @f4
(\ @x1  ; (holds (clc (neg v0) cln))
(satlem _ _ _ (R _ _ @x0 @x1 @v0)
(\ @done @done))
)))))))))))))))))))

pcc and pc_nil are two constructors for pc_form, formula lists,
corresponding with cons and nil for the standard list type in functional
programming.

decl_atom_* and subst_atom_* rules are used to abstract (atomic) formulas
and also recognize already abstracted formulas (to abstract with the same
propositional variables). On the paper, we showed the "literal" rule
as a concept for these actual rules. It's proof generators responsibility
to issue subst_atom_* rules to recognize the same formulas, otherwise
the same formula may be abstracted with several different propositional
variables.


* A QF_IDL EXAMPLE PROOF
Consider this formula:

  ~(x-y > -3) and (y-z <= 1) and (x-z >= -1)

Here is the proof:

(check
(% x (term Int)
(% y (term Int)
(% z (term Int)
(% @f (th_holds (and (not (> (- x y) (an_int (~ 3))))
                (and (<= (- y z) (an_int 1))
                     (>= (- x z) (an_int (~ 1))))))
(: (holds cln)
(start _ @f
(\ @f0
(dist_pos _ _ _ _ @f0
(\ @f1
(\ @f2
(decl_atom_neg _ _ _ @f1
(\ @v0
(\ @a0
(\ @f3
(clausify _ @f3
(\ @x0
(dist_pos _ _ _ _ @f2
(\ @f4
(\ @f5
(decl_atom_pos _ _ _ @f4
(\ @v1
(\ @a1
(\ @f6
(clausify _ @f6
(\ @x1
(decl_atom_pos _ _ _ @f5
(\ @v2
(\ @a2
(\ @f7
(clausify _ @f7
(\ @x2
(satlem _ _ _
  (Q _ _ @x0 (R _ _ @x1 (R _ _ @x2
    (assume_false _ _ _ @a0
    (\ @h0
    (assume_true _ _ _ @a1
    (\ @h1
    (assume_true _ _ _ @a2
    (\ @h2
      (idl_contra _ _
				(idl_trans _ _ _ _ _ _
				  (not_>_to_<= _ _ _ @h0)
					(idl_trans _ _ _ _ _ _ @h1 (>=_to_<= _ _ _ _ @h2))
				)
			)
    ))))))		; closing assume_* applications
  @v2) @v1) @v0)	; for resolution rules (R/Q)
(\ @done @done))
))))))))))))))))))))))))))))))))

not_>_to_<= and >=_to_<= are IDL normalization rules. Currently,
they are normalized within each theory lemma.