summaryrefslogtreecommitdiff
path: root/src/printer/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2')
-rw-r--r--src/printer/smt2/smt2_printer.cpp113
-rw-r--r--src/printer/smt2/smt2_printer.h16
2 files changed, 74 insertions, 55 deletions
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) { }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback