SEH-PILoT: A System for Property-Directed Symbol Elimination - Work in Progress

Abstract

We describe the implementation of a system for propertydirected symbol elimination in extensions of a theory T0 with additional function symbols whose properties are axiomatised using a set of clauses. The system performs the symbol elimination in a hierarchical way, relying on existing mechanisms for symbol elimination in T0. Many reasoning problems in mathematics or program verification can be reduced to checking satisfiability of ground formulae w.r.t. a theory (this can be a standard theory, e.g. linear arithmetic, or a complex theory - e.g. the extension of a base theory with additional function symbols axiomatized by a set of formulae, or a combination of theories). More interesting is to go beyond yes/no answers, i.e. to consider problems - in mathematics or verification - in which the properties of certain function symbols are underspecified (these symbols are considered to be parametric) and (weakest) additional conditions need to be derived under which given properties hold. In [13] a method for property-directed symbol elimination in local theory extensions was proposed which can be used for obtaining such constraints on parameters. The goal of this paper is to present the current state of an implementation of this method in the system SEH-PILoT. Structure of the paper: In Section 2.2 we first present the theoretical background and then the implementation details. In Section 3 we discuss in detail an example, then present an overview of a (small) subset of the tests we considered so far.

Introduction

2.1

Theoretical Background

Let Π0=(Σ0, Pred) be a signature, and T0 be a “base” theory with signature Π0. We consider extensions T := T0∪K of T0 with new function symbols Σ (extension functions) whose properties are axiomatized using a set K of (universally closed) clauses in the extended signature Π = (Σ0 ∪ Σ, Pred), such that each clause in K contains function symbols in Σ. Let Σpar ⊆ Σ be a set of parameters. Let Σc be an additional set of constants.

Task: Let G be a set of ground Π ∪ Σc clauses. We want to check whether G is satisfiable w.r.t. T0 ∪ K or not and – if it is satisfiable – to generate a weakest universal Π0 ∪ Σpar-formula Γ such that T0 ∪ K ∪ Γ ∪ G is unsatisfiable. Method. For satisfiability checking we use a method for hierarchical reduction to checking satisfiability in the base theory. For symbol elimination (i.e. for determining Γ ) we use a method for hierarchically reducing the problem to a quantifier elimination problem w.r.t. T0. If T0 allows quantifier elimination (i.e. for every formula φ over Π0 there exists a quantifier-free formula φ∗ over Π0 which is equivalent to φ modulo T0) a method for quantifier elimination w.r.t. T0 can be used for this.

In what follows we present situations in which hierarchical reasoning is complete and weakest constraints on parameters can be generated.

Local Theory Extensions. Let Ψ be a closure operator on sets of ground terms. A theory extension T0 ⊆ T0 ∪ K is Ψ -local if it satisfies the condition: (LocfΨ )

For every finite set G of ground ΠC -clauses (for an additional set C of constants) it holds that T0 ∪ K ∪ G |= ⊥ if and only if

T0 ∪ K[ΨK(G)] ∪ G is unsatisfiable. where, for every set G of ground ΠC -clauses, K[ΨK(G)] is the set of instances of K in which the terms starting with a function symbol in Σ are in ΨK(G) = Ψ (est(K, G)), where est(K, G) is the set of ground terms starting with a function in Σ occurring in G or K. Ψ -local extensions can be recognized by showing that certain partial models embed into total ones [ 11,7 ]. Especially well-behaved are theory extensions with Ψ the property (Compf ) which requires that every partial model of T whose reduct to Π0 is total and the “set of defined terms” is finite and closed under Ψ , embeds into a total model of T with the same support (cf. e.g. [ 5 ]). If Ψ is the identity, we denote LocfΨ by Locf and CompfΨ by Compf . Examples of local theory extensions can be found in [ 14 ].

Hierarchical Reasoning. Consider a Ψ -local theory extension T0 ⊆ T0 ∪ K. Condition (LocfΨ ) requires that for every finite set G of ground ΠC clauses: T0 ∪ K∪G |=⊥ if and only if T0∪K[ΨK(G)]∪G |=⊥ . In all clauses in K[ΨK(G)]∪G the function symbols in Σ only have ground terms as arguments, so K[ΨK(G)]∪G can be flattened and purified1 by introducing, in a bottom-up manner, new 1 i.e. the function symbols in Σ are separated from the other symbols. constants ct ∈ C for subterms t=f (c1, . . . , cn) where f ∈Σ and ci are constants, together with definitions ct≈f (c1, . . . , cn) which are all included in a set Def. We thus obtain a set of clauses K0∪G0∪Def, where K0 and G0 do not contain Σ-function symbols and Def contains clauses of the form c≈f (c1, . . . , cn), where f ∈Σ, c, c1, . . . , cn are constants.

