1 /*-----------------------------------------------------------------------
2
3 File : cte_subst.h
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Definitions for substitutions. Substitutions are really represented
10 by term cells with bindings. The substitution type is only a
11 disguised stack keeping track of the bound variables for
12 backtracking.
13
14 Copyright 1998, 1999 by the author.
15 This code is released under the GNU General Public Licence and
16 the GNU Lesser General Public License.
17 See the file COPYING in the main E directory for details..
18 Run "eprover -h" for contact information.
19
20 Changes
21
22 <1> Thu Mar 5 00:22:28 MET 1998
23 New
24
25 -----------------------------------------------------------------------*/
26
27 #ifndef CTE_SUBST
28
29 #define CTE_SUBST
30
31 #include <clb_pstacks.h>
32 #include <clb_pqueue.h>
33 #include <cte_termbanks.h>
34
35 /*---------------------------------------------------------------------*/
36 /* Data type declarations */
37 /*---------------------------------------------------------------------*/
38
39 typedef PStackCell SubstCell;
40 typedef PStack_p Subst_p;
41
42 /*---------------------------------------------------------------------*/
43 /* Exported Functions and Variables */
44 /*---------------------------------------------------------------------*/
45
46 #define SubstAlloc() PStackAlloc()
47 #define SubstFree(junk) PStackFree(junk)
48
49 #define SubstDelete(junk) SubstBacktrack(junk);SubstFree(junk)
50 #define SubstDeleteSkolem(junk) SubstBacktrackSkolem(junk);SubstFree(junk)
51 #define SubstIsEmpty(subst) PStackEmpty(subst)
52
53 static __inline__ PStackPointer SubstAddBinding(Subst_p subst, Term_p var, Term_p bind);
54 bool SubstBacktrackSingle(Subst_p subst);
55 int SubstBacktrackToPos(Subst_p subst, PStackPointer pos);
56 int SubstBacktrack(Subst_p subst);
57
58 PStackPointer SubstNormTerm(Term_p term, Subst_p subst, VarBank_p vars);
59
60 bool SubstBindingPrint(FILE* out, Term_p var, Sig_p sig, DerefType deref);
61 long SubstPrint(FILE* out, Subst_p subst, Sig_p sig, DerefType deref);
62 bool SubstIsRenaming(Subst_p subt);
63
64 void SubstBacktrackSkolem(Subst_p subst);
65 void SubstSkolemizeTerm(Term_p term, Subst_p subst, Sig_p sig);
66 void SubstCompleteInstance(Subst_p subst, Term_p term,
67 Term_p default_binding);
68
69
70 /*-----------------------------------------------------------------------
71 //
72 // Function: SubstAddBinding()
73 //
74 // Perform a new binding and store it in the subst. Return the old
75 // stackpointer (i.e. the value that you'll have to backtrack to to
76 // get rid of this binding).
77 //
78 //
79 // Global Variables: -
80 //
81 // Side Effects : Changes bindings, adds to the substitution.
82 //
83 /----------------------------------------------------------------------*/
84
SubstAddBinding(Subst_p subst,Term_p var,Term_p bind)85 PStackPointer SubstAddBinding(Subst_p subst, Term_p var, Term_p bind)
86 {
87 PStackPointer ret = PStackGetSP(subst);
88
89 assert(subst);
90 assert(var);
91 assert(bind);
92 assert(TermIsVar(var));
93 assert(!(var->binding));
94 assert(!TermCellQueryProp(bind, TPPredPos));
95 assert(var->sort != STNoSort);
96 assert(bind->sort != STNoSort);
97 assert(var->sort == bind->sort);
98
99 /* printf("# %ld <- %ld \n", var->f_code, bind->f_code); */
100 var->binding = bind;
101 PStackPushP(subst, var);
102
103 return ret;
104 }
105
106 #endif
107
108 /*---------------------------------------------------------------------*/
109 /* End of File */
110 /*---------------------------------------------------------------------*/
111
112
113
114
115
116