SEH-PILoT: A System for Property-Directed Symbol Elimination – Work in Progress (Short Paper) Philipp Marohn and Viorica Sofronie-Stokkermans University Koblenz-Landau, Koblenz, Germany {pmarohn,sofronie}@uni-koblenz.de Abstract. We describe the implementation of a system for property- directed 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 . 1 Introduction 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 stan- dard 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 proper- ties 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 elim- ination 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. 2 Description of the SEH-PILoT Implementation SEH-PILoT (Symbol Elimination based on Hierarchical Proving In Local Theory extensions) is an implementation of the method for symbol elimination presented in [12,13]. SEH-PILoT is implemented in Python 3.9. Its general structure is presented in Figure 1. Examples which show how SEH-PILoT can be used in various application areas (mathematics, verification, wireless network theory) can be found at https://userpages.uni-koblenz.de/~sofronie/sehpilot/. Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 76 Philipp Marohn and Viorica Sofronie-Stokkermans 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 reduc- tion 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 (CompΨ f ) 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 LocΨ Ψ f 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 (LocΨ f ) 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. SEH-PILoT 77 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 property- directed 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 (CompΨ f ) for a suitable closure operator Ψ . Let T = ΨK (G). Then Algorithm 1 yields a universal Π0 ∪ Σpar - formula ∀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). 78 Philipp Marohn and Viorica Sofronie-Stokkermans 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. SEH-PILoT 79 Symbol Elimination: SEH-PILoT (Symbol Elimination with H-PILoT): For obtaining constraints on parameters we used the method described in Al- gorithm 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 op- tion -redlog) for the hierarchical reduction to a problem in the base theory. H-PILoT com- putes the necessary instances K[TG ], where TG is the set of ground terms necessary for in- stantiation (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 sym- bols to be eliminated, the constants are clas- sified 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 after- wards 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 occur- ring 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]. 80 Philipp Marohn and Viorica Sofronie-Stokkermans 3 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 ); (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 :={( i n f l o w , 1 , 1)} R e l a t i o n s :={(<=, 2 ) , ( < , 2 ) , (>=, 2 ) , ( > , 2 ) } C l a u s e s := l <= l o v e r f l o w ; l > l a l a r m ; l p = ( l+i n f l o w ( t )) − o u t f l o w ; tp = t+ 1 ; Query := lp > loverflow ; 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 addi- tional constraints on the parameters (lalarm0)). This is done in the command line: sehpilot inv2.loc -e l lp tp -a ’lalarm0’ --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. Alter- natively, 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 as- sumptions 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/. SEH-PILoT 81 load package redlog ; r l s e t OFSF ; off r l v e r b o s e ; on r l n z d e n ; o f f nat ; vars := { l a l a r m , e 1 , l , l p , o u t f l o w , l o v e r f l o w , t , tp } ; f o r m u l a := ( 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 ) ; q u e r y := ( r l q e ex ( v a r s , f o r m u l a ) ) ; end ; 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 universally and obtains the weakest constraint: (Γ1 ) ∀t. (inflow(t) ≤ outflow) for which (2) becomes unsatisfiable. A similar procedure yields the constraint (Γ2 ) ∀t. (lalarm + inflow(t) ≤ loverflow) for (3). Test runs for SEH-PILoT. We analyzed examples from mathematics, verifi- cation 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 pro- vides 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. Name # clauses time H-PILoT # atoms # atoms time QE # atoms # atoms Time input (s) (1) (2) (ms) (3) (4) (s) Mathematics Case distinction 4 0.23 16 12 0.81 34 8 2.5 Example 5.6 in [13] Lipschitz 12 0.25 64 22 5.26 2925 3 9.5 Verification Water tank, -a 7 0.22 5 5 0.19 2 2 1.7 without SLFQ Water tank, no -a 6 0.10 6 6 0.08 2 2 0.8 without SLFQ Array sorted 6 0.23 11 8 0.82 2 2 2.5 Example 4 in [9] Maximum in array 7 0.22 11 6 0.8 1 1 3.0 Example 4.13 [14] Networks Graph class consist. 3 0.22 3 3 0.79 1 1 2.4 Example 4 in [10] Class inclusion (g4 ) 19 0.24 111 22 0.90 20 4 2.5 Class inclusion (g5 ) 19 0.24 114 22 1.01 20 4 2.7 Example 8 in [10,8] Table 1. Run on an Intel(R) Core(TM) i7-3770 CPU @ 3.40GHz, 8192 K-byte cache. # clauses is the number of clauses in the input to H-PILoT. # atoms refer to the number of atoms in the Redlog file generated by H-PILoT before (1) resp. after (2) simplification; resp. in the formu- la obtained after quantifier elimination before (3) resp. after (4) simplification. For all examples (with exception of the water tank) simplification with SLFQ was used, which is responsible for a significant amount of the runtime. 5 If SEH-PILoT is called with assumptions (-a) in the command line, redlog- simplification with assumptions is performed and the resulting formula is simpler. 82 Philipp Marohn and Viorica Sofronie-Stokkermans 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, ed- itors, 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 ver- ification. 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 combi- nations of theories. In J. Giesl and R. Hä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 para- metric 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 Inter- national 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 ex- tensions. In N. Olivetti and A. Tiwari, editors, Automated Reasoning - 8th Inter- national Joint Conference, IJCAR 2016, Proceedings, LNCS 9706, pages 273–289. Springer, 2016. 13. V. Sofronie-Stokkermans. On interpolation and symbol elimination in theory ex- tensions. Log. Methods Comput. Sci., 14(3), 2018. 14. V. Sofronie-Stokkermans. Parametric systems: Verification and synthesis. Fundam. Informaticae, 173(2-3):91–138, 2020.