Theorem 1 ([ 11,5 ]) Let K be a set of clauses. Assume that T0 ⊆ T1 = T0 ∪K is a Ψ -local theory extension. For any finite set G of ground clauses, let K0∪G0∪Def be obtained from K[ΨK(G)] ∪ G by flattening and purification, as explained above. Then the following are equivalent to T1 ∪ G |=⊥: (1) T0∪K[ΨK(G)]∪G |=⊥ . n f (c1, . . . , cn)≈c∈Def (2) T0∪K0∪G0∪Con0 |=⊥, where Con0={ ^ ci≈di → c≈d | f (d1, . . . , dn)≈d∈Def }. i=1 We can also consider chains of theory extensions:

T0 ⊆ T1 = T0 ∪ K1 ⊆ T2 = T0 ∪ K1 ∪ K2 ⊆ · · · ⊆ Tn = T0 ∪ K1 ∪ ... ∪ Kn in which each theory is a local extension of the preceding one. For a chain of n local extensions a satisfiability check w.r.t. the last extension can be reduced (in n steps) to a satisfiability check w.r.t. T0. The only restriction we need to impose in order to ensure that such a reduction is possible is that at each step the clauses reduced so far need to be ground. Groundness is assured if each variable in a clause appears at least once under an extension function. This iterated instantiation procedure for chains of local theory extensions has been implemented in H-PILoT [ 6 ].2 Hierarchical Symbol Elimination. In [ 13 ] we proposed a method for propertydirected symbol elimination described in Algorithm 1.

Theorem 2 ([ 12,13 ]) Let T0 be a Π0-theory allowing quantifier elimination, Σpar be a set of parameters (function and constant symbols) and Σ a set of function symbols such that Σ ∩ (Σ0 ∪ Σpar) = ∅. Let K be a set of clauses in the signature Π0∪Σpar∪Σ in which all variables occur also below functions in Σ1 = Σpar ∪ Σ. Assume T ⊆ T0 ∪ K satisfies condition (CompfΨ ) for a suitable closure operator Ψ . Let T = ΨK(G). Then Algorithm 1 yields a universal Π0 ∪ Σparformula ∀x. ΓT (x) such that T0 ∪ ∀x. ΓT (x) ∪ K ∪ G |=⊥ which is entailed by every universal formula Γ with T0 ∪ Γ ∪ K ∪ G |=⊥.

Algorithm 1 yields a formula ∀x. ΓT (x) with T0 ∪ ∀x. ΓT (x) ∪ K ∪ G |=⊥ also if the extension T ⊆ T0 ∪ K is not Ψ -local or T 6= ΨK(G), but in this case there is no guarantee that ∀x. ΓT (x) is the weakest universal formula with this property. A similar result holds for chains of local theory extensions. 2 H-PILoT allows the user to specify a chain of extensions by tagging the extension functions with their place in the chain (e.g., if f occurs in K3 but not in K1 ∪ K2 it is declared as level 3). Algorithm 1 Symbol elimination in theory extensions [ 12,13 ] Input: Theory extension T0 ∪ K with signature Π = Π0 ∪ (Σ ∪ Σpar) where Σpar is a set of parameters

Set T of ground ΠC -terms Output: ∀y. ΓT (y) (universal Π0 ∪ Σpar-formula) Step 1 Purify K[T ] ∪ G as described in Theorem 1 (with set of extension symbols Σ1).

Let K0 ∪ G0 ∪ Con0 be the set of Π0C -clauses obtained this way.

Step 2 Let G1 = K0 ∪ G0 ∪ Con0. Among the constants in G1, we identify (i) the constants cf , f ∈ Σpar, where cf is a constant parameter or cf is introduced by a definition cf ≈ f (c1, . . . , ck) in the hierarchical reasoning method, (ii) all constants cp occurring as arguments of functions in Σpar in such definitions. Replace all the other constants c with existentially quantified variables x (i.e. replace G1(cp, cf , c) with ∃x. G1(cp, cf , x)).

