diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 377 |
1 files changed, 90 insertions, 287 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bf26b80ee..c51d00b5d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -566,194 +566,91 @@ void Smt2Printer::toStream(std::ostream& out, } switch(k) { // builtin theory - case kind::EQUAL: - case kind::DISTINCT: - out << smtKindString(k, d_variant) << " "; - break; - case kind::FUNCTION_TYPE: - out << "->"; - for (Node nc : n) - { - out << " "; - toStream(out, nc, toDepth); - } - out << ")"; - return; - case kind::SEXPR: break; - - // bool theory - case kind::NOT: - case kind::AND: - case kind::IMPLIES: - case kind::OR: - case kind::XOR: - case kind::ITE: - out << smtKindString(k, d_variant) << " "; - break; + case kind::FUNCTION_TYPE: + out << "->"; + for (Node nc : n) + { + out << " "; + toStream(out, nc, toDepth); + } + out << ")"; + return; + case kind::SEXPR: break; - // uf theory - case kind::APPLY_UF: break; - // higher-order - case kind::HO_APPLY: - if (!options::flattenHOChains()) - { - break; - } - // collapse "@" chains, i.e. - // - // ((a b) c) --> (a b c) - // - // (((a b) ((c d) e)) f) --> (a b (c d e) f) - { - Node head = n; - std::vector<Node> args; - while (head.getKind() == kind::HO_APPLY) + // uf theory + case kind::APPLY_UF: break; + // higher-order + case kind::HO_APPLY: + if (!options::flattenHOChains()) { - args.insert(args.begin(), head[1]); - head = head[0]; + break; } - toStream(out, head, toDepth, lbind); - for (unsigned i = 0, size = args.size(); i < size; ++i) + // collapse "@" chains, i.e. + // + // ((a b) c) --> (a b c) + // + // (((a b) ((c d) e)) f) --> (a b (c d e) f) { - out << " "; - toStream(out, args[i], toDepth, lbind); + Node head = n; + std::vector<Node> args; + while (head.getKind() == kind::HO_APPLY) + { + args.insert(args.begin(), head[1]); + head = head[0]; + } + toStream(out, head, toDepth, lbind); + for (unsigned i = 0, size = args.size(); i < size; ++i) + { + out << " "; + toStream(out, args[i], toDepth, lbind); + } + out << ")"; } - out << ")"; - } - return; + return; - case kind::MATCH: - out << smtKindString(k, d_variant) << " "; - toStream(out, n[0], toDepth, lbind); - out << " ("; - for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++) - { - if (i > 1) + case kind::MATCH: + out << smtKindString(k, d_variant) << " "; + toStream(out, n[0], toDepth, lbind); + out << " ("; + for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++) { - out << " "; + if (i > 1) + { + out << " "; + } + toStream(out, n[i], toDepth, lbind); } - toStream(out, n[i], toDepth, lbind); - } - out << "))"; - return; - case kind::MATCH_BIND_CASE: - // ignore the binder - toStream(out, n[1], toDepth, lbind); - out << " "; - toStream(out, n[2], toDepth, lbind); - out << ")"; - return; - case kind::MATCH_CASE: - // do nothing - break; + out << "))"; + return; + case kind::MATCH_BIND_CASE: + // ignore the binder + toStream(out, n[1], toDepth, lbind); + out << " "; + toStream(out, n[2], toDepth, lbind); + out << ")"; + return; + case kind::MATCH_CASE: + // do nothing + break; - // arith theory - case kind::PLUS: - case kind::MULT: - case kind::NONLINEAR_MULT: - case kind::EXPONENTIAL: - case kind::SINE: - case kind::COSINE: - case kind::TANGENT: - case kind::COSECANT: - case kind::SECANT: - case kind::COTANGENT: - case kind::ARCSINE: - case kind::ARCCOSINE: - case kind::ARCTANGENT: - case kind::ARCCOSECANT: - case kind::ARCSECANT: - case kind::ARCCOTANGENT: - case kind::PI: - case kind::SQRT: - case kind::MINUS: - case kind::UMINUS: - case kind::LT: - case kind::LEQ: - case kind::GT: - case kind::GEQ: - case kind::DIVISION: - case kind::DIVISION_TOTAL: - case kind::INTS_DIVISION: - case kind::INTS_DIVISION_TOTAL: - case kind::INTS_MODULUS: - case kind::INTS_MODULUS_TOTAL: - case kind::ABS: - case kind::IS_INTEGER: - case kind::TO_INTEGER: - case kind::TO_REAL: - case kind::POW: - case kind::POW2: out << smtKindString(k, d_variant) << " "; break; - case kind::IAND: - out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") "; - stillNeedToPrintParams = false; - break; + // arith theory + case kind::IAND: + out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") "; + stillNeedToPrintParams = false; + break; - case kind::DIVISIBLE: - out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")"; - stillNeedToPrintParams = false; - break; - case kind::INDEXED_ROOT_PREDICATE_OP: - { - const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>(); - out << "(_ root_predicate " << irp.d_index << ")"; - break; + case kind::DIVISIBLE: + out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")"; + stillNeedToPrintParams = false; + break; + case kind::INDEXED_ROOT_PREDICATE_OP: + { + const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>(); + out << "(_ root_predicate " << irp.d_index << ")"; + break; } - // arrays theory - case kind::SELECT: - case kind::STORE: - case kind::PARTIAL_SELECT_0: - case kind::PARTIAL_SELECT_1: - case kind::ARRAY_TYPE: - case kind::EQ_RANGE: out << smtKindString(k, d_variant) << " "; break; - // string theory - case kind::STRING_CONCAT: - out << "str.++ "; - break; - case kind::STRING_IN_REGEXP: { - stringstream ss; - out << smtKindString(k, d_variant) << " "; - break; - } - case kind::STRING_LENGTH: - case kind::STRING_SUBSTR: - case kind::STRING_UPDATE: - case kind::STRING_CHARAT: - case kind::STRING_CONTAINS: - case kind::STRING_INDEXOF: - case kind::STRING_INDEXOF_RE: - case kind::STRING_REPLACE: - case kind::STRING_REPLACE_ALL: - case kind::STRING_REPLACE_RE: - case kind::STRING_REPLACE_RE_ALL: - case kind::STRING_TOLOWER: - case kind::STRING_TOUPPER: - case kind::STRING_REV: - case kind::STRING_PREFIX: - case kind::STRING_SUFFIX: - case kind::STRING_LEQ: - case kind::STRING_LT: - case kind::STRING_ITOS: - case kind::STRING_STOI: - case kind::STRING_FROM_CODE: - case kind::STRING_TO_CODE: - case kind::STRING_TO_REGEXP: - case kind::REGEXP_CONCAT: - case kind::REGEXP_UNION: - case kind::REGEXP_INTER: - case kind::REGEXP_STAR: - case kind::REGEXP_PLUS: - case kind::REGEXP_OPT: - case kind::REGEXP_RANGE: - case kind::REGEXP_COMPLEMENT: - case kind::REGEXP_DIFF: - case kind::REGEXP_EMPTY: - case kind::REGEXP_SIGMA: - case kind::SEQ_UNIT: - case kind::SEQ_NTH: - case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break; case kind::REGEXP_REPEAT: case kind::REGEXP_LOOP: { @@ -766,41 +663,17 @@ void Smt2Printer::toStream(std::ostream& out, case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; // bv theory - case kind::BITVECTOR_CONCAT: out << "concat "; forceBinary = true; break; - case kind::BITVECTOR_AND: out << "bvand "; forceBinary = true; break; - case kind::BITVECTOR_OR: out << "bvor "; forceBinary = true; break; - case kind::BITVECTOR_XOR: out << "bvxor "; forceBinary = true; break; - case kind::BITVECTOR_NOT: out << "bvnot "; break; - case kind::BITVECTOR_NAND: out << "bvnand "; break; - case kind::BITVECTOR_NOR: out << "bvnor "; break; - case kind::BITVECTOR_XNOR: out << "bvxnor "; break; - case kind::BITVECTOR_COMP: out << "bvcomp "; break; - case kind::BITVECTOR_MULT: out << "bvmul "; forceBinary = true; break; + case kind::BITVECTOR_CONCAT: + case kind::BITVECTOR_AND: + case kind::BITVECTOR_OR: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_MULT: case kind::BITVECTOR_ADD: - out << "bvadd "; + { + out << smtKindString(k, d_variant) << " "; forceBinary = true; - break; - case kind::BITVECTOR_SUB: out << "bvsub "; break; - case kind::BITVECTOR_NEG: out << "bvneg "; break; - case kind::BITVECTOR_UDIV: out << "bvudiv "; break; - case kind::BITVECTOR_UREM: out << "bvurem "; break; - case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; - case kind::BITVECTOR_SREM: out << "bvsrem "; break; - case kind::BITVECTOR_SMOD: out << "bvsmod "; break; - case kind::BITVECTOR_SHL: out << "bvshl "; break; - case kind::BITVECTOR_LSHR: out << "bvlshr "; break; - case kind::BITVECTOR_ASHR: out << "bvashr "; break; - case kind::BITVECTOR_ULT: out << "bvult "; break; - case kind::BITVECTOR_ULE: out << "bvule "; break; - case kind::BITVECTOR_UGT: out << "bvugt "; break; - case kind::BITVECTOR_UGE: out << "bvuge "; break; - case kind::BITVECTOR_SLT: out << "bvslt "; break; - case kind::BITVECTOR_SLE: out << "bvsle "; break; - case kind::BITVECTOR_SGT: out << "bvsgt "; break; - case kind::BITVECTOR_SGE: out << "bvsge "; break; - case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break; - case kind::BITVECTOR_REDOR: out << "bvredor "; break; - case kind::BITVECTOR_REDAND: out << "bvredand "; break; + } + break; case kind::BITVECTOR_EXTRACT: case kind::BITVECTOR_REPEAT: @@ -814,19 +687,7 @@ void Smt2Printer::toStream(std::ostream& out, stillNeedToPrintParams = false; break; - // sets - case kind::UNION: - case kind::INTERSECTION: - case kind::SETMINUS: - case kind::SUBSET: - case kind::CARD: - case kind::JOIN: - case kind::PRODUCT: - case kind::TRANSPOSE: - case kind::TCLOSURE: - case kind::IDEN: - case kind::JOIN_IMAGE: out << smtKindString(k, d_variant) << " "; break; - case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break; + // sets case kind::SINGLETON: { out << smtKindString(k, d_variant) << " "; @@ -837,29 +698,9 @@ void Smt2Printer::toStream(std::ostream& out, return; } break; - case kind::MEMBER: - case kind::INSERT: - case kind::SET_TYPE: - case kind::COMPLEMENT: - case kind::CHOOSE: - case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // bags - case kind::BAG_TYPE: - case kind::UNION_MAX: - case kind::UNION_DISJOINT: - case kind::INTERSECTION_MIN: - case kind::DIFFERENCE_SUBTRACT: - case kind::DIFFERENCE_REMOVE: - case kind::SUBBAG: - case kind::BAG_COUNT: - case kind::DUPLICATE_REMOVAL: - case kind::BAG_CARD: - case kind::BAG_CHOOSE: - case kind::BAG_IS_SINGLETON: - case kind::BAG_FROM_SET: - case kind::BAG_TO_SET: out << smtKindString(k, d_variant) << " "; break; case kind::MK_BAG: { // print (bag (mkBag_op Real) 1 3) as (bag 1.0 3) @@ -871,43 +712,7 @@ void Smt2Printer::toStream(std::ostream& out, return; } - // fp theory - case kind::FLOATINGPOINT_FP: - case kind::FLOATINGPOINT_EQ: - case kind::FLOATINGPOINT_ABS: - case kind::FLOATINGPOINT_NEG: - case kind::FLOATINGPOINT_ADD: - case kind::FLOATINGPOINT_SUB: - case kind::FLOATINGPOINT_MULT: - case kind::FLOATINGPOINT_DIV: - case kind::FLOATINGPOINT_FMA: - case kind::FLOATINGPOINT_SQRT: - case kind::FLOATINGPOINT_REM: - case kind::FLOATINGPOINT_RTI: - case kind::FLOATINGPOINT_MIN: - case kind::FLOATINGPOINT_MAX: - case kind::FLOATINGPOINT_LEQ: - case kind::FLOATINGPOINT_LT: - case kind::FLOATINGPOINT_GEQ: - case kind::FLOATINGPOINT_GT: - case kind::FLOATINGPOINT_ISN: - case kind::FLOATINGPOINT_ISSN: - case kind::FLOATINGPOINT_ISZ: - case kind::FLOATINGPOINT_ISINF: - case kind::FLOATINGPOINT_ISNAN: - case kind::FLOATINGPOINT_ISNEG: - case kind::FLOATINGPOINT_ISPOS: - case kind::FLOATINGPOINT_TO_REAL: - case kind::FLOATINGPOINT_COMPONENT_NAN: - case kind::FLOATINGPOINT_COMPONENT_INF: - case kind::FLOATINGPOINT_COMPONENT_ZERO: - case kind::FLOATINGPOINT_COMPONENT_SIGN: - case kind::FLOATINGPOINT_COMPONENT_EXPONENT: - case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: - case kind::ROUNDINGMODE_BITBLAST: - out << smtKindString(k, d_variant) << ' '; - break; - + // fp theory case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: case kind::FLOATINGPOINT_TO_FP_REAL: @@ -991,11 +796,6 @@ void Smt2Printer::toStream(std::ostream& out, case kind::PARAMETRIC_DATATYPE: break; // separation logic - case kind::SEP_EMP: - case kind::SEP_PTO: - case kind::SEP_STAR: - case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break; - case kind::SEP_NIL: out << "(as sep.nil " << n.getType() << ")"; break; @@ -1062,10 +862,9 @@ void Smt2Printer::toStream(std::ostream& out, case kind::INST_NO_PATTERN: case kind::INST_PATTERN_LIST: break; default: - // fall back on however the kind prints itself; this probably - // won't be SMT-LIB v2 compliant, but it will be clear from the - // output that support for the kind needs to be added here. - out << n.getKind() << ' '; + // by default, print the kind using the smtKindString utility + out << smtKindString(k, d_variant) << " "; + break; } if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { @@ -1236,6 +1035,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left"; case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right"; case kind::INT_TO_BITVECTOR: return "int2bv"; + case kind::BITVECTOR_BB_TERM: return "bbT"; // datatypes theory case kind::APPLY_TESTER: return "is"; @@ -1389,6 +1189,9 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) ; /* fall through */ } + // fall back on however the kind prints itself; this probably + // won't be SMT-LIB v2 compliant, but it will be clear from the + // output that support for the kind needs to be added here. // no SMT way to print these return kind::kindToString(k); } |