1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Class for condition fragment supporting equality test.
25 //
26 #ifndef _equalityConditionFragment_hh_
27 #define _equalityConditionFragment_hh_
28 #include "conditionFragment.hh"
29 #include "rhsBuilder.hh"
30
31 class EqualityConditionFragment : public ConditionFragment
32 {
33 NO_COPYING(EqualityConditionFragment);
34
35 public:
36 EqualityConditionFragment(Term* lhs, Term* rhs);
37 ~EqualityConditionFragment();
38
39 void check(VariableInfo& varInfo, NatSet& boundVariables);
40 void preprocess();
41 void compileBuild(VariableInfo& variableInfo, TermBag& availableTerms);
42 void compileMatch(VariableInfo& variableInfo, NatSet& boundUniquely);
43 bool solve(bool findFirst,
44 RewritingContext& solution,
45 stack<ConditionState*>& state);
46
47 Term* getLhs() const;
48 Term* getRhs() const;
49
50 void normalize(bool full);
51 //
52 // This function exists to enable equality condition fragments to have
53 // a special operational semantics under rewriting modulo SMT.
54 //
55 void buildInstances(Substitution& substitution, DagNode*& lhs, DagNode*& rhs);
56
57 #ifdef DUMP
58 void dump(ostream& s, const VariableInfo& variableInfo, int indentLevel);
59 #endif
60
61 private:
62 Term* lhs;
63 Term* rhs;
64 RhsBuilder builder;
65 int lhsIndex;
66 int rhsIndex;
67 };
68
69 inline Term*
getLhs() const70 EqualityConditionFragment::getLhs() const
71 {
72 return lhs;
73 }
74
75 inline Term*
getRhs() const76 EqualityConditionFragment::getRhs() const
77 {
78 return rhs;
79 }
80
81 inline void
normalize(bool full)82 EqualityConditionFragment::normalize(bool full)
83 {
84 lhs = lhs->normalize(full);
85 rhs = rhs->normalize(full);
86 }
87
88 #endif
89