Step 3 Construct a formula Γ1(cp, cf ) equivalent to ∃x. G1(cp, cf , x) w.r.t. T0 using a method for quantifier elimination in T0 and let Γ2(cp, cf ) be ¬Γ1(cp, cf ). Step 4 Replace (i) each constant cf introduced by definition cf ≈ f (c1, . . . , ck) with the term f (c1, . . . , ck) and (ii) cp with universally quantified variables y in Γ2(cp, cf ). The formula obtained this way is ∀y. ΓT (y).

Theorem 3 ([ 13 ]) Consider the following chain of theory extensions:

T0 ⊆ T0 ∪ K1 ⊆ T0 ∪ K1 ∪ K2 ⊆ . . . ⊆ T0 ∪ K1 ∪ K2 ∪ · · · ∪ Kn where every extension in the chain satisfies condition (Compf ), Ki are all flat and linear, and in all Ki all variables occur below the extension terms on level i.

Let G be a set of ground clauses, and let G1 be the result of the hierarchical reduction of satisfiability of G to a satisfiability test w.r.t. T0. Let T = T (G) be the set of all instances used in the chain of hierarchical reductions and let ∀y. ΓT (G)(y) be the formula obtained by applying Steps 2–4 of Alg. 1 to G1. Then ∀y. ΓT (G)(y) is entailed by every conjunction Γ of clauses with the property that T0 ∪ Γ ∪ K1 ∪ · · · ∪ Kn ∪ G is unsatisfiable (i.e. it is the weakest such constraint). 2.2

Implementation

Hierarchical reasoning: H-PILoT. The method for hierarchical reasoning in local theory extensions described before was implemented in the system H-PILoT [ 6 ]. H-PILoT carries out a hierarchical reduction to the base theory. Standard SMT provers or specialized provers can be used for testing the satisfiability of the formulae obtained after the reduction. H-PILoT uses eager instantiation and the hierarchical reduction, so provers like CVC4 [ 1 ] or Z3 [ 2 ] are in general faster in proving unsatisfiability. The advantage of using H-PILoT is that knowing the instances needed for a complete instantiation allows us to correctly detect satisfiability (and generate models) in situations in which e.g. CVC4 returns “unknown”, and use property-directed symbol elimination to obtain additional constraints on parameters which ensure unsatisfiability. Symbol Elimination: SEH-PILoT (Symbol Elimination with H-PILoT): For obtaining constraints on parameters we used the method described in Algorithm 1 [ 13 ] which was implemented in SEH-PILoT for the case in which the theory can be structured as a local theory extension or a chain of theory extensions and the base theory T0 is the theory of real closed fields. Input. SEH-PILoT receives a list of symbols to be eliminated (and possibly a list of already existing constraints on the parameters) and an input file for H-PILoT3. This file contains (i) the specification of the signature and of the hierarchy of local theory extensions to be considered; (ii) an axiomatization K of the theory extension(s); (iii) a set G of ground clauses possibly containing additional constants. Currently the only supported base theory for SEH-PILoT is the theory of real numbers (the theory of real closed fields).

Main Algorithm. SEH-PILoT follows the steps of Algorithm 1. Step 1: SEH-PILoT uses H-PILoT (with option -redlog) for the hierarchical reduction to a problem in the base theory. H-PILoT computes the necessary instances K[TG], where TG is the set of ground terms necessary for instantiation (cf. Thm.3), generates the formula K0 ∪ G0 ∪ Con0 and writes it in a file which can be used as input for Redlog [ 4 ].

Step 2: Taking into account the function symbols to be eliminated, the constants are classified as required in Step 2 of Alg. 1 and the Redlog file is changed accordingly such that only those symbols that do not correspond to a parameter or argument of a parameter are considered to be existentially quantified.

Step 3: SEH-PILoT uses Redlog to eliminate the existentially quantified symbols and afterwards to negate the resulting formula.

Step 4: The constants contained in the formula obtained by Step 3 are replaced back with the terms they represent and the constants occurring as arguments are replaced by universally quantified variables. Fig. 1. SEH-PILoT structure Finally SEH-PILoT translates the generated constraints from the syntax of Redlog back to the syntax of H-PILoT such that they can easily be used for verification or an iterative approach of constraint generation. Since Redlog is not very efficient in simplifying formulae, SLFQ can be used, which allows Redlog to use the possibilities of simplification offered by QEPCAD B [ 3 ]. 3 A detailed description of the form of such input files can be found in the system description of H-PILoT [ 6 ].

