CVC3  2.4.1
LFSCPrinter.cpp
Go to the documentation of this file.
1 #include "LFSCPrinter.h"
2 
3 
4 LFSCPrinter::LFSCPrinter( Expr pf_expr, Expr qExpr, std::vector<Expr> assumps,
5  int lfscm, CommonProofRules* commonRules ):
6  d_user_assumptions(assumps),
7  d_common_pf_rules(commonRules){
8 
9  printer = this;
10 
11  if( !qExpr.isFalse() ){
12  d_user_assumptions.push_back( cascade_expr( Expr( NOT, qExpr ) ) );
13  }
14 
16 
17  let_i = 1;
18  LFSCObj::initialize( pf_expr, lfscm );
19  converter = new LFSCConvert( lfscm );
20 }
21 
22 ///////////////////////////////////////
23 // main print method
24 ///////////////////////////////////////
25 
26 void LFSCPrinter::print_LFSC( const Expr& pf )
27 {
28  ostringstream cparen;
29 
30  //(AJR-1) Print the input formula and (: bottom ascription
31 
32  cout << "(check " << endl;
33  cparen << ")";
34 
35  // collecting variables from assumptions
36  std::vector<Expr>::iterator a = d_user_assumptions.begin(), aend = d_user_assumptions.end();
37  while(a!=aend){
38  Expr ce = cascade_expr( *a );
39  queryM( ce );
40  d_assump_map[ ce ] = true;
41  collect_vars(*a);
42  a++;
43  }
44 
45  //////scan for the assumptions
46  //std::vector< Expr > assumps;
47  //collect_assumptions( pf, assumps );
48  ////we must record skolemizations
49  //for( int a=1; a<(int)assumps.size(); a++ ){
50  // if( !d_assump_map[ assumps[a] ] ){
51  // ostringstream ose;
52  // ose << "Unexpected non-discharged assumption " << assumps[a];
53  // print_error( ose.str().c_str(), cout );
54  // }
55  //}
56 
57  //printing variables
59  while(v!= vend){
60  cout<<"(% "<<(*v).first<<" var_real"<<endl;
61  v++;
62  cparen<<")";
63  }
64  v = input_preds.begin(), vend = input_preds.end();
65  while(v!= vend){
66  cout<<"(% "<<(*v).first<<" formula"<<endl;
67  v++;
68  cparen<<")";
69  }
70  //cout << "here1" << std::endl;
71  //(AJR-2) Run T0( pf )
72  define_skolem_vars( pf );
73  //cout << "here2" << std::endl;
74  //convert the proof
75  converter->convert( pf );
76 
77  //make the let map for input formulas
78  a = d_user_assumptions.begin();
79  while(a!=aend){
80  make_let_map( cascade_expr( *a ) );
81  a++;
82  }
83  //make the let map for trusted formulas
85  while( j != jend){
86  make_let_map( cascade_expr( (*j).first ) );
87  j++;
88  }
89  //make the let map for output atomic formulas and terms
91  while( j2 != j2end){
92  if( (*j2).second ){
93  make_let_map( cascade_expr( (*j2).first ) );
94  }
95  j2++;
96  }
97  //j = d_terms.begin(), jend = d_terms.end();
98  //while( j != jend){
99  // make_let_map((*j).first);
100  // j++;
101  //}
102 
103  ////output skolem vars
104  //j = skolem_vars.begin(), jend = skolem_vars.end();
105  //while( j != jend ){
106  // if( (*j).second!=0 ){
107  // cout<<"(% "<<(*j).first<<" var_real"<<endl;
108  // cparen << ")";
109  // }
110  // j++;
111  //}
112 
113  //output let definitions
115  while( j2 != j2end ){
116  int val = d_print_map[(*j2).first];
117  if( val!=0 ){
118  cout << "(@ ";
119  d_print_map[(*j2).first] = 0;
120  if( isFormula( (*j2).first ) ){
121  cout << "@f" << val << " ";
122  print_formula( (*j2).first, cout );
123  }else{
124  cout << "@x" << val << " ";
125  print_terms( (*j2).first, cout );
126  }
127  d_print_map[(*j2).first] = val;
128  cout << endl;
129  cparen << ")";
130  }
131  j2++;
132  }
133  if( !d_print_map.empty() )
134  cout << endl;
135 
136  // printing user assumptions
137  a = d_user_assumptions.begin();
138  int m = 1;
139  while(a!=aend){
140  cout<<"(% @F"<<m<<" (th_holds ";
141  print_formula(*a, cout);
142  cout<<")"<<endl;
143  a++;
144  m++;
145  cparen << ")";
146  }
147 
148  //print trusted formulas
149  j = d_trusted.begin(), jend = d_trusted.end();
150  while( j != jend){
151  cout <<"(% @T" << (*j).second <<" (th_holds ";
152  print_formula((*j).first, cout);
153  cout<<")"<<endl;
154  cparen << ")";
155  j++;
156  }
157 
158  cout << "(: bottom" << endl;
159  cparen << ")";
160 
161 
162  //outer lambda abstractions
163  //cout << "number of outer lam abstractions = " << LFSCProof::lambdaCounter << std::endl;
165 
166 
167  ////debug----
168  //j = d_formulas.begin(), jend = d_formulas.end();
169  //while( j != jend){
170  // ExprMap< int >::iterator jPrev = j;
171  // j++;
172  // while( j != jend ){
173  // Expr e1 = cascade_expr( (*j).first );
174  // Expr e2 = cascade_expr( (*jPrev).first );
175  // if( e1==e2 ){
176  // ostringstream ose;
177  // ose << "Warning: Atomizing identical formulas " << (*j).second << " " << (*jPrev).second << std::endl;
178  // print_error( ose.str().c_str(), cout );
179  // }
180  // j++;
181  // }
182  // j = jPrev;
183  // j++;
184  //}
185  ////debug----
186 
187  //(AJR-3) Print the atoms used in the proof, these are contained in M.
188  j = d_formulas.begin(), jend = d_formulas.end();
189  while( j != jend){
190  cout <<"(decl_atom ";
191  //if( d_formulas_printed[(*j).first] ){ //HACK to ignore this
192  print_formula( (*j).first, cout );
193  //}else{
194  // cout << "_";
195  //}
196  cout<< " (\\ @b"<<(*j).second<<" (\\ @a"<<(*j).second<<endl;
197  cparen << ")))";
198  j++;
199  }
200  //need to print out atomized terms too
201  j = d_terms.begin(), jend = d_terms.end();
202  while( j != jend){
203  cout <<"(decl_term_atom ";
204  print_terms( (*j).first, cout );
205  cout<< " (\\ @bt"<<(*j).second<<" (\\ @at"<<(*j).second<<endl;
206  cparen << ")))";
207  j++;
208  }
209 
210  //(AJR-4) Print all polynomial normalization proofs. These are stored in M_t.
211  //print out the term normalizations
212  j = d_pn_form.begin(), jend = d_pn_form.end();
213  while(j !=jend ){
214  pntNeeded[ (*j).second ] = true;
215  j++;
216  }
217  j = d_pn.begin(), jend = d_pn.end();
218  while(j !=jend){
219  if( cvc3_mimic || pntNeeded[ (*j).second ] ){
220  cout << "(pn_let _ _ ";
221  Expr ce = cascade_expr( (*j).first );
222  print_poly_norm( ce, cout);
223  cout << "(\\ @pnt" << (*j).second << endl;
224  cparen << "))";
225  }
226  j++;
227  }
228 
229  //print out the equation normalizations
230  j = d_pn_form.begin(), jend = d_pn_form.end();
231  while(j !=jend){
232  cout << "(poly_norm_" << kind_to_str( (*j).first.getKind() ) << " _ _ _ @pnt";
233  //mapped to the polynomial norm proof
234  cout << (*j).second << " ";
235  //print out the same number as the equation in M
236  cout << "(\\ @pn" << abs( queryM( (*j).first ) ) << endl;
237  cparen << "))";
238  j++;
239  }
240 
241  //(AJR-5) print the proof and closing parentheses.
242  if( lfsc_mode%10==7 ){
243  LFSCProof::indentFlag = true;
244  lambda_pf->print_structure( cout );
245  }else
246  lambda_pf->print( cout );
247  cout << endl;
248 
249 
250  //print closing parentheses
251  cout << cparen.str() << endl;
252 }
253 
254 
255 void LFSCPrinter::print_poly_norm(const Expr& expr, std::ostream& s, bool pnRat, bool ratNeg ){
256  // if +, -, etc.
257  if(expr.arity()==2 ){
258  if( expr.getKind()==MULT ){
259  ostringstream cparen;
260  int nrIndex = -1; //the non-rational child
261  for( int a=0; a<2; a++ ){
262  if( nrIndex==-1 )
263  {
264  Expr ec = expr[a];
265  bool rNeg = ratNeg;
266  while( ec.getKind()==UMINUS ){
267  ec = ec[0];
268  if( !cvc3_mimic )
269  rNeg = !rNeg;
270  }
271  if( ec.isRational() || ec.getKind()==DIVIDE )
272  {
273  s<<"(pn_mul_";
274  if( cvc3_mimic && expr[a].getKind()==UMINUS ){
275  s << "u-_";
276  }
277  s<< "c_" << ( a==0 ? "L" : "R" );
278  s<<" _ _ _ ";
279  print_poly_norm( ec, s, false, rNeg );
280  s << " ";
281  nrIndex = (1-a);
282  cparen << ")";
283  }
284  }
285  }
286  if( nrIndex==-1 )
287  {
288  ostringstream ose;
289  ose << "ERROR: Multiplying by non-constant " << expr;
290  print_error( ose.str().c_str(), s );
291  }
292  else
293  {
294  print_poly_norm(expr[nrIndex],s);
295  }
296  s << cparen.str();
297  }
298  else if( expr.getKind()==DIVIDE )
299  {
300  //this should be 2 constants
301  if( expr[0].isRational() && expr[1].isRational() )
302  {
303  if( pnRat )
304  s<<"(pn_const ";
305  Rational r = expr[0].getRational();
306  print_rational_divide( ratNeg ? -r : r, expr[1].getRational(), s );
307  if( pnRat )
308  s << ")";
309  }
310  else
311  {
312  print_error("ERROR: Pn Dividing by non-constant", s );
313  }
314  }
315  else
316  {
317  //TODO: checks for appropriate op
318  //cout<<"e0 and e1"<<expr[0]<<" "<<expr[1]<<endl;
319  s<<"(pn_"<<kind_to_str(expr.getKind())<<" _ _ _ _ _ ";
320  print_poly_norm(expr[0],s);
321  s<<" ";
322  print_poly_norm(expr[1],s);
323  s<<")";
324  }
325  }else if(expr.getKind()==UMINUS ){
326  if( !cvc3_mimic )
327  print_poly_norm( expr[0], s, pnRat, !ratNeg );
328  else{
329  s << "(pn_u- _ _ _ ";
330  print_poly_norm( expr[0], s, pnRat, ratNeg );
331  s << ")";
332  }
333  }else if(expr.isRational()){
334  if( pnRat )
335  s<<"(pn_const ";
336  Rational r = expr.getRational();
337  print_rational( ratNeg ? -r : r, s );
338  if( pnRat )
339  s << ")";
340  }
341  else if( expr.getKind()==SKOLEM_VAR )
342  {
343  bool success = false;
344  if( skolem_vars.find( expr )!=skolem_vars.end() )
345  {
346  int val = d_terms[skolem_vars[expr]];
347  if( val!=0 ){
348  success = true;
349  s << "(pn_var_atom _ _ @at" << val << ")";
350  }
351  }
352  if( !success ){
353  ostringstream ose;
354  ose << "Trying to pn_var_atom a non-atomized skolem var " << expr;
355  print_error( ose.str().c_str(), cout );
356  }
357  }
358  else if( expr.getKind()==ITE ){
359  int val = d_terms[expr];
360  if( val!=0 ){
361  s << "(pn_var_atom _ _ @at" << val << ")";
362  }else{
363  ostringstream ose;
364  ose << "Trying to pn_var_atom a non-atomized ITE " << expr;
365  print_error( ose.str().c_str(), cout );
366  }
367  }else if(expr.isVar()){
368  s<<"(pn_var "<<expr<<")";
369  }
370  else{
371  ostringstream ose;
372  ose<<"ERROR printing polynomial norm for "<<expr;
373  print_error( ose.str().c_str(), s );
374  }
375 }
376 
377 // recursively prints arithm terms
378 void LFSCPrinter::print_terms_h( const Expr& expr,std::ostream& s ){
379  int val = d_print_map[expr];
380  if( val!=0 ){
381  s << "@x" << val;
382  }else if(expr.isRational()){
383  s<<"(a_real ";
384  print_rational( expr.getRational(), s );
385  s<<")";
386  }else if(expr.isVar()){
387  s<<"(a_var_real "<<expr<<")";
388  }else if(expr.arity()==2 ){
389  if( expr.getKind()==DIVIDE ){
390  if( expr[0].isRational() && expr[1].isRational() ){
391  s<<"(a_real ";
392  print_rational_divide( expr[0].getRational(), expr[1].getRational(), s );
393  s<<")";
394  }else{
395  print_error( "ERROR: Dividing by non constant", s );
396  }
397  }else{
398  //TODO: checks for appropriate op
399  s<<"("<<kind_to_str(expr.getKind())<<"_Real ";
400  print_terms_h(expr[0],s);
401  s<< " ";
402  print_terms_h(expr[1],s);
403  s<<")";
404  }
405  }else if( expr.getKind()==ITE ){
406  s << "(ite Real ";
407  print_formula_h( expr[0], s );
408  s << " ";
409  print_terms_h( expr[1], s );
410  s << " ";
411  print_terms_h( expr[2], s );
412  s << ")";
413  }else if( expr.getKind()==UMINUS ){
414  if( !cvc3_mimic ){
415  s<<"(a_real ";
416  if( expr[0].isRational() ){
417  Rational r = expr[0].getRational();
418  r = -r;
419  print_rational( r, s );
420  }else if( expr[0].getKind()==DIVIDE && expr[0][0].isRational() && expr[0][1].isRational() ){
421  print_rational_divide( -expr[0][0].getRational(), expr[0][1].getRational(), s );
422  }else{
423  cout << "cannot determine rational " << expr << endl;
424  }
425  s<<")";
426  }else{
427  s<<"(u-_Real ";
428  print_terms_h( expr[0], s );
429  s<<")";
430  }
431  }else if(expr.arity()>2){
432  //cout<<"term debug"<<expr<<" "<<expr.arity()<<endl;
433  vector<Expr> kids = expr.getKids();
434  vector<Expr>::iterator i = kids.begin(), iend= kids.end();
435  while(i+1!=iend){
436  s<<"("<<kind_to_str(expr.getKind())<<"_Real ";
437  print_terms_h(*i,s);
438  i++;
439  s << " ";
440  }
441  print_terms_h(*i,s);
442  for(int j=0; j<expr.arity();j++){
443  s<<")";
444 
445  }
446  }else{
447  ostringstream os;
448  os << "ERROR printing term "<<expr<<" "<<expr.arity();
449  print_error( os.str().c_str(), s );
450  }
451 }
452 
453 void LFSCPrinter::print_formula_h(const Expr& clause, std::ostream& s){
454  int val = d_print_map[clause];
455  if( val!=0 ){
456  s << "@f" << val;
457  }else if(clause.isNot()){
458  s<<"(not ";
459  print_formula_h(clause[0],s);
460  s<<")";
461  }else if(clause.isOr()){
462  s<<"(or ";
463  print_formula_h(clause[0],s);
464  s << " ";
465  print_formula_h(clause[1],s);
466  s<<")";
467  }else if(clause.isAnd()){
468  s<<"(and ";
469  print_formula_h(clause[0],s);
470  s << " ";
471  print_formula_h(clause[1],s);
472  s<<")";
473  }else if(clause.isImpl()){
474  s<<"(impl ";
475  print_formula_h(clause[0],s);
476  s << " ";
477  print_formula_h(clause[1],s);
478  s<<")";
479  }else if(clause.isIff()){
480  s<<"(iff ";
481  print_formula_h(clause[0],s);
482  s << " ";
483  print_formula_h(clause[1],s);
484  s<<")";
485  }else if(clause.getKind()==ITE){
486  s<<"(ifte ";
487  print_formula_h( clause[0], s );
488  s << " ";
489  print_formula_h( clause[1], s );
490  s << " ";
491  print_formula_h( clause[2], s );
492  s << ")";
493  }else if( is_eq_kind( clause.getKind() ) ){
494  int k = clause.getKind();
495  s<<"("<<kind_to_str(k);
496  s<<(is_smt_kind( k ) ? " " : "_" );
497  s<<"Real ";
498  print_terms_h(clause[0],s);
499  s << " ";
500  print_terms_h(clause[1],s);
501  s<<")";
502  }else if( clause.isFalse() ){
503  s << "false";
504  }else if( clause.isTrue() ){
505  s << "true";
506  }else{
507  s << clause;
508  }
509 }
510 
512  if( e.arity()<=1 || d_print_visited_map.find( e )==d_print_visited_map.end() ){
513  for( int a=0; a<(int)e.arity(); a++ ){
514  make_let_map( e[a] );
515  }
516  if( e.arity()>1 ){
517  if( d_print_map[e]==0 ){
518  d_print_map[e] = let_i;
519  let_i++;
520  }
521  d_print_visited_map[e] = true;
522  }
523  }
524 }
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
void print_structure(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:43
void print_formula(const Expr &clause, std::ostream &s)
Definition: LFSCPrinter.h:42
static ExprMap< bool > d_formulas_printed
Definition: LFSCObject.h:62
void print_rational(const Rational &r, std::ostream &s)
Definition: Util.cpp:136
void print_terms(const Expr &expr, std::ostream &s)
Definition: LFSCPrinter.h:48
Data structure of expressions in CVC3.
Definition: expr.h:133
static std::map< int, bool > pntNeeded
Definition: LFSCObject.h:60
static void define_skolem_vars(const Expr &e)
Definition: LFSCObject.cpp:308
static Expr cascade_expr(const Expr &e)
Definition: LFSCObject.cpp:281
bool isTrue() const
Definition: expr.h:356
bool isRational() const
Definition: expr.h:431
bool isImpl() const
Definition: expr.h:425
static ExprMap< bool > d_assump_map
Definition: LFSCObject.h:66
bool is_smt_kind(int knd)
Definition: Util.cpp:60
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
iterator find(const Expr &e)
Definition: expr_map.h:194
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
Definition: LFSCObject.cpp:386
RefPtr< LFSCConvert > converter
Definition: LFSCPrinter.h:12
bool isFalse() const
Definition: expr.h:355
static void initialize()
Definition: Object.h:111
static bool cvc3_mimic
Definition: LFSCObject.h:26
iterator begin()
Definition: expr_map.h:190
Definition: kinds.h:66
static int lfsc_mode
Definition: LFSCObject.h:23
void print_LFSC(const Expr &pf_expr)
Definition: LFSCPrinter.cpp:26
bool isOr() const
Definition: expr.h:422
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
static LFSCPrinter * printer
Definition: LFSCObject.h:16
bool is_eq_kind(int knd)
Definition: Util.cpp:47
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
Definition: theory_arith.h:177
static void print_error(const char *c, std::ostream &s)
Definition: Object.h:95
bool isNot() const
Definition: expr.h:420
void make_let_map(const Expr &e)
static void collect_vars(const Expr &e, bool readPred=true)
Definition: LFSCObject.cpp:342
bool empty() const
Definition: expr_map.h:170
void print_poly_norm(const Expr &expr, std::ostream &s, bool pnRat=true, bool ratNeg=false)
static ExprMap< int > d_terms
Definition: LFSCObject.h:54
int getKind() const
Definition: expr.h:1168
static ExprMap< int > d_formulas
Definition: LFSCObject.h:46
T abs(T t)
Definition: cvc_util.h:53
static ExprMap< int > d_pn
Definition: LFSCObject.h:50
void convert(const Expr &pf)
Definition: LFSCConvert.cpp:18
string kind_to_str(int knd)
Definition: Util.cpp:17
void print(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:23
static bool isFormula(const Expr &e)
Definition: LFSCObject.cpp:514
std::vector< Expr > d_user_assumptions
Definition: LFSCPrinter.h:10
bool isVar() const
Definition: expr.h:1005
static ExprMap< bool > input_vars
Definition: LFSCObject.h:56
LFSCPrinter(const Expr pf_expr, Expr qExpr, std::vector< Expr > assumps, int lfscm, CommonProofRules *commonRules)
Definition: LFSCPrinter.cpp:4
static ExprMap< bool > input_preds
Definition: LFSCObject.h:58
Definition: kinds.h:81
static ExprMap< int > d_trusted
Definition: LFSCObject.h:48
ExprMap< bool > d_print_visited_map
Definition: LFSCPrinter.h:19
static ExprMap< Expr > skolem_vars
Definition: LFSCObject.h:37
ExprMap< int > d_print_map
Definition: LFSCPrinter.h:18
static bool indentFlag
Definition: Object.h:71
void print_rational_divide(const Rational &n, const Rational &d, std::ostream &s)
Definition: Util.cpp:149
LFSCProof * getLFSCProof()
Definition: LFSCConvert.h:51
iterator end()
Definition: expr_map.h:191
void print_terms_h(const Expr &expr, std::ostream &s)
static ExprMap< int > d_pn_form
Definition: LFSCObject.h:52
void print_formula_h(const Expr &clause, std::ostream &s)
bool isAnd() const
Definition: expr.h:421