29 print_warning(
"Warning: printing out lambda abstracted proof more than once");
30 #ifdef IGNORE_PRINT_MULTI_LAMBDA
51 print_warning(
"ERROR: printing out lambda abstracted proof more than once" );
52 #ifdef IGNORE_PRINT_MULTI_LAMBDA
70 void LFSCProof::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
107 #ifdef PRINT_MAJOR_METHODS
108 cout <<
";[M] CNF " << reason <<
" " << pos <<
std::endl;
128 ostringstream oss1, oss2;
130 for(
int a=(form.
arity()-2); a>=0; a-- ){
131 int m1 =
queryM( form[a] );
132 oss1 <<
"(or_elim_1 _ _ ";
133 oss1 << ( m1<0 ?
"(not_not_intro _ " :
"" );
134 oss1 <<
"@v" <<
abs( m1 );
135 oss1 << ( m1<0 ?
") " :
" " );
141 for(
int a=0; a<(form.
arity()-1); a++ ){
153 for(
int a=0; a<form.
arity(); a++ ){
154 if( a<(form.
arity()-1))
155 os1 <<
"(and_intro _ _ ";
157 if( a<(form.
arity()-1)){
162 os2 <<
" @v" <<
abs(m) <<
")";
165 for(
int a=0; a<form.
arity(); a++ ){
171 std::vector< Expr > assumes;
176 os1 <<
"(and_intro _ _ ";
177 os1 <<
"@v" <<
abs(
queryM( curr[0] ) ) <<
" ";
179 assumes.push_back( curr[0] );
182 os2 <<
" @v" <<
abs(m) <<
")";
184 for(
int a=0; a<(int)assumes.size(); a++ ){
206 os <<
"(impl_elim _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
225 os <<
"(ite_elim_2" << (m1<0 ?
"n" :
"" );
226 os <<
" _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
236 os <<
"(not_ite_elim_2 _ _ _ @v" << (m1<0 ?
"n" :
"" );
237 os <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
248 os <<
"(not_ite_elim_1 _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
260 os <<
" _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
270 os <<
"(not_ite_elim_3 _ _ _ @v" <<
abs( m2 ) <<
" @v" <<
abs( m ) <<
")";
282 os <<
" _ _ _ @v" <<
abs( m2 ) <<
" @v" <<
abs( m ) <<
")";
300 os <<
"(not_iff_elim_1 _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
310 os <<
"(not_iff_elim_2 _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
320 os <<
"(impl_elim _ _ @v" <<
abs( m1 ) <<
"(iff_elim_1 _ _ @v" <<
abs( m ) <<
"))";
331 os <<
"(impl_elim _ _ @v" <<
abs( m2 ) <<
"(iff_elim_2 _ _ @v" <<
abs( m ) <<
"))";
343 ostringstream os1, os2;
344 if( form[pos].isNot() )
345 os1 <<
"(not_not_elim _ ";
346 os1 <<
"(or_elim" << ( (pos==form.
arity()) ?
"_end" :
"" );
347 os1 <<
" _ _ " << pos <<
" ";
349 if( form[pos].isNot() )
367 ose <<
"CNF, " << reason <<
" unknown position = " << pos <<
std::endl;
376 ostringstream os1, os2;
377 os1 <<
"(not_not_elim _ ";
386 ostringstream os1, os2;
389 for(
int a=0; a<numHoles; a++ )
400 for(
int a=0; a<n; a++ ){
404 print_error(
"WARNING: and elim out of range", cout );
409 ostringstream os1, os2;
411 if( n==form.
arity()-1 )
413 os1 <<
" _ _ " << n <<
" ";
void print_structure(std::ostream &s, int ind=0)
Data structure of expressions in CVC3.
static Expr cascade_expr(const Expr &e)
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
virtual int getNumChildren()
static LFSCProof * Make_CNF(const Expr &form, const Expr &reason, int pos)
static LFSCProof * Make(const char *c, int v)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void indent(std::ostream &s, int ind=0)
static void print_error(const char *c, std::ostream &s)
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
static LFSCProof * Make(vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static Expr d_and_final_s
static LFSCProof * Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected)
static LFSCProof * Make(int v, LFSCProof *pf)
static LFSCProof * MakeStr(const char *c, bool db_str=false)
virtual void print_struct(std::ostream &s, int ind=0)
virtual LFSCProof * getChild(int n)
void print(std::ostream &s, int ind=0)
virtual void print_pf(std::ostream &s, int ind=0)=0
static LFSCProof * Make_not_not_elim(const Expr &pf, LFSCProof *p)
static std::map< LFSCProof *, int > lambdaMap
static LFSCProof * Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static void print_warning(const char *c)