Examples

We illustrate the way SEH-PILoT works on the following example4. Consider a discrete water level controller in which the inflow varies during the evolution of the system, and can be modeled by a function inflow : R → R, where inflow(t) is the inflow at time step t. If the water level becomes greater than an alarm level Lalarm (positioned below the overflow level Loverflow) a valve is opened and a fixed quantity of water (outflow) is left out. Otherwise, the valve remains closed. Assume that the formula Init(L) := L<Loverflow describes the initial states. Then L ≤ Loverflow is an inductive invariant iff the following formulae are unsatisfiable w.r.t. the extension of the theory of real numbers with a function inflow: (1) ∃L. (L < Loverflow ∧ L > Loverflow); (2) ∃L, L0, t, t0. (L≤Loverflow∧L>Lalarm∧L0≈L+inflow(t)−outflow∧t0≈t+1∧L0>Loverflow); (3) ∃L, L0, t, t0. (L≤Loverflow ∧ L≤Lalarm ∧ L0≈L+inflow(t) ∧ t0≈t+1 ∧ L0>Loverflow). We want to obtain conditions on the parameters (inflow, outflow, Lalarm, Loverflow) under which L < Loverflow is an inductive invariant. (1) is clearly unsatisfiable. SEH-PILoT (with assumptions Lalarm < Loverflow, ∀x. inflow(x) > 0) generated weakest universal conditions under which (2) resp. (3) are unsatisfiable. Consider e.g. (2). The problem is described in the H-PILoT syntax as follows: B a s e f u n c t i o n s :={(+ ,2) , ( − ,2) , ( ∗ , 2 ) } E x t e n s i o n f u n c t i o n s :={( inflow , 1 , 1)} R e l a t i o n s :={(<=, 2 ) , (<, 2 ) , (>=, 2 ) , (>, 2)} Clauses := l <= l o v e r f l o w ; l > lalarm ; l p = ( l+i n f l o w ( t ))− outflow ; tp = t+ 1 ; Query:= l p > l o v e r f l o w ; It can be checked that the extension R ⊆ R∪K of R with a function symbol inflow satisfying the axiom K = ∀x.(inflow(x) > 0) defines a local theory extension. When using SEH-PILoT the user has to specify the name of the H-PILoT file (in this case inv2.loc), the symbols to be eliminated (l, lp and tp) and any additional constraints on the parameters (lalarm<loverflow and ∀x.(inflow(x)>0)). This is done in the command line: sehpilot inv2.loc -e l lp tp -a ’lalarm<loverflow’ ’inflow(?)>0’ --stats If called with the additional constraints added to the command line (example “Water tank, -a” in Table 1) SEH-PILoT generates the right instances. Alternatively, the clause ∀x.(inflow(x) > 0) can be added to the Clauses in the inv2.loc-file (example “Water tank, no -a” in Table 1). In both cases H-PILoT performs the hierarchical reduction described in Theorem 1 for G being the conjunction of the ground formulae in Clauses, Query and in the additional assumptions if option -a is used, by determining the set T = est(G) = {inflow(t)} of terms in G starting with an extension function, considering the instances of K containing this term, K[T ] = {inflow(t) > 0} and introducing a constant e1 for inflow(t), and generates the Redlog file: 4 This example as well as several additional examples can be found under https: //userpages.uni-koblenz.de/~sofronie/sehpilot/. l o a d p a c k a g e r e d l o g ; r l s e t OFSF ; o f f r l v e r b o s e ; on r l n z d e n ; o f f nat ; v a r s := { lalarm , e 1 , l , lp , outflow , l o v e r f l o w , t , tp } ; formula := ( l p > l o v e r f l o w and l > l a l a r m and l <= l o v e r f l o w and tp = t + 1 and l p = ( l + e1 ) − o u t f l o w ) ; query := ( r l q e ex ( vars , formula ) ) ; end ; universally and obtains the weakest constraint: SEH-PILoT classifies the constants and updates the Redlog file by simplifying the input and changing vars to the set of symbols to be eliminated l, lp, tp, eliminates these variables, negates the result and simplifies5 the resulting formula and obtains e1 − outflow ≤ 0. It then replaces e1 with inflow(t), quantifies t (Γ1) (Γ2) ∀t. (inflow(t) ≤ outflow) ∀t. (lalarm + inflow(t) ≤ loverflow) for (3). for which (2) becomes unsatisfiable. A similar procedure yields the constraint Test runs for SEH-PILoT. We analyzed examples from mathematics, verification and wireless network theory. We used H-PILoT for testing satisfiability of the formulae; if the formulae were satisfiable SEH-PILoT was used for symbol elimination and generating constraints on the parameters. The table below provides some data on the size of the problems we analyzed and the time H-PILoT needed for hierarchical reduction and SEH-PILoT for symbol elimination. # clauses time H-PILoT # atoms # atoms time QE # atoms # atoms Time

