6 d_user_assumptions(assumps),
7 d_common_pf_rules(commonRules){
32 cout <<
"(check " <<
endl;
60 cout<<
"(% "<<(*v).first<<
" var_real"<<
endl;
66 cout<<
"(% "<<(*v).first<<
" formula"<<
endl;
115 while( j2 != j2end ){
121 cout <<
"@f" << val <<
" ";
124 cout <<
"@x" << val <<
" ";
140 cout<<
"(% @F"<<m<<
" (th_holds ";
151 cout <<
"(% @T" << (*j).second <<
" (th_holds ";
158 cout <<
"(: bottom" <<
endl;
190 cout <<
"(decl_atom ";
196 cout<<
" (\\ @b"<<(*j).second<<
" (\\ @a"<<(*j).second<<
endl;
203 cout <<
"(decl_term_atom ";
205 cout<<
" (\\ @bt"<<(*j).second<<
" (\\ @at"<<(*j).second<<
endl;
220 cout <<
"(pn_let _ _ ";
223 cout <<
"(\\ @pnt" << (*j).second <<
endl;
232 cout <<
"(poly_norm_" <<
kind_to_str( (*j).first.getKind() ) <<
" _ _ _ @pnt";
234 cout << (*j).second <<
" ";
246 lambda_pf->
print( cout );
251 cout << cparen.str() <<
endl;
257 if(expr.
arity()==2 ){
259 ostringstream cparen;
261 for(
int a=0; a<2; a++ ){
277 s<<
"c_" << ( a==0 ?
"L" :
"R" );
289 ose <<
"ERROR: Multiplying by non-constant " << expr;
312 print_error(
"ERROR: Pn Dividing by non-constant", s );
329 s <<
"(pn_u- _ _ _ ";
343 bool success =
false;
349 s <<
"(pn_var_atom _ _ @at" << val <<
")";
354 ose <<
"Trying to pn_var_atom a non-atomized skolem var " << expr;
361 s <<
"(pn_var_atom _ _ @at" << val <<
")";
364 ose <<
"Trying to pn_var_atom a non-atomized ITE " << expr;
367 }
else if(expr.
isVar()){
368 s<<
"(pn_var "<<expr<<
")";
372 ose<<
"ERROR printing polynomial norm for "<<expr;
386 }
else if(expr.
isVar()){
387 s<<
"(a_var_real "<<expr<<
")";
388 }
else if(expr.
arity()==2 ){
395 print_error(
"ERROR: Dividing by non constant", s );
423 cout <<
"cannot determine rational " << expr <<
endl;
431 }
else if(expr.
arity()>2){
433 vector<Expr> kids = expr.
getKids();
434 vector<Expr>::iterator i = kids.begin(), iend= kids.end();
442 for(
int j=0; j<expr.
arity();j++){
448 os <<
"ERROR printing term "<<expr<<
" "<<expr.
arity();
457 }
else if(clause.
isNot()){
461 }
else if(clause.
isOr()){
467 }
else if(clause.
isAnd()){
473 }
else if(clause.
isImpl()){
479 }
else if(clause.
isIff()){
504 }
else if( clause.
isTrue() ){
513 for(
int a=0; a<(int)e.
arity(); a++ ){
void print_structure(std::ostream &s, int ind=0)
void print_formula(const Expr &clause, std::ostream &s)
static ExprMap< bool > d_formulas_printed
void print_rational(const Rational &r, std::ostream &s)
void print_terms(const Expr &expr, std::ostream &s)
Data structure of expressions in CVC3.
static std::map< int, bool > pntNeeded
static void define_skolem_vars(const Expr &e)
static Expr cascade_expr(const Expr &e)
static ExprMap< bool > d_assump_map
bool is_smt_kind(int knd)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
iterator find(const Expr &e)
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
RefPtr< LFSCConvert > converter
void print_LFSC(const Expr &pf_expr)
const std::vector< Expr > & getKids() const
static LFSCPrinter * printer
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
static void print_error(const char *c, std::ostream &s)
void make_let_map(const Expr &e)
static void collect_vars(const Expr &e, bool readPred=true)
void print_poly_norm(const Expr &expr, std::ostream &s, bool pnRat=true, bool ratNeg=false)
static ExprMap< int > d_terms
static ExprMap< int > d_formulas
static ExprMap< int > d_pn
void convert(const Expr &pf)
string kind_to_str(int knd)
void print(std::ostream &s, int ind=0)
static bool isFormula(const Expr &e)
std::vector< Expr > d_user_assumptions
static ExprMap< bool > input_vars
LFSCPrinter(const Expr pf_expr, Expr qExpr, std::vector< Expr > assumps, int lfscm, CommonProofRules *commonRules)
static ExprMap< bool > input_preds
static ExprMap< int > d_trusted
ExprMap< bool > d_print_visited_map
static ExprMap< Expr > skolem_vars
ExprMap< int > d_print_map
void print_rational_divide(const Rational &n, const Rational &d, std::ostream &s)
LFSCProof * getLFSCProof()
void print_terms_h(const Expr &expr, std::ostream &s)
static ExprMap< int > d_pn_form
void print_formula_h(const Expr &clause, std::ostream &s)