9 d_lfsc_pf(lfsc_pf), d_c( r ), d_provesY(pvY){
11 for(
int a=0; a<(int)L.size(); a++ )
12 d_L.push_back( L[a] );
13 for(
int a=0; a<(int)Lused.size(); a++ )
16 #ifdef DEBUG_MEM_STATS
17 static int counter = 0;
19 cout <<
"make a tret " << counter <<
std::endl;
37 void TReturn::getL( std::vector< int >& lget, std::vector< int >& lgetu ){
39 std::vector< int >::iterator i;
40 for(
int a=0; a<(int)
d_L.size(); a++ ){
41 i = std::find( lget.begin(), lget.end(),
d_L[a] );
43 lget.push_back(
d_L[a] );
46 for(
int a=0; a<(int)
d_L_used.size(); a++ ){
47 i = std::find( lgetu.begin(), lgetu.end(),
d_L_used[a] );
56 void TReturn::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
63 std::vector< int >::iterator i;
64 for(
int a=0; a<(int)
d_L.size(); a++ ){
65 i = std::find( lget.begin(), lget.end(),
d_L[a] );
67 lget.push_back(
d_L[a] );
70 for(
int a=0; a<(int)
d_L_used.size(); a++ ){
71 i = std::find( lgetu.begin(), lgetu.end(),
d_L_used[a] );
114 os << pf1[0] <<
" " << pf2[0] <<
std::endl;
130 std::vector< int > emptyL;
131 std::vector< int > emptyLUsed;
132 t1->
getL( emptyL, emptyLUsed );
137 cout <<
"normalizing tr " << t1->
getProvesY() <<
" to " << y <<
" rev_pol = " << rev_pol <<
std::endl;
181 }
else if( e[0]==e[1] ){
182 ostringstream os1, os2;
187 emptyL, emptyLUsed,
nullRat,
false, 0 );
190 #ifdef PRINT_MAJOR_METHODS
191 cout <<
";[M]: Normalize 1 to 0, iff" <<
std::endl;
197 ostringstream os1, os2;
198 os1 <<
"(" << ( e[0].
getKind()==
NOT ?
"not_to_iff" :
"iff_not_false" );
202 emptyL, emptyLUsed,
nullRat,
false, 0 );
204 else if( e[1].isTrue() )
207 ostringstream os1, os2;
208 os1 <<
"(iff_true _ ";
211 emptyL, emptyLUsed,
nullRat,
false, 0 );
226 ostringstream os1, os2, os3, os4;
227 os1 <<
"(impl_elim _ _ ";
228 os2 <<
"(impl_intro _ _ (\\ @V0 (iff_intro _ _ ";
231 std::vector< RefPtr< LFSCProof > > pfs;
233 pfs.push_back( ti1->getLFSCProof() );
234 pfs.push_back( ti2->getLFSCProof() );
235 std::vector< string > strs;
236 strs.push_back( os1.str() );
237 strs.push_back( os2.str() );
238 strs.push_back( os3.str() );
239 strs.push_back( os4.str() );
253 ostringstream os1, os2;
254 os1 <<
"(iff_elim_1 _ _ ";
272 int val1 =
queryM( e[0] );
273 int val2 =
queryM( e[1] );
279 os <<
"(impl_refl_atom" << (val1<0 ?
"_not" :
"" );
280 os <<
" _ _ @a" <<
abs( val1 ) <<
")";
283 emptyL, emptyLUsed,
nullRat,
false, 2 );
287 #ifdef PRINT_MAJOR_METHODS
288 cout <<
";[M]: Normalize 1 to 2, iff/impl double logical iff" <<
std::endl;
292 ose <<
"Warning: normalize logical atoms, not equal ";
297 os <<
"impl_refl_" << ( eatom2.
isFalse() ?
"false" :
"true" );
299 emptyL, emptyLUsed,
nullRat,
false, 2 );
301 else if( eatom2.
isTrue() )
304 ostringstream oss1, oss2;
305 oss1 <<
"(iff_true_impl _ ";
308 emptyL, emptyLUsed,
nullRat,
false, 2 );
312 #ifdef PRINT_MAJOR_METHODS
324 ostringstream oss1, oss2;
327 oss1 <<
"(impl_intro";
328 oss1 <<
" _ _ (\\ @v" <<
abs( val1 ) <<
" ";
329 oss1 <<
"(bottom_elim ";
337 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 2 );
342 #ifdef PRINT_MAJOR_METHODS
347 ostringstream os1, os2;
350 os1 <<
"(impl_intro";
352 os1 <<
"@v" <<
abs( val1 ) <<
" ";
384 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 2 );
389 ose <<
"NTret 12 could not handle " << eatom1 <<
" " << eatom2;
405 ose <<
"proven_expr = " << e <<
std::endl;
412 #ifdef IGNORE_NORMALIZE
431 std::vector< int > emptyL;
432 std::vector< int > emptyLUsed;
433 t1->
getL( emptyL, emptyLUsed );
437 #ifdef PRINT_MAJOR_METHODS
438 cout <<
";[M]: Normalize 1 to " << y <<
", simplify case" <<
std::endl;
445 #ifdef PRINT_MAJOR_METHODS
446 cout <<
";[M]: Normalize 1 to " << y <<
", iff/impl, atom" <<
std::endl;
473 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, y );
void print_formula(const Expr &clause, std::ostream &s)
Data structure of expressions in CVC3.
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
static LFSCProof * Make(LFSCProof *pf, int op)
static LFSCProof * Make(const Expr &e, bool isH=false)
virtual LFSCLraPoly * AsLFSCLraPoly()
static LFSCProof * Make(const char *c, int v)
Rational mult_rational(TReturn *lhs)
static LFSCPrinter * printer
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int get_normalized(int knd, bool isnot)
static void print_error(const char *c, std::ostream &s)
static Expr queryAtomic(const Expr &expr, bool getBase=false)
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static int normalize_tr(const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true)
void getL(std::vector< int > &lget, std::vector< int > &lgetu)
static bool what_is_proven(const Expr &pf, Expr &pe)
LFSCProof * getLFSCProof()
static bool can_pnorm(const Expr &e)
static LFSCProof * Make(int v, LFSCProof *pf)
static LFSCProof * MakeStr(const char *c, bool db_str=false)
static LFSCProof * Make(LFSCProof *pf, Rational r, int op)
TReturn(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)
virtual LFSCProof * getChild(int n)
static LFSCProof * Make(LFSCProof *pf, int var, int op)
bool is_comparison(int knd)
static Expr queryElimNotNot(const Expr &expr)
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
std::vector< int > d_L_used
static int normalize_tret(const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false)
RefPtr< LFSCProof > d_lfsc_pf
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static void normalize_to_tf(const Expr &pf, TReturn *&t1, int y)