CVC3  2.4.1
uf_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file uf_theorem_producer.cpp
4  *\brief TRUSTED implementation of uninterpreted function/predicate rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Tue Aug 31 23:20:27 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 // This code is trusted
24 #define _CVC3_TRUSTED_
25 
26 
27 #include "uf_theorem_producer.h"
28 #include "theory_uf.h"
29 #include "theory_core.h"
30 
31 
32 using namespace std;
33 using namespace CVC3;
34 
35 
36 ////////////////////////////////////////////////////////////////////
37 // TheoryUF: trusted method for creating UFTheoremProducer
38 ////////////////////////////////////////////////////////////////////
39 
40 
41 UFProofRules* TheoryUF::createProofRules() {
42  return new UFTheoremProducer(theoryCore()->getTM(), this);
43 }
44 
45 
46 ////////////////////////////////////////////////////////////////////
47 // Proof rules
48 ////////////////////////////////////////////////////////////////////
49 
50 
51 #define CLASS_NAME "CVC3::UFTheoremProducer"
52 
53 
54 Theorem UFTheoremProducer::relToClosure(const Theorem& rel)
55 {
56  const Expr& relExpr = rel.getExpr();
57 
58  if(CHECK_PROOFS)
59  CHECK_SOUND(relExpr.isApply() && relExpr.arity() == 2,
61  "theorem is not a relation or has wrong arity:\n"
62  + rel.getExpr().toString());
63 
64  Proof pf;
65  if(withProof()) {
66  pf = newPf("rel_closure", rel.getProof());
67  }
68 
69  const string& name = relExpr.getOp().getExpr().getName();
70  Expr tc = d_theoryUF->transClosureExpr(name, relExpr[0], relExpr[1]);
71 
72  return newTheorem(tc, rel.getAssumptionsRef(), pf);
73 }
74 
75 
76 Theorem UFTheoremProducer::relTrans(const Theorem& t1, const Theorem& t2)
77 {
78  const Expr& e1 = t1.getExpr();
79  const Expr& e2 = t2.getExpr();
80 
81  if (CHECK_PROOFS) {
83  e1.arity() == 2,
84  (CLASS_NAME
85  "theorem is not a proper trans_closure expr:\n"
86  + e1.toString()).c_str());
88  e2.arity() == 2,
89  (CLASS_NAME
90  "theorem is not a proper trans_closure expr:\n"
91  + e2.toString()).c_str());
92  }
93 
94  if (CHECK_PROOFS) {
95  CHECK_SOUND(e1.getOpExpr().getName() == e2.getOpExpr().getName() &&
96  e1[1] == e2[0],
97  (CLASS_NAME
98  "Expr's don't match:\n"
99  + e1.toString() + " and " + e2.toString()).c_str());
100  }
101 
102  Assumptions a(t1, t2);
103  Proof pf;
104  if(withProof()) {
105  vector<Proof> pfs;
106  pfs.push_back(t1.getProof());
107  pfs.push_back(t2.getProof());
108  pf = newPf("rel_trans", pfs);
109  }
110  return newTheorem(Expr(e1.getOp(), e1[0], e2[1]), a, pf);
111 }
112 
113 
114 Theorem UFTheoremProducer::applyLambda(const Expr& e) {
115  if(CHECK_PROOFS) {
116  CHECK_SOUND(e.isApply() && e.getOpKind() == LAMBDA,
117  "applyLambda("+e.toString()
118  +"):\n\n expression is not an APPLY");
119  }
120  Expr lambda(e.getOpExpr());
121 
122  if (CHECK_PROOFS) {
123  CHECK_SOUND(lambda.isLambda(),
124  "applyLambda:\n"
125  "Operator is not LAMBDA: " + lambda.toString());
126  }
127 
128  Expr body(lambda.getBody());
129  const vector<Expr>& vars = lambda.getVars();
130 
131  if(CHECK_PROOFS) {
132  CHECK_SOUND(vars.size() == (size_t)e.arity(),
133  "wrong number of arguments applied to lambda\n");
134  }
135 
136  // Use the Expr's efficient substitution
137  body = body.substExpr(vars, e.getKids());
138 // for (unsigned i = 0; i < vars.size(); i++) {
139 // body = substFreeTerm(body, vars[i], e[i]);
140 // }
141 
142  Proof pf;
143  if(withProof())
144  pf = newPf("apply_lambda", e);
145  return newRWTheorem(e, body, Assumptions::emptyAssump(), pf);
146 }
147 
148 
149 Theorem UFTheoremProducer::rewriteOpDef(const Expr& e) {
150  if(CHECK_PROOFS) {
151  CHECK_SOUND(e.isApply(),
152  "UFTheoremProducer::rewriteOpDef: 'e' is not a "
153  "function application:\n\n "+e.toString());
154  }
155 
156  Expr op = e.getOpExpr();
157  int opKind = op.getKind();
158 
159  if(CHECK_PROOFS) {
160  CHECK_SOUND(opKind==LETDECL,
161  "UFTheoremProducer::rewriteOpDef: operator is not a "
162  "named function in:\n\n "+e.toString());
163  }
164  // Now actually replace the name with the definition
165  while(opKind==LETDECL) {
166  if(CHECK_PROOFS) {
167  CHECK_SOUND(op.arity()==2,
168  "UFTheoremProducer::rewriteOpDef: bad named "
169  "operator in:\n\n "+e.toString());
170  }
171  op = op[1];
172  opKind = op.getKind();
173  }
174  // ...and construct a Theorem
175  Proof pf;
176  if(withProof())
177  pf = newPf("rewrite_op_def", e);
178  return newRWTheorem(e, Expr(op.mkOp(), e.getKids()), Assumptions::emptyAssump(), pf);
179 }
int arity() const
Definition: expr.h:1201
const Expr & getExpr() const
Definition: expr_op.h:84
Data structure of expressions in CVC3.
Definition: expr.h:133
Definition: kinds.h:227
STL namespace.
#define CHECK_SOUND(cond, msg)
#define CHECK_PROOFS
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
int getKind() const
Definition: expr.h:1168
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr getExpr() const
Definition: theorem.cpp:230
bool isApply() const
Definition: expr.h:1014
TRUSTED implementation of uninterpreted function/predicate proof rules.
const std::string & getName() const
Definition: expr.h:1050
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
Op mkOp() const
Make the expr into an operator.
Definition: expr.h:1178
Definition: expr.cpp:35
Definition: kinds.h:229
#define CLASS_NAME