input (s) (1) (2) (ms) (3) (4) (s) Name Mathematics Case distinction Example 5.6 in [ 13 ] Lipschitz Verification Water tank, -a without SLFQ Water tank, no -a without SLFQ Array sorted Example 4 in [ 9 ] Maximum in array Example 4.13 [ 14 ] Networks Graph class consist.

Example 4 in [ 10 ] Class inclusion (g4) Class inclusion (g5) Example 8 in [ 10,8 ] 4 12 7 6 6 7 3 5 If SEH-PILoT is called with assumptions (-a) in the command line, redlogsimplification with assumptions is performed and the resulting formula is simpler.

References

1. C. W. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings, LNCS 6806 , pages 171 - 177 . Springer, 2011 .

2. N. Bjørner , L. de Moura, L. Nachmanson, and C. M. Wintersteiger . Programming Z3 . In J. P. Bowen , Z. Liu , and Z . Zhang, editors, Engineering Trustworthy Software Systems - 4th International School, SETSS 2018 , Tutorial Lectures, LNCS 11430 , pages 148 - 201 . Springer, 2019 .

3. C. W. Brown. QEPCAD B: a system for computing with semi-algebraic sets via cylindrical algebraic decomposition . SIGSAM Bull. , 38 ( 1 ): 23 - 24 , 2004 .

4. A. Dolzmann and T. Sturm . REDLOG: computer algebra meets computer logic . SIGSAM Bull. , 31 ( 2 ): 2 - 9 , 1997 .

5. C. Ihlemann , S. Jacobs , and V. Sofronie-Stokkermans . On local reasoning in verification . In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Proceedings, LNCS 4963 , pages 265 - 281 . Springer, 2008 .

6. C. Ihlemann and V. Sofronie-Stokkermans . System description: H-PILoT . In R. A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Proceedings, LNCS 5663 , pages 131 - 139 . Springer, 2009 .

7. C. Ihlemann and V. Sofronie-Stokkermans . On hierarchical reasoning in combinations of theories . In J. Giesl and R . Ha¨hnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173 , pages 30 - 45 . Springer, 2010 .

8. D. Peuter , P. Marohn , and V. Sofronie-Stokkermans . Symbol elimination for parametric second-order entailment problems (with applications to problems in wireless network theory) . CoRR , https://arxiv.org/abs/2107.02333, 2021 .

9. D. Peuter and V. Sofronie-Stokkermans . On invariant synthesis for parametric systems . In P. Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Proceedings, LNCS 11716 , pages 385 - 405 . Springer, 2019 .

10. D. Peuter and V. Sofronie-Stokkermans . Symbol elimination and applications to parametric entailment problems . In B. Konev and G. Reger, editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021 , Proceedings, LNCS 12941 , pages 43 - 62 . Springer, 2021 .

11. V. Sofronie-Stokkermans . Hierarchic reasoning in local theory extensions . In R. Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, LNCS 3632 , pages 219 - 234 . Springer, 2005 .

12. V. Sofronie-Stokkermans . On interpolation and symbol elimination in theory extensions . In N. Olivetti and A . Tiwari, editors, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings, LNCS 9706 , pages 273 - 289 . Springer, 2016 .

13. V. Sofronie-Stokkermans . On interpolation and symbol elimination in theory extensions . Log. Methods Comput. Sci. , 14 ( 3 ), 2018 .

14. V. Sofronie-Stokkermans . Parametric systems: Verification and synthesis . Fundam. Informaticae , 173 ( 2-3 ): 91 - 138 , 2020 .