1 #include "LFSCConvert.h"
2
3 #include "LFSCUtilProof.h"
4 #include "LFSCBoolProof.h"
5 #include "LFSCLraProof.h"
6
7 std::map< Expr, int > vMap;
8
LFSCConvert(int lfscm)9 LFSCConvert::LFSCConvert( int lfscm )
10 {
11 nodeCount = 0;
12 nodeCountTh = 0;
13 unodeCount = 0;
14 unodeCountTh = 0;
15 ignore_theory_lemmas = lfsc_mode==22;
16 }
17
convert(const Expr & pf)18 void LFSCConvert::convert( const Expr& pf )
19 {
20 TReturn* tfinal = cvc3_to_lfsc( pf, false, false );
21 pfinal = tfinal->getLFSCProof();
22
23 //print out sat_lem if we are in clausal form
24 if( tfinal->getProvesY()==3 ){
25 ostringstream os1, os2;
26 os1 << "(satlem _ _ _ ";
27 os2 << "(\\ @done @done))" << endl;
28 pfinal = LFSCProofGeneric::Make( os1.str(), pfinal.get(), os2.str() );
29 }
30
31 //print out all necessary proof let's
32 pfinal = make_let_proof( pfinal.get() );
33
34 //double ratio = (double)( nodeCountTh )/double( nodeCount + nodeCountTh );
35 //cout << "Theory Node ratio : " << ratio << endl;
36 //cout << "Node Count : " << nodeCount << endl;
37 //cout << "Th Node Count : " << nodeCountTh << endl;
38 //cout << "Total Count : " << ( nodeCount + nodeCountTh ) << endl;
39 //cout << (double)( nodeCountTh )/double( nodeCount + nodeCountTh ) << endl;
40 //cout << "uNode Count : " << unodeCount << endl;
41 //cout << "Th uNode Count : " << unodeCountTh << endl;
42 //cout << "LFSC proof count: " << LFSCProof::get_proof_counter() << endl;
43 //cout << "getNumNodes : " << getNumNodes( pf, false ) << endl;
44 //nnode_map.clear();
45 //cout << "getNumNodes(rc) : " << getNumNodes( pf, true ) << endl;
46 //cout << "map size 1 : " << (int)d_th_trans_map[1].size() << endl;
47 //cout << "map size 2 : " << (int)d_th_trans_map[0].size() << endl;
48 //std::map< Expr, int >::iterator vmIt = vMap.begin();
49 //while( vmIt != vMap.end() ){
50 // cout << (*vmIt).first << ": " << (*vmIt).second << endl;
51 // ++vmIt;
52 //}
53 //exit( 0 );
54 }
55
56 // helper method to identify axioms of the form |- 0 = 0
isTrivialTheoryAxiom(const Expr & expr,bool checkBody)57 bool LFSCConvert::isTrivialTheoryAxiom(const Expr& expr, bool checkBody){
58 if( expr[0]==d_plus_predicate_str || expr[0]==d_right_minus_left_str ||
59 expr[0]==d_minus_to_plus_str || expr[0]==d_mult_ineqn_str ||
60 expr[0]==d_canon_mult_str || expr[0]==d_canon_plus_str ||
61 expr[0]==d_flip_inequality_str || expr[0]==d_negated_inequality_str ||
62 expr[0]==d_rewrite_eq_symm_str || expr[0]==d_refl_str ||
63 expr[0]==d_mult_eqn_str || expr[0]==d_canon_invert_divide_str ||
64 expr[0]==d_rewrite_eq_refl_str || expr[0]==d_uminus_to_mult_str ||
65 expr[0]==d_rewrite_not_true_str || expr[0]==d_rewrite_not_false_str ||
66 expr[0]==d_int_const_eq_str ){
67 Expr pe;
68 Expr yexpr;
69 if( !checkBody || ( what_is_proven( expr, pe ) && getY( pe, yexpr ) ) ){
70 return true;
71 }else{
72 //cout << "Trivial theory axiom with bad arguments : " << expr[0] << std::endl;
73 }
74 }
75 return false;
76 //FIXME: should rewrite_not_true be used in theory lemma? expr==d_rewrite_not_true_str
77 }
78
isTrivialBooleanAxiom(const Expr & expr)79 bool LFSCConvert::isTrivialBooleanAxiom(const Expr& expr)
80 {
81 return ( expr==d_rewrite_not_not_str );
82 }
83
84
85 // *****NOTE that these rules must have a subproof expr[2]
isIgnoredRule(const Expr & expr)86 bool LFSCConvert::isIgnoredRule(const Expr& expr)
87 {
88 return ( expr==d_iff_not_false_str || expr==d_iff_true_str ||
89 expr==d_iff_false_elim_str || expr==d_iff_true_elim_str ||
90 expr==d_not_not_elim_str || expr==d_not_to_iff_str );
91 }
92
cvc3_to_lfsc(const Expr & pf,bool beneath_lc,bool rev_pol)93 TReturn* LFSCConvert::cvc3_to_lfsc(const Expr& pf, bool beneath_lc, bool rev_pol){
94 if( beneath_lc )
95 nodeCountTh++;
96 else
97 nodeCount++;
98 if( lfsc_mode==5){
99 cvc3_mimic = cvc3_mimic_input || !beneath_lc;
100 }
101 int cvcm = cvc3_mimic ? 1 : 0;
102 TReturn* tRetVal = NULL;
103 //if( !tRetVal && cvcm==0 ){
104 // tRetVal = d_th_trans_map[1][pf];
105 //}
106 if( d_th_trans_map[cvcm].find( pf )!=d_th_trans_map[cvcm].end() ){
107 tRetVal = d_th_trans_map[cvcm][pf];
108 if( d_th_trans_lam[cvcm].find( tRetVal )==d_th_trans_lam[cvcm].end() ){
109 if( debug_conv )
110 cout << "set th_trans" << std::endl;
111 //set this TReturn to be lambda'ed into a let proof
112 d_th_trans_lam[cvcm][tRetVal] = true;
113 }
114 return tRetVal;
115 }
116
117 if( beneath_lc )
118 unodeCountTh++;
119 else
120 unodeCount++;
121
122 //if( (unodeCountTh + unodeCount)%10000==0 )
123 // cout << unodeCount << " " << unodeCountTh << endl;
124 //if( pf.isSelected() )
125 // std::cout << "already did this one?" << std::endl;
126
127 if( vMap.find( pf[0] )==vMap.end() ){
128 vMap[ pf[0] ] = 0;
129 }
130 vMap[ pf[0] ]++;
131
132
133 std::vector< int > emptyL;
134 std::vector< int > emptyLUsed;
135 int yMode = -2;
136 ostringstream ose;
137 if( debug_conv ){
138 cout << "handle ";
139 pf[0].print();
140 }
141 Expr pfMod;
142 int pfPat = get_proof_pattern( pf, pfMod );
143 if( pfPat==0 )
144 {
145 if (pf[0] == d_CNF_str ){
146 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[2], pf[1], pf[4].getRational().getNumerator().getInt() );
147 if( p.get() )
148 {
149 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
150 }
151 }
152 else if( pf[0] == d_CNFITE_str ){
153 if( pf[5].isRational() ){
154 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[1], d_ite_s, pf[5].getRational().getNumerator().getInt() );
155 if( p.get() ){
156 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
157 }
158 }
159 }else if( pf[0] == d_cnf_add_unit_str ){
160 TReturn* t = cvc3_to_lfsc( pf[2] );
161 yMode = TReturn::normalize_tr( pf[2], t, 3 );
162 if( yMode==3 ){
163 tRetVal = t;
164 }
165 }
166 else if( pf[0] == d_cnf_convert_str ){
167 if( pf.arity()>3 ){
168 if( ignore_theory_lemmas && pf[3][0]==d_learned_clause_str ){
169 TReturn* t = make_trusted( pf );
170 tRetVal = new TReturn( LFSCClausify::Make( pf[1], t->getLFSCProof(), true ), emptyL, emptyLUsed, nullRat, false, 3 );
171 }else{
172 TReturn* t = cvc3_to_lfsc( pf[3],beneath_lc, rev_pol);
173 if( TReturn::normalize_tr( pf[3], t, 3, rev_pol )==3 ){
174 RefPtr< LFSCProof > p = t->getLFSCProof();
175 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
176 }
177 }
178 }
179 }
180 else if( pf[0] == d_bool_res_str ){
181 //ajr_debug_print( pf );
182 TReturn* t1 = cvc3_to_lfsc( pf[2],beneath_lc, rev_pol);
183 TReturn* t2 = cvc3_to_lfsc( pf[3],beneath_lc, rev_pol);
184 //t1->getL( emptyL, emptyLUsed );
185 //t2->getL( emptyL, emptyLUsed );
186 TReturn::normalize_tr( pf[2], t1, 3, rev_pol );
187 TReturn::normalize_tr( pf[3], t2, 3, rev_pol );
188 if( t1->getProvesY()==3 && t2->getProvesY()==3 ){
189 tRetVal = new TReturn( LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[1], pf ),
190 emptyL, emptyLUsed, nullRat, false, 3 );
191 }
192 }
193 else if( pf[0] == d_minisat_proof_str ){
194 tRetVal = cvc3_to_lfsc( pf[2] );
195 }
196 else if(pf[0]==d_assump_str){ //assumptions rule
197 Expr ce = cascade_expr( pf[1] );
198 int val = queryM( ce );
199 RefPtr< LFSCProof > p;
200 yMode = 0;
201 if( d_assump_map.find( ce ) != d_assump_map.end() ){
202 //cout << "This is an assumption: " << pf[1] << std::endl;
203 p = LFSCPfVar::Make( "@F", abs( val ) );
204 if( !cvc3_mimic ){
205 #ifndef LRA2_PRIME
206 p = LFSCProof::Make_not_not_elim( pf[1], p.get() );
207 #endif
208 }
209 }else if( beneath_lc ){
210 p = LFSCPfVar::MakeV( abs( val ) );
211 if( cvc3_mimic ){
212 //ostringstream os1, os2;
213 //os1 << "(spec ";
214 //RefPtr< LFSCProof > ps = LFSCProofExpr::Make( pf[1] );
215 //os2 << ")";
216 //p = LFSCProofGeneric::Make( os1.str(), p.get(), ps.get(), os2.str() );
217 d_formulas_printed[queryAtomic( ce, true )] = true;
218 }
219 #ifdef OPTIMIZE
220 p->assumeVarUsed = val;
221 #else
222 emptyLUsed.push_back( val );
223 #endif
224 }else{
225 ostringstream os;
226 os << "WARNING: Assuming a trusted formula: " << ce << std::endl;
227 print_error( os.str().c_str(), cout );
228 int valT = queryM( ce, true, true );
229 p = LFSCPfVar::Make( "@T", abs( valT ) );
230 }
231 if( beneath_lc ){
232 #ifdef OPTIMIZE
233 p->assumeVar = val;
234 #else
235 emptyL.push_back( val );
236 #endif
237 if( !cvc3_mimic ){
238 Expr ey;
239 if( getY( ce, ey ) ){
240 p = LFSCLraPoly::Make( ce, p.get() );
241 yMode = 1;
242 }else{
243 ostringstream os;
244 os << "WARNING: Beneath a learned clause and Y is not defined for assumption " << pf[1] << std::endl;
245 print_error( os.str().c_str(), cout );
246 }
247 }
248 }
249 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, yMode );
250 }
251 else if( pf[0] == d_iff_trans_str ){
252 TReturn* t1 = cvc3_to_lfsc(pf[4],beneath_lc, rev_pol);
253 #ifdef LRA2_PRIME
254 if( ( isTrivialBooleanAxiom( pf[5][0] ) || pf[5][0]==d_rewrite_not_true_str ) && !cvc3_mimic && t1->getProvesY()==1 ){
255 #else
256 if( ( isTrivialBooleanAxiom( pf[5][0] ) || pf[5][0]==d_rewrite_not_true_str ) && !cvc3_mimic ){
257 #endif
258 tRetVal = t1;
259 }else{
260 TReturn* t2 = cvc3_to_lfsc(pf[5],beneath_lc, rev_pol);
261 t1->getL( emptyL, emptyLUsed );
262 t2->getL( emptyL, emptyLUsed );
263 yMode = TReturn::normalize_tret( pf[4], t1, pf[5], t2, rev_pol );
264 //case for arithmetic simplification
265 if( yMode==1 )
266 {
267 int knd2 = queryAtomic( pf[2] ).getKind();
268 int knd3 = queryAtomic( pf[3] ).getKind();
269 //if we have an equation on the RHS
270 if( is_eq_kind( knd3 ) )
271 {
272 RefPtr< LFSCProof > lfsc_pf = t1->getLFSCProof();
273 if( t2->hasRational() )
274 lfsc_pf = LFSCLraMulC::Make(t1->getLFSCProof(), t2->getRational(), EQ);
275 LFSCLraAdd::Make( lfsc_pf.get(), t2->getLFSCProof(), EQ, EQ);
276
277 Rational newR = t1->mult_rational( t2 );
278 tRetVal = new TReturn(lfsc_pf.get(), emptyL, emptyLUsed, t1->mult_rational( t2 ), t1->hasRational() || t2->hasRational(),1);
279 }
280 else if( knd3==FALSE_EXPR || knd3==TRUE_EXPR )
281 {
282 #ifdef PRINT_MAJOR_METHODS
283 cout << ";[M]: iff_trans, logical " << (knd3==TRUE_EXPR) << std::endl;
284 #endif
285 RefPtr< LFSCProof > p;
286 if ( knd3==TRUE_EXPR ){
287 p = LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ );
288 }else{
289 p = LFSCLraSub::Make( t2->getLFSCProof(), t1->getLFSCProof(), is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ, EQ );
290 }
291 if( t1->hasRational() ){
292 Rational r = 1/t1->getRational();
293 p = LFSCLraMulC::Make( p.get(), r, is_eq_kind( knd2 ) ? get_normalized( knd2, true ) : EQ );
294 }
295 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
296 }
297 }else if( yMode == 3 ){
298 //#ifdef PRINT_MAJOR_METHODS
299 // cout << ";[M]: iff_trans, boolean " << std::endl;
300 //#endif
301 // //resolving on the middle formula
302 // RefPtr< LFSCProof > p;
303 // if( rev_pol ){
304 // p = LFSCBoolRes::Make( t2->getLFSCProof(), t1->getLFSCProof(), pf[2], pf );
305 // }else{
306 // p = LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[2], pf );
307 // }
308 //tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, 1, 1, 3 );
309 }else if( yMode == 0 || yMode==2 ){
310 ostringstream os1;
311 os1 << "(" << (yMode==0 ? "iff" : "impl" ) << "_trans _ _ _ ";
312 //if( yMode==2 && t1->getLFSCProof()->get_string_length()<100 ){
313 // os1 << "[";
314 // t1->getLFSCProof()->print( os1, 0 );
315 // os1 << "]";
316 //}
317 ostringstream os2;
318 os2 << ")";
319
320 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
321 emptyL, emptyLUsed, nullRat, false, yMode );
322 }
323 }
324 }
325 else if (pf[0] == d_iff_mp_str ){ //iff_mp rule
326 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
327 #ifdef LRA2_PRIME
328 if( isTrivialBooleanAxiom( pf[4][0] ) && !cvc3_mimic && t1->getProvesY()==1 ){
329 #else
330 if( isTrivialBooleanAxiom( pf[4][0] ) && !cvc3_mimic ){
331 #endif
332 tRetVal = t1;
333 }else{
334 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
335 t1->getL( emptyL, emptyLUsed );
336 t2->getL( emptyL, emptyLUsed );
337 if( t1->getProvesY()==1 && t2->getProvesY()==1 )
338 {
339 yMode = 1;
340 int knd = queryAtomic( pf[1] ).getKind();
341 int knd2 = queryAtomic( pf[2] ).getKind();
342 if( is_eq_kind( knd2 ) )
343 {
344 RefPtr< LFSCProof > p = t1->getLFSCProof();
345 if( t2->hasRational() )
346 p = LFSCLraMulC::Make(p.get(), t2->getRational(), get_normalized( knd ));
347 p = LFSCLraSub::Make( p.get(), t2->getLFSCProof(), get_normalized( knd ), EQ);
348 tRetVal = new TReturn(p.get(), emptyL, emptyLUsed, t2->getRational(), t2->hasRational() , 1);
349 }else if( knd2==FALSE_EXPR ){ //false case
350 #ifdef PRINT_MAJOR_METHODS
351 //cout << ";[M]: iff_mp, false" << std::endl;
352 #endif
353 //becomes a contradiction
354 RefPtr< LFSCProof > p = t1->getLFSCProof();
355 p = LFSCLraAdd::Make( p.get(), t2->getLFSCProof(),
356 get_normalized( knd ),
357 get_normalized( knd, true ) );
358 p = LFSCLraContra::Make( p.get(), is_comparison( knd ) ? (int)GT : (int)DISTINCT );
359 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
360 }
361 }else if( t2->getProvesY()==3 || t1->getProvesY()==3 ){
362 // yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
363 // if( yMode==3 ){
364 //#ifdef PRINT_MAJOR_METHODS
365 // cout << ";[M]: iff_mp, boolean" << std::endl;
366 //#endif
367 // //do boolean resolution
368 // tRetVal = new TReturn( LFSCBoolRes::Make( t1->getLFSCProof(), t2->getLFSCProof(), pf[1], pf ),
369 // emptyL, emptyLUsed, nullRat, false, 3 );
370 // }
371 }else{
372 if( t2->getProvesY()!=1 || TReturn::normalize_tr( pf[4], t2, 2, rev_pol )!=-1 ){
373 if( t1->getProvesY()!=1 || TReturn::normalize_tr( pf[3], t1, 2, rev_pol )!=-1 ){
374 ostringstream os1;
375 os1 << "(" << (t2->getProvesY()==0 ? "iff" : "impl" ) << "_mp _ _ ";
376 ostringstream os2;
377 os2 << ")";
378 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
379 }
380 }
381 }
382 }
383 }
384 else if(pf[0]==d_iff_symm_str )
385 {
386 TReturn* t = cvc3_to_lfsc( pf[3], beneath_lc, !rev_pol );
387 yMode = t->getProvesY();
388 t->getL( emptyL, emptyLUsed );
389 if( yMode==1 )
390 {
391 #ifdef PRINT_MAJOR_METHODS
392 cout << ";[M]: iff_symm" << std::endl;
393 #endif
394 if( t->hasRational() ){
395 Rational r = 1/t->getRational();
396 //adding this
397 Rational rNeg = -1/t->getRational();
398 RefPtr< LFSCProof > p = LFSCLraMulC::Make( t->getLFSCProof(), rNeg, EQ );
399 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, r, true, 1 );
400 }else{
401 Rational r = Rational( -1 );
402 RefPtr< LFSCProof > p = LFSCLraMulC::Make( t->getLFSCProof(), r, EQ );
403 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
404 }
405 }
406 else if( yMode==0 )
407 {
408 tRetVal = new TReturn( LFSCProof::Make_mimic( pf, t->getLFSCProof(), 2 ), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
409 }
410 }
411 else if(pf[0]==d_impl_mp_str){ // impl_mp rule
412 // get subproofs
413 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
414 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
415 t1->getL( emptyL, emptyLUsed );
416 t2->getL( emptyL, emptyLUsed );
417 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2);
418 if( yMode==1 ){
419 int knd1 = get_normalized( queryAtomic( pf[1] ).getKind() );
420 int knd2 = get_normalized( queryAtomic( pf[2] ).getKind() );
421 if( is_eq_kind( knd2 ) )
422 {
423 #ifdef PRINT_MAJOR_METHODS
424 cout << ";[M]: impl_mp" << std::endl;
425 #endif
426 RefPtr< LFSCProof > p1 = LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), knd1, knd2 );
427 // if non-homogenous case
428 if( knd1 == GT && knd2 == GE ){
429 ostringstream os1;
430 os1 <<"(>0_to_>=0_Real _";
431 ostringstream os2;
432 os2 <<")";
433 p1 = LFSCProofGeneric::Make(os1.str(), p1.get(), os2.str());
434 p1->setChOp( GE );
435 }
436 tRetVal = new TReturn(p1.get(), emptyL, emptyLUsed, nullRat, false, 1);
437 }else{
438 cout << "Kind = " << kind_to_str( knd2 ) << std::endl;
439 }
440 }
441 else
442 {
443 ostringstream os1, os2;
444 os1 << "(impl_mp _ _ ";
445 os2 << ")";
446 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0);
447 }
448 }
449 else if( pf[0]==d_basic_subst_op_str || pf[0]==d_basic_subst_op1_str )
450 {
451 if( pf.arity()==5 ){
452 // get subproofs
453 bool prevCvc3Mimic = cvc3_mimic;
454 #ifdef LRA2_PRIME
455 if( pf[1].getKind()==IFF || pf[1].getKind()==AND || pf[1].getKind()==OR && getNumNodes( pf )<=3 ){
456 #else
457 if( pf[1].getKind()==IFF ){
458 #endif
459 cvc3_mimic = true;
460 }
461 #ifdef PRINT_MAJOR_METHODS
462 cout << ";[M]: basic_subst_op1 " << kind_to_str( pf[1].getKind() ) << std::endl;
463 #endif
464 //cvc3_mimic = (( pe1.getKind()==AND || pe1.getKind()==OR ) && getNumNodes( pf1 )<5 ) ? true : prevCvc3Mimic;
465 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc, rev_pol);
466 //cvc3_mimic = (( pe1.getKind()==AND || pe1.getKind()==OR ) && getNumNodes( pf2 )<5 ) ? true : prevCvc3Mimic;
467 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc, rev_pol);
468 cvc3_mimic = prevCvc3Mimic;
469
470 tRetVal = do_bso( pf, beneath_lc, rev_pol, t1, t2, ose );
471 }
472 }
473 else if( pf[0]==d_basic_subst_op0_str ){
474 if( pf.arity()==4 ){
475 TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc, !rev_pol);
476 yMode = t->getProvesY();
477 t->getL( emptyL, emptyLUsed );
478 if( yMode==1 ){
479 if( pf[1].isNot() || pf[1].getKind()==UMINUS ){
480 if( !pf[2][0].isFalse() && !pf[2][0].isTrue() ){
481 RefPtr< LFSCProof > p = LFSCLraMulC::Make( t->getLFSCProof(), Rational( -1 ), EQ );
482 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 1 );
483 }else{
484 tRetVal = t;
485 }
486 }
487 }else if( yMode==3 ){
488 }else if( yMode==2 ){
489 if( pf[1].isNot() ) //rev_pol should have switched things already
490 tRetVal = t;
491 }else if( yMode==0 ){
492 ostringstream os1;
493 os1 << "(basic_subst_op0_" << kind_to_str( pf[1].getKind() ) << " _ _ ";
494 ostringstream os2;
495 os2 << ")";
496 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
497 }
498 }
499 if( !tRetVal ){
500 ose << "subst0 kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
501 ose << "subst0 arity = " << pf.arity() << std::endl;
502 }
503 }
504 else if( pf[0]==d_optimized_subst_op_str )
505 {
506 if( pf[1].getKind()==ITE ){
507 #ifdef PRINT_MAJOR_METHODS
508 cout << ";[M]: optimized_subst_op, ite " << std::endl;
509 #endif
510 //make reflexive proof of proven statement
511 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1] );
512
513 ostringstream os1, os2;
514 if( isFormula( pf[1] ) ){
515 os1 << "(iff_refl ";
516 }else{
517 os1 << "(refl Real ";
518 }
519 os2 << ")";
520 p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
521
522 bool success = true;
523 for( int a=3; a<pf.arity(); a++ ){
524 if( success ){
525 success = false;
526 Expr pe;
527 if( what_is_proven( pf[a], pe ) )
528 {
529 int type = -1;
530 for( int b=0; b<3; b++ ){
531 if( pe[0]==pf[1][b] )
532 type = b;
533 }
534 //set cvc3 mimic to true if we are proving an equivalence of the conditional formula
535 bool prev_cvc3_mimic = cvc3_mimic;
536 if( type==0 || isFormula( pf[1] ) )
537 cvc3_mimic = true;
538
539 TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
540
541 cvc3_mimic = prev_cvc3_mimic;
542
543 t->getL( emptyL, emptyLUsed );
544 if( TReturn::normalize_tr( pf[a], t, 0 )==0 ){
545 if( type!=-1 ){
546 ostringstream os1, os2;
547 os1 << "(optimized_subst_op_";
548 if( isFormula( pf[1] ) )
549 os1 << "ifte";
550 else
551 os1 << "ite";
552 if( type==1 )
553 os1 << "_t1";
554 else if( type==2 )
555 os1 << "_t2";
556 os1 << " _ _ _ _ _ _ _ ";
557 os2 << ")";
558 p = LFSCProofGeneric::Make( os1.str(), p.get(), t->getLFSCProof(), os2.str() );
559 success = true;
560 }
561 }
562 }
563 }
564 }
565 if( success ){
566 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 0 );
567 }
568 }else if( pf[1].getKind()==PLUS ){
569 //cout << ";[M]: optimized_subst_op, plus " << std::endl;
570 TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc);
571 yMode = t->getProvesY();
572 t->getL( emptyL, emptyLUsed );
573 if( t->getProvesY()==1 ){
574 tRetVal = t;
575 }else{
576 //tRetVal = make_trusted( pf );
577 Expr pe;
578 if( what_is_proven( pf[3], pe ) )
579 {
580 if( pe.getKind()==EQ )
581 {
582 ostringstream os1, os2;
583 os1 << "(canonize_conv _ _ _ _ _ _ ";
584 int pnt1 = queryMt( Expr( MINUS, pe[0], pe[1] ) );
585 int pnt2 = queryMt( Expr( MINUS, pf[1], pf[2] ) );
586 os1 << "@pnt" << pnt1 << " @pnt" << pnt2 << " ";
587 os2 << ")";
588 pntNeeded[ pnt1 ] = true;
589 pntNeeded[ pnt2 ] = true;
590 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ),
591 emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
592 }else{
593 cout << "proving kind " << kind_to_str( pe.getKind() ) << std::endl;
594 cout << pf[3][0] << " " << pe << std::endl;
595 }
596 }
597 }
598 }else{
599 //tRetVal = make_trusted( pf );
600 if( pf[1].arity()==pf.arity()-3 ){
601 #ifdef PRINT_MAJOR_METHODS
602 cout << ";[M]: optimized_subst_op, cascade " << kind_to_str( pf[1].getKind() ) << std::endl;
603 #endif
604 Expr pfn = pf[pf.arity()-1];
605 Expr cf1 = pf[1][pf.arity()-4];
606 Expr cf2 = pf[2][pf.arity()-4];
607 tRetVal = cvc3_to_lfsc( pf[pf.arity()-1], beneath_lc, rev_pol );
608 for( int a=(int)pf.arity()-2; a>=3; a-- ){
609 cf1 = Expr( pf[1].getKind(), pf[1][a-3], cf1 );
610 cf2 = Expr( pf[2].getKind(), pf[2][a-3], cf2 );
611 std::vector < Expr > exprs;
612 exprs.push_back( d_basic_subst_op1_str );
613 exprs.push_back( cf1 );
614 exprs.push_back( cf2 );
615 exprs.push_back( pf[a] );
616 exprs.push_back( pfn );
617 //cascade it, turn it into a different proof
618 pfn = Expr(PF_APPLY, exprs );
619 TReturn* tc = cvc3_to_lfsc( pf[a], beneath_lc, rev_pol );
620 tRetVal = do_bso( pfn, beneath_lc, rev_pol, tc, tRetVal, ose );
621 }
622 }else{
623 ose << "opt_subst_op arity pv1 = " << pf[1].arity() << " " << pf.arity()-3 << std::endl;
624 ose << "opt_subst_op arity pv2 = " << pf[2].arity() << " " << pf.arity()-3 << std::endl;
625 }
626 }
627 if( !tRetVal ){
628 for( int a=0; a<pf.arity(); a++ ){
629 if( a>=3 && pf[a].arity()>0 ){
630 ose << a << ": ";
631 ose << pf[a][0] << std::endl;
632 Expr pre;
633 what_is_proven( pf[a], pre );
634 ose << "wip: " << pre << std::endl;
635 }else{
636 ose << a << ": " << pf[a] << std::endl;
637 }
638 }
639 //RefPtr< LFSCProof > p;
640 //TReturn* curr = NULL;
641 //for( int a=(int)(pf.arity()-1); a>=4; a-- ){
642 // TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
643 // if( curr ){
644 // int cyMode = TReturn::normalize_tret(
645 // if( pf[1].getKind()==AND || pf[1].getKind()==OR ){
646 // ostringstream os1, os2;
647 // os1 << "(optimized_subst_op_";
648 // if( yMode==2 )
649 // os1 << "impl_";
650 // os1 << kind_to_str( pf[1].getKind() );
651 // os1 << " _ _ _ _ ";
652 // os2 << ")";
653 // p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
654 // }else{
655 // curr = t;
656 // }
657 // tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, t->getProvesY() );
658 //}
659 ose << "opt_subst_op kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
660 ose << "opt_subst_op arity = " << pf.arity() << std::endl;
661 }
662 }
663 else if( pf[0]==d_eq_trans_str ){
664 // get subproofs
665 TReturn* t1 = cvc3_to_lfsc(pf[5],beneath_lc);
666 TReturn* t2 = cvc3_to_lfsc(pf[6],beneath_lc);
667 t1->getL( emptyL, emptyLUsed );
668 t2->getL( emptyL, emptyLUsed );
669 yMode = TReturn::normalize_tret( pf[5], t1, pf[6], t2 );
670 if( yMode==1 ){
671 // merge literals
672 tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(),
673 EQ, EQ ), emptyL, emptyLUsed, nullRat, false, 1 );
674 }else if( yMode==0 ){
675 std::vector< RefPtr< LFSCProof > > pfs;
676 std::vector< string > strs;
677 ostringstream os1, os2, os3;
678 os1 << "(trans Real ";
679 os2 << " ";
680 os3 << ")";
681 pfs.push_back( LFSCProofExpr::Make( pf[2] ) );
682 pfs.push_back( LFSCProofExpr::Make( pf[3] ) );
683 pfs.push_back( LFSCProofExpr::Make( pf[4] ) );
684 pfs.push_back( t1->getLFSCProof() );
685 pfs.push_back( t2->getLFSCProof() );
686 strs.push_back( os1.str() );
687 strs.push_back( os2.str() );
688 strs.push_back( os2.str() );
689 strs.push_back( os2.str() );
690 strs.push_back( os2.str() );
691 strs.push_back( os3.str() );
692 tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 );
693 }
694 }
695 else if(pf[0] == d_eq_symm_str){ // eq_symm rule
696 TReturn* t = cvc3_to_lfsc(pf[4],beneath_lc);
697 t->getL( emptyL, emptyLUsed );
698 if( t->getProvesY()==1 )
699 {
700 tRetVal = new TReturn(LFSCLraMulC::Make(t->getLFSCProof(), Rational( -1 ), EQ), emptyL, emptyLUsed, nullRat, false, 1);
701 }
702 else if( t->getProvesY()==0 )
703 {
704 ostringstream os1, os2;
705 os1 << "(symm Real _ _ ";
706 os2 << ")";
707 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0);
708 }
709 }
710 else if( pf[0]==d_real_shadow_str )
711 {
712 // get subproofs
713 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
714 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
715 t1->getL( emptyL, emptyLUsed );
716 t2->getL( emptyL, emptyLUsed );
717 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
718 if( yMode==1 )
719 {
720 int op1 = get_normalized( queryAtomic( pf[1] ).getKind() );
721 int op2 = get_normalized( queryAtomic( pf[2] ).getKind() );
722 tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), op1, op2 ), emptyL, emptyLUsed, nullRat, false, 1 );
723 }
724 else if( yMode==0 )
725 {
726 ostringstream os1, os2;
727 os1 << "(real_shadow_" << kind_to_str( pf[1].getKind() );
728 os1 << "_" << kind_to_str( pf[2].getKind() );
729 os1 << " _ _ _ ";
730 os2 << ")";
731 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
732 emptyL, emptyLUsed, nullRat, false, 0 );
733 }
734 }
735 else if( pf[0]==d_addInequalities_str )
736 {
737 // get subproofs
738 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
739 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
740 t1->getL( emptyL, emptyLUsed );
741 t2->getL( emptyL, emptyLUsed );
742 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
743 if( yMode==1 )
744 {
745 tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(),
746 pf[1].getKind(), pf[2].getKind() ), emptyL, emptyLUsed, nullRat, false, 1 );
747 }
748 else if( yMode==0 )
749 {
750 ostringstream os1, os2;
751 os1 << "(add_inequalities_" << kind_to_str( pf[1].getKind() );
752 os1 << "_" << kind_to_str( pf[2].getKind() );
753 os1 << " _ _ _ _ ";
754 os2 << ")";
755 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
756 emptyL, emptyLUsed, nullRat, false, 0 );
757 }
758 }
759 else if( pf[0] == d_real_shadow_eq_str){
760 TReturn* t1 = cvc3_to_lfsc(pf[3], beneath_lc);
761 TReturn* t2 = cvc3_to_lfsc(pf[4], beneath_lc);
762 t1->getL( emptyL, emptyLUsed );
763 t2->getL( emptyL, emptyLUsed );
764 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2 );
765 if( yMode==1 ){
766 ostringstream os1, os2;
767 os1 << "(lra_>=_>=_to_= _ _ ";
768 os2 << ")";
769 RefPtr< LFSCProof > p = LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() );
770 p->setChOp( EQ );
771 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
772 }else if( yMode==0 || yMode==2 ){
773 ostringstream os1, os2;
774 os1 << "(real_shadow_eq _ _";
775 os2 << ")";
776 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ),
777 emptyL, emptyLUsed, nullRat, false, 0 );
778 }
779 }
780 else if( pf[0]==d_cycle_conflict_str )
781 {
782 // get subproofs
783 bool isErr = false;
784 int n = ( pf.arity() - 1 )/2 + 1;
785 std::vector < TReturn* > trets;
786 for( int a=n; a<pf.arity(); a++ ){
787 if( !isErr ){
788 TReturn* t = cvc3_to_lfsc(pf[a],beneath_lc);
789 if( TReturn::normalize_tr( pf[a], t, 1 )!=1 ){
790 isErr = true;
791 }else{
792 trets.push_back( t );
793 t->getL( emptyL, emptyLUsed );
794 }
795 }
796 }
797 //add them together
798 if( !isErr ){
799 int currOp = get_normalized( pf[1].getKind() );
800 RefPtr< LFSCProof > p1 = trets[0]->getLFSCProof();
801 for( int a=1; a<(int)trets.size(); a++ ){
802 int op = get_normalized( pf[a+1].getKind() );
803 p1 = LFSCLraAdd::Make( trets[a]->getLFSCProof(), p1.get(), op, currOp );
804 if( op==GT ){
805 currOp = GT;
806 }else if( op==GE ){
807 currOp = currOp==GT ? GT : GE;
808 }
809 }
810 tRetVal = new TReturn( LFSCLraContra::Make( p1.get(), GT ), emptyL, emptyLUsed, nullRat, false, 0 );
811 }
812 }
813 else if( pf[0]==d_learned_clause_str )
814 {
815 if( pf.arity()==2 )
816 {
817 TReturn* t = cvc3_to_lfsc(pf[1],true);
818 t->getL( emptyL, emptyLUsed );
819 RefPtr< LFSCProof > p = t->getLFSCProof();
820
821 Expr pe;
822 what_is_proven( pf[1], pe );
823 bool success = true;
824 if( !pe.isFalse() ){
825 success = false;
826 if( TReturn::normalize_tr( pf[1], t, 3, false )==3 )
827 {
828 p = t->getLFSCProof();
829 success = true;
830 }
831 #ifdef PRINT_MAJOR_METHODS
832 cout << ";[M]: learned clause, not proven false" << std::endl;
833 #endif
834 }
835 else if( cvc3_mimic && pf[1][0]!=d_cycle_conflict_str )
836 {
837 ostringstream os1, os2;
838 os1 << "(clausify_false ";
839 os2 << ")";
840 p = LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() );
841 }
842 if( success ){
843 //ostringstream os1, os2;
844 //if( debug_var )
845 // os1 << "LC:";
846 //we must close all proof-lets that contain free variables
847 //p = make_let_proof( p.get(), emptyL, false );
848 #ifdef OPTIMIZE
849 std::vector< int > assumes, assumesUsed;
850 t->calcL( assumes, assumesUsed );
851 for( int a=0; a<(int)assumes.size(); a++ ){
852 p = LFSCAssume::Make( assumes[a], p.get(), true );
853 }
854 #else
855 for( int a=0; a<(int)emptyL.size(); a++ ){
856 p = LFSCAssume::Make( emptyL[a], p.get(), true );
857 }
858 #endif
859 emptyL.clear();
860 emptyLUsed.clear();
861 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
862 }
863 }
864 }
865 else if( pf[0]==d_andE_str )
866 {
867 TReturn* t = cvc3_to_lfsc(pf[3],beneath_lc);
868 t->getL( emptyL, emptyLUsed );
869 if( t->getProvesY()==0 )
870 {
871 int pos = pf[1].getRational().getNumerator().getInt();
872 RefPtr< LFSCProof > p = LFSCProof::Make_and_elim( pf[2], t->getLFSCProof(), pos, pf[2][pos] );
873 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, t->getRational(), t->hasRational(), 0 );
874 }
875 else if( t->getProvesY()==3 )
876 {
877 //need to use and CNF rules
878 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[2], d_and_mid_s,
879 pf[1].getRational().getNumerator().getInt() );
880 p = LFSCBoolRes::Make( t->getLFSCProof(), p.get(), pf[2], pf );
881 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
882 }
883 }
884 else if( pf[0]==d_rewrite_implies_str )
885 {
886 if( !cvc3_mimic )
887 {
888 Expr ei = Expr( IMPLIES, pf[1], pf[2] );
889 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( ei, d_imp_s, 3 );
890 if( p.get() )
891 {
892 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 3 );
893 }
894 }
895 else
896 {
897 //tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "(rewrite_implies _ _)" ), emptyL, emptyLUsed, nullRat, false, 0 );
898 }
899 }
900 else if( pf[0]==d_rewrite_ite_same_str )
901 {
902 ostringstream os1, os2;
903 os1 << "(rewrite_ite_same ";
904 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2] );
905 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[3] );
906 os2 << ")";
907 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ),
908 emptyL, emptyLUsed, nullRat, false, 0 );
909 }
910 else if( pf[0]==d_rewrite_and_str || pf[0]==d_rewrite_or_str )
911 {
912 //Expr e = Expr( IFF, pf[1], pf[2] );
913 bool isAnd = pf[0]==d_rewrite_and_str;
914 if( pf[1].arity()==2 && pf[1][0]==pf[1][1] ){ //try to apply binary redundant rule
915 ostringstream os1, os2 ;
916 os1 << "(" << ( isAnd ? "and" : "or" ) << "_redundant ";
917 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1][0] );
918 os2 << ")";
919 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
920 }else if( isFlat( pf[2] ) ){ //try to do the normalize
921 Expr e1 = cascade_expr( pf[1] );
922 Expr e2 = cascade_expr( pf[2] );
923 Expr pe;
924 make_flatten_expr( e1, pe, pf[1].getKind() );
925 //cout << "we have an and normalize " << e1 << std::endl;
926 //cout << "making and normalize for " << pe << std::endl;
927 //cout << "this should be equal to " << e2 << std::endl;
928 //cout << (pe==e2) << std::endl;
929 if( pe==e2 ){ //standard and normalize
930 ostringstream os1, os2;
931 os1 << "(" << ( isAnd ? "and" : "or" ) << "_normalize _ ";
932 os2 << ")";
933 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1] );
934 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
935 }
936 //else if( pf[1].arity()==2 ){ //try to normalize the symm version
937 // Expr e1s = cascade_expr( Expr( pf[1].getKind(), pf[1][1], pf[1][0] ) );
938 // make_flatten_expr( e1s, pe, pf[1].getKind() );
939 // if( pe==e2 ){
940 // ostringstream oss1, oss2, oss3, oss4;
941 // oss1 << "(iff_trans _ _ (" << ( isAnd ? "and" : "or" );
942 // oss1 << "_symm ";
943 // RefPtr< LFSCProof > pex1 = LFSCProofExpr::Make( pf[1][0] );
944 // oss2 << " ";
945 // RefPtr< LFSCProof > pex2 = LFSCProofExpr::Make( pf[1][1] );
946 // oss3 << ") " << "(" << ( isAnd ? "and" : "or" ) << "_normalize _ ";
947 // RefPtr< LFSCProof > ps = LFSCProofExpr::Make( e1s );
948 // oss4 << "))";
949 // std::vector< RefPtr< LFSCProof > > pfs;
950 // pfs.push_back( pex1.get() );
951 // pfs.push_back( pex2.get() );
952 // pfs.push_back( ps.get() );
953 // std::vector< string > strs;
954 // strs.push_back( oss1.str() );
955 // strs.push_back( oss2.str() );
956 // strs.push_back( oss3.str() );
957 // strs.push_back( oss4.str() );
958 // tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, 0 );
959 // }
960 //}
961 }
962 if( !tRetVal ){
963 //going to have to trust it
964 TReturn* t = make_trusted( pf );
965 //this code runs the normalize side condition, but ignores it (for consistency with proof checking times)
966 ostringstream os1, os2;
967 os1 << "(" << (isAnd ? "and" : "or" ) << "_nd _ _ _ ";
968 os2 << ")";
969 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
970 }
971 }
972 else if( pf[0]==d_rewrite_iff_symm_str )
973 {
974 ostringstream os1, os2;
975 os1 << "(rewrite_iff_symm ";
976 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
977 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[2] );
978 os2 << ")";
979 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
980 }
981 else if( pf[0]== d_implyEqualities_str){
982
983 if( pf.arity()==5 ){
984 TReturn* t1 = cvc3_to_lfsc(pf[3],beneath_lc);
985 TReturn* t2 = cvc3_to_lfsc(pf[4],beneath_lc);
986 t1->getL( emptyL, emptyLUsed );
987 t2->getL( emptyL, emptyLUsed );
988 if( TReturn::normalize_tr( pf[3], t1, 0 )==0 && TReturn::normalize_tr( pf[4], t2, 0 )==0 )
989 {
990 Expr e1, e2;
991 if( what_is_proven( pf[3], e1 ) && what_is_proven( pf[4], e2 ) )
992 {
993 int m1 = queryMt( Expr( MINUS, e1[1], e1[0] ) );
994 int m2 = queryMt( Expr( MINUS, e2[1], e2[0] ) );
995
996 ostringstream os1, os2;
997 os1<<"(imply_equalities _ _ _ _ _ _ ";
998 os1 << "@pnt" << abs( m1 ) << " @pnt" << abs( m2 ) << " ";
999 os2 << ")";
1000 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t1->getLFSCProof(), t2->getLFSCProof(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1001 }
1002 }
1003 }
1004 }
1005 else if( pf[0]==d_implyWeakerInequality_str )
1006 {
1007 #ifdef PRINT_MAJOR_METHODS
1008 //cout << ";[M]: imply weaker equality " << pf[1] << std::endl;
1009 #endif
1010 if( !cvc3_mimic ){
1011 if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].isRational() && pf[2][1][0].isRational() )
1012 {
1013 //Rational r = pf[1][1][0].getRational() - pf[2][1][0].getRational();
1014 //tRetVal = new TReturn( LFSCLraAxiom::Make( r, GT ), emptyL, emptyLUsed, nullRat, false, 1 );
1015 tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1016 }
1017 }else{
1018 Rational r1, r2;
1019 ostringstream os1, os2;
1020 getRat(pf[1][1][0], r1);
1021 getRat(pf[2][1][0], r2);
1022 RefPtr <LFSCProof> p;
1023
1024 os1 <<"(imply_weaker_inequality_" << kind_to_str( pf[1].getKind() ) << "_" << kind_to_str( pf[2].getKind() );
1025 if(pf[1][1].arity() > 2)
1026 {
1027 vector<Expr> t1_children;
1028 int start_i = 1;
1029 int end_i = pf[1][1].arity();
1030 for(int i = start_i; i < end_i; i ++) {
1031 const Expr& term = pf[1][1][i];
1032 t1_children.push_back(term);
1033 }
1034 p = LFSCProofExpr::Make(Expr(pf[1][1].getKind(), t1_children));
1035 }
1036 else
1037 {
1038 p = LFSCProofExpr::Make(pf[1][1][1]);
1039 }
1040 os2<<" ";
1041 print_rational(r1, os2);
1042 os2 << " ";
1043 print_rational(r2, os2);
1044 os2<<")";
1045 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1046 emptyL, emptyLUsed, nullRat, false, 0 );
1047 }
1048 }
1049 else if( pf[0]==d_implyNegatedInequality_str )
1050 {
1051 #ifdef PRINT_MAJOR_METHODS
1052 //cout << ";[M]: imply negated equality " << pf[1] << std::endl;
1053 #endif
1054 if( !cvc3_mimic ){
1055 if( pf[1].arity()==2 && pf[2].arity()==2 && pf[1][1][0].isRational() && pf[2][1][0].isRational() )
1056 {
1057 //Rational r = -( pf[1][1][0].getRational() + pf[2][1][0].getRational() );
1058 //tRetVal = new TReturn( LFSCLraAxiom::Make( r, GT ), emptyL, emptyLUsed, nullRat, false, 1 );
1059 tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1060 }
1061 }else{
1062 Rational r1, r2;
1063 if( getRat( pf[1][1][0], r1 ) && getRat(pf[2][1][0], r2) ){
1064 Expr ep = pf[1][1][1];
1065 Rational negOne = Rational( -1 );
1066 bool isNeg = false;
1067 if ( pf[1][1][1].getKind()==MULT && pf[1][1][1][0].isRational() && pf[1][1][1][0].getRational()==negOne ){
1068 isNeg = true;
1069 if(pf[1][1].arity() > 2)
1070 {
1071 vector<Expr> t1_children;
1072 int start_i = 1;
1073 int end_i = pf[1][1].arity();
1074 for(int i = start_i; i < end_i; i ++) {
1075 const Expr& term = pf[1][1][i];
1076 t1_children.push_back(term);
1077 }
1078 ep = Expr(pf[1][1].getKind(), t1_children);
1079 }
1080 else
1081 {
1082 ep = pf[1][1][1][1];
1083 }
1084
1085 }
1086 if(r1 == r2) {
1087 ostringstream os1, os2;
1088 os1 << "(imply_negated_inequality_<" << (isNeg ? "n" : "" );
1089 os1 << " ";
1090 RefPtr< LFSCProof > p = LFSCProofExpr::Make( ep );
1091 os2 << " ";
1092 print_rational( r1, os2 );
1093 os2 << ")";
1094 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1095 emptyL, emptyLUsed, nullRat, false, 0 );
1096 }else{
1097 ostringstream os1, os2;
1098 os1 << "(imply_negated_inequality_";
1099 os1 << kind_to_str(pf[1].getKind()) << "_"<<kind_to_str(pf[2].getKind()) << (isNeg ? "n" : "" );
1100 os1 << " ";
1101 RefPtr< LFSCProof > p = LFSCProofExpr::Make( ep );
1102 os2 << " ";
1103 print_rational( r1, os2 );
1104 os2 << " ";
1105 print_rational( r2, os2 );
1106 os2 << ")";
1107 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ),
1108 emptyL, emptyLUsed, nullRat, false, 0 );
1109 }
1110 }
1111 }
1112 }
1113 else if( pf[0]==d_rewrite_iff_str){
1114 ostringstream os1, os2;
1115
1116 // then it's just the iff_refl rule
1117 if(pf[1] == pf[2]){
1118 os1 << "(iff_refl ";
1119 os2 << ")";
1120 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1] );
1121 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1122 nullRat, false, 0 );
1123 }
1124 if(pf[1] == d_pf_expr.getEM()->trueExpr()){
1125 os1 << "(rewrite_iff_true_l ";
1126 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2] );
1127 os2 << ")";
1128 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1129 }
1130 if(pf[1] == d_pf_expr.getEM()->falseExpr()){
1131 os1 << "(rewrite_iff_false_l ";
1132 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2] );
1133 os2 << ")";
1134 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1135 }
1136 if(pf[2] == d_pf_expr.getEM()->trueExpr()){
1137 os1 << "(rewrite_iff_true_r ";
1138 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
1139 os2 << ")";
1140 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1141 }
1142 if(pf[2] == d_pf_expr.getEM()->falseExpr()){
1143 os1 << "(rewrite_iff_false_r ";
1144 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
1145 os2 << ")";
1146 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1147 }
1148 if(pf[1].isNot() && pf[1][0] == pf[2]){
1149 os1 << "(rewrite_iff_not_l ";
1150 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1151
1152 os2 << ")";
1153 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1154 }
1155 if(pf[2].isNot() && pf[2][0] == pf[1]){
1156 os1 << "(rewrite_iff_not_r ";
1157 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2][0] );
1158 os2 << ")";
1159 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1160 }
1161 // just flips them
1162 if(pf[1] < pf[2]){
1163 os1 << "(rewrite_iff_symm ";
1164 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
1165 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[2] );
1166 os2 << ")";
1167 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1168 }
1169 if( !tRetVal ){
1170 os1 << "(iff_refl ";
1171 os2 << ")";
1172 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1].iffExpr(pf[2]) );
1173 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1174 nullRat, false, 0 );
1175 }
1176 }
1177 else if( isIgnoredRule( pf[0] ) )
1178 {
1179 TReturn* t = cvc3_to_lfsc(pf[2],beneath_lc);
1180 yMode = t->getProvesY();
1181 t->getL( emptyL, emptyLUsed );
1182 if( !cvc3_mimic )
1183 {
1184 if( yMode==1 ){
1185 tRetVal = t;
1186 }
1187 }
1188 else
1189 {
1190 if( yMode==0 || yMode==2 )
1191 {
1192 ostringstream os1, os2;
1193 os1 << "(" << pf[0] << (yMode==2 ? "_impl" : "" ) << " _ ";
1194 os2 << ")";
1195 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), t->getLFSCProof(), os2.str() ), emptyL, emptyLUsed,
1196 t->getRational(), t->hasRational(), 0 );
1197 }
1198 }
1199 }
1200 else if( isTrivialTheoryAxiom( pf ) )
1201 {
1202 //find the rational multiplier for the axiom
1203 Rational r;
1204 bool hasRat = false;
1205 if( pf[0]==d_mult_ineqn_str || pf[0]==d_mult_eqn_str || pf[0]==d_rewrite_eq_symm_str || pf[0]==d_int_const_eq_str ){
1206 if( pf[0]==d_mult_ineqn_str && pf[2].arity()==2 && pf[2][1].arity()==2 ){
1207 if( pf[2][1][1].isRational() ){
1208 r = pf[2][1][1].getRational();
1209 hasRat = true;
1210 }else if( pf[2][1][0].isRational() ){
1211 r = pf[2][1][0].getRational();
1212 hasRat = true;
1213 }
1214 }else if( pf[0]==d_mult_eqn_str && pf[3].isRational() ){
1215 r = pf[3].getRational();
1216 hasRat = true;
1217 }else if( pf[0]==d_rewrite_eq_symm_str ){
1218 r = -1;
1219 hasRat = true;
1220 }else if( pf[0]==d_int_const_eq_str ){
1221 if( pf[1].getKind()==EQ && !pf[2].isFalse() ){
1222 if( pf[1][1].getKind()==MULT && getRat( pf[1][1][0], r ) ){
1223 r = -r;
1224 }else if( pf[1][1].getKind()==PLUS && pf[1][1][1].getKind()==MULT && getRat( pf[1][1][1][0], r ) ){
1225 r = -r;
1226 }else{
1227 r = -1;
1228 }
1229 hasRat = true;
1230 }
1231 }
1232 if( !hasRat )
1233 {
1234 ose << pf[0] << ", Warning: Can't find rational multiplier " << std::endl;
1235 ose << pf[2] << std::endl;
1236 }
1237 }
1238 //handle the axiom - only do it if the term is polynomial normalizable
1239 if( !cvc3_mimic && isTrivialTheoryAxiom( pf, true ) )
1240 {
1241 //ignore it if cvc3_mimic is false
1242 if( hasRat && r<0 && pf[0]==d_mult_ineqn_str ){
1243 r = -r;
1244 }
1245 //if( debug_conv && !beneath_lc ){
1246 // cout << "WARNING: Trivial theory axiom used, not underneath learned clause: " << pf[0] << std::endl;
1247 //}
1248 tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, r, hasRat, 1 );
1249 }else{
1250 //int val = queryM( pf[1] );
1251 if( pf[0] == d_refl_str )
1252 {
1253 if( isFormula( pf[1] ) ){
1254 ostringstream os1, os2;
1255 os1 << "(iff_refl ";
1256 os2 << ")";
1257 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1] );
1258 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1259 nullRat, false, 0 );
1260 }else{
1261 ostringstream os1, os2;
1262 os1 << "(refl Real ";
1263 os2 << ")";
1264 RefPtr< LFSCProof > p = LFSCProofExpr::Make( pf[1] );
1265 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p.get(), os2.str() ), emptyL, emptyLUsed,
1266 nullRat, false, 0 );
1267 }
1268 }
1269 else if( pf[0] == d_flip_inequality_str )
1270 {
1271 ostringstream os1, os2;
1272 os1 << "(flip_inequality_" << kind_to_str( pf[1].getKind() );
1273 os1 << "_" << kind_to_str( pf[2].getKind() ) << " ";
1274 os2 << ")";
1275 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1276 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1277 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1278 nullRat, false, 0 );
1279 }
1280 else if( pf[0] == d_right_minus_left_str )
1281 {
1282 ostringstream os1, os2;
1283 os1 << "(right_minus_left_" << kind_to_str( pf[1].getKind() ) << " ";
1284 os2 << ")";
1285 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1286 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1287 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1288 nullRat, false, 0 );
1289 }
1290 else if( pf[0] == d_minus_to_plus_str )
1291 {
1292 ostringstream os1, os2;
1293 os1 << "(minus_to_plus ";
1294 os2 << ")";
1295 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
1296 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[2] );
1297 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1298 nullRat, false, 0 );
1299 }
1300 else if( pf[0] == d_plus_predicate_str )
1301 {
1302 ostringstream os1, os2;
1303 os1 << "(plus_predicate_" << kind_to_str( pf[1].getKind() ) << " ";
1304 std::vector< string > strs;
1305 std::vector< RefPtr< LFSCProof > > pfs;
1306 pfs.push_back( LFSCProofExpr::Make( pf[1][0] ) );
1307 pfs.push_back( LFSCProofExpr::Make( pf[1][1] ) );
1308 pfs.push_back( LFSCProofExpr::Make( pf[2][0][1] ) );
1309 os2 << ")";
1310 std::string spc( " " );
1311 strs.push_back( os1.str() );
1312 strs.push_back( spc );
1313 strs.push_back( spc );
1314 strs.push_back( os2.str() );
1315 tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed,
1316 nullRat, false, 0 );
1317 }
1318 else if( pf[0] == d_canon_plus_str || pf[0]==d_canon_mult_str )
1319 {
1320 int m = queryMt( Expr( MINUS, pf[1], pf[2] ) );
1321 ostringstream os;
1322 os << "(canonize_= _ _ _ ";
1323 os << "@pnt" << m << ")";
1324 pntNeeded[ m ] = true;
1325 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1326 nullRat, false, 0 );
1327 }
1328 else if( pf[0] == d_canon_invert_divide_str )
1329 {
1330 Rational r1 = Rational( 1 );
1331 Expr er1 = d_pf_expr.getEM()->newRatExpr( pf[1][0].getRational() );
1332 Expr er2 = d_pf_expr.getEM()->newRatExpr( r1/pf[1][1].getRational() );
1333 //cout << "we have made " << er1 << " " << er2 << std::endl;
1334 int m = queryMt( Expr( MINUS, pf[1], Expr( MULT, er1, er2 )) );
1335 ostringstream os;
1336 os << "(canonize_= _ _ _ ";
1337 os << "@pnt" << m << ")";
1338 pntNeeded[ m ] = true;
1339 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1340 nullRat, false, 0 );
1341 }
1342 else if( pf[0] == d_mult_ineqn_str && hasRat )
1343 {
1344 ostringstream os1, os2;
1345 os1 << "(mult_ineqn_" << (r<0 ? "neg_" : "");
1346 os1 << kind_to_str( pf[1].getKind() ) << " ";
1347 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0] );
1348 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][1] );
1349 os2 << " ";
1350 print_rational( r, os2 );
1351 os2 << ")";
1352 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1353 nullRat, false, 0 );
1354 }
1355 else if( pf[0] == d_mult_eqn_str && hasRat )
1356 {
1357 ostringstream os1, os2;
1358 os1 << "(mult_eqn ";
1359 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1] );
1360 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[2] );
1361 os2 << " ";
1362 print_rational( r, os2 );
1363 os2 << ")";
1364 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1365 nullRat, false, 0 );
1366 }
1367 else if( pf[0] == d_negated_inequality_str )
1368 {
1369 Expr e1 = queryAtomic( pf[1], true );
1370
1371 ostringstream os1, os2;
1372 os1 << "(negated_inequality_" << kind_to_str( e1.getKind() );
1373 os1 << "_" << kind_to_str( get_not( e1.getKind() ) ) << " ";
1374 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[1][0][0] );
1375 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[1][0][1] );
1376 os2 << ")";
1377 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1378 nullRat, false, 0 );
1379 }
1380 else if( pf[0] == d_rewrite_eq_symm_str )
1381 {
1382 ostringstream os1, os2;
1383 os1 << "(rewrite_eq_symm ";
1384 RefPtr< LFSCProof > p1 = LFSCProofExpr::Make( pf[2] );
1385 RefPtr< LFSCProof > p2 = LFSCProofExpr::Make( pf[3] );
1386 os2 << ")";
1387 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), p1.get(), p2.get(), os2.str() ), emptyL, emptyLUsed,
1388 nullRat, false, 0 );
1389 }
1390 else if( pf[0] == d_rewrite_eq_refl_str )
1391 {
1392 ostringstream os1, os2;
1393 os1 << "(rewrite_eq_refl ";
1394 os2 << ")";
1395 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), LFSCProofExpr::Make( pf[2] ), os2.str() ),
1396 emptyL, emptyLUsed, nullRat, false, 0 );
1397 }
1398 else if( pf[0] == d_uminus_to_mult_str )
1399 {
1400 if( pf[1].isRational() )
1401 {
1402 ostringstream os;
1403 os << "(uminus_to_mult ";
1404 print_rational( pf[1].getRational(), os );
1405 os << ")";
1406 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed,
1407 nullRat, false, 0 );
1408 }
1409 }
1410 else if( pf[0] == d_rewrite_not_true_str )
1411 {
1412 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_true" ), emptyL, emptyLUsed, nullRat, false, 0 );
1413 }
1414 else if( pf[0] == d_rewrite_not_false_str )
1415 {
1416 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( "rewrite_not_false" ), emptyL, emptyLUsed, nullRat, false, 0 );
1417 }
1418 else if( pf[0] == d_int_const_eq_str )
1419 {
1420 int m1 = queryMt( Expr( MINUS, pf[1][0], pf[1][1] ) );
1421 int m2 = queryMt( Expr( MINUS, pf[2][0], pf[2][1] ) );
1422 ostringstream os;
1423 os << "(canonize_iff _ _ _ _ _ _ @pnt" << m1 << " @pnt" << m2 << ")";
1424 pntNeeded[ m1 ] = true;
1425 pntNeeded[ m2 ] = true;
1426 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ), emptyL, emptyLUsed, nullRat, false, 0 );
1427 }
1428 }
1429 }
1430 else if( pf[0]==d_lessThan_To_LE_rhs_rwr_str )
1431 {
1432 //FIXME: this introduces weirdness into the logic of completeness of the proof conversion
1433 //why is integer reasoning used in CVC3 QF_LRA proofs?
1434 if( !cvc3_mimic )
1435 tRetVal = new TReturn( LFSCLraAxiom::MakeEq(), emptyL, emptyLUsed, nullRat, false, 1 );
1436 else{
1437 tRetVal = make_trusted( pf );
1438 }
1439 }
1440 else if( pf[0]==d_rewrite_not_not_str )
1441 {
1442 //note that "not not" is already taken care of FIXME
1443 #ifdef LRA2_PRIME
1444 tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1445 #else
1446 if( !cvc3_mimic ){
1447 tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(iff_refl _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1448 }else{
1449 tRetVal = new TReturn( LFSCProofGeneric::MakeStr("(rewrite_not_not _)"), emptyL, emptyLUsed, nullRat, false, 0 );
1450 }
1451 #endif
1452 }
1453 else if( isTrivialBooleanAxiom( pf[0] ) )
1454 {
1455 if( !cvc3_mimic ){
1456 tRetVal = new TReturn( LFSCLem::Make( queryM( pf[1] ) ), emptyL, emptyLUsed, nullRat, false, 3 );
1457 }else{
1458
1459 }
1460 }
1461 else if( pf[0]==d_const_predicate_str )
1462 {
1463 if( is_eq_kind( pf[1].getKind() ) )
1464 {
1465 Rational r1, r2;
1466 //int knd = pf[2].isFalse() ? get_not( pf[1].getKind() ) : pf[1].getKind();
1467 RefPtr< LFSCProof > p;
1468 if( getRat( pf[1][0], r1 ) && getRat( pf[1][1], r2 ) ){
1469 #ifdef PRINT_MAJOR_METHODS
1470 cout << ";[M]: const_pred " << kind_to_str( pf[1].getKind() );
1471 cout << " " << pf[2].isFalse();
1472 cout << ", rp=" << rev_pol << ", cvc=" << cvc3_mimic << std::endl;
1473 #endif
1474 if( !cvc3_mimic ){
1475 //if( rev_pol ){
1476 // ostringstream ose1;
1477 // ose1 << "Warning: Const predicate, rev pol true" << std::endl;
1478 // print_warning( ose1.str().c_str() );
1479 // knd = get_not( knd );
1480 //}
1481 if( pf[1].getKind()==EQ ){
1482 p = LFSCLraAxiom::MakeEq();
1483 }else{
1484 //Rational r = is_opposite( knd ) ? r2 - r1 : r1 - r2;
1485 //if( knd==GT )
1486 // r = Rational( 1, 1000000 );
1487 //if( knd==GE
1488 // r = Rational( 0 );
1489 //p = LFSCLraAxiom::Make( r, get_normalized( knd ) );
1490 p = LFSCLraAxiom::MakeEq();
1491 }
1492 if( p.get() ){
1493 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1494 }
1495 }
1496 else
1497 {
1498 ostringstream os;
1499 os << "(const_predicate_" << kind_to_str( pf[1].getKind() );
1500 if( pf[2].getKind()==TRUE_EXPR )
1501 os << "_t";
1502 os << " ";
1503 print_rational( r1, os );
1504 os << " ";
1505 print_rational( r2, os );
1506 os << ")";
1507 tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os.str().c_str() ),
1508 emptyL, emptyLUsed, nullRat, false, 0 );
1509 }
1510 }else{
1511 ose << "ERROR: Could not find rational for const predicate" << std::endl;
1512 }
1513 }
1514 if( !tRetVal )
1515 ose << "kind = " << kind_to_str( pf[1].getKind() );
1516 }
1517 }
1518 else
1519 {
1520 //use Expr pfMod
1521 //switch( pfPat )
1522 //{
1523 //}
1524 if( pfPat==1 )
1525 {
1526 ostringstream os1, os2, os3;
1527 os1 << "(ite_axiom ";
1528 os2 << " ";
1529 os3 << ")";
1530 std::vector< string > strs;
1531 std::vector< RefPtr< LFSCProof > > pfs;
1532
1533 strs.push_back( os1.str() );
1534 pfs.push_back( LFSCProofExpr::Make( pf[1][0] ) );
1535 strs.push_back( os2.str() );
1536 pfs.push_back( LFSCProofExpr::Make( pf[1][1][1] ) );
1537 strs.push_back( os2.str() );
1538 pfs.push_back( LFSCProofExpr::Make( pf[1][2][1] ) );
1539 strs.push_back( os3.str() );
1540 RefPtr< LFSCProof > p = LFSCProofGeneric::Make( pfs, strs );
1541
1542 tRetVal = new TReturn( LFSCClausify::Make( pf[1], p.get() ), emptyL, emptyLUsed,
1543 nullRat, false, 3 );
1544 }else{
1545 ostringstream ose;
1546 ose << "WARNING: Unknown proof pattern [" << pfPat << "]";
1547 print_error( ose.str().c_str(), cout );
1548 //ostringstream os1;
1549 //os1 << "PROOF_PAT_" << pfPat;
1550 //tRetVal = new TReturn( LFSCProofGeneric::MakeStr( os1.str().c_str() ), emptyL, emptyLUsed, nullRat, false, 3 );
1551 }
1552 }
1553 if( !tRetVal ){
1554 static bool firstTime = true;
1555 if(pf.arity()>0 && (yMode!=-1 || firstTime ) ){
1556 firstTime = false;
1557 ose << "Unknown proof rule (" << d_rules[pf[0]] << ") " << pf[0] << endl;
1558 ose << "YMode : ";
1559 if( yMode==-2 )
1560 ose << "unknown";
1561 else if( yMode==-1 )
1562 ose << "fail";
1563 else
1564 ose << yMode;
1565 ose << std::endl;
1566 if( rev_pol )
1567 ose << "rev_pol = true" << std::endl;
1568 if( pfPat!=0 )
1569 {
1570 ose << "proof pattern = " << pfPat << std::endl;
1571 }
1572 print_error( ose.str().c_str(), cout );
1573 }
1574 tRetVal = new TReturn( LFSCProofGeneric::MakeUnk(), emptyL, emptyLUsed, nullRat, false, -1 );
1575 }
1576
1577
1578 if( debug_conv ){
1579 //cout << "print length = " << tRetVal->getLFSCProof()->get_string_length() << std::endl;
1580 cout << "...done " << pf[0] << " " << tRetVal->getProvesY() << std::endl;
1581 }
1582 if( debug_var ){
1583 ostringstream os1, os2;
1584 os1 << "[" << pf[0];
1585 if( pf[0]==d_basic_subst_op1_str || pf[0]==d_optimized_subst_op_str || pf[0]==d_basic_subst_op0_str || pf[0]==d_const_predicate_str || pf[0]==d_basic_subst_op_str )
1586 os1 << "_" << kind_to_str( pf[1].getKind() );
1587 if( pf[0]==d_const_predicate_str )
1588 os1 << "_" << pf[2];
1589 os1 << " ";
1590 os2 << "]";
1591 std::vector< int > lv, lvUsed;
1592 tRetVal->getL( lv, lvUsed );
1593 tRetVal = new TReturn( LFSCProofGeneric::Make( os1.str(), tRetVal->getLFSCProof(), os2.str(), true ),
1594 lv, lvUsed, tRetVal->getRational(), tRetVal->hasRational(), tRetVal->getProvesY() );
1595 }
1596 //dont bother making small proofs into lambdas (length less than 30), or they are trivial
1597 if( !tRetVal->getLFSCProof()->isTrivial() && tRetVal->getLFSCProof()->get_string_length()>30 )
1598 {
1599 d_th_trans[pf] = true;
1600 //if( !d_th_trans_map[cvcm][pf] && pf.isSelected() ){
1601 // std::cout << "already selected" << std::endl;
1602 //}
1603 d_th_trans_map[cvcm][pf] = tRetVal;
1604 //pf.setSelected();
1605 }
1606 //else if( tRetVal->getLFSCProof()->get_string_length()<=30 && getNumNodes( pf )>10 ){
1607 // std::cout << "strange proof " << pf[0] << " " << getNumNodes( pf ) << std::endl;
1608 // tRetVal->getLFSCProof()->print( cout );
1609 // cout << endl;
1610 //}
1611 //if( cvc3_mimic && ( tRetVal->getProvesY()==1 || tRetVal->getProvesY()==2 ) ){
1612 // ostringstream ose;
1613 // ose << "Warning: After " << pf[0] << ", cvc_mimic, Ymode = " << tRetVal->getProvesY() << std::endl;
1614 // print_warning( ose.str().c_str() );
1615 //}
1616 //if( tRetVal->getProvesY()==1 ){
1617 // if( tRetVal->getLFSCProof()->checkOp()==-1 ){
1618 // ostringstream ose;
1619 // ose << "Error: After " << pf[0] << ", check op failed. " << tRetVal->getLFSCProof()->getNumChildren() << std::endl;
1620 // ose << pf << std::endl;
1621 // tRetVal->getLFSCProof()->print_pf( ose );
1622 // print_warning( ose.str().c_str() );
1623 // }
1624 //}
1625 //if( tRetVal->getProvesY()==1 ){
1626 // Expr pe;
1627 // Expr yexpr;
1628 // if( !what_is_proven( pf, pe ) || !getY( pe, yexpr ) ){
1629 // ostringstream ose;
1630 // ose << "Warning: Bad yMode 1 formula after " << pf[0] << std::endl;
1631 // if( pe.isInitialized() )
1632 // ose << pe << std::endl;
1633 // ose << pf << std::endl;
1634 // print_error( ose.str().c_str(), cout );
1635 // }
1636 //}
1637 return tRetVal;
1638 }
1639
1640 //look at the pattern of the proof, return relevant information in modE
1641 int LFSCConvert::get_proof_pattern( const Expr& pf, Expr& modE )
1642 {
1643 if( pf[0]==d_cnf_add_unit_str )
1644 {
1645 if( pf[2][0]==d_iff_mp_str )
1646 {
1647 if( pf[2][3][0]==d_eq_symm_str && pf[2][4][0]==d_if_lift_rule_str )
1648 {
1649 if( pf[2][3][4][0]==d_iff_mp_str )
1650 {
1651 if( pf[2][3][4][3][0]==d_var_intro_str &&
1652 pf[2][3][4][4][0]==d_assump_str )
1653 {
1654 return 1;
1655 }
1656 }
1657 }
1658 }
1659 }
1660 return 0;
1661 }
1662
1663 LFSCProof* LFSCConvert::make_let_proof( LFSCProof* p )
1664 {
1665 if( debug_conv )
1666 cout << "make let proof..." << std::endl;
1667 //std::map< TReturn*, bool >::iterator t_lbend = d_th_trans_lam.begin(), t_lb = d_th_trans_lam.end();
1668 //--t_lb;
1669 if( !d_th_trans.empty() ){
1670 //ExprMap< TReturn* >::iterator t_lb = d_th_trans.begin(), t_lbend = d_th_trans.end();
1671 ExprMap< bool >::iterator t_lbend = d_th_trans.begin(), t_lb = d_th_trans.end();
1672 --t_lb;
1673 while(t_lb != t_lbend){
1674 for( int cvcm=0; cvcm<2; cvcm++ ){
1675 if( d_th_trans_map[cvcm].find( (*t_lb).first )!= d_th_trans_map[cvcm].end() )
1676 {
1677 TReturn* t = d_th_trans_map[cvcm][(*t_lb).first];
1678 if( t ){
1679 std::vector< int > lv;
1680 std::vector< int > lvUsed;
1681 #ifdef OPTIMIZE
1682 t->calcL( lv, lvUsed );
1683 #else
1684 t->getL( lv, lvUsed );
1685 #endif
1686 if( d_th_trans_lam[cvcm][t] ){
1687 d_th_trans_lam[cvcm][t] = false;
1688 int lmt1 = LFSCProof::make_lambda( t->getLFSCProof() );
1689 RefPtr< LFSCProof > pfV = LFSCPfVar::Make( "@l", lmt1 );
1690 p = LFSCPfLet::Make( t->getLFSCProof(), (LFSCPfVar*)pfV.get(), p,
1691 t->getProvesY()!=3, lvUsed );
1692 }
1693 }
1694 }
1695 }
1696 --t_lb;
1697 //t_lb++;
1698 }
1699 }
1700 if( debug_conv )
1701 cout << "...done " << std::endl;
1702 return p;
1703 }
1704
1705 TReturn* LFSCConvert::make_trusted( const Expr& pf )
1706 {
1707 Expr e;
1708 std::vector< int > emptyL;
1709 std::vector< int > emptyLUsed;
1710 if( what_is_proven( pf, e ) ){
1711 int valT = queryM( e, true, true );
1712 return new TReturn( LFSCPfVar::Make( "@T", valT ), emptyL, emptyLUsed, nullRat, false, 0 );
1713 }else{
1714 return new TReturn( LFSCProofGeneric::MakeStr( "@T-unk" ), emptyL, emptyLUsed, nullRat, false, 0 );
1715 }
1716 }
1717
1718 TReturn* LFSCConvert::do_bso( const Expr& pf, bool beneath_lc, bool rev_pol,
1719 TReturn* t1, TReturn* t2, ostringstream& ose )
1720 {
1721 std::vector< int > emptyL;
1722 std::vector< int > emptyLUsed;
1723 int yMode = -2;
1724 TReturn* tRetVal = NULL;
1725 // merge literals
1726 t1->getL( emptyL, emptyLUsed );
1727 t2->getL( emptyL, emptyLUsed );
1728 bool isErr = false;
1729 if( pf[1].getKind()==PLUS || pf[1].getKind()==MINUS ||
1730 pf[1].getKind()==MULT || is_eq_kind( pf[1].getKind() ) )
1731 {
1732 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
1733 if( yMode==1 )
1734 {
1735 if( pf[1].getKind()==PLUS )
1736 tRetVal = new TReturn( LFSCLraAdd::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ ),
1737 emptyL, emptyLUsed, nullRat, false, 1 );
1738 else if( pf[1].getKind()==MINUS )
1739 tRetVal = new TReturn( LFSCLraSub::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ ),
1740 emptyL, emptyLUsed, nullRat, false, 1 );
1741 else if( pf[1].getKind()==MULT ){
1742 #ifdef PRINT_MAJOR_METHODS
1743 cout << ";[M]: basic_subst_op1_* " << std::endl;
1744 #endif
1745 Rational r;
1746 if( getRat( pf[1][0], r ) ){
1747 tRetVal = new TReturn( LFSCLraMulC::Make( t2->getLFSCProof(), r, EQ ),
1748 emptyL, emptyLUsed, nullRat, false, 1 );
1749 }else if( getRat( pf[1][1], r ) ){
1750 tRetVal = new TReturn( LFSCLraMulC::Make( t1->getLFSCProof(), r, EQ ),
1751 emptyL, emptyLUsed, nullRat, false, 1 );
1752 }else{
1753 print_error( "Could not find rational mult in basic_subst_op1", cout );
1754 isErr = true;
1755 }
1756 }else if( is_eq_kind( pf[1].getKind() ) ){
1757 RefPtr< LFSCProof > p;
1758 if( is_opposite( pf[1].getKind() ) ){
1759 p = LFSCLraSub::Make( t2->getLFSCProof(), t1->getLFSCProof(), EQ, EQ );
1760 }else{
1761 p = LFSCLraSub::Make( t1->getLFSCProof(), t2->getLFSCProof(), EQ, EQ );
1762 }
1763 tRetVal = new TReturn( p.get(), emptyL, emptyLUsed, nullRat, false, 1 );
1764 }
1765 if( !tRetVal && debug_conv ){
1766 cout << "basic_subst_op1: abort, have to normalize to 2, for " << kind_to_str( pf[1].getKind() ) << std::endl;
1767 }
1768 }
1769 }
1770 if( !tRetVal ){
1771 if( !isErr ){
1772 if( t1->getProvesY()==1 ){
1773 TReturn::normalize_tr( pf[3], t1, 2, rev_pol );
1774 }
1775 if( t2->getProvesY()==1 ){
1776 TReturn::normalize_tr( pf[4], t2, 2, rev_pol );
1777 }
1778 }
1779 yMode = TReturn::normalize_tret( pf[3], t1, pf[4], t2, rev_pol );
1780 if( yMode==0 || yMode==2 )
1781 {
1782 if( pf[1].getKind()==OR || pf[1].getKind()==AND ||
1783 pf[1].getKind()==IFF || pf[1].getKind()==PLUS ||
1784 is_eq_kind( pf[1].getKind() ) || pf[1].getKind()==MULT || pf[1].getKind()==MINUS ){
1785
1786 ostringstream os1, os2, os3;
1787 os1 << "(basic_subst_op1_";
1788 if( yMode==2 )
1789 os1 << "impl_";
1790 os1 << kind_to_str( pf[1].getKind() ) << " ";
1791 os3 << " ";
1792 os2 << ")";
1793 std::vector< string > strs;
1794 std::vector< RefPtr< LFSCProof > > pfs;
1795 strs.push_back( os1.str() );
1796 pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[1][0] ), true ) );
1797 strs.push_back( os3.str() );
1798 pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[2][0] ), true ) );
1799 strs.push_back( os3.str() );
1800 pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[1][1] ), true ) );
1801 strs.push_back( os3.str() );
1802 pfs.push_back( LFSCProofExpr::Make( cascade_expr( pf[2][1] ), true ) );
1803 strs.push_back( os3.str() );
1804 pfs.push_back( t1->getLFSCProof() );
1805 strs.push_back( os3.str() );
1806 pfs.push_back( t2->getLFSCProof() );
1807 strs.push_back( os2.str() );
1808 tRetVal = new TReturn( LFSCProofGeneric::Make( pfs, strs ), emptyL, emptyLUsed, nullRat, false, yMode );
1809 }
1810 }
1811 }
1812 if( !tRetVal ){
1813 ose << pf[0] << endl;
1814 for( int a=0; a<pf.arity(); a++ ){
1815 if( a>=3 ){
1816 ose << a << ": " << pf[a][0] << std::endl;
1817 Expr pre;
1818 what_is_proven( pf[a], pre );
1819 ose << "wip: " << pre << std::endl;
1820 }else{
1821 ose << a << ": " << pf[a] << std::endl;
1822 }
1823 }
1824 ose << "subst kind = " << kind_to_str( pf[1].getKind() ) << std::endl;
1825 ose << "subst arity = " << pf.arity() << std::endl;
1826 }
1827 return tRetVal;
1828 }
1829