diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-02 20:25:09 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-02 18:25:09 -0700 |
commit | 716ce9168d846ea991f8404a78aeb1ccccfbce14 (patch) | |
tree | 5a617909b7d82ed2265693461f4f9f0a4c811f56 /src/printer | |
parent | d3f4ac852146c41341e485d9035f3631993e3fa5 (diff) |
Initial support for string standard in smt lib 2.6 (#1848)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 113 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 16 |
3 files changed, 78 insertions, 55 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index e8ebadeb8..f9486f017 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -50,6 +50,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) return unique_ptr<Printer>( new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case LANG_SMTLIB_V2_6_1: + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant)); + case LANG_TPTP: return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8c9680a74..5d2b8972d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -42,7 +42,13 @@ namespace smt2 { static OutputLanguage variantToLanguage(Variant v); -static string smtKindString(Kind k); +static string smtKindString(Kind k, Variant v); + +/** returns whether the variant is smt-lib 2.6 or greater */ +bool isVariant_2_6(Variant v) +{ + return v == smt2_6_variant || v == smt2_6_1_variant; +} static void printBvParameterizedOp(std::ostream& out, TNode n); static void printFpParameterizedOp(std::ostream& out, TNode n); @@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out, out << (n.getConst<bool>() ? "true" : "false"); break; case kind::BUILTIN: - out << smtKindString(n.getConst<Kind>()); + out << smtKindString(n.getConst<Kind>(), d_variant); break; case kind::CHAIN_OP: - out << smtKindString(n.getConst<Chain>().getOperator()); + out << smtKindString(n.getConst<Chain>().getOperator(), d_variant); break; case kind::CONST_RATIONAL: { const Rational& r = n.getConst<Rational>(); @@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out, if (force_nt.isReal()) { out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER - : kind::TO_REAL) + : kind::TO_REAL, + d_variant) << " "; toStream(out, n, toDepth, types, TypeNode::null()); out << ")"; @@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out, // builtin theory case kind::APPLY: break; case kind::EQUAL: - case kind::DISTINCT: - out << smtKindString(k) << " "; + case kind::DISTINCT: + out << smtKindString(k, d_variant) << " "; parametricTypeChildren = true; break; case kind::CHAIN: break; @@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out, case kind::IMPLIES: case kind::OR: case kind::XOR: - case kind::ITE: out << smtKindString(k) << " "; break; + case kind::ITE: + out << smtKindString(k, d_variant) << " "; + break; - // uf theory + // uf theory case kind::APPLY_UF: typeChildren = true; break; // higher-order case kind::HO_APPLY: break; case kind::LAMBDA: - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; // arith theory @@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::TO_REAL: case kind::POW: parametricTypeChildren = true; - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; case kind::DIVISIBLE: @@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STORE: typeChildren = true; case kind::PARTIAL_SELECT_0: case kind::PARTIAL_SELECT_1: - case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; + case kind::ARRAY_TYPE: + out << smtKindString(k, d_variant) << " "; + break; - // string theory + // string theory case kind::STRING_CONCAT: if(d_variant == z3str_variant) { out << "Concat "; @@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out, out << ")"; return; } - out << "str.in.re "; + out << smtKindString(k, d_variant) << " "; break; } - case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break; - case kind::STRING_SUBSTR: out << "str.substr "; break; - case kind::STRING_CHARAT: out << "str.at "; break; - case kind::STRING_STRCTN: out << "str.contains "; break; - case kind::STRING_STRIDOF: out << "str.indexof "; break; - case kind::STRING_STRREPL: out << "str.replace "; break; - case kind::STRING_PREFIX: out << "str.prefixof "; break; - case kind::STRING_SUFFIX: out << "str.suffixof "; break; - case kind::STRING_ITOS: out << "int.to.str "; break; - case kind::STRING_STOI: out << "str.to.int "; break; - case kind::STRING_TO_REGEXP: out << "str.to.re "; break; - case kind::REGEXP_CONCAT: out << "re.++ "; break; - case kind::REGEXP_UNION: out << "re.union "; break; - case kind::REGEXP_INTER: out << "re.inter "; break; - case kind::REGEXP_STAR: out << "re.* "; break; - case kind::REGEXP_PLUS: out << "re.+ "; break; - case kind::REGEXP_OPT: out << "re.opt "; break; - case kind::REGEXP_RANGE: out << "re.range "; break; - case kind::REGEXP_LOOP: out << "re.loop "; break; - case kind::REGEXP_EMPTY: out << "re.nostr "; break; - case kind::REGEXP_SIGMA: out << "re.allchar "; break; + case kind::STRING_LENGTH: + case kind::STRING_SUBSTR: + case kind::STRING_CHARAT: + case kind::STRING_STRCTN: + case kind::STRING_STRIDOF: + case kind::STRING_STRREPL: + case kind::STRING_PREFIX: + case kind::STRING_SUFFIX: + case kind::STRING_ITOS: + case kind::STRING_STOI: + 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_LOOP: + case kind::REGEXP_EMPTY: + case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break; case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; @@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out, case kind::TRANSPOSE: case kind::TCLOSURE: parametricTypeChildren = true; - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; case kind::MEMBER: typeChildren = true; case kind::SET_TYPE: case kind::SINGLETON: - case kind::COMPLEMENT:out << smtKindString(k) << " "; break; + case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // fp theory @@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_ISNEG: case kind::FLOATINGPOINT_ISPOS: case kind::FLOATINGPOINT_TO_REAL: - out << smtKindString(k) << ' '; break; + out << smtKindString(k, d_variant) << ' '; + break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: @@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SEP_EMP: case kind::SEP_PTO: case kind::SEP_STAR: - case kind::SEP_WAND: out << smtKindString(k) << " "; break; + case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break; case kind::SEP_NIL: out << "(as sep.nil " << n.getType() << ")"; @@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out, }else if( n.getKind()==kind::APPLY_TESTER ){ unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - if( d_variant==smt2_6_variant ){ + if (isVariant_2_6(d_variant)) + { out << "(_ is "; toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); out << ")"; @@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out, if(forceBinary && i < n.getNumChildren() - 1) { // not going to work properly for parameterized kinds! Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); - out << " (" << smtKindString(n.getKind()) << ' '; + out << " (" << smtKindString(n.getKind(), d_variant) << ' '; parens << ')'; ++c; } else { @@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out, } }/* Smt2Printer::toStream(TNode) */ -static string smtKindString(Kind k) +static string smtKindString(Kind k, Variant v) { switch(k) { // builtin theory @@ -1039,7 +1052,7 @@ static string smtKindString(Kind k) //string theory case kind::STRING_CONCAT: return "str.++"; - case kind::STRING_LENGTH: return "str.len"; + case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len"; case kind::STRING_SUBSTR: return "str.substr" ; case kind::STRING_STRCTN: return "str.contains" ; case kind::STRING_CHARAT: return "str.at" ; @@ -1047,10 +1060,14 @@ static string smtKindString(Kind k) case kind::STRING_STRREPL: return "str.replace" ; case kind::STRING_PREFIX: return "str.prefixof" ; case kind::STRING_SUFFIX: return "str.suffixof" ; - case kind::STRING_ITOS: return "int.to.str" ; - case kind::STRING_STOI: return "str.to.int" ; - case kind::STRING_IN_REGEXP: return "str.in.re"; - case kind::STRING_TO_REGEXP: return "str.to.re"; + case kind::STRING_ITOS: + return v == smt2_6_1_variant ? "str.from-int" : "int.to.str"; + case kind::STRING_STOI: + return v == smt2_6_1_variant ? "str.to-int" : "str.to.int"; + case kind::STRING_IN_REGEXP: + return v == smt2_6_1_variant ? "str.in-re" : "str.in.re"; + case kind::STRING_TO_REGEXP: + return v == smt2_6_1_variant ? "str.to-re" : "str.to.re"; case kind::REGEXP_CONCAT: return "re.++"; case kind::REGEXP_UNION: return "re.union"; case kind::REGEXP_INTER: return "re.inter"; @@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out, const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn); if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr) { - if (variant == smt2_6_variant) + if (isVariant_2_6(variant)) { out << "(declare-datatypes ((" << command.getSymbol() << " 0)) ("; } @@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out, out << "co"; } out << "datatypes"; - if (v == smt2_6_variant) + if (isVariant_2_6(v)) { out << " ("; for (vector<DatatypeType>::const_iterator i = datatypes.begin(), diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 922b69a9e..1d281aed4 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -27,14 +27,16 @@ namespace CVC4 { namespace printer { namespace smt2 { -enum Variant { +enum Variant +{ no_variant, - smt2_0_variant, // old-style 2.0 syntax, when it makes a difference - smt2_6_variant, // new-style 2.6 syntax, when it makes a difference - z3str_variant, // old-style 2.0 and also z3str syntax - sygus_variant // variant for sygus -};/* enum Variant */ - + smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + smt2_6_variant, // new-style 2.6 syntax, when it makes a difference + smt2_6_1_variant, // new-style 2.6 syntax, when it makes a difference, with + // support for the string standard + z3str_variant, // old-style 2.0 and also z3str syntax + sygus_variant // variant for sygus +}; /* enum Variant */ class Smt2Printer : public CVC4::Printer { public: Smt2Printer(Variant variant = no_variant) : d_variant(variant) { } |