The quanti er-free logic of Equality with Uninterpreted Function symbols (EUF) is at the core of Satis ability Modulo Theory (SMT) solvers. There exist several competing proof formats for EUF proofs. We propose original proof formats obtained from proof forests that are the artifacts proposed by Nieuwenhuis and Oliveras to extract e ciently EUF unsatis able cores. Our proof formats can be generated by SMT solvers for almost free. Moreover, our preliminary experiments show that our novel veri ers outperform other existing EUF veri ers and that our proof formats appear to be more concise than existing EUF proofs.
the running time of all the veri ers is negligible w.r.t. the type-checking of the EUF proofs. Another result of our experiments is that proof forests veri ers are very fast and that (trimmed down) proof forests appear to be more concise than existing EUF proofs. Another advantage is that proof forests can be generated for almost free by SMT solvers based on proof forests.
The rest of the paper is organised as follows. Section 2 provides basic de nitions and known facts about the EUF logic. Section 3 recalls the nature of proof forests and explains the workings of our novel EUF proof veri ers. Section 4 is devoted to experiments. Section 5 concludes. 2
We write T ( ; V) the smallest set of terms built upon a set of variables V and a ranked alphabet of uninterpreted function symbols. For EUF, an atomic formula is of the form t = t0 for t, t0 2 T ( ; ;) and a literal is an atomic formula or its negation. Equality (=) is re exive, symmetric, transitive and closed under congruence: x = x x = y y = x x = y; y = z x = z
x1 = y1; : : : ; xn = yn f (x1; : : : ; xn) = f (y1; : : : ; yn)
Ackermann has proved using a reduction approach that the EUF logic is decidable [
In the following, we assume w.l.o.g. that EUF terms are at and curried [20, Section 3.1] i.e., are of the form a or f (a1; a2) where f represents an explicit application symbol and a, a1 and a2 are constants. In the rest, we drop the f and write a1(a2) for f (a1; a2). These transformations can be performed in linear time and simplify the decision procedure. 3.1
Nieuwenhuis and Oliveras have proposed a proof-producing congruence closure algorithm for
deciding EUF [
The Explain algorithm is based on a speci c data structure: the proof forest. A proof forest is a collection of trees and each edge a ! b in the proof forest is labelled by a reason justifying why the equality a = b holds. A reason is either an input equation a = b or a pair of input equations a1(a2) = a and b1(b2) = b. For the second case, there must be justi cations in the forest for a1 = b1 and a2 = b2.
We give in Figure 1 a modi ed version of the original Explain algorithm. The NearestAncestor and Parent functions return (if it exists) respectively the nearest common ancestor of two nodes l e t E x p l a i n A l o n g P a t h ( a , c ) := a := H i g h e s t N o d e ( a ) ; c := H i g h e s t N o d e ( c ) ; i f a = c t h e n r e t u r n e l s e b:= P a r e n t ( a ) ; i f e d g e h a s form a a=!b b t h e n Output ( a = b ) e l s e f / e d g e h a s form a b1(b2)=!b b /
a1(a2)=a Output a1 ( a2)=a and b1 ( b2)=b ;
E x p l a i n ( a1 , b1 ) ; E x p l a i n ( a2 , b2 ) g ; Union ( a , b ) ; E x p l a i n A l o n g P a t h ( b , c ) (a) ExplainAlongPath l e t E x p l a i n ( a , b ) := c := N e a r e s t A n c e s t o r ( a , b ) ; E x p l a i n A l o n g P a t h ( a , c ) ; E x p l a i n A l o n g P a t h ( b , c )
(b) Explain
in the proof forest and the parent of a node in the proof forest. A union- nd data structure [
Contrary to the original version, our algorithm is recursive. The Union operation has also been moved. As a consequence output equations are ordered di erently. This will ease our futur proof production. Another di erence is that the original algorithm always terminates but does not detect certain ill-formed proof forests e.g., a b=f(b!) b. In this case, the recursive a=f(a) algorithm does not terminate (this issue is dealt with in section 4.1). 3.2
The Explain algorithm of Figure 1 can be turned into a EUF proof veri er. The veri er is a version of Explain augmented with additional checks to ensure that the edges obtained from the SMT solver correspond to a well-formed proof forest. For instance, the veri er checks that edges are only labelled by input equations. Moreover, for edges of the form a b1(b2)=!b b, the recursive a1(a2)=a calls to Explain ensure that a1 = b1 and a2 = b2 have proofs in the proof forest i.e., a1 (resp. a2) is connected with b1 (resp. b2) by some valid path in the proof forest. For e ciency and simplicity, the least common ancestors are not computed by the veri er but used as untrusted hints. The soundness of the veri er does not depend on the validity of this information as the proposed least common ancestor is just used to guide the proof. If the return node is not a common ancestor, the veri er will simply fail.
For the veri er, a EUF proof is a pruned proof forest corresponding to the edges walked through during a preliminary run of Explain. As the SMT solver needs to traverse the proof forest to extract unsatis able core, we argue that the proof forest is a EUF proof that requires no extra-work from the SMT solver. l e t UFchecker i n p u t e d g e s ( x , y ) := f o r ( a = b ) 2 i n p u t do Union ( a , b ) done f o r a b1(b2)=!b b i n e d g e s do
a1(a2)=a i f ( a1 ( a2)=a ) 2 i n p u t & ( b1 ( b2)=b ) 2 i n p u t
& i s E q u a l ( a1 , b1 ) & i s E q u a l ( a2 , b2 ) t h e n Union ( a , b ) e l s e f a i l done r e t u r n i s E q u a l ( x , y ) To avoid traversing the same edge several times, the Explain algorithm and its veri er are using a union- nd data structure. Therefore, the Explain veri er implicitly embeds a decision procedure for the theory of equality. Our optimised veri er fully exploits this observation and starts by feeding all the input equalities of the form a = b into its union- nd. For the decision procedure, new equalities are obtained by applying the congruence rule and e ciency crucially depends on a clever indexing of the equations. The veri er does not require this costly machinery and takes as argument a trimmed down proof forest reduced to the list of edges of the forest of form a b1(b2)=!b b. The edge labels indicate the equations that need to be paired to derive a1(a2)=a a = b by the congruence rule. The algorithm of the veri er is given in Figure 2 where the predicate isEqual(a,b) checks whether a and b have the same representative in the union- nd i.e., Find(a) = Find(b). Once again, a preliminary run of Explain is su cient to generate a proof for this optimised veri er. 4 4.1
Our veri ers are implemented using the native version of Coq [
Compared to other languages, a constraint imposed by Coq is that all programs must be terminating. The UFchecker (see Section 3.3) is trivially terminating. Termination of the proof-forest veri er is more intricate because the Explain algorithm (see Figure 3.2) does not terminate if the proof forest is ill-formed e.g., has cycles. However, if the proof forest is wellformed, an edge is only traversed once. As a result, at each recursive call, our veri er decrements an integer initialised to the size of the proof forest. In Coq, the veri er fails after exhausting the maximum number of allowed recursive calls.
For the sake of comparison, we have also implemented the EUF proof format of Z3. Z3 refutations are also generated using Explain [14, Section 3.4.2]. Unlike our veri ers, Z3 proofs use explicit boolean reasoning and modus ponens. As a consequence formulae do not have 90 VeriT 80 Proof Forest
Z3
UFchecker
70
.)60
c
(se50
e
m
itc40
q
o
c30
a constant size. As already noticed by others [
We have assessed the e ciency of our EUF veri ers on several families of handcrafted
conjunctive EUF benchmarks. The benchmarks are large and all the literals are necessary to prove
unsatis ability. The formulae are not representative of con ict clauses obtained from
SMTLIB [
00 10000 20000 30000 40000 50000 60000 benchmark size (number of vari7a0b0le0s0) 80000 90000 100000 00 10000 20000 30000 40000 50000 60000 benchmark size (number of var7ia0b0l0e0s) 80000 90000 100000 (a) Total running time (b) Size of proofs 100 10 .) (scee 1 m it g n ikce 0.1 h c x0 = x1 x0 6= x(j+1) j f (xi j; xi j) = xi j+1 = ::: = xi j+j for i 2 f0 : : : jg The benchmarks are indexed by the number of EUF variables and the results are obtained using a Linux laptop with a processor Intel Core 2 Duo T9600 (2.80GHz) and 4GB of Ram. Figure 3a shows the time needed to construct and compile Coq proof terms. Figure 3b shows the size of the compiled proof terms. Figure 3c is focusing on the running time of the veri ers excluding the time needed to construct and dump proof terms.
For all our benchmarks, the UFchecker shows a noticeable advantage over the other veri ers.
We can also remark that its behaviour is more predicable. The veriT veri er [
Our Z3 veri er scales well despite being slightly but constantly outrun by the veri ers based on proof-forests. The running time of the di erent veri ers is given Figure 3c using a logarithmic scale. This emphases the fact that, except for the veriT veri er, the running time of the all the veri ers is below the second and is therefore not the limiting factor of the veri cation. Not surprisingly, the UFchecker requires smaller proofs and therefore its global checking time is also smaller. For big benchmarks, its running time also tends to be smaller than the running time of other veri ers. 5
Proof generating SMT solvers such as Z3 [