#include "proof/lfsc/lfsc_node_converter.h"
+#include <algorithm>
#include <iomanip>
#include <sstream>
#include "expr/array_store_all.h"
+#include "expr/cardinality_constraint.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/nary_term_util.h"
#include "theory/strings/word.h"
#include "theory/uf/theory_uf_rewriter.h"
#include "util/bitvector.h"
+#include "util/floatingpoint.h"
#include "util/iand.h"
#include "util/rational.h"
#include "util/regexp.h"
{
NodeManager* nm = NodeManager::currentNM();
Kind k = n.getKind();
+ // we eliminate MATCH at preConvert above
+ Assert(k != MATCH);
if (k == ASCRIPTION_TYPE)
{
// dummy node, return it
{
return mkInternalSymbol(getNameForUserNameOf(n), tn);
}
+ else if (k == CARDINALITY_CONSTRAINT)
+ {
+ Trace("lfsc-term-process-debug")
+ << "...convert cardinality constraint" << std::endl;
+ const CardinalityConstraint& cc =
+ n.getOperator().getConst<CardinalityConstraint>();
+ Node tnn = typeAsNode(convertType(cc.getType()));
+ Node ub = nm->mkConstInt(Rational(cc.getUpperBound()));
+ TypeNode tnc =
+ nm->mkFunctionType({tnn.getType(), ub.getType()}, nm->booleanType());
+ Node fcard = getSymbolInternal(k, tnc, "fmf.card");
+ return nm->mkNode(APPLY_UF, fcard, tnn, ub);
+ }
else if (k == APPLY_UF)
{
return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
{
TypeNode btn = nm->booleanType();
TypeNode tnv = nm->mkFunctionType(btn, tn);
- TypeNode btnv = nm->mkFunctionType({btn, btn}, btn);
BitVector bv = n.getConst<BitVector>();
- size_t w = bv.getSize();
- Node ret = getSymbolInternal(k, btn, "bvn");
- Node b0 = getSymbolInternal(k, btn, "b0");
- Node b1 = getSymbolInternal(k, btn, "b1");
- Node bvc = getSymbolInternal(k, btnv, "bvc");
- for (size_t i = 0; i < w; i++)
- {
- Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
- ret = nm->mkNode(APPLY_UF, bvc, arg, ret);
- }
+ Node ret = convertBitVector(bv);
Node bconstf = getSymbolInternal(k, tnv, "bv");
return nm->mkNode(APPLY_UF, bconstf, ret);
}
+ else if (k == CONST_FLOATINGPOINT)
+ {
+ BitVector s, e, i;
+ n.getConst<FloatingPoint>().getIEEEBitvectors(s, e, i);
+ Node sn = convert(nm->mkConst(s));
+ Node en = convert(nm->mkConst(e));
+ Node in = convert(nm->mkConst(i));
+ TypeNode btn = nm->booleanType();
+ TypeNode tnv = nm->mkFunctionType({btn, btn, btn}, tn);
+ Node bconstf = getSymbolInternal(k, tnv, "fp");
+ return nm->mkNode(APPLY_UF, {bconstf, sn, en, in});
+ }
else if (k == CONST_STRING)
{
//"" is emptystr
Node n2 = nm->mkConstInt(Rational(op.d_loopMaxOcc));
return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]);
}
- else if (k == MATCH)
- {
- // currently unsupported
- return n;
- }
else if (k == BITVECTOR_BB_TERM)
{
TypeNode btn = nm->booleanType();
return cur;
}
-std::string LfscNodeConverter::getNameForUserName(const std::string& name)
+std::string LfscNodeConverter::getNameForUserName(const std::string& name,
+ size_t variant)
{
// For user name X, we do cvc.Y, where Y contains an escaped version of X.
// Specifically, since LFSC does not allow these characters in identifier
// The "cvc." prefix ensures we do not clash with LFSC definitions.
//
// The escaping ensures that all names are valid LFSC identifiers.
- std::string sanitized("cvc.");
+ std::stringstream ss;
+ ss << "cvc";
+ if (variant != 0)
+ {
+ ss << variant;
+ }
+ ss << ".";
+ std::string sanitized = ss.str();
size_t found = sanitized.size();
sanitized += name;
// The following sanitizes symbols that are not allowed in LFSC identifiers
{
std::string name;
v.getAttribute(expr::VarNameAttr(), name);
- return getNameForUserName(name);
+ std::vector<Node>& syms = d_userSymbolList[name];
+ size_t variant = 0;
+ std::vector<Node>::iterator itr = std::find(syms.begin(), syms.end(), v);
+ if (itr != syms.cend())
+ {
+ variant = std::distance(syms.begin(), itr);
+ }
+ else
+ {
+ variant = syms.size();
+ syms.push_back(v);
+ }
+ return getNameForUserName(name, variant);
}
bool LfscNodeConverter::shouldTraverse(Node n)
}
}
+Node LfscNodeConverter::convertBitVector(const BitVector& bv)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode btn = nm->booleanType();
+ TypeNode btnv = nm->mkFunctionType({btn, btn}, btn);
+ size_t w = bv.getSize();
+ Node ret = getSymbolInternal(CONST_BITVECTOR, btn, "bvn");
+ Node b0 = getSymbolInternal(CONST_BITVECTOR, btn, "b0");
+ Node b1 = getSymbolInternal(CONST_BITVECTOR, btn, "b1");
+ Node bvc = getSymbolInternal(CONST_BITVECTOR, btnv, "bvc");
+ for (size_t i = 0; i < w; i++)
+ {
+ Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
+ ret = nm->mkNode(APPLY_UF, bvc, arg, ret);
+ }
+ return ret;
+}
+
bool LfscNodeConverter::isIndexedOperatorKind(Kind k)
{
return k == REGEXP_LOOP || k == BITVECTOR_EXTRACT || k == BITVECTOR_REPEAT
|| k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND
|| k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT
- || k == INT_TO_BITVECTOR || k == IAND || k == APPLY_UPDATER
- || k == APPLY_TESTER;
+ || k == INT_TO_BITVECTOR || k == IAND
+ || k == FLOATINGPOINT_TO_FP_FLOATINGPOINT
+ || k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
+ || k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
+ || k == FLOATINGPOINT_TO_FP_REAL || k == FLOATINGPOINT_TO_FP_GENERIC
+ || k == APPLY_UPDATER || k == APPLY_TESTER;
}
std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
case IAND:
indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size)));
break;
+ case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ {
+ const FloatingPointToFPFloatingPoint& ffp =
+ n.getConst<FloatingPointToFPFloatingPoint>();
+ indices.push_back(nm->mkConstInt(ffp.getSize().exponentWidth()));
+ indices.push_back(nm->mkConstInt(ffp.getSize().significandWidth()));
+ }
+ break;
+ case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ {
+ const FloatingPointToFPIEEEBitVector& fbv =
+ n.getConst<FloatingPointToFPIEEEBitVector>();
+ indices.push_back(nm->mkConstInt(fbv.getSize().exponentWidth()));
+ indices.push_back(nm->mkConstInt(fbv.getSize().significandWidth()));
+ }
+ break;
+ case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ {
+ const FloatingPointToFPSignedBitVector& fsbv =
+ n.getConst<FloatingPointToFPSignedBitVector>();
+ indices.push_back(nm->mkConstInt(fsbv.getSize().exponentWidth()));
+ indices.push_back(nm->mkConstInt(fsbv.getSize().significandWidth()));
+ }
+ break;
+ case FLOATINGPOINT_TO_FP_REAL:
+ {
+ const FloatingPointToFPReal& fr = n.getConst<FloatingPointToFPReal>();
+ indices.push_back(nm->mkConstInt(fr.getSize().exponentWidth()));
+ indices.push_back(nm->mkConstInt(fr.getSize().significandWidth()));
+ }
+ break;
+ case FLOATINGPOINT_TO_FP_GENERIC:
+ {
+ const FloatingPointToFPGeneric& fg =
+ n.getConst<FloatingPointToFPGeneric>();
+ indices.push_back(nm->mkConstInt(fg.getSize().exponentWidth()));
+ indices.push_back(nm->mkConstInt(fg.getSize().significandWidth()));
+ }
+ break;
case APPLY_TESTER:
{
unsigned index = DType::indexOf(n);
opName << "f_";
}
}
- opName << printer::smt2::Smt2Printer::smtKindString(k);
+ // must avoid overloading for to_fp variants
+ if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
+ {
+ opName << "to_fp_fp";
+ }
+ else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
+ {
+ opName << "to_fp_ieee_bv";
+ }
+ else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
+ {
+ opName << "to_fp_sbv";
+ }
+ else if (k == FLOATINGPOINT_TO_FP_REAL)
+ {
+ opName << "to_fp_real";
+ }
+ else if (k == FLOATINGPOINT_TO_FP_GENERIC)
+ {
+ opName << "to_fp_generic";
+ }
+ else
+ {
+ opName << printer::smt2::Smt2Printer::smtKindString(k);
+ }
}
else if (k == APPLY_CONSTRUCTOR)
{
// get its variable name
opName << getNameForUserNameOf(dt[index].getConstructor());
}
- else if (k == APPLY_SELECTOR)
+ else if (k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL)
{
if (k == APPLY_SELECTOR_TOTAL)
{
unsigned index = DType::indexOf(op);
const DType& dt = DType::datatypeOf(op);
unsigned cindex = DType::cindexOf(op);
- std::stringstream sss;
- sss << dt[cindex][index].getSelector();
- opName << getNameForUserName(sss.str());
+ opName << getNameForUserNameOf(dt[cindex][index].getSelector());
}
}
else if (k == SET_SINGLETON || k == BAG_MAKE)
}
if (ret.isNull())
{
+ Trace("lfsc-term-process-debug2") << "...default symbol" << std::endl;
ret = getSymbolInternal(k, ftype, opName.str());
}
// if indexed, apply to index
projects / cvc5.git / commitdiff