{
case DIVISIBLE:
{
- t = d_solver->mkValHelper<Rational>(
+ t = d_solver->mkRationalValHelper(
Rational(d_node->getConst<Divisible>().k));
break;
}
case BITVECTOR_REPEAT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRepeat>().d_repeatAmount);
break;
}
case BITVECTOR_ZERO_EXTEND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount);
break;
}
case BITVECTOR_SIGN_EXTEND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorSignExtend>().d_signExtendAmount);
break;
}
case BITVECTOR_ROTATE_LEFT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount);
break;
}
case BITVECTOR_ROTATE_RIGHT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount);
break;
}
case INT_TO_BITVECTOR:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<IntToBitVector>().d_size);
break;
}
case IAND:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
- d_node->getConst<IntAnd>().d_size);
+ t = d_solver->mkRationalValHelper(d_node->getConst<IntAnd>().d_size);
break;
}
case FLOATINGPOINT_TO_UBV:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size);
break;
}
case FLOATINGPOINT_TO_SBV:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size);
break;
}
case REGEXP_REPEAT:
{
- t = d_solver->mkValHelper<cvc5::Rational>(
+ t = d_solver->mkRationalValHelper(
d_node->getConst<RegExpRepeat>().d_repeatAmount);
break;
}
case BITVECTOR_EXTRACT:
{
cvc5::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_high)
- : d_solver->mkValHelper<cvc5::Rational>(ext.d_low);
+ t = index == 0 ? d_solver->mkRationalValHelper(ext.d_high)
+ : d_solver->mkRationalValHelper(ext.d_low);
break;
}
case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
cvc5::FloatingPointToFPIEEEBitVector ext =
d_node->getConst<FloatingPointToFPIEEEBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
{
cvc5::FloatingPointToFPFloatingPoint ext =
d_node->getConst<FloatingPointToFPFloatingPoint>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_REAL:
cvc5::FloatingPointToFPReal ext =
d_node->getConst<FloatingPointToFPReal>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
{
cvc5::FloatingPointToFPSignedBitVector ext =
d_node->getConst<FloatingPointToFPSignedBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
{
cvc5::FloatingPointToFPUnsignedBitVector ext =
d_node->getConst<FloatingPointToFPUnsignedBitVector>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case FLOATINGPOINT_TO_FP_GENERIC:
{
cvc5::FloatingPointToFPGeneric ext =
d_node->getConst<FloatingPointToFPGeneric>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().exponentWidth())
- : d_solver->mkValHelper<cvc5::Rational>(
- ext.getSize().significandWidth());
+ t = index == 0
+ ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth())
+ : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
break;
}
case REGEXP_LOOP:
{
cvc5::RegExpLoop ext = d_node->getConst<RegExpLoop>();
- t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMinOcc)
- : d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMaxOcc);
+ t = index == 0 ? d_solver->mkRationalValHelper(ext.d_loopMinOcc)
+ : d_solver->mkRationalValHelper(ext.d_loopMaxOcc);
break;
}
{
const std::vector<uint32_t>& projectionIndices =
d_node->getConst<TupleProjectOp>().getIndices();
- t = d_solver->mkValHelper<cvc5::Rational>(projectionIndices[index]);
+ t = d_solver->mkRationalValHelper(projectionIndices[index]);
break;
}
default:
return Term(this, res);
}
+Term Solver::mkRationalValHelper(const Rational& r) const
+{
+ //////// all checks before this line
+ Node res = getNodeManager()->mkConst(kind::CONST_RATIONAL, r);
+ (void)res.getType(true); /* kick off type checking */
+ return Term(this, res);
+}
+
Term Solver::mkRealFromStrHelper(const std::string& s) const
{
//////// all checks before this line
cvc5::Rational r = s.find('/') != std::string::npos
? cvc5::Rational(s)
: cvc5::Rational::fromDecimal(s);
- return mkValHelper<cvc5::Rational>(r);
+ return mkRationalValHelper(r);
}
catch (const std::invalid_argument& e)
{
res = Term(this,
d_nodeMgr->mkNode(extToIntKind(DIVISION),
*res.d_node,
- d_nodeMgr->mkConst(cvc5::Rational(1))));
+ d_nodeMgr->mkConst(kind::CONST_RATIONAL,
+ cvc5::Rational(1))));
}
Assert(res.getSort() == sort);
return res;
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term integer = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
+ Term integer = mkRationalValHelper(cvc5::Rational(val));
Assert(integer.getSort() == getIntegerSort());
return integer;
////////
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
+ Term rational = mkRationalValHelper(cvc5::Rational(val));
return ensureRealSort(rational);
////////
CVC5_API_TRY_CATCH_END;
{
CVC5_API_TRY_CATCH_BEGIN;
//////// all checks before this line
- Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(num, den));
+ Term rational = mkRationalValHelper(cvc5::Rational(num, den));
return ensureRealSort(rational);
////////
CVC5_API_TRY_CATCH_END;
class TypeNode;
class Options;
class Random;
+class Rational;
class Result;
class StatisticsRegistry;
/** Helper for mk-functions that call d_nodeMgr->mkConst(). */
template <typename T>
Term mkValHelper(T t) const;
+ /** Helper for making rational values. */
+ Term mkRationalValHelper(const Rational& r) const;
/** Helper for mkReal functions that take a string as argument. */
Term mkRealFromStrHelper(const std::string& s) const;
/** Helper for mkBitVector functions that take a string as argument. */
#include "expr/node_manager_attributes.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
BoundVarManager::BoundVarManager() : d_keepCacheVals(false) {}
Node BoundVarManager::getCacheValue(size_t i)
{
- return NodeManager::currentNM()->mkConst(Rational(i));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(i));
}
Node BoundVarManager::getCacheValue(TNode cv, size_t i)
ss << "sel_" << index;
SkolemManager* sm = nm->getSkolemManager();
TypeNode stype = nm->mkSelectorType(dtt, t);
- Node nindex = nm->mkConst(Rational(index));
+ Node nindex = nm->mkConst(CONST_RATIONAL, Rational(index));
s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex);
d_sharedSel[dtt][t][index] = s;
Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
echo "$kf:$lineno: warning: constant $1 hasher \`$4' isn't fully-qualified (e.g., ::cvc5::RationalHashFunction)" >&2
fi
+ if [[ "$3" =~ '+'$ ]]; then
+ # Remove last character
+ class="${3%?}"
+ skip_const_map=true
+ else
+ class="$3"
+ skip_const_map=false
+ fi
+
if [[ "$2" != "skip" ]]; then
metakind_fwd_decls="${metakind_fwd_decls}
-$2 $3;"
+$2 ${class};"
fi
# Avoid including the same header multiple times
register_metakind CONSTANT "$1" 0
metakind_getConst_decls="${metakind_getConst_decls}
template <>
-$3 const& NodeValue::getConst< $3 >() const;
+${class} const& NodeValue::getConst< ${class} >() const;
"
- metakind_constantMaps_decls="${metakind_constantMaps_decls}
+ if [ "${skip_const_map}" != true ]; then
+ metakind_constantMaps_decls="${metakind_constantMaps_decls}
template <>
-struct ConstantMap< $3 > {
- // typedef $theory_class OwningTheory;
- enum { kind = ::cvc5::kind::$1 };
-};/* ConstantMap< $3 > */
+struct ConstantMap< ${class} > {
+ static constexpr Kind kind = ::cvc5::kind::$1;
+};/* ConstantMap< ${class} > */
+"
+ fi
+ metakind_constantMaps_decls="${metakind_constantMaps_decls}
template <>
struct ConstantMapReverse< ::cvc5::kind::$1 > {
- typedef $3 T;
+ using T = ${class};
};/* ConstantMapReverse< ::cvc5::kind::$1 > */
- "
+"
+
metakind_constantMaps="${metakind_constantMaps}
-// The reinterpret_cast of d_children to \"$3 const*\"
+// The reinterpret_cast of d_children to \"${class} const*\"
// flags a \"strict aliasing\" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored \"-Wstrict-aliasing\"
template <>
-$3 const& NodeValue::getConst< $3 >() const {
+${class} const& NodeValue::getConst< ${class} >() const {
AssertArgument(getKind() == ::cvc5::kind::$1, *this,
- \"Improper kind for getConst<$3>()\");
+ \"Improper kind for getConst<${class}>()\");
// To support non-inlined CONSTANT-kinded NodeValues (those that are
// \"constructed\" when initially checking them against the NodeManager
// pool), we must check d_nchildren here.
return d_nchildren == 0
- ? *reinterpret_cast< $3 const* >(d_children)
- : *reinterpret_cast< $3 const* >(d_children[0]);
+ ? *reinterpret_cast< ${class} const* >(d_children)
+ : *reinterpret_cast< ${class} const* >(d_children[0]);
}
// re-enable the warning
"
metakind_constHashes="${metakind_constHashes}
case kind::$1:
- return $4()(nv->getConst< $3 >());
+ return $4()(nv->getConst< ${class} >());
"
metakind_constPrinters="${metakind_constPrinters}
case kind::$1:
- out << nv->getConst< $3 >();
+ out << nv->getConst< ${class} >();
break;
"
- cname=`echo "$3" | awk 'BEGIN {FS="::"} {print$NF}'`
+ cname=`echo "${class}" | awk 'BEGIN {FS="::"} {print$NF}'`
metakind_constDeleters="${metakind_constDeleters}
case kind::$1:
- std::destroy_at(reinterpret_cast< $3* >(nv->d_children));
+ std::destroy_at(reinterpret_cast< ${class}* >(nv->d_children));
break;
"
}
case OR: nullTerm = nm->mkConst(false); break;
case AND:
case SEP_STAR: nullTerm = nm->mkConst(true); break;
- case PLUS: nullTerm = nm->mkConst(Rational(0)); break;
+ case PLUS: nullTerm = nm->mkConst(CONST_RATIONAL, Rational(0)); break;
case MULT:
- case NONLINEAR_MULT: nullTerm = nm->mkConst(Rational(1)); break;
+ case NONLINEAR_MULT:
+ nullTerm = nm->mkConst(CONST_RATIONAL, Rational(1));
+ break;
case STRING_CONCAT:
// handles strings and sequences
nullTerm = theory::strings::Word::mkEmptyWord(tn);
template <class T>
Node mkConst(const T&);
+ /**
+ * Create a constant of type `T` with an explicit kind `k`.
+ */
+ template <class T>
+ Node mkConst(Kind k, const T&);
+
template <class T>
TypeNode mkTypeConst(const T&);
template <class NodeClass, class T>
- NodeClass mkConstInternal(const T&);
+ NodeClass mkConstInternal(Kind k, const T&);
/** Create a node with children. */
TypeNode mkTypeNode(Kind kind, TypeNode child1);
template <class T>
Node NodeManager::mkConst(const T& val) {
- return mkConstInternal<Node, T>(val);
+ return mkConstInternal<Node, T>(kind::metakind::ConstantMap<T>::kind, val);
+}
+
+template <class T>
+Node NodeManager::mkConst(Kind k, const T& val)
+{
+ return mkConstInternal<Node, T>(k, val);
}
template <class T>
TypeNode NodeManager::mkTypeConst(const T& val) {
- return mkConstInternal<TypeNode, T>(val);
+ return mkConstInternal<TypeNode, T>(kind::metakind::ConstantMap<T>::kind,
+ val);
}
template <class NodeClass, class T>
-NodeClass NodeManager::mkConstInternal(const T& val) {
- // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
+NodeClass NodeManager::mkConstInternal(Kind k, const T& val)
+{
NVStorage<1> nvStorage;
expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
nvStack.d_id = 0;
- nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
+ nvStack.d_kind = k;
nvStack.d_rc = 0;
nvStack.d_nchildren = 1;
}
nv->d_nchildren = 0;
- nv->d_kind = kind::metakind::ConstantMap<T>::kind;
+ nv->d_kind = k;
nv->d_id = next_id++;// FIXME multithreading
nv->d_rc = 0;
- //OwningTheory::mkConst(val);
new (&nv->d_children) T(val);
poolInsert(nv);
#include "expr/term_context.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
TCtxNode::TCtxNode(Node n, const TermContext* tctx)
Node TCtxNode::computeNodeHash(Node n, uint32_t val)
{
NodeManager* nm = NodeManager::currentNM();
- return nm->mkNode(kind::SEXPR, n, nm->mkConst(Rational(val)));
+ return nm->mkNode(kind::SEXPR, n, nm->mkConst(CONST_RATIONAL, Rational(val)));
}
Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val)
using namespace std;
using namespace cvc5;
using namespace cvc5::parser;
-using namespace cvc5::kind;
namespace cvc5 {
namespace parser {
using namespace std;
using namespace cvc5;
using namespace cvc5::parser;
-using namespace cvc5::kind;
namespace cvc5 {
namespace parser {
#include "smt/command.h"
using namespace std;
-using namespace cvc5::kind;
namespace cvc5 {
namespace parser {
namespace passes {
using namespace std;
+using namespace cvc5::kind;
using namespace cvc5::theory;
using namespace cvc5::theory::bv;
{
Assert(k > 0);
Rational max_value = intpow2(k) - 1;
- return d_nm->mkConst<Rational>(max_value);
+ return d_nm->mkConst(CONST_RATIONAL, max_value);
}
Node BVToInt::pow2(uint64_t k)
{
Assert(k >= 0);
- return d_nm->mkConst<Rational>(intpow2(k));
+ return d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(k)));
}
Node BVToInt::modpow2(Node n, uint64_t exponent)
{
- Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
+ Node p2 = d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(exponent)));
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
}
Rational max_of_amount = intpow2(amount) - 1;
Rational mul = max_of_amount * intpow2(bvsize);
Rational sum = mul + c;
- returnNode = d_nm->mkConst(sum);
+ returnNode = d_nm->mkConst(CONST_RATIONAL, sum);
}
}
else
else
{
Rational twoToKMinusOne(intpow2(bvsize - 1));
- Node minSigned = d_nm->mkConst(twoToKMinusOne);
+ Node minSigned = d_nm->mkConst(CONST_RATIONAL, twoToKMinusOne);
/* condition checks whether the msb is 1.
* This holds when the integer value is smaller than
* 100...0, which is 2^{bvsize-1}.
// Bit-vector constants are transformed into their integer value.
BitVector constant(original.getConst<BitVector>());
Integer c = constant.toInteger();
- translation = d_nm->mkConst<Rational>(c);
+ translation = d_nm->mkConst(CONST_RATIONAL, Rational(c));
}
else
{
d_rangeAssertions(userContext())
{
d_nm = NodeManager::currentNM();
- d_zero = d_nm->mkConst<Rational>(0);
- d_one = d_nm->mkConst<Rational>(1);
+ d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
};
PreprocessingPassResult BVToInt::applyInternal(
{
body = d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i));
}
- ite = d_nm->mkNode(kind::ITE,
- d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(i)),
- body,
- ite);
+ ite = d_nm->mkNode(
+ kind::ITE,
+ d_nm->mkNode(
+ kind::EQUAL, y, d_nm->mkConst(CONST_RATIONAL, Rational(i))),
+ body,
+ ite);
}
return ite;
}
#include "theory/trust_substitutions.h"
#include "util/rational.h"
+using namespace std;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+
namespace cvc5 {
namespace preprocessing {
namespace passes {
-using namespace std;
-using namespace cvc5::theory;
-
namespace {
/**
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)),
+ one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node trueNode = nm->mkConst(true);
unordered_map<TNode, Node> intVars;
NodeBuilder sumb(kind::PLUS);
for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
{
- sumb << nm->mkNode(
- kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]);
+ sumb << nm->mkNode(kind::MULT,
+ nm->mkConst(CONST_RATIONAL, coef[pos_var][jj]),
+ newVars[jj]);
}
sum = sumb;
}
else
{
- sum = nm->mkNode(
- kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]);
+ sum = nm->mkNode(kind::MULT,
+ nm->mkConst(CONST_RATIONAL, coef[pos_var][0]),
+ newVars[0]);
}
Debug("miplib") << "vars[] " << var << endl
<< " eq " << rewrite(sum) << endl;
#include "theory/theory_model.h"
#include "util/rational.h"
+using namespace cvc5::kind;
using namespace cvc5::theory;
namespace cvc5 {
{
Assert(c.isConst());
coeffs.push_back(NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL,
Rational(c.getConst<Rational>().getDenominator())));
}
}
Node s;
if (c.isNull())
{
- c = cc.isNull() ? NodeManager::currentNM()->mkConst(Rational(1))
+ c = cc.isNull() ? NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL, Rational(1))
: cc;
}
else
}
Node sumt =
sum.empty()
- ? NodeManager::currentNM()->mkConst(Rational(0))
+ ? NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(0))
: (sum.size() == 1
? sum[0]
: NodeManager::currentNM()->mkNode(kind::PLUS, sum));
ret = NodeManager::currentNM()->mkNode(
ret_lit.getKind(),
sumt,
- NodeManager::currentNM()->mkConst(Rational(0)));
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)));
if (!ret_pol)
{
ret = ret.negate();
#include "util/bitvector.h"
#include "util/rational.h"
+using namespace std;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+
namespace cvc5 {
namespace preprocessing {
namespace passes {
-using namespace std;
-using namespace cvc5::theory;
-
UnconstrainedSimplifier::UnconstrainedSimplifier(
PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "unconstrained-simplifier"),
if (current.getType().isInteger())
{
// div/mult by 1 should have been simplified
- Assert(other != nm->mkConst<Rational>(1));
+ Assert(other != nm->mkConst(CONST_RATIONAL, Rational(1)));
// div by -1 should have been simplified
- if (other != nm->mkConst<Rational>(-1))
+ if (other != nm->mkConst(CONST_RATIONAL, Rational(-1)))
{
break;
}
else
{
// TODO(#2377): could build ITE here
- Node test = other.eqNode(nm->mkConst<Rational>(0));
+ Node test =
+ other.eqNode(nm->mkConst(CONST_RATIONAL, Rational(0)));
if (rewrite(test) != nm->mkConst<bool>(false))
{
break;
#include "theory/builtin/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace proof {
res,
nm->mkNode(kind::SEXPR, d_cl, res),
children,
- {nm->mkConst(Rational(1))},
+ {nm->mkConst(CONST_RATIONAL, Rational(1))},
*cdp);
}
default:
{
Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res);
std::vector<Node> new_children = {vp1, children[0]};
- new_args.push_back(nm->mkConst<Rational>(1));
+ new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1));
return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
&& addAletheStep(AletheRule::RESOLUTION,
res,
{
Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res);
std::vector<Node> new_children = {vp1, children[0]};
- new_args.push_back(nm->mkConst<Rational>(1));
+ new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1));
return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
&& addAletheStep(AletheRule::RESOLUTION,
res,
}
std::vector<Node> new_args = std::vector<Node>();
- new_args.push_back(
- NodeManager::currentNM()->mkConst<Rational>(static_cast<unsigned>(rule)));
+ new_args.push_back(NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL, Rational(static_cast<unsigned>(rule))));
new_args.push_back(res);
new_args.push_back(sanitized_conclusion);
new_args.insert(new_args.end(), args.begin(), args.end());
}
// bound variable v is (bvar x T)
TypeNode intType = nm->integerType();
- Node x = nm->mkConst(Rational(getOrAssignIndexForVar(n)));
+ Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
Node tc = typeAsNode(convertType(tn));
TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn);
Node bvarOp = getSymbolInternal(k, ftype, "bvar");
TypeNode intType = nm->integerType();
TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn);
Node var = mkInternalSymbol("var", varType);
- Node index = nm->mkConst(Rational(getOrAssignIndexForVar(n)));
+ Node index =
+ nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
Node tc = typeAsNode(convertType(tn));
return nm->mkNode(APPLY_UF, var, index, tc);
}
{
// use LFSC syntax for mpz negation
Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~");
- arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(r.abs()));
+ arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs()));
}
else
{
Node rop = getSymbolInternal(
k, relType, printer::smt2::Smt2Printer::smtKindString(k));
RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
- Node n1 = nm->mkConst(Rational(op.d_loopMinOcc));
- Node n2 = nm->mkConst(Rational(op.d_loopMaxOcc));
+ Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc));
+ Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc));
return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]);
}
else if (k == MATCH)
else if (k == BITVECTOR_TYPE)
{
tnn = d_typeKindToNodeCons[k];
- Node w = nm->mkConst(Rational(tn.getBitVectorSize()));
+ Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize()));
tnn = nm->mkNode(APPLY_UF, tnn, w);
}
else if (k == FLOATINGPOINT_TYPE)
{
tnn = d_typeKindToNodeCons[k];
- Node e = nm->mkConst(Rational(tn.getFloatingPointExponentSize()));
- Node s = nm->mkConst(Rational(tn.getFloatingPointSignificandSize()));
+ Node e = nm->mkConst(CONST_RATIONAL,
+ Rational(tn.getFloatingPointExponentSize()));
+ Node s = nm->mkConst(CONST_RATIONAL,
+ Rational(tn.getFloatingPointSignificandSize()));
tnn = nm->mkNode(APPLY_UF, tnn, e, s);
}
else if (tn.getNumChildren() == 0)
Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char");
for (unsigned i = 0, size = vec.size(); i < size; i++)
{
- Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConst(Rational(vec[i])));
+ Node cc = nm->mkNode(
+ APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i])));
chars.push_back(cc);
}
}
case BITVECTOR_EXTRACT:
{
BitVectorExtract p = n.getConst<BitVectorExtract>();
- indices.push_back(nm->mkConst(Rational(p.d_high)));
- indices.push_back(nm->mkConst(Rational(p.d_low)));
+ indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high)));
+ indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low)));
break;
}
case BITVECTOR_REPEAT:
indices.push_back(
- nm->mkConst(Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
+ nm->mkConst(CONST_RATIONAL,
+ Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
break;
case BITVECTOR_ZERO_EXTEND:
indices.push_back(nm->mkConst(
+ CONST_RATIONAL,
Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount)));
break;
case BITVECTOR_SIGN_EXTEND:
indices.push_back(nm->mkConst(
+ CONST_RATIONAL,
Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount)));
break;
case BITVECTOR_ROTATE_LEFT:
indices.push_back(nm->mkConst(
+ CONST_RATIONAL,
Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount)));
break;
case BITVECTOR_ROTATE_RIGHT:
indices.push_back(nm->mkConst(
+ CONST_RATIONAL,
Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount)));
break;
case INT_TO_BITVECTOR:
- indices.push_back(
- nm->mkConst(Rational(n.getConst<IntToBitVector>().d_size)));
+ indices.push_back(nm->mkConst(
+ CONST_RATIONAL, Rational(n.getConst<IntToBitVector>().d_size)));
break;
case IAND:
- indices.push_back(nm->mkConst(Rational(n.getConst<IntAnd>().d_size)));
+ indices.push_back(
+ nm->mkConst(CONST_RATIONAL, Rational(n.getConst<IntAnd>().d_size)));
break;
case APPLY_TESTER:
{
Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
{
NodeManager* nm = NodeManager::currentNM();
- Node x = nm->mkConst(Rational(getOrAssignIndexForVar(v)));
+ Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v)));
Node tc = typeAsNode(convertType(v.getType()));
return nm->mkNode(APPLY_UF, cop, x, tc);
}
#include "proof/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace proof {
Node mkLfscRuleNode(LfscRule r)
{
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(r)));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(static_cast<uint32_t>(r)));
}
bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn)
#include "proof/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
const char* toString(MethodId id)
Node mkMethodId(MethodId id)
{
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(static_cast<uint32_t>(id)));
}
bool getMethodId(TNode n, MethodId& i)
// UNDEFINED_KIND is negative, hence return null to avoid cast
return Node::null();
}
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(static_cast<uint32_t>(k)));
}
ProofCheckerStatistics::ProofCheckerStatistics()
#include "theory/builtin/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace prop {
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
{
// Create a proof step for each n_i
- Node iNode = nm->mkConst<Rational>(i);
+ Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode});
Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
<< " added norm " << node[i] << "\n";
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
{
// Create a proof step for each (not n_i)
- Node iNode = nm->mkConst<Rational>(i);
+ Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
d_proof.addStep(
node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode});
Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
if (added)
{
Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]);
- Node iNode = nm->mkConst<Rational>(i);
+ Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode});
Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i
<< " added " << clauseNode << "\n";
if (added)
{
Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode());
- Node iNode = nm->mkConst<Rational>(i);
+ Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode});
Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
<< clauseNode << "\n";
NodeManager* nm = NodeManager::currentNM();
for (const std::pair<const Node, uint64_t>& d : d_accMap)
{
- dmap[d.first] = nm->mkConst(Rational(d.second));
+ dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second));
}
}
for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
j++)
{
- Node nodej = nm->mkConst(Rational(j));
+ Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j));
cdp->addStep(
children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
}
TNode child = children[i];
TNode scalar = args[i];
bool isPos = scalar.getConst<Rational>() > 0;
- Node scalarCmp =
- nm->mkNode(isPos ? GT : LT, scalar, nm->mkConst(Rational(0)));
+ Node scalarCmp = nm->mkNode(
+ isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0)));
// (= scalarCmp true)
Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp});
Assert(!scalarCmpOrTrue.isNull());
return nm->mkConst(true);
case OR:
return nm->mkConst(false);
- case PLUS:
- return nm->mkConst(Rational(0));
- case MULT:
- return nm->mkConst(Rational(1));
+ case PLUS: return nm->mkConst(CONST_RATIONAL, Rational(0));
+ case MULT: return nm->mkConst(CONST_RATIONAL, Rational(1));
default:
return Node::null();
}
std::map<Node, Node>::iterator it2 = msum.find(it->first);
if (it2 != msum.end())
{
- Node r = nm->mkNode(
- MINUS,
- it2->second.isNull() ? nm->mkConst(Rational(1)) : it2->second,
- it->second.isNull() ? nm->mkConst(Rational(1)) : it->second);
+ Node r = nm->mkNode(MINUS,
+ it2->second.isNull()
+ ? nm->mkConst(CONST_RATIONAL, Rational(1))
+ : it2->second,
+ it->second.isNull()
+ ? nm->mkConst(CONST_RATIONAL, Rational(1))
+ : it->second);
msum[it->first] = Rewriter::rewrite(r);
}
else
{
- msum[it->first] = it->second.isNull() ? nm->mkConst(Rational(-1))
- : negate(it->second);
+ msum[it->first] = it->second.isNull()
+ ? nm->mkConst(CONST_RATIONAL, Rational(-1))
+ : negate(it->second);
}
}
return true;
}
children.push_back(m);
}
- return children.size() > 1
- ? nm->mkNode(PLUS, children)
- : (children.size() == 1 ? children[0] : nm->mkConst(Rational(0)));
+ return children.size() > 1 ? nm->mkNode(PLUS, children)
+ : (children.size() == 1
+ ? children[0]
+ : nm->mkConst(CONST_RATIONAL, Rational(0)));
}
int ArithMSum::isolate(
}
val = children.size() > 1
? NodeManager::currentNM()->mkNode(PLUS, children)
- : (children.size() == 1
- ? children[0]
- : NodeManager::currentNM()->mkConst(Rational(0)));
+ : (children.size() == 1 ? children[0]
+ : NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL, Rational(0)));
if (!r.isOne() && !r.isNegativeOne())
{
if (v.getType().isInteger())
{
- veq_c = NodeManager::currentNM()->mkConst(r.abs());
+ veq_c = NodeManager::currentNM()->mkConst(CONST_RATIONAL, r.abs());
}
else
{
val = NodeManager::currentNM()->mkNode(
MULT,
val,
- NodeManager::currentNM()->mkConst(Rational(1) / r.abs()));
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(1) / r.abs()));
}
}
val = r.sgn() == 1 ? negate(val) : Rewriter::rewrite(val);
Node ArithMSum::negate(Node t)
{
Node tt = NodeManager::currentNM()->mkNode(
- MULT, NodeManager::currentNM()->mkConst(Rational(-1)), t);
+ MULT, NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1)), t);
tt = Rewriter::rewrite(tt);
return tt;
}
Node ArithMSum::offset(Node t, int i)
{
Node tt = NodeManager::currentNM()->mkNode(
- PLUS, NodeManager::currentNM()->mkConst(Rational(i)), t);
+ PLUS, NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(i)), t);
tt = Rewriter::rewrite(tt);
return tt;
}
#include "util/divisible.h"
#include "util/iand.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
if(rat >= 0) {
return RewriteResponse(REWRITE_DONE, t[0]);
} else {
- return RewriteResponse(REWRITE_DONE,
- NodeManager::currentNM()->mkConst(-rat));
+ return RewriteResponse(
+ REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, -rat));
}
}
return RewriteResponse(REWRITE_DONE, t);
if(rat >= 0) {
return RewriteResponse(REWRITE_DONE, t[0]);
} else {
- return RewriteResponse(REWRITE_DONE,
- NodeManager::currentNM()->mkConst(-rat));
+ return RewriteResponse(
+ REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, -rat));
}
}
return RewriteResponse(REWRITE_DONE, t);
case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]);
case kind::TO_INTEGER:
if(t[0].isConst()) {
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor())));
+ return RewriteResponse(
+ REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL, Rational(t[0].getConst<Rational>().floor())));
}
if(t[0].getType().isInteger()) {
return RewriteResponse(REWRITE_DONE, t[0]);
{
return RewriteResponse(
REWRITE_DONE,
- nm->mkConst<Rational>(Rational(Integer(0), Integer(1))));
+ nm->mkConst(CONST_RATIONAL, Rational(Integer(0), Integer(1))));
}
unsigned long k = i.getUnsignedLong();
- Node ret = nm->mkConst<Rational>(Rational(Integer(2).pow(k), Integer(1)));
+ Node ret =
+ nm->mkConst(CONST_RATIONAL, Rational(Integer(2).pow(k), Integer(1)));
return RewriteResponse(REWRITE_DONE, ret);
}
return RewriteResponse(REWRITE_DONE, t);
switch( t.getKind() ){
case kind::EXPONENTIAL: {
if(t[0].getKind() == kind::CONST_RATIONAL){
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
if(t[0].getConst<Rational>().sgn()>=0 && t[0].getType().isInteger() && t[0]!=one){
return RewriteResponse(
REWRITE_AGAIN,
if(t[0].getKind() == kind::CONST_RATIONAL){
const Rational& rat = t[0].getConst<Rational>();
if(rat.sgn() == 0){
- return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(0)));
+ return RewriteResponse(REWRITE_DONE,
+ nm->mkConst(CONST_RATIONAL, Rational(0)));
}
else if (rat.sgn() == -1)
{
- Node ret =
- nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, nm->mkConst(-rat)));
+ Node ret = nm->mkNode(
+ kind::UMINUS,
+ nm->mkNode(kind::SINE, nm->mkConst(CONST_RATIONAL, -rat)));
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
}else{
nm->mkNode(kind::SINE,
nm->mkNode(kind::MINUS,
nm->mkNode(kind::MULT,
- nm->mkConst(Rational(1) / Rational(2)),
+ nm->mkConst(CONST_RATIONAL,
+ Rational(1) / Rational(2)),
mkPi()),
t[0])));
}
if(atom.getOperator().getConst<Divisible>().k.isOne()) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
}
- return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], NodeManager::currentNM()->mkConst(Rational(atom.getOperator().getConst<Divisible>().k))), NodeManager::currentNM()->mkConst(Rational(0))));
+ return RewriteResponse(
+ REWRITE_AGAIN,
+ NodeManager::currentNM()->mkNode(
+ kind::EQUAL,
+ NodeManager::currentNM()->mkNode(
+ kind::INTS_MODULUS_TOTAL,
+ atom[0],
+ NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL,
+ Rational(atom.getOperator().getConst<Divisible>().k))),
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))));
}
// left |><| right
{
NodeManager* nm = NodeManager::currentNM();
Kind k = t.getKind();
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
if (k == kind::INTS_MODULUS)
{
if (t[1].isConst() && !t[1].getConst<Rational>().isZero())
// pull negation
// (div x (- c)) ---> (- (div x c))
// (mod x (- c)) ---> (mod x c)
- Node nn = nm->mkNode(k, t[0], nm->mkConst(-t[1].getConst<Rational>()));
+ Node nn = nm->mkNode(
+ k, t[0], nm->mkConst(CONST_RATIONAL, -t[1].getConst<Rational>()));
Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
? nm->mkNode(kind::UMINUS, nn)
: nn;
curr_r = Rational(curr - 1) / den;
}
curr_r = curr_r * pow_ten;
- cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
+ cret = nm->mkConst(CONST_RATIONAL, csign == 1 ? curr_r : -curr_r);
}
else
{
typedef DenseMap<Node> ArithVarToNodeMap;
inline Node mkRationalNode(const Rational& q){
- return NodeManager::currentNM()->mkConst<Rational>(q);
+ return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, q);
}
inline Node mkBoolNode(bool b){
#include "theory/arith/normal_form.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
auto* nm = NodeManager::currentNM();
switch (relation)
{
- case Kind::LEQ: bound = nm->mkConst<Rational>(br.floor()); break;
+ case Kind::LEQ:
+ bound = nm->mkConst<Rational>(CONST_RATIONAL, br.floor());
+ break;
case Kind::LT:
- bound = nm->mkConst<Rational>((br - 1).ceiling());
+ bound = nm->mkConst<Rational>(CONST_RATIONAL, (br - 1).ceiling());
relation = Kind::LEQ;
break;
case Kind::GT:
- bound = nm->mkConst<Rational>((br + 1).floor());
+ bound = nm->mkConst<Rational>(CONST_RATIONAL, (br + 1).floor());
relation = Kind::GEQ;
break;
- case Kind::GEQ: bound = nm->mkConst<Rational>(br.ceiling()); break;
+ case Kind::GEQ:
+ bound = nm->mkConst<Rational>(CONST_RATIONAL, br.ceiling());
+ break;
default:;
}
Trace("bound-inf") << "Strengthened " << n << " to " << lhs << " "
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_equality_engine.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
TNode isZero = d_watchedEqualities[s];
const auto isZeroPf = d_pnm->mkAssume(isZero);
const auto nm = NodeManager::currentNM();
- const auto sumPf = d_pnm->mkNode(
- PfRule::MACRO_ARITH_SCALE_SUM_UB,
- {isZeroPf, pf},
- // Trick for getting correct, opposing signs.
- {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});
+ const auto sumPf =
+ d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+ {isZeroPf, pf},
+ // Trick for getting correct, opposing signs.
+ {nm->mkConst(CONST_RATIONAL, Rational(-1 * cSign)),
+ nm->mkConst(CONST_RATIONAL, Rational(cSign))});
const auto botPf = d_pnm->mkNode(
PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
std::vector<Node> assumption = {isZero};
auto nGeqPf = d_database->d_pnm->mkAssume(geqNode.negate());
auto ltPf = d_database->d_pnm->mkNode(
PfRule::MACRO_SR_PRED_TRANSFORM, {nGeqPf}, {ltNode});
- auto sumPf = d_database->d_pnm->mkNode(
- PfRule::MACRO_ARITH_SCALE_SUM_UB,
- {gtPf, ltPf},
- {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
+ auto sumPf =
+ d_database->d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+ {gtPf, ltPf},
+ {nm->mkConst(CONST_RATIONAL, Rational(-1)),
+ nm->mkConst(CONST_RATIONAL, Rational(1))});
auto botPf = d_database->d_pnm->mkNode(
PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
std::vector<Node> a = {leqNode.negate(), geqNode.negate()};
std::vector<Node> farkasCoeffs;
for (Rational r : *getFarkasCoefficients())
{
- farkasCoeffs.push_back(nm->mkConst<Rational>(r));
+ farkasCoeffs.push_back(nm->mkConst(CONST_RATIONAL, Rational(r)));
}
// Apply the scaled-sum rule.
default: Unreachable() << d_type;
}
NodeManager* nm = NodeManager::currentNM();
- Node constPart = nm->mkConst<Rational>(d_value.getNoninfinitesimalPart());
+ Node constPart =
+ nm->mkConst(CONST_RATIONAL, Rational(d_value.getNoninfinitesimalPart()));
Node posLit = nm->mkNode(cmp, varPart, constPart);
return neg ? posLit.negate() : posLit;
}
{d_pnm->mkAssume(lb.negate())},
{b->getNegation()->getProofLiteral()});
int sndSign = negateSecond ? -1 : 1;
- auto bot_pf =
- d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
- {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
- {pf_neg_la, pf_neg_lb},
- {nm->mkConst<Rational>(-1 * sndSign),
- nm->mkConst<Rational>(sndSign)})},
- {nm->mkConst(false)});
+ auto bot_pf = d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM,
+ {d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+ {pf_neg_la, pf_neg_lb},
+ {nm->mkConst(CONST_RATIONAL, Rational(-1 * sndSign)),
+ nm->mkConst(CONST_RATIONAL, Rational(sndSign))})},
+ {nm->mkConst(false)});
std::vector<Node> as;
std::transform(orN.begin(), orN.end(), std::back_inserter(as), [](Node n) {
return n.negate();
#include "theory/arith/infer_bounds.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
Node InferBoundsResult::getLiteral() const{
const Rational& q = getValue().getNoninfinitesimalPart();
NodeManager* nm = NodeManager::currentNM();
- Node qnode = nm->mkConst(q);
+ Node qnode = nm->mkConst(CONST_RATIONAL, q);
Kind k;
if(d_upperBound){
sort REAL_TYPE \
Cardinality::REALS \
well-founded \
- "NodeManager::currentNM()->mkConst(Rational(0))" \
+ "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \
"expr/node_manager.h" \
"real type"
sort INTEGER_TYPE \
Cardinality::INTEGERS \
well-founded \
- "NodeManager::currentNM()->mkConst(Rational(0))" \
+ "NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0))" \
"expr/node_manager.h" \
"integer type"
constant CONST_RATIONAL \
class \
- Rational \
+ Rational+ \
::cvc5::RationalHashFunction \
"util/rational.h" \
"a multiple-precision rational constant; payload is an instance of the cvc5::Rational class"
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace std {
/** Generic streaming operator for std::vector. */
template <typename T>
// construct phi := (and (= p_i 0)) with p_i the coefficients of p
std::vector<Node> conditions;
- auto zero = NodeManager::currentNM()->mkConst(Rational(0));
+ auto zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
for (const auto& coeff : poly::coefficients(p))
{
conditions.emplace_back(NodeManager::currentNM()->mkNode(
#include "theory/arith/nl/poly_conversion.h"
#include "util/indexed_root_predicate.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
: d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
{
d_false = NodeManager::currentNM()->mkConst<bool>(false);
- d_zero = NodeManager::currentNM()->mkConst<Rational>(0);
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
void CADProofGenerator::startNewProof()
#include "theory/arith/nl/nl_model.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
{
d_false = NodeManager::currentNM()->mkConst(false);
d_true = NodeManager::currentNM()->mkConst(true);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
if (d_env.isTheoryProofProducing())
{
d_proof.reset(new CDProofSet<CDProof>(
#include "theory/rewriter.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
FactoringCheck::FactoringCheck(Env& env, ExtState* data)
: EnvObj(env), d_data(data)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
}
void FactoringCheck::check(const std::vector<Node>& asserts,
MonomialDb::MonomialDb()
{
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
}
void MonomialDb::registerMonomial(Node n)
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
proof->addStep(exp[1][0],
PfRule::AND_ELIM,
{exp[1]},
- {nm->mkConst(Rational(0))});
+ {nm->mkConst(CONST_RATIONAL, Rational(0))});
proof->addStep(exp[1][1],
PfRule::AND_ELIM,
{exp[1]},
- {nm->mkConst(Rational(1))});
+ {nm->mkConst(CONST_RATIONAL, Rational(1))});
Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]);
Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]);
if (rew->rewrite(lb) == rew->rewrite(exp[1][0]))
const std::vector<Node>& args)
{
NodeManager* nm = NodeManager::currentNM();
- auto zero = nm->mkConst<Rational>(0);
- auto one = nm->mkConst<Rational>(1);
- auto mone = nm->mkConst<Rational>(-1);
+ auto zero = nm->mkConst<Rational>(CONST_RATIONAL, 0);
+ auto one = nm->mkConst<Rational>(CONST_RATIONAL, 1);
+ auto mone = nm->mkConst<Rational>(CONST_RATIONAL, -1);
auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
auto mpi = nm->mkNode(Kind::MULT, mone, pi);
Trace("nl-ext-checker") << "Checking " << id << std::endl;
#include "theory/rewriter.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
if (d_data->isProofEnabled())
{
proof = d_data->getProof();
- proof->addStep(tlem,
- PfRule::ARITH_MULT_TANGENT,
- {},
- {t,
- a,
- b,
- a_v,
- b_v,
- nm->mkConst(Rational(d == 0 ? -1 : 1))});
+ proof->addStep(
+ tlem,
+ PfRule::ARITH_MULT_TANGENT,
+ {},
+ {t,
+ a,
+ b,
+ a_v,
+ b_v,
+ nm->mkConst(CONST_RATIONAL, Rational(d == 0 ? -1 : 1))});
}
d_data->d_im.addPendingLemma(tlem,
InferenceId::ARITH_NL_TANGENT_PLANE,
NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
bool NlExtTheoryCallback::getCurrentSubstitution(
NodeManager* nm = NodeManager::currentNM();
d_false = nm->mkConst(false);
d_true = nm->mkConst(true);
- d_zero = nm->mkConst(Rational(0));
- d_one = nm->mkConst(Rational(1));
- d_two = nm->mkConst(Rational(2));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+ d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
}
IAndSolver::~IAndSolver() {}
#include "theory/rewriter.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
{
Assert(k >= 0);
NodeManager* nm = NodeManager::currentNM();
- return nm->mkConst<Rational>(intpow2(k));
+ return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k)));
}
bool oneBitAnd(bool a, bool b) { return (a && b); }
IAndUtils::IAndUtils()
{
NodeManager* nm = NodeManager::currentNM();
- d_zero = nm->mkConst(Rational(0));
- d_one = nm->mkConst(Rational(1));
- d_two = nm->mkConst(Rational(2));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+ d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
}
Node IAndUtils::createITEFromTable(
Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
// start with the default, most common value.
// this value is represented in the table by (-1, -1).
- Node ite = nm->mkConst<Rational>(table.at(std::make_pair(-1, -1)));
+ Node ite =
+ nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(-1, -1))));
for (uint64_t i = 0; i < num_of_values; i++)
{
for (uint64_t j = 0; j < num_of_values; j++)
// append the current value to the ite.
ite = nm->mkNode(
kind::ITE,
- nm->mkNode(kind::AND,
- nm->mkNode(kind::EQUAL, x, nm->mkConst<Rational>(i)),
- nm->mkNode(kind::EQUAL, y, nm->mkConst<Rational>(j))),
- nm->mkConst<Rational>(table.at(std::make_pair(i, j))),
+ nm->mkNode(
+ kind::AND,
+ nm->mkNode(
+ kind::EQUAL, x, nm->mkConst(CONST_RATIONAL, Rational(i))),
+ nm->mkNode(
+ kind::EQUAL, y, nm->mkConst(CONST_RATIONAL, Rational(j)))),
+ nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(i, j)))),
ite);
}
}
// number of elements in the sum expression
uint64_t sumSize = bvsize / granularity;
// initialize the sum
- Node sumNode = nm->mkConst<Rational>(0);
+ Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0));
// compute the table for the current granularity if needed
if (d_bvandTable.find(granularity) == d_bvandTable.end())
{
{
// could be faster
NodeManager* nm = NodeManager::currentNM();
- Node ret = nm->mkNode(kind::POW, d_two, nm->mkConst(Rational(k)));
+ Node ret =
+ nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k)));
ret = Rewriter::rewrite(ret);
return ret;
}
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- d_two = NodeManager::currentNM()->mkConst(Rational(2));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_two = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(2));
}
NlModel::~NlModel() {}
Assert(false);
return false;
}
- Node val = nm->mkConst(-c.getConst<Rational>() / b.getConst<Rational>());
+ Node val = nm->mkConst(CONST_RATIONAL,
+ -c.getConst<Rational>() / b.getConst<Rational>());
if (Trace.isOn("nl-ext-cm"))
{
Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = ";
if (witnessToValue)
{
// witness is the midpoint
- witness = nm->mkNode(
- MULT, nm->mkConst(Rational(1, 2)), nm->mkNode(PLUS, l, u));
+ witness = nm->mkNode(MULT,
+ nm->mkConst(CONST_RATIONAL, Rational(1, 2)),
+ nm->mkNode(PLUS, l, u));
witness = Rewriter::rewrite(witness);
Trace("nl-model") << v << " witness is " << witness << std::endl;
}
d_extTheory.addFunctionKind(kind::IAND);
d_extTheory.addFunctionKind(kind::POW2);
d_true = NodeManager::currentNM()->mkConst(true);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
if (d_env.isTheoryProofProducing())
{
#include "theory/arith/bound_inference.h"
#include "util/poly_util.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
auto* nm = NodeManager::currentNM();
- Node res = nm->mkConst(Rational(0));
- Node monomial = nm->mkConst(Rational(1));
+ Node res = nm->mkConst(CONST_RATIONAL, Rational(0));
+ Node monomial = nm->mkConst(CONST_RATIONAL, Rational(1));
for (std::size_t i = 0, n = coeffs.size(); i < n; ++i)
{
if (!is_zero(coeffs[i]))
{
- Node coeff = nm->mkConst(poly_utils::toRational(coeffs[i]));
+ Node coeff =
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRational(coeffs[i]));
Node term = nm->mkNode(Kind::MULT, coeff, monomial);
res = nm->mkNode(Kind::PLUS, res, term);
}
{
CollectMonomialData* d = static_cast<CollectMonomialData*>(data);
// constant
- Node term =
- d->d_nm->mkConst<Rational>(poly_utils::toRational(poly::Integer(&m->a)));
+ Node term = d->d_nm->mkConst<Rational>(
+ CONST_RATIONAL, poly_utils::toRational(poly::Integer(&m->a)));
for (std::size_t i = 0; i < m->n; ++i)
{
// variable exponent pair
Node var = d->d_vm(m->p[i].x);
if (m->p[i].d > 1)
{
- Node exp = d->d_nm->mkConst<Rational>(m->p[i].d);
+ Node exp = d->d_nm->mkConst<Rational>(CONST_RATIONAL, m->p[i].d);
term = d->d_nm->mkNode(
Kind::NONLINEAR_MULT, term, d->d_nm->mkNode(Kind::POW, var, exp));
}
if (cmd.d_terms.empty())
{
- return cmd.d_nm->mkConst<Rational>(0);
+ return cmd.d_nm->mkConst<Rational>(CONST_RATIONAL, 0);
}
if (cmd.d_terms.size() == 1)
{
const poly::DyadicInterval& di = get_isolating_interval(an);
if (is_point(di))
{
- return nm->mkConst(poly_utils::toRational(get_point(di)));
+ return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_point(di)));
}
Assert(di.get_internal()->a_open && di.get_internal()->b_open)
<< "We assume an open interval here.";
Node poly = as_cvc_upolynomial(get_defining_polynomial(an), ran_variable);
- Node lower = nm->mkConst(poly_utils::toRational(get_lower(di)));
- Node upper = nm->mkConst(poly_utils::toRational(get_upper(di)));
+ Node lower =
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_lower(di)));
+ Node upper =
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRational(get_upper(di)));
// Construct witness:
- return nm->mkNode(Kind::AND,
- // poly(var) == 0
- nm->mkNode(Kind::EQUAL, poly, nm->mkConst(Rational(0))),
- // lower_bound < var
- nm->mkNode(Kind::LT, lower, ran_variable),
- // var < upper_bound
- nm->mkNode(Kind::LT, ran_variable, upper));
+ return nm->mkNode(
+ Kind::AND,
+ // poly(var) == 0
+ nm->mkNode(Kind::EQUAL, poly, nm->mkConst(CONST_RATIONAL, Rational(0))),
+ // lower_bound < var
+ nm->mkNode(Kind::LT, lower, ran_variable),
+ // var < upper_bound
+ nm->mkNode(Kind::LT, ran_variable, upper));
}
Node value_to_node(const poly::Value& v, const Node& ran_variable)
auto* nm = NodeManager::currentNM();
if (is_dyadic_rational(v))
{
- return nm->mkConst(poly_utils::toRational(as_dyadic_rational(v)));
+ return nm->mkConst(CONST_RATIONAL,
+ poly_utils::toRational(as_dyadic_rational(v)));
}
if (is_integer(v))
{
- return nm->mkConst(poly_utils::toRational(as_integer(v)));
+ return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(as_integer(v)));
}
if (is_rational(v))
{
- return nm->mkConst(poly_utils::toRational(as_rational(v)));
+ return nm->mkConst(CONST_RATIONAL, poly_utils::toRational(as_rational(v)));
}
Assert(false) << "All cases should be covered.";
- return nm->mkConst(Rational(0));
+ return nm->mkConst(CONST_RATIONAL, Rational(0));
}
Node lower_bound_as_node(const Node& var,
auto* nm = NodeManager::currentNM();
if (!poly::is_algebraic_number(lower))
{
- return nm->mkNode(open ? Kind::LEQ : Kind::LT,
- var,
- nm->mkConst(poly_utils::toRationalAbove(lower)));
+ return nm->mkNode(
+ open ? Kind::LEQ : Kind::LT,
+ var,
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(lower)));
}
if (poly::represents_rational(lower))
{
return nm->mkNode(
open ? Kind::LEQ : Kind::LT,
var,
- nm->mkConst(poly_utils::toRationalAbove(poly::get_rational(lower))));
+ nm->mkConst(CONST_RATIONAL,
+ poly_utils::toRationalAbove(poly::get_rational(lower))));
}
if (!allowNonlinearLemma)
{
}
return nm->mkNode(
Kind::OR,
- nm->mkNode(Kind::LEQ, var, nm->mkConst(l)),
- nm->mkNode(Kind::AND,
- nm->mkNode(Kind::LT, var, nm->mkConst(u)),
- nm->mkNode(relation, poly, nm->mkConst(Rational(0)))));
+ nm->mkNode(Kind::LEQ, var, nm->mkConst(CONST_RATIONAL, l)),
+ nm->mkNode(
+ Kind::AND,
+ nm->mkNode(Kind::LT, var, nm->mkConst(CONST_RATIONAL, u)),
+ nm->mkNode(
+ relation, poly, nm->mkConst(CONST_RATIONAL, Rational(0)))));
}
Node upper_bound_as_node(const Node& var,
auto* nm = NodeManager::currentNM();
if (!poly::is_algebraic_number(upper))
{
- return nm->mkNode(open ? Kind::GEQ : Kind::GT,
- var,
- nm->mkConst(poly_utils::toRationalAbove(upper)));
+ return nm->mkNode(
+ open ? Kind::GEQ : Kind::GT,
+ var,
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(upper)));
}
if (poly::represents_rational(upper))
{
return nm->mkNode(
open ? Kind::GEQ : Kind::GT,
var,
- nm->mkConst(poly_utils::toRationalAbove(poly::get_rational(upper))));
+ nm->mkConst(CONST_RATIONAL,
+ poly_utils::toRationalAbove(poly::get_rational(upper))));
}
if (!allowNonlinearLemma)
{
}
return nm->mkNode(
Kind::OR,
- nm->mkNode(Kind::GEQ, var, nm->mkConst(u)),
- nm->mkNode(Kind::AND,
- nm->mkNode(Kind::GT, var, nm->mkConst(l)),
- nm->mkNode(relation, poly, nm->mkConst(Rational(0)))));
+ nm->mkNode(Kind::GEQ, var, nm->mkConst(CONST_RATIONAL, u)),
+ nm->mkNode(
+ Kind::AND,
+ nm->mkNode(Kind::GT, var, nm->mkConst(CONST_RATIONAL, l)),
+ nm->mkNode(
+ relation, poly, nm->mkConst(CONST_RATIONAL, Rational(0)))));
}
Node excluding_interval_to_lemma(const Node& variable,
if (poly::is_rational(alg))
{
Trace("nl-cad") << "Rational point interval: " << interval << std::endl;
- return nm->mkNode(Kind::DISTINCT,
- variable,
- nm->mkConst(poly_utils::toRational(
- poly::to_rational_approximation(alg))));
+ return nm->mkNode(
+ Kind::DISTINCT,
+ variable,
+ nm->mkConst(
+ CONST_RATIONAL,
+ poly_utils::toRational(poly::to_rational_approximation(alg))));
}
Trace("nl-cad") << "Algebraic point interval: " << interval << std::endl;
// p(x) != 0 or x <= lb or ub <= x
Node poly = as_cvc_upolynomial(get_defining_polynomial(alg), variable);
return nm->mkNode(
Kind::OR,
- nm->mkNode(Kind::DISTINCT, poly, nm->mkConst(Rational(0))),
- nm->mkNode(Kind::LT,
- variable,
- nm->mkConst(poly_utils::toRationalBelow(lv))),
- nm->mkNode(Kind::GT,
- variable,
- nm->mkConst(poly_utils::toRationalAbove(lv))));
+ nm->mkNode(
+ Kind::DISTINCT, poly, nm->mkConst(CONST_RATIONAL, Rational(0))),
+ nm->mkNode(
+ Kind::LT,
+ variable,
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRationalBelow(lv))),
+ nm->mkNode(
+ Kind::GT,
+ variable,
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRationalAbove(lv))));
}
return Node();
}
else
{
Trace("nl-cad") << "Rational point interval: " << interval << std::endl;
- return nm->mkNode(Kind::DISTINCT,
- variable,
- nm->mkConst(poly_utils::toRationalBelow(lv)));
+ return nm->mkNode(
+ Kind::DISTINCT,
+ variable,
+ nm->mkConst(CONST_RATIONAL, poly_utils::toRationalBelow(lv)));
}
}
if (li)
NodeManager* nm = NodeManager::currentNM();
d_false = nm->mkConst(false);
d_true = nm->mkConst(true);
- d_zero = nm->mkConst(Rational(0));
- d_one = nm->mkConst(Rational(1));
- d_two = nm->mkConst(Rational(2));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+ d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
}
Pow2Solver::~Pow2Solver() {}
#include "theory/arith/nl/transcendental/transcendental_state.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
proof->addStep(lem,
PfRule::ARITH_TRANS_EXP_APPROX_BELOW,
{},
- {nm->mkConst<Rational>(d), e[0]});
+ {nm->mkConst(CONST_RATIONAL, Rational(d)), e[0]});
}
d_data->d_im.addPendingLemma(
lem, InferenceId::ARITH_NL_T_TANGENT, proof, true);
PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
{
NodeManager* nm = NodeManager::currentNM();
- auto zero = nm->mkConst<Rational>(0);
- auto one = nm->mkConst<Rational>(1);
- auto mone = nm->mkConst<Rational>(-1);
+ auto zero = nm->mkConst<Rational>(CONST_RATIONAL, 0);
+ auto one = nm->mkConst<Rational>(CONST_RATIONAL, 1);
+ auto mone = nm->mkConst<Rational>(CONST_RATIONAL, -1);
auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
auto mpi = nm->mkNode(Kind::MULT, mone, pi);
Trace("nl-trans-checker") << "Checking " << id << std::endl;
nm->mkNode(Kind::LEQ, x, pi),
}),
x.eqNode(y),
- x.eqNode(nm->mkNode(
- Kind::PLUS,
- y,
- nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
+ x.eqNode(
+ nm->mkNode(Kind::PLUS,
+ y,
+ nm->mkNode(Kind::MULT,
+ nm->mkConst<Rational>(CONST_RATIONAL, 2),
+ s,
+ pi)))),
nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
}
else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
#include "theory/arith/nl/transcendental/transcendental_state.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
nm->mkNode(Kind::ITE,
mkValidPhase(a[0], d_data->d_pi),
a[0].eqNode(y),
- a[0].eqNode(nm->mkNode(Kind::PLUS,
- y,
- nm->mkNode(Kind::MULT,
- nm->mkConst(Rational(2)),
- shift,
- d_data->d_pi)))),
+ a[0].eqNode(nm->mkNode(
+ Kind::PLUS,
+ y,
+ nm->mkNode(Kind::MULT,
+ nm->mkConst(CONST_RATIONAL, Rational(2)),
+ shift,
+ d_data->d_pi)))),
new_a.eqNode(a));
CDProof* proof = nullptr;
if (d_data->isProofEnabled())
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
{},
- {nm->mkConst<Rational>(2 * d),
+ {nm->mkConst(CONST_RATIONAL, Rational(2 * d)),
e[0],
c,
regionToLowerBound(region),
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
{},
- {nm->mkConst<Rational>(2 * d),
+ {nm->mkConst(CONST_RATIONAL, Rational(2 * d)),
e[0],
c,
c,
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
{},
- {nm->mkConst<Rational>(2 * d),
+ {nm->mkConst(CONST_RATIONAL, Rational(2 * d)),
e[0],
c,
regionToLowerBound(region),
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
{},
- {nm->mkConst<Rational>(2 * d),
+ {nm->mkConst(CONST_RATIONAL, Rational(2 * d)),
e[0],
c,
c,
#include "theory/arith/nl/nl_model.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
// the current factorial `counter!`
Integer factorial = 1;
// the current variable power `x^counter`
- Node varpow = nm->mkConst(Rational(1));
+ Node varpow = nm->mkConst(CONST_RATIONAL, Rational(1));
std::vector<Node> sum;
for (std::uint64_t counter = 1; counter <= n; ++counter)
{
// Maclaurin series for exponential:
// \sum_{n=0}^\infty x^n / n!
sum.push_back(
- nm->mkNode(Kind::DIVISION, varpow, nm->mkConst<Rational>(factorial)));
+ nm->mkNode(Kind::DIVISION,
+ varpow,
+ nm->mkConst<Rational>(CONST_RATIONAL, factorial)));
}
else if (k == Kind::SINE)
{
if (counter % 2 == 0)
{
int sign = (counter % 4 == 0 ? -1 : 1);
- sum.push_back(nm->mkNode(Kind::MULT,
- nm->mkNode(Kind::DIVISION,
- nm->mkConst<Rational>(sign),
- nm->mkConst<Rational>(factorial)),
- varpow));
+ sum.push_back(nm->mkNode(
+ Kind::MULT,
+ nm->mkNode(Kind::DIVISION,
+ nm->mkConst<Rational>(CONST_RATIONAL, sign),
+ nm->mkConst<Rational>(CONST_RATIONAL, factorial)),
+ varpow));
}
}
factorial *= counter;
Node taylor_sum =
Rewriter::rewrite(sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum));
Node taylor_rem = Rewriter::rewrite(
- nm->mkNode(Kind::DIVISION, varpow, nm->mkConst<Rational>(factorial)));
+ nm->mkNode(Kind::DIVISION,
+ varpow,
+ nm->mkConst<Rational>(CONST_RATIONAL, factorial)));
auto res = std::make_pair(taylor_sum, taylor_rem);
pbounds.d_lower = taylor_sum;
pbounds.d_upperNeg =
Rewriter::rewrite(nm->mkNode(Kind::PLUS, taylor_sum, ru));
- pbounds.d_upperPos = Rewriter::rewrite(
- nm->mkNode(Kind::MULT,
- taylor_sum,
- nm->mkNode(Kind::PLUS, nm->mkConst(Rational(1)), ru)));
+ pbounds.d_upperPos = Rewriter::rewrite(nm->mkNode(
+ Kind::MULT,
+ taylor_sum,
+ nm->mkNode(
+ Kind::PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), ru)));
}
else
{
// at zero, its trivial
if (k == Kind::SINE)
{
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
return std::pair<Node, Node>(zero, zero);
}
Assert(k == Kind::EXPONENTIAL);
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
return std::pair<Node, Node>(one, one);
}
bool isNeg = csign == -1;
#include "theory/arith/nl/transcendental/taylor_generator.h"
#include "theory/rewriter.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
if (d_env.isTheoryProofProducing())
{
d_proof.reset(new CDProofSet<CDProof>(
{
d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
d_pi_2 = Rewriter::rewrite(
- nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(1) / Rational(2))));
+ nm->mkNode(Kind::MULT,
+ d_pi,
+ nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2))));
d_pi_neg_2 = Rewriter::rewrite(
- nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(-1) / Rational(2))));
- d_pi_neg = Rewriter::rewrite(
- nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(-1))));
+ nm->mkNode(Kind::MULT,
+ d_pi,
+ nm->mkConst(CONST_RATIONAL, Rational(-1) / Rational(2))));
+ d_pi_neg = Rewriter::rewrite(nm->mkNode(
+ Kind::MULT, d_pi, nm->mkConst(CONST_RATIONAL, Rational(-1))));
// initialize bounds
- d_pi_bound[0] = nm->mkConst(Rational(103993) / Rational(33102));
- d_pi_bound[1] = nm->mkConst(Rational(104348) / Rational(33215));
+ d_pi_bound[0] =
+ nm->mkConst(CONST_RATIONAL, Rational(103993) / Rational(33102));
+ d_pi_bound[1] =
+ nm->mkConst(CONST_RATIONAL, Rational(104348) / Rational(33215));
}
}
{
if (csign == 1)
{
- proof->addStep(
- lem,
- PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS,
- {},
- {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS,
+ {},
+ {nm->mkConst<Rational>(CONST_RATIONAL, 2 * actual_d),
+ tf[0],
+ lower,
+ upper});
}
else
{
- proof->addStep(
- lem,
- PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
- {},
- {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
+ {},
+ {nm->mkConst<Rational>(CONST_RATIONAL, 2 * actual_d),
+ tf[0],
+ lower,
+ upper});
}
}
else if (tf.getKind() == Kind::SINE)
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS,
{},
- {nm->mkConst<Rational>(2 * actual_d),
+ {nm->mkConst<Rational>(CONST_RATIONAL, 2 * actual_d),
tf[0],
lower,
upper,
proof->addStep(lem,
PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
{},
- {nm->mkConst<Rational>(2 * actual_d),
+ {nm->mkConst<Rational>(CONST_RATIONAL, 2 * actual_d),
tf[0],
lower,
upper,
nm->mkNode(
LT,
num,
- nm->mkNode(MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
+ nm->mkNode(
+ MULT,
+ den,
+ nm->mkNode(
+ PLUS, v, nm->mkConst(CONST_RATIONAL, Rational(1))))));
}
else
{
lem = nm->mkNode(
AND,
leqNum,
- nm->mkNode(
- LT,
- num,
- nm->mkNode(MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
+ nm->mkNode(LT,
+ num,
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(PLUS,
+ v,
+ nm->mkConst(CONST_RATIONAL,
+ Rational(-1))))));
}
}
else
AND,
nm->mkNode(
IMPLIES,
- nm->mkNode(GT, den, nm->mkConst(Rational(0))),
+ nm->mkNode(GT, den, nm->mkConst(CONST_RATIONAL, Rational(0))),
nm->mkNode(
AND,
leqNum,
nm->mkNode(
LT,
num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(PLUS,
+ v,
+ nm->mkConst(CONST_RATIONAL,
+ Rational(1))))))),
nm->mkNode(
IMPLIES,
- nm->mkNode(LT, den, nm->mkConst(Rational(0))),
+ nm->mkNode(LT, den, nm->mkConst(CONST_RATIONAL, Rational(0))),
nm->mkNode(
AND,
leqNum,
nm->mkNode(
LT,
num,
- nm->mkNode(
- MULT,
- den,
- nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
+ nm->mkNode(MULT,
+ den,
+ nm->mkNode(PLUS,
+ v,
+ nm->mkConst(CONST_RATIONAL,
+ Rational(-1))))))));
}
Node intVar = mkWitnessTerm(
v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
checkNonLinearLogic(node);
Node rw = nm->mkNode(k, num, den);
Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
- Node lem = nm->mkNode(IMPLIES,
- den.eqNode(nm->mkConst(Rational(0))).negate(),
- nm->mkNode(MULT, den, v).eqNode(num));
+ Node lem = nm->mkNode(
+ IMPLIES,
+ den.eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))).negate(),
+ nm->mkNode(MULT, den, v).eqNode(num));
return mkWitnessTerm(
v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
break;
{
checkNonLinearLogic(node);
Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO);
- Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+ Node denEq0 =
+ nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0)));
ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
}
return ret;
checkNonLinearLogic(node);
Node intDivByZeroNum =
getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO);
- Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+ Node denEq0 =
+ nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0)));
ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
}
return ret;
{
checkNonLinearLogic(node);
Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO);
- Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
+ Node denEq0 =
+ nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0)));
ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
}
return ret;
case ABS:
{
- return nm->mkNode(ITE,
- nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
- nm->mkNode(UMINUS, node[0]),
- node[0]);
+ return nm->mkNode(
+ ITE,
+ nm->mkNode(LT, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))),
+ nm->mkNode(UMINUS, node[0]),
+ node[0]);
break;
}
case SQRT:
// satisfiable. On the original formula, this would require that we
// simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
// model.
- lem = nm->mkNode(ITE,
- nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
- nonNeg,
- uf);
+ lem = nm->mkNode(
+ ITE,
+ nm->mkNode(GEQ, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))),
+ nonNeg,
+ uf);
}
else
{
Node rlem;
if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
{
- Node half = nm->mkConst(Rational(1) / Rational(2));
+ Node half = nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2));
Node pi2 = nm->mkNode(MULT, half, pi);
- Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
+ Node npi2 =
+ nm->mkNode(MULT, nm->mkConst(CONST_RATIONAL, Rational(-1)), pi2);
// -pi/2 < var <= pi/2
rlem = nm->mkNode(
AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
else
{
// 0 <= var < pi
- rlem = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
- nm->mkNode(LT, var, pi));
+ rlem = nm->mkNode(
+ AND,
+ nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), var),
+ nm->mkNode(LT, var, pi));
}
Kind rk =
#include "theory/arith/normal_form.h"
#include "theory/arith/operator_elim.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace arith {
const std::vector<Node>& args)
{
NodeManager* nm = NodeManager::currentNM();
- auto zero = nm->mkConst<Rational>(0);
+ auto zero = nm->mkConst<Rational>(CONST_RATIONAL, 0);
if (Debug.isOn("arith::pf::check"))
{
Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl;
<< "Bad kind: " << children[i].getKind() << std::endl;
}
}
- leftSum << nm->mkNode(
- Kind::MULT, nm->mkConst<Rational>(scalar), children[i][0]);
- rightSum << nm->mkNode(
- Kind::MULT, nm->mkConst<Rational>(scalar), children[i][1]);
+ leftSum << nm->mkNode(Kind::MULT,
+ nm->mkConst<Rational>(CONST_RATIONAL, scalar),
+ children[i][0]);
+ rightSum << nm->mkNode(Kind::MULT,
+ nm->mkConst<Rational>(CONST_RATIONAL, scalar),
+ children[i][1]);
}
Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
leftSum.constructNode(),
{
Rational originalBound = children[0][1].getConst<Rational>();
Rational newBound = leastIntGreaterThan(originalBound);
- Node rational = nm->mkConst<Rational>(newBound);
+ Node rational = nm->mkConst<Rational>(CONST_RATIONAL, newBound);
return nm->mkNode(kind::GEQ, children[0][0], rational);
}
}
{
Rational originalBound = children[0][1].getConst<Rational>();
Rational newBound = greatestIntLessThan(originalBound);
- Node rational = nm->mkConst<Rational>(newBound);
+ Node rational = nm->mkConst<Rational>(CONST_RATIONAL, newBound);
return nm->mkNode(kind::LEQ, children[0][0], rational);
}
}
Pf pfNotGeq = d_pnm->mkAssume(geq.getNode().negate());
Pf pfLt =
d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pfNotGeq}, {lt});
- Pf pfSum =
- d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
- {pfGt, pfLt},
- {nm->mkConst<Rational>(-1), nm->mkConst<Rational>(1)});
+ Pf pfSum = d_pnm->mkNode(PfRule::MACRO_ARITH_SCALE_SUM_UB,
+ {pfGt, pfLt},
+ {nm->mkConst<Rational>(CONST_RATIONAL, -1),
+ nm->mkConst<Rational>(CONST_RATIONAL, 1)});
Pf pfBot = d_pnm->mkNode(
PfRule::MACRO_SR_PRED_TRANSFORM, {pfSum}, {nm->mkConst<bool>(false)});
std::vector<Node> assumptions = {leq.getNode().negate(),
std::vector<Node> farkasCoefficients;
farkasCoefficients.reserve(coeffs->size());
auto nm = NodeManager::currentNM();
- std::transform(
- coeffs->begin(),
- coeffs->end(),
- std::back_inserter(farkasCoefficients),
- [nm](const Rational& r) { return nm->mkConst<Rational>(r); });
+ std::transform(coeffs->begin(),
+ coeffs->end(),
+ std::back_inserter(farkasCoefficients),
+ [nm](const Rational& r) {
+ return nm->mkConst<Rational>(CONST_RATIONAL, r);
+ });
// Prove bottom.
auto sumPf = d_pnm->mkNode(
&& type.getConst<TypeConstant>() == REAL_TYPE);
}
- Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); }
+ Node operator*() override
+ {
+ return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, d_rat);
+ }
RationalEnumerator& operator++() override
{
// sequence is 0, then diagonal with negatives interleaved
Node operator*() override
{
- return NodeManager::currentNM()->mkConst(Rational(d_int));
+ return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL,
+ Rational(d_int));
}
IntegerEnumerator& operator++() override
d_termReg(tr),
d_mapCache(userContext())
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
: d_statistics(statistics)
{
d_nm = NodeManager::currentNM();
- d_zero = d_nm->mkConst(Rational(0));
- d_one = d_nm->mkConst(Rational(1));
+ d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
}
RewriteResponse BagsRewriter::postRewrite(TNode n)
d_nm = NodeManager::currentNM();
d_sm = d_nm->getSkolemManager();
d_true = d_nm->mkConst(true);
- d_zero = d_nm->mkConst(Rational(0));
- d_one = d_nm->mkConst(Rational(1));
+ d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
}
InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)
}
TypeNode elementType = t.getBagElementType();
std::map<Node, Rational>::const_reverse_iterator it = elements.rbegin();
- Node bag =
- nm->mkBag(elementType, it->first, nm->mkConst<Rational>(it->second));
+ Node bag = nm->mkBag(elementType,
+ it->first,
+ nm->mkConst<Rational>(CONST_RATIONAL, it->second));
while (++it != elements.rend())
{
- Node n =
- nm->mkBag(elementType, it->first, nm->mkConst<Rational>(it->second));
+ Node n = nm->mkBag(elementType,
+ it->first,
+ nm->mkConst<Rational>(CONST_RATIONAL, it->second));
bag = nm->mkNode(UNION_DISJOINT, n, bag);
}
return bag;
NodeManager* nm = NodeManager::currentNM();
if (it != elements.end())
{
- Node count = nm->mkConst(it->second);
+ Node count = nm->mkConst(CONST_RATIONAL, it->second);
return count;
}
- return nm->mkConst(Rational(0));
+ return nm->mkConst(CONST_RATIONAL, Rational(0));
}
Node NormalForm::evaluateDuplicateRemoval(TNode n)
}
NodeManager* nm = NodeManager::currentNM();
- Node sumNode = nm->mkConst(sum);
+ Node sumNode = nm->mkConst(CONST_RATIONAL, sum);
return sumNode;
}
Node emptyBag = nm->mkConst(EmptyBag(bagType));
Node isEmpty = A.eqNode(emptyBag);
Node count = nm->mkNode(BAG_COUNT, x, A);
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node geqOne = nm->mkNode(GEQ, count, one);
Node geqOneAndEqual = geqOne.andNode(equal);
Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual);
#include "theory_bags_type_enumerator.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace bags {
BagEnumerator& BagEnumerator::operator++()
{
// increase the multiplicity by one
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
TypeNode elementType = d_elementTypeEnumerator.getType();
Node singleton = d_nodeManager->mkBag(elementType, d_element, one);
if (d_currentBag.getKind() == kind::EMPTYBAG)
#include "proof/proof_node_manager.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace booleans {
template <typename T>
Node mkRat(T val)
{
- return NodeManager::currentNM()->mkConst<Rational>(val);
+ return NodeManager::currentNM()->mkConst<Rational>(CONST_RATIONAL, val);
}
/**
Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
{
return NodeManager::currentNM()->mkConst(
- Rational(static_cast<uint32_t>(tid)));
+ CONST_RATIONAL, Rational(static_cast<uint32_t>(tid)));
}
} // namespace builtin
#include "util/iand.h"
#include "util/rational.h"
-namespace cvc5 {
+using namespace cvc5::kind;
using namespace cvc5::theory;
+namespace cvc5 {
+
namespace {
// A helper function to compute 2^b as a Rational
d_introduceFreshIntVars(introduceFreshIntVars)
{
d_nm = NodeManager::currentNM();
- d_zero = d_nm->mkConst<Rational>(0);
- d_one = d_nm->mkConst<Rational>(1);
+ d_zero = d_nm->mkConst<Rational>(CONST_RATIONAL, 0);
+ d_one = d_nm->mkConst<Rational>(CONST_RATIONAL, 1);
};
IntBlaster::~IntBlaster() {}
{
Assert(k > 0);
Rational max_value = intpow2(k) - 1;
- return d_nm->mkConst<Rational>(max_value);
+ return d_nm->mkConst<Rational>(CONST_RATIONAL, max_value);
}
Node IntBlaster::pow2(uint64_t k)
{
Assert(k >= 0);
- return d_nm->mkConst<Rational>(intpow2(k));
+ return d_nm->mkConst<Rational>(CONST_RATIONAL, intpow2(k));
}
Node IntBlaster::modpow2(Node n, uint64_t exponent)
{
- Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
+ Node p2 = d_nm->mkConst<Rational>(CONST_RATIONAL, intpow2(exponent));
return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
}
// Bit-vector constants are transformed into their integer value.
BitVector constant(original.getConst<BitVector>());
Integer c = constant.toInteger();
- translation = d_nm->mkConst<Rational>(c);
+ translation = d_nm->mkConst<Rational>(CONST_RATIONAL, c);
}
else
{
#include "util/bitvector.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace bv {
{
const unsigned size = utils::getSize(node[0]);
NodeManager* const nm = NodeManager::currentNM();
- const Node z = nm->mkConst(Rational(0));
+ const Node z = nm->mkConst(CONST_RATIONAL, Rational(0));
const Node bvone = utils::mkOne(1);
Integer i = 1;
nm->mkNode(kind::EQUAL,
nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
bvone);
- children.push_back(
- nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
+ children.push_back(nm->mkNode(
+ kind::ITE, cond, nm->mkConst(CONST_RATIONAL, Rational(i)), z));
}
// avoid plus with one child
return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
Integer i = 2;
while (v.size() < size)
{
- Node cond = nm->mkNode(
- kind::GEQ,
- nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
- nm->mkConst(Rational(i, 2)));
+ Node cond = nm->mkNode(kind::GEQ,
+ nm->mkNode(kind::INTS_MODULUS_TOTAL,
+ node[0],
+ nm->mkConst(CONST_RATIONAL, Rational(i))),
+ nm->mkConst(CONST_RATIONAL, Rational(i, 2)));
v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
i *= 2;
}
const DType& dt = utils::datatypeOf(constructor);
const DTypeConstructor& c = dt[constructorIndex];
unsigned weight = c.getWeight();
- children.push_back(nm->mkConst(Rational(weight)));
+ children.push_back(nm->mkConst(CONST_RATIONAL, Rational(weight)));
Node res =
children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
Trace("datatypes-rewrite")
res = nm->mkConst(false);
break;
}
- children.push_back(
- nm->mkNode(kind::DT_HEIGHT_BOUND, in[0][i], nm->mkConst(rmo)));
+ children.push_back(nm->mkNode(kind::DT_HEIGHT_BOUND,
+ in[0][i],
+ nm->mkConst(CONST_RATIONAL, rmo)));
}
}
if (res.isNull())
}
if (argSuccess)
{
- narg = nm->mkConst(Rational(i));
+ narg = nm->mkConst(CONST_RATIONAL, Rational(i));
break;
}
}
if (n >= 0)
{
Node t = exp[0];
- Node nn = nm->mkConst(Rational(n));
+ Node nn = nm->mkConst(CONST_RATIONAL, Rational(n));
Node eq = exp.eqNode(conc);
cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});
d_active_terms(context()),
d_currTermSize(context())
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
d_true = NodeManager::currentNM()->mkConst(true);
}
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
d_measure_value = sm->mkDummySkolem("mt", nm->integerType());
- Node mtlem =
- nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0)));
+ Node mtlem = nm->mkNode(
+ kind::GEQ, d_measure_value, nm->mkConst(CONST_RATIONAL, Rational(0)));
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
}
return d_measure_value;
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
Node new_mt = sm->mkDummySkolem("mt", nm->integerType());
- Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0)));
+ Node mtlem =
+ nm->mkNode(kind::GEQ, new_mt, nm->mkConst(CONST_RATIONAL, Rational(0)));
d_measure_value_active = new_mt;
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
}
NodeManager* nm = NodeManager::currentNM();
Trace("sygus-engine") << "******* Sygus : allocate size literal " << s
<< " for " << d_this << std::endl;
- return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
+ return nm->mkNode(
+ DT_SYGUS_BOUND, d_this, nm->mkConst(CONST_RATIONAL, Rational(s)));
}
int SygusExtension::getGuardStatus( Node g ) {
rt.d_children[0].d_req_kind = PLUS;
rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
rt.d_children[0].d_children[1].d_req_const =
- NodeManager::currentNM()->mkConst(Rational(1));
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
rt.d_children[1].d_req_type = dt[c].getArgType(0);
}
else if (k == LT || k == GEQ)
rt.d_children[1].d_req_kind = PLUS;
rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
rt.d_children[1].d_children[1].d_req_const =
- NodeManager::currentNM()->mkConst(Rational(1));
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
}
}
else if (pk == BITVECTOR_NOT)
{
d_true = NodeManager::currentNM()->mkConst( true );
- d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
d_dtfCounter = 0;
// indicate we are using the default theory state object
#include "theory/theory_model.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
NodeManager* nm = NodeManager::currentNM();
for (const std::pair<const Node, uint64_t> p : d_dfmap)
{
- dmap[p.first] = nm->mkConst(Rational(p.second));
+ dmap[p.first] = nm->mkConst(CONST_RATIONAL, Rational(p.second));
}
}
#include "theory/theory.h"
#include "util/integer.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
{
case EvalResult::BOOL: return nm->mkConst(d_bool);
case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
- case EvalResult::RATIONAL: return nm->mkConst(d_rat);
+ case EvalResult::RATIONAL: return nm->mkConst(CONST_RATIONAL, d_rat);
case EvalResult::STRING: return nm->mkConst(d_str);
case EvalResult::UCONST: return nm->mkConst(d_uc);
default:
#include "util/floatingpoint.h"
using namespace std;
+using namespace cvc5::kind;
namespace cvc5 {
namespace theory {
Node realValueOfAbstract =
rewrite(nm->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
abstractValue,
- nm->mkConst(Rational(0U))));
+ nm->mkConst(CONST_RATIONAL, Rational(0U))));
Node bg = nm->mkNode(
kind::IMPLIES,
nm->mkNode(kind::EQUAL, node, node[1]));
handleLemma(pd, InferenceId::FP_REGISTER_TERM);
- Node z =
- nm->mkNode(kind::IMPLIES,
- nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
- nm->mkNode(kind::EQUAL, node, nm->mkConst(Rational(0U))));
+ Node z = nm->mkNode(
+ kind::IMPLIES,
+ nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+ nm->mkNode(
+ kind::EQUAL, node, nm->mkConst(CONST_RATIONAL, Rational(0U))));
handleLemma(z, InferenceId::FP_REGISTER_TERM);
return;
Node z = nm->mkNode(
kind::IMPLIES,
- nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))),
+ nm->mkNode(
+ kind::EQUAL, node[1], nm->mkConst(CONST_RATIONAL, Rational(0U))),
nm->mkNode(kind::EQUAL,
node,
nm->mkConst(FloatingPoint::makeZero(
#include "theory/fp/fp_word_blaster.h"
#include "util/floatingpoint.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace fp {
FloatingPoint::PartialRational res(arg.convertToRational());
if (res.second) {
- Node lit = NodeManager::currentNM()->mkConst(res.first);
+ Node lit = NodeManager::currentNM()->mkConst(CONST_RATIONAL, res.first);
return RewriteResponse(REWRITE_DONE, lit);
} else {
// Can't constant fold the underspecified case
Rational partialValue(node[1].getConst<Rational>());
Rational folded(arg.convertToRationalTotal(partialValue));
- Node lit = NodeManager::currentNM()->mkConst(folded);
+ Node lit = NodeManager::currentNM()->mkConst(CONST_RATIONAL, folded);
return RewriteResponse(REWRITE_DONE, lit);
} else {
FloatingPoint::PartialRational res(arg.convertToRational());
if (res.second) {
- Node lit = NodeManager::currentNM()->mkConst(res.first);
- return RewriteResponse(REWRITE_DONE, lit);
+ Node lit = NodeManager::currentNM()->mkConst(CONST_RATIONAL, res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
} else {
// Can't constant fold the underspecified case
return RewriteResponse(REWRITE_DONE, node);
#include "proof/proof_checker.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
Node mkInferenceIdNode(InferenceId i)
{
- return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i)));
+ return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ Rational(static_cast<uint32_t>(i)));
}
bool getInferenceId(TNode n, InferenceId& i)
ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc)
: Instantiator(env, tn), d_vtc(vtc)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
- d_one = NodeManager::currentNM()->mkConst(Rational(1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
}
void ArithInstantiator::reset(CegInstantiator* ci,
uval = nm->mkNode(
PLUS,
val,
- nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
+ nm->mkConst(CONST_RATIONAL,
+ Rational(isUpperBoundCTT(uires) ? 1 : -1)));
uval = rewrite(uval);
}
else
if (d_type.isInteger())
{
uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER;
- uval = nm->mkNode(
- PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)));
+ uval =
+ nm->mkNode(PLUS,
+ val,
+ nm->mkConst(CONST_RATIONAL,
+ Rational(isUpperBoundCTT(uires) ? 1 : -1)));
uval = rewrite(uval);
}
else
{
if (options().quantifiers.cegqiModel)
{
- Node delta_coeff =
- nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
+ Node delta_coeff = nm->mkConst(
+ CONST_RATIONAL, Rational(isUpperBoundCTT(uires) ? 1 : -1));
if (vts_coeff_delta.isNull())
{
vts_coeff_delta = delta_coeff;
Assert(d_mbp_coeff[rr][j].isConst());
value[t] = nm->mkNode(
MULT,
- nm->mkConst(Rational(1)
- / d_mbp_coeff[rr][j].getConst<Rational>()),
+ nm->mkConst(
+ CONST_RATIONAL,
+ Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>()),
value[t]);
value[t] = rewrite(value[t]);
}
}
else
{
- val = nm->mkNode(MULT,
- nm->mkNode(PLUS, vals[0], vals[1]),
- nm->mkConst(Rational(1) / Rational(2)));
+ val =
+ nm->mkNode(MULT,
+ nm->mkNode(PLUS, vals[0], vals[1]),
+ nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)));
val = rewrite(val);
}
}
vts_coeff[t] = itminf->second;
if (vts_coeff[t].isNull())
{
- vts_coeff[t] = nm->mkConst(Rational(1));
+ vts_coeff[t] = nm->mkConst(CONST_RATIONAL, Rational(1));
}
// negate if coefficient on variable is positive
std::map<Node, Node>::iterator itv = msum.find(pv);
{
vts_coeff[t] = nm->mkNode(
MULT,
- nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()),
+ nm->mkConst(CONST_RATIONAL,
+ Rational(-1) / itv->second.getConst<Rational>()),
vts_coeff[t]);
vts_coeff[t] = rewrite(vts_coeff[t]);
}
}
}
// multiply everything by this coefficient
- Node rcoeff = nm->mkConst(Rational(coeff));
+ Node rcoeff = nm->mkConst(CONST_RATIONAL, Rational(coeff));
std::vector<Node> real_part;
for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
++it)
else
{
NodeManager* nm = NodeManager::currentNM();
- d_coeff = nm->mkConst(Rational(d_coeff.getConst<Rational>()
+ d_coeff = nm->mkConst(CONST_RATIONAL,
+ Rational(d_coeff.getConst<Rational>()
* p.d_coeff.getConst<Rational>()));
}
}
Assert(new_theta.getKind() == CONST_RATIONAL);
Assert(pv_prop.d_coeff.getKind() == CONST_RATIONAL);
NodeManager* nm = NodeManager::currentNM();
- new_theta = nm->mkConst(Rational(new_theta.getConst<Rational>()
+ new_theta = nm->mkConst(CONST_RATIONAL,
+ Rational(new_theta.getConst<Rational>()
* pv_prop.d_coeff.getConst<Rational>()));
}
d_theta.push_back(new_theta);
if( !prop[i].d_coeff.isNull() ){
Assert(vars[i].getType().isInteger());
Assert(prop[i].d_coeff.isConst());
- Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
+ Node nn = NodeManager::currentNM()->mkNode(
+ MULT,
+ subs[i],
+ NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL,
+ Rational(1) / prop[i].d_coeff.getConst<Rational>()));
nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
nn = rewrite(nn);
nsubs.push_back( nn );
Node c_coeff;
if( !msum_coeff[it->first].isNull() ){
c_coeff = rewrite(NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL,
pv_prop.d_coeff.getConst<Rational>()
- / msum_coeff[it->first].getConst<Rational>()));
+ / msum_coeff[it->first].getConst<Rational>()));
}else{
c_coeff = pv_prop.d_coeff;
}
}else{
atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
atom_lhs = rewrite(atom_lhs);
- atom_rhs = nm->mkConst(Rational(0));
+ atom_rhs = nm->mkConst(CONST_RATIONAL, Rational(0));
}
//must be an eligible term
if( isEligible( atom_lhs ) ){
d_added_cbqi_lemma(userContext()),
d_vtsCache(new VtsTermCache(qim)),
d_bv_invert(nullptr),
- d_small_const_multiplier(
- NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))),
+ d_small_const_multiplier(NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL, Rational(1) / Rational(1000000))),
d_small_const(d_small_const_multiplier)
{
d_check_vts_lemma_lc = false;
d_vtsCache->getVtsTerms(inf, true, false, false);
for( unsigned i=0; i<inf.size(); i++ ){
Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
- Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
+ Node inf_lem_lb = NodeManager::currentNM()->mkNode(
+ GT,
+ inf[i],
+ NodeManager::currentNM()->mkConst(
+ CONST_RATIONAL,
+ Rational(1) / d_small_const.getConst<Rational>()));
d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
}
}
VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
void VtsTermCache::getVtsTerms(std::vector<Node>& t,
{
if (pat.getKind() == GT)
{
- t_match = nm->mkNode(MINUS, t, nm->mkConst(Rational(1)));
+ t_match =
+ nm->mkNode(MINUS, t, nm->mkConst(CONST_RATIONAL, Rational(1)));
}else{
t_match = t;
}
else
{
Assert(t.getType().isReal());
- t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
+ t_match =
+ nm->mkNode(PLUS, t, nm->mkConst(CONST_RATIONAL, Rational(1)));
}
}
else if (pat.getKind() == GEQ)
{
- t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
+ t_match = nm->mkNode(PLUS, t, nm->mkConst(CONST_RATIONAL, Rational(1)));
}
else if (pat.getKind() == GT)
{
Assert(nc.isConst());
if (x.getType().isInteger())
{
- Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
+ Node coeff =
+ nm->mkConst(CONST_RATIONAL, nc.getConst<Rational>().abs());
if (!nc.getConst<Rational>().abs().isOne())
{
x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
}
else
{
- Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
+ Node coeff = nm->mkConst(CONST_RATIONAL,
+ Rational(1) / nc.getConst<Rational>());
x = nm->mkNode(MULT, x, coeff);
}
}
s = rhs;
if (!checkPol)
{
- s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1)));
+ s = nm->mkNode(
+ PLUS,
+ s,
+ nm->mkConst(CONST_RATIONAL, Rational(d_rel == GEQ ? -1 : 1)));
}
d_counter++;
Trace("relational-match-gen")
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
void ExtendedRewriter::setCache(Node n, Node ret) const
Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
{
NodeManager* nm = NodeManager::currentNM();
- Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1));
+ Node cn = nm->mkConst(CONST_RATIONAL, Rational(n == 0 ? 0 : n - 1));
return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn);
}
d_ranges_proxied[curr] = true;
NodeManager* nm = NodeManager::currentNM();
Node currLit = getLiteral(curr);
- Node lem =
- nm->mkNode(EQUAL,
- currLit,
- nm->mkNode(curr == 0 ? LT : LEQ,
- d_range,
- nm->mkConst(Rational(curr == 0 ? 0 : curr - 1))));
+ Node lem = nm->mkNode(
+ EQUAL,
+ currLit,
+ nm->mkNode(
+ curr == 0 ? LT : LEQ,
+ d_range,
+ nm->mkConst(CONST_RATIONAL, Rational(curr == 0 ? 0 : curr - 1))));
return lem;
}
}
choices.pop_back();
Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
- Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i)));
+ Node cMinCard =
+ nm->mkNode(LEQ, srCardN, nm->mkConst(CONST_RATIONAL, Rational(i)));
choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
d_setm_choice[sro].push_back(choice_i);
}
Node range = rewrite(nm->mkNode(MINUS, u, l));
// 9999 is an arbitrary range past which we do not do exhaustive
// bounded instantation, based on the check below.
- Node ra = rewrite(nm->mkNode(LEQ, range, nm->mkConst(Rational(9999))));
+ Node ra = rewrite(nm->mkNode(
+ LEQ, range, nm->mkConst(CONST_RATIONAL, Rational(9999))));
Node tl = l;
Node tu = u;
getBounds( q, v, rsi, tl, tu );
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
for (long k = 0; k < rr; k++)
{
- Node t = nm->mkNode(PLUS, tl, nm->mkConst(Rational(k)));
+ Node t =
+ nm->mkNode(PLUS, tl, nm->mkConst(CONST_RATIONAL, Rational(k)));
t = rewrite(t);
elements.push_back( t );
}
if (!c.isLargeFinite())
{
NodeManager* nm = NodeManager::currentNM();
- Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+ Node card =
+ nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality()));
// check if less than fixed upper bound
- Node oth = nm->mkConst(Rational(maxCard));
+ Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard));
Node eq = nm->mkNode(LEQ, card, oth);
eq = Rewriter::rewrite(eq);
mc = eq.isConst() && eq.getConst<bool>();
if( it==d_zero.end() ){
Node nn;
if( k==PLUS ){
- nn = NodeManager::currentNM()->mkConst( Rational(0) );
+ nn = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
d_zero[k] = nn;
return nn;
for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
{
TypeNode tn = tspec[j];
- Node rn = nm->mkConst(Rational(j));
+ Node rn = nm->mkConst(CONST_RATIONAL, Rational(j));
Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
newChildren.push_back(v);
}
else if (options::intWfInduction() && tn.isInteger())
{
- Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0)));
- Node iret = ret.substitute(ind_vars[0],
- nm->mkNode(MINUS, k, nm->mkConst(Rational(1))))
- .negate();
+ Node icond = nm->mkNode(GEQ, k, nm->mkConst(CONST_RATIONAL, Rational(0)));
+ Node iret =
+ ret.substitute(
+ ind_vars[0],
+ nm->mkNode(MINUS, k, nm->mkConst(CONST_RATIONAL, Rational(1))))
+ .negate();
n_str_ind = nm->mkNode(OR, icond.negate(), iret);
n_str_ind = nm->mkNode(AND, icond, n_str_ind);
}
std::set<TypeNode> unresolvedTypes;
unresolvedTypes.insert(u);
std::vector<TypeNode> cargsEmpty;
- Node cr = nm->mkConst(Rational(1));
+ Node cr = nm->mkConst(CONST_RATIONAL, Rational(1));
sdt.addConstructor(cr, "1", cargsEmpty);
std::vector<TypeNode> cargsPlus;
cargsPlus.push_back(u);
if (pow_two > 0)
{
Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
- Node fair_lemma =
- nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
+ Node fair_lemma = nm->mkNode(
+ GEQ, size_ve, nm->mkConst(CONST_RATIONAL, Rational(pow_two - 1)));
fair_lemma = nm->mkNode(OR, newLit, fair_lemma);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
// more aggressive merging of constructor classes. On the negative side,
// this adds another level of indirection to remember which argument
// positions the argument types occur in, for each constructor.
- Node n = nm->mkConst(Rational(i));
+ Node n = nm->mkConst(CONST_RATIONAL, Rational(i));
nToC[n] = i;
tnit.add(n, argTypes[i]);
}
TypeNode tn = cur.getType();
Node c = cur;
if( tn.isReal() ){
- c = nm->mkConst( c.getConst<Rational>().abs() );
+ c = nm->mkConst(CONST_RATIONAL, c.getConst<Rational>().abs());
}
consts[tn].insert(c);
if (tn.isInteger())
NodeManager* nm = NodeManager::currentNM();
if (type.isReal())
{
- ops.push_back(nm->mkConst(Rational(0)));
- ops.push_back(nm->mkConst(Rational(1)));
+ ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(0)));
+ ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(1)));
}
else if (type.isBitVector())
{
Assert(bArgType.isReal() || bArgType.isBitVector());
if (bArgType.isReal())
{
- zarg = nm->mkConst(Rational(0));
+ zarg = nm->mkConst(CONST_RATIONAL, Rational(0));
}
else
{
/* Add operator 1 */
Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
std::vector<TypeNode> cargsEmpty;
- sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty);
+ sdts.back().addConstructor(
+ nm->mkConst(CONST_RATIONAL, Rational(1)), "1", cargsEmpty);
/* Add operator PLUS */
Kind kind = PLUS;
Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n";
#include "util/sampler.h"
#include "util/string.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace theory {
namespace quantifiers {
std::vector<Node> sum;
for (unsigned j = 0, size = vec.size(); j < size; j++)
{
- Node digit = nm->mkConst(Rational(vec[j]) * curr);
+ Node digit = nm->mkConst(CONST_RATIONAL, Rational(vec[j]) * curr);
sum.push_back(digit);
curr = curr * baser;
}
Node ret;
if (sum.empty())
{
- ret = nm->mkConst(Rational(0));
+ ret = nm->mkConst(CONST_RATIONAL, Rational(0));
}
else if (sum.size() == 1)
{
}
else
{
- return nm->mkConst(sr / rr);
+ return nm->mkConst(CONST_RATIONAL, sr / rr);
}
}
}
if (tn.isInteger() || tn.isReal())
{
Rational c(val);
- n = NodeManager::currentNM()->mkConst(c);
+ n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c);
}
else if (tn.isBitVector())
{
d_finite_type_constants_processed(false)
{
d_true = NodeManager::currentNM()->mkConst(true);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
void CardinalityExtension::reset()
if (finiteType)
{
- Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
+ Node typeCardinality =
+ nm->mkConst(CONST_RATIONAL, Rational(card.getFiniteCardinality()));
Node cardUniv = nm->mkNode(kind::SET_CARD, proxy);
Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality);
}
if (!members.empty())
{
- Node conc =
- nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size())));
+ Node conc = nm->mkNode(
+ GEQ, cardTerm, nm->mkConst(CONST_RATIONAL, Rational(members.size())));
Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
}
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
TheorySetsPrivate::~TheorySetsPrivate()
{
if(node[0].isConst()) {
std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]);
- return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(elements.size())));
+ return RewriteResponse(
+ REWRITE_DONE, nm->mkConst(CONST_RATIONAL, Rational(elements.size())));
}
else if (node[0].getKind() == kind::SET_SINGLETON)
{
- return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(1)));
+ return RewriteResponse(REWRITE_DONE,
+ nm->mkConst(CONST_RATIONAL, Rational(1)));
}
else if (node[0].getKind() == kind::SET_UNION)
{
ArithEntail::ArithEntail(Rewriter* r) : d_rr(r)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
}
Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); }
}
Node ar = strict ? NodeManager::currentNM()->mkNode(
- kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1)))
+ kind::MINUS,
+ a,
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)))
: a;
ar = d_rr->rewrite(ar);
<< "Get approximations " << v << "..." << std::endl;
if (v.isNull())
{
- Node mn = c.isNull() ? nm->mkConst(Rational(1)) : c;
+ Node mn = c.isNull() ? nm->mkConst(CONST_RATIONAL, Rational(1)) : c;
aarSum.push_back(mn);
}
else
{
// x >= 0 implies
// x+1 >= len( int.to.str( x ) )
- approx.push_back(
- nm->mkNode(PLUS, nm->mkConst(Rational(1)), a[0][0]));
+ approx.push_back(nm->mkNode(
+ PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), a[0][0]));
}
}
}
{
// x >= 0 implies
// len( int.to.str( x ) ) >= 1
- approx.push_back(nm->mkConst(Rational(1)));
+ approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(1)));
}
// other crazy things are possible here, e.g.
// len( int.to.str( len( y ) + 10 ) ) >= 2
// ...hard to test, runs risk of non-termination
// -1 <= indexof( x, y, n )
- approx.push_back(nm->mkConst(Rational(-1)));
+ approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1)));
}
}
else if (ak == STRING_STOI)
else
{
// -1 <= str.to.int( x )
- approx.push_back(nm->mkConst(Rational(-1)));
+ approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1)));
}
}
Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl;
// (not (>= s t)) --> (>= (t - 1) s)
Assert(assumption.getKind() == kind::NOT
&& assumption[0].getKind() == kind::GEQ);
- x = nm->mkNode(kind::MINUS, assumption[0][1], nm->mkConst(Rational(1)));
+ x = nm->mkNode(kind::MINUS,
+ assumption[0][1],
+ nm->mkConst(CONST_RATIONAL, Rational(1)));
y = assumption[0][0];
}
NodeManager* nm = NodeManager::currentNM();
if (s.isConst())
{
- ret = nm->mkConst(Rational(Word::getLength(s)));
+ ret = nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(s)));
}
else if (s.getKind() == STRING_CONCAT)
{
}
if (success)
{
- ret = nm->mkConst(sum);
+ ret = nm->mkConst(CONST_RATIONAL, sum);
}
}
else if (isLower)
d_eqProc(context())
{
NodeManager* nm = NodeManager::currentNM();
- d_zero = nm->mkConst(Rational(0));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
}
ArraySolver::~ArraySolver() {}
if (lr.isConst())
{
// if constant, compare
- Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need)));
+ Node cmp =
+ nm->mkNode(GEQ, lr, nm->mkConst(CONST_RATIONAL, Rational(card_need)));
cmp = rewrite(cmp);
needsSplit = !cmp.getConst<bool>();
}
bool success = true;
while (r < card_need && success)
{
- Node rr = nm->mkConst(Rational(r));
+ Node rr = nm->mkConst(CONST_RATIONAL, Rational(r));
if (d_state.areDisequal(rr, lr))
{
r++;
<< std::endl;
if (int_k + 1 > ei->d_cardinalityLemK.get())
{
- Node k_node = nm->mkConst(Rational(int_k));
+ Node k_node = nm->mkConst(CONST_RATIONAL, Rational(int_k));
// add cardinality lemma
Node dist = nm->mkNode(DISTINCT, cols[i]);
std::vector<Node> expn;
d_nfPairs(context()),
d_extDeq(userContext())
{
- d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
- d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
}
{
// we can assume its length is greater than zero
Node emp = Word::mkEmptyWord(sk1.getType());
- conc = nm->mkNode(
- AND,
- conc,
- sk1.eqNode(emp).negate(),
- nm->mkNode(
- GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConst(Rational(0))));
+ conc = nm->mkNode(AND,
+ conc,
+ sk1.eqNode(emp).negate(),
+ nm->mkNode(GT,
+ nm->mkNode(STRING_LENGTH, sk1),
+ nm->mkConst(CONST_RATIONAL, Rational(0))));
}
}
else if (rule == PfRule::CONCAT_CSPLIT)
{
// it should be the case that lenConstraint => lenReq
lenReq = nm->mkNode(STRING_LENGTH, t0)
- .eqNode(nm->mkConst(Rational(0)))
+ .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0)))
.notNode();
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
rule = PfRule::CONCAT_CSPLIT;
{
// it should be the case that lenConstraint => lenReq
lenReq = nm->mkNode(STRING_LENGTH, t0)
- .eqNode(nm->mkConst(Rational(0)))
+ .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0)))
.notNode();
lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
rule = PfRule::CONCAT_CPROP;
std::vector<Node> childrenAE;
childrenAE.push_back(eunf);
std::vector<Node> argsAE;
- argsAE.push_back(nm->mkConst(Rational(0)));
+ argsAE.push_back(nm->mkConst(CONST_RATIONAL, Rational(0)));
Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE);
Trace("strings-ipc-prefix")
<< "--- and elim to " << eunfAE << std::endl;
: nullptr)
{
NodeManager* nm = NodeManager::currentNM();
- d_zero = nm->mkConst(Rational(0));
- d_one = nm->mkConst(Rational(1));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
d_true = nm->mkConst(true);
d_false = nm->mkConst(false);
}
else if (id == PfRule::CONCAT_CSPLIT)
{
Assert(children.size() == 2);
- Node zero = nm->mkConst(Rational(0));
- Node one = nm->mkConst(Rational(1));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
|| children[1][0][0].getKind() != STRING_LENGTH
|| children[1][0][0][0] != t0 || children[1][0][1] != zero)
else if (id == PfRule::CONCAT_CPROP)
{
Assert(children.size() == 2);
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
Trace("pfcheck-strings-cprop")
<< "CONCAT_PROP, isRev=" << isRev << std::endl;
{
return Node::null();
}
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
return clen.eqNode(zero).notNode();
}
&& args[1].getType().isStringLike());
Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
- Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1)));
+ Node eqNegOne = c1.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1)));
Node deq = c1.eqNode(c2).negate();
Node eqn = args[0].eqNode(args[1]);
return nm->mkNode(kind::OR, eqNegOne, deq, eqn);
Node x = atom[0];
Node lenx = nm->mkNode(STRING_LENGTH, x);
Node re = atom[1];
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
std::vector<Node> children;
utils::getConcat(re, children);
{
// the gap to this child is at least gap_minsize[i]
prev_end =
- nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize[i])));
+ nm->mkNode(PLUS,
+ prev_end,
+ nm->mkConst(CONST_RATIONAL, Rational(gap_minsize[i])));
}
prev_ends.push_back(prev_end);
Node sc = sep_children[i];
}
// if the gap after this one is strict, we need a non-greedy find
// thus, we add a symbolic constant
- Node cacheVal =
- BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i)));
+ Node cacheVal = BoundVarManager::getCacheValue(
+ atom, nm->mkConst(CONST_RATIONAL, Rational(i)));
TypeNode intType = nm->integerType();
Node k =
bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
prev_end = nm->mkNode(PLUS, prev_end, k);
}
Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end);
- Node idofFind = curr.eqNode(nm->mkConst(Rational(-1))).negate();
+ Node idofFind =
+ curr.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))).negate();
conj.push_back(idofFind);
prev_end = nm->mkNode(PLUS, curr, lensc);
}
// then the last indexof/substr constraint entails the following
// constraint, so it is not necessary to add.
// Below, we may write "A" for (str.to.re "A") and _ for re.allchar:
- Node cEnd = nm->mkConst(Rational(gap_minsize_end));
+ Node cEnd = nm->mkConst(CONST_RATIONAL, Rational(gap_minsize_end));
if (gap_exact_end)
{
Assert(!sep_children.empty());
}
else
{
- Node cacheVal =
- BoundVarManager::getCacheValue(atom, nm->mkConst(Rational(i)));
+ Node cacheVal = BoundVarManager::getCacheValue(
+ atom, nm->mkConst(CONST_RATIONAL, Rational(i)));
TypeNode intType = nm->integerType();
k = bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
Node bound =
Node x = atom[0];
Node lenx = nm->mkNode(STRING_LENGTH, x);
Node re = atom[1];
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
// for regular expression star,
// if the period is a fixed constant, we can turn it into a bounded
// quantifier
std::vector<Node> char_constraints;
TypeNode intType = nm->integerType();
Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType);
- Node substr_ch =
- nm->mkNode(STRING_SUBSTR, x, index, nm->mkConst(Rational(1)));
+ Node substr_ch = nm->mkNode(
+ STRING_SUBSTR, x, index, nm->mkConst(CONST_RATIONAL, Rational(1)));
substr_ch = Rewriter::rewrite(substr_ch);
// handle the case where it is purely characters
for (const Node& r : disj)
}
else
{
- Node num2 = nm->mkConst(cvc5::Rational(u - 1));
+ Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(u - 1));
Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2);
if (testConstStringInRegExp(s, index_start + len, r2))
{
cvc5::String t = s.substr(index_start, len);
if (testConstStringInRegExp(t, 0, r[0]))
{
- Node num2 = nm->mkConst(cvc5::Rational(l - 1));
+ Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(l - 1));
Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2);
if (testConstStringInRegExp(s, index_start + len, r2))
{
}
else if (n.getKind() == REGEXP_ALLCHAR || n.getKind() == REGEXP_RANGE)
{
- return nm->mkConst(Rational(1));
+ return nm->mkConst(CONST_RATIONAL, Rational(1));
}
else if (n.getKind() == REGEXP_UNION || n.getKind() == REGEXP_INTER)
{
d_false(NodeManager::currentNM()->mkConst(false)),
d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE,
std::vector<Node>{})),
- d_zero(NodeManager::currentNM()->mkConst(::cvc5::Rational(0))),
- d_one(NodeManager::currentNM()->mkConst(::cvc5::Rational(1))),
+ d_zero(NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ ::cvc5::Rational(0))),
+ d_one(NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ ::cvc5::Rational(1))),
d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR,
std::vector<Node>{})),
d_sigma_star(
Node r = mem[0][1];
NodeManager* nm = NodeManager::currentNM();
Kind k = r.getKind();
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
Node conc;
if (k == REGEXP_CONCAT)
{
Node r = mem[0][1];
NodeManager* nm = NodeManager::currentNM();
Assert(r.getKind() == REGEXP_CONCAT);
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
// The following simplification states that
// ~( s in R1 ++ R2 ++... ++ Rn )
// is equivalent to
}
else
{
- Node ivalue = nm->mkConst(Rational(i));
+ Node ivalue = nm->mkConst(CONST_RATIONAL, Rational(i));
Node sk = sm->mkSkolemFunction(SkolemFunId::RE_UNFOLD_POS_COMPONENT,
s.getType(),
{mem[0], mem[1], ivalue});
std::map< PairNodes, Node > cache2(cache);
cache2[p] = NodeManager::currentNM()->mkNode(
kind::REGEXP_RV,
- NodeManager::currentNM()->mkConst(cvc5::Rational(cnt)));
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL,
+ cvc5::Rational(cnt)));
rt = intersectInternal(r1l, r2l, cache2, cnt+1);
cacheX[ pp ] = rt;
}
}
else if (ne.getKind() == STRING_SUBSTR)
{
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
if (d_arithEntail.check(ne[1], false)
&& d_arithEntail.check(ne[2], true))
Kind nk0 = node[0].getKind();
if (node[0].isConst())
{
- Node retNode = nm->mkConst(Rational(Word::getLength(node[0])));
+ Node retNode =
+ nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(node[0])));
return returnRewrite(node, retNode, Rewrite::LEN_EVAL);
}
else if (nk0 == kind::STRING_CONCAT)
{
if (tmpNode[i].isConst())
{
- node_vec.push_back(
- nm->mkConst(Rational(Word::getLength(tmpNode[i]))));
+ node_vec.push_back(nm->mkConst(
+ CONST_RATIONAL, Rational(Word::getLength(tmpNode[i]))));
}
else
{
}
else if (nk0 == SEQ_UNIT)
{
- Node retNode = nm->mkConst(Rational(1));
+ Node retNode = nm->mkConst(CONST_RATIONAL, Rational(1));
return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT);
}
return node;
}
else if (r.getKind() == kind::REGEXP_ALLCHAR)
{
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA);
}
Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]);
if (!flr.isNull())
{
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
if (flr == one)
{
NodeBuilder nb(AND);
if (constStr.isNull())
{
// x in re.++(_*, _, _) ---> str.len(x) >= 2
- Node num = nm->mkConst(Rational(allSigmaMinSize));
+ Node num = nm->mkConst(CONST_RATIONAL, Rational(allSigmaMinSize));
Node lenx = nm->mkNode(STRING_LENGTH, x);
Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
Node s = node[0];
Node n = node[1];
// seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
- Node cond = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkConst(Rational(0)), n),
- nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
+ Node cond =
+ nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), n),
+ nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
Node u = nm->mkNode(APPLY_UF, uf, s, n);
{
Assert(node.getKind() == STRING_CHARAT);
NodeManager* nm = NodeManager::currentNM();
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one);
return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM);
}
}
}
}
- Node zero = nm->mkConst(cvc5::Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0));
// if entailed non-positive length or negative start point
if (d_arithEntail.check(zero, node[1], true))
if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0)
{
// z<0 implies str.indexof( x, y, z ) --> -1
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_NEG);
}
// We know that, due to limitations on the size of string constants
// in our implementation, that accessing a position greater than
// rMaxInt is guaranteed to be out of bounds.
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_MAX);
}
Assert(node[2].getConst<Rational>().sgn() >= 0);
std::size_t ret = Word::find(s, t, start);
if (ret != std::string::npos)
{
- Node retv = nm->mkConst(Rational(static_cast<unsigned>(ret)));
+ Node retv =
+ nm->mkConst(CONST_RATIONAL, Rational(static_cast<unsigned>(ret)));
return returnRewrite(node, retv, Rewrite::IDOF_FIND);
}
else if (children0.size() == 1)
{
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
}
}
if (node[2].getConst<Rational>().sgn() == 0)
{
// indexof( x, x, 0 ) --> 0
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
}
}
if (d_arithEntail.check(node[2], true))
{
// y>0 implies indexof( x, x, y ) --> -1
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
}
Node emp = Word::mkEmptyWord(stype);
if (d_arithEntail.check(len1, len0m2, true))
{
// len(x)-z < len(y) implies indexof( x, y, z ) ----> -1
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_LEN);
}
else
{
// str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
}
}
Node s = node[0];
Node r = node[1];
Node n = node[2];
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
Node slen = nm->mkNode(STRING_LENGTH, s);
if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true))
{
- Node ret = nm->mkConst(Rational(-1));
+ Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX);
}
// We know that, due to limitations on the size of string constants
// in our implementation, that accessing a position greater than
// rMaxInt is guaranteed to be out of bounds.
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, negone, Rewrite::INDEXOF_RE_MAX_INDEX);
}
Node rem = nm->mkConst(s.getConst<String>().substr(start));
std::pair<size_t, size_t> match = firstMatch(rem, r);
Node ret = nm->mkConst(
+ CONST_RATIONAL,
Rational(match.first == string::npos
? -1
: static_cast<int64_t>(start + match.first)));
nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype));
Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
- Node zero = nm->mkConst(Rational(0));
- Node one = nm->mkConst(Rational(1));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
// Check len(t) + j > len(x) + 1
Node val;
if (isPrefix)
{
- val = NodeManager::currentNM()->mkConst(::cvc5::Rational(0));
+ val =
+ NodeManager::currentNM()->mkConst(CONST_RATIONAL, ::cvc5::Rational(0));
}
else
{
{
NodeManager* nm = NodeManager::currentNM();
d_strType = nm->stringType();
- d_zero = nm->mkConst(Rational(0));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
}
Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
{
// SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
id = SK_SUFFIX_REM;
- b = nm->mkConst(Rational(1));
+ b = nm->mkConst(CONST_RATIONAL, Rational(1));
}
else if (id == SK_ID_VC_SPT_REV)
{
// SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
id = SK_PREFIX;
- b = nm->mkNode(
- MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)));
+ b = nm->mkNode(MINUS,
+ nm->mkNode(STRING_LENGTH, a),
+ nm->mkConst(CONST_RATIONAL, Rational(1)));
}
else if (id == SK_ID_DC_SPT)
{
// SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
id = SK_PREFIX;
- b = nm->mkConst(Rational(1));
+ b = nm->mkConst(CONST_RATIONAL, Rational(1));
}
else if (id == SK_ID_DC_SPT_REM)
{
// SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
id = SK_SUFFIX_REM;
- b = nm->mkConst(Rational(1));
+ b = nm->mkConst(CONST_RATIONAL, Rational(1));
}
else if (id == SK_ID_DEQ_X)
{
d_pendingConflictSet(env.getContext(), false),
d_pendingConflict(InferenceId::UNKNOWN)
{
- d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
d_false = NodeManager::currentNM()->mkConst(false);
}
Assert(dir == 1 || dir == -1);
Assert(nr.empty());
NodeManager* nm = NodeManager::currentNM();
- Node zero = nm->mkConst(cvc5::Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0));
bool ret = false;
bool success = true;
unsigned sindex = 0;
Assert(d_arithEntail.check(curr, true));
Node s = n1[sindex_use];
size_t slen = Word::getLength(s);
- Node ncl = nm->mkConst(cvc5::Rational(slen));
+ Node ncl = nm->mkConst(CONST_RATIONAL, cvc5::Rational(slen));
Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
next_s = d_rr->rewrite(next_s);
Assert(next_s.isConst());
}
if (dir != -1)
{
- n1rb = nm->mkNode(
- STRING_SUBSTR, n2[0], nm->mkConst(Rational(0)), start_pos);
+ n1rb = nm->mkNode(STRING_SUBSTR,
+ n2[0],
+ nm->mkConst(CONST_RATIONAL, Rational(0)),
+ start_pos);
}
if (dir != 1)
{
bool StringsEntail::checkLengthOne(Node s, bool strict)
{
NodeManager* nm = NodeManager::currentNM();
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
Node len = nm->mkNode(STRING_LENGTH, s);
len = d_rr->rewrite(len);
return d_arithEntail.check(one, len)
return Node::null();
}
NodeManager* nm = NodeManager::currentNM();
- Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConst(Rational(i)));
+ Node lit = nm->mkNode(
+ LEQ, d_inputVarLsum.get(), nm->mkConst(CONST_RATIONAL, Rational(i)));
Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
return lit;
}
String s = node[0].getConst<String>();
if (s.isNumber())
{
- ret = nm->mkConst(s.toNumber());
+ ret = nm->mkConst(CONST_RATIONAL, s.toNumber());
}
else
{
- ret = nm->mkConst(Rational(-1));
+ ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
}
return returnRewrite(node, ret, Rewrite::STOI_EVAL);
}
String t = nc.getConst<String>();
if (!t.isNumber())
{
- Node ret = nm->mkConst(Rational(-1));
+ Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
}
}
{
std::vector<unsigned> vec = s.getVec();
Assert(vec.size() == 1);
- ret = nm->mkConst(Rational(vec[0]));
+ ret = nm->mkConst(CONST_RATIONAL, Rational(vec[0]));
}
else
{
- ret = nm->mkConst(Rational(-1));
+ ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
}
return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
}
NodeManager* nm = NodeManager::currentNM();
// eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
Node t = nm->mkNode(STRING_TO_CODE, n[0]);
- Node retNode = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkConst(Rational(48)), t),
- nm->mkNode(LEQ, t, nm->mkConst(Rational(57))));
+ Node retNode =
+ nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(48)), t),
+ nm->mkNode(LEQ, t, nm->mkConst(CONST_RATIONAL, Rational(57))));
return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
}
: nullptr)
{
NodeManager* nm = NodeManager::currentNM();
- d_zero = nm->mkConst(Rational(0));
- d_one = nm->mkConst(Rational(1));
- d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+ d_negOne = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
Assert(options().strings.stringsAlphaCard <= String::num_codes());
d_alphaCard = options().strings.stringsAlphaCard;
}
if (tk == STRING_TO_CODE)
{
// ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
- Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
- Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
- Node code_range =
- nm->mkNode(AND,
- nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
- nm->mkNode(LT, t, nm->mkConst(Rational(alphaCard))));
+ Node code_len =
+ utils::mkNLength(t[0]).eqNode(nm->mkConst(CONST_RATIONAL, Rational(1)));
+ Node code_eq_neg1 = t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node code_range = nm->mkNode(
+ AND,
+ nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(0))),
+ nm->mkNode(LT, t, nm->mkConst(CONST_RATIONAL, Rational(alphaCard))));
lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
}
else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
Node l = nm->mkNode(STRING_LENGTH, t[0]);
lemma = nm->mkNode(
AND,
- nm->mkNode(
- OR, t.eqNode(nm->mkConst(Rational(-1))), nm->mkNode(GEQ, t, t[2])),
+ nm->mkNode(OR,
+ t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))),
+ nm->mkNode(GEQ, t, t[2])),
nm->mkNode(LEQ, t, l));
}
else if (tk == STRING_STOI)
{
// (>= (str.to_int x) (- 1))
- lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
+ lemma = nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(-1)));
}
else if (tk == STRING_CONTAINS)
{
Node TermRegistry::lengthPositive(Node t)
{
NodeManager* nm = NodeManager::currentNM();
- Node zero = nm->mkConst(Rational(0));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
Node emp = Word::mkEmptyWord(t.getType());
Node tlen = nm->mkNode(STRING_LENGTH, t);
Node tlenEqZero = tlen.eqNode(zero);
}
else if (n.isConst())
{
- lsum = nm->mkConst(Rational(Word::getLength(n)));
+ lsum = nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(n)));
}
Assert(!lsum.isNull());
d_proxyVarToLength[sk] = lsum;
{
lenN = nm->mkNode(STRING_LENGTH, n[2]);
}
- Node one = nm->mkConst(Rational(1));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
return d_aent.checkEq(lenN, one);
}
{
d_termReg.finishInit(&d_im);
- d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
- d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
- d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
+ d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+ d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+ d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
lvalue++;
}
Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
- lts_values[i] = nm->mkConst(Rational(lvalue));
+ lts_values[i] = nm->mkConst(CONST_RATIONAL, Rational(lvalue));
values_used[lvalue] = Node::null();
}
Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
SkolemCache* sc = d_termReg.getSkolemCache();
Node k = sc->mkSkolemCached(atom, SkolemCache::SK_PURIFY, "kFromCode");
Node t = atom[0];
- Node card = nm->mkConst(Rational(d_termReg.getAlphabetCardinality()));
+ Node card = nm->mkConst(CONST_RATIONAL,
+ Rational(d_termReg.getAlphabetCardinality()));
Node cond =
nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
Node emp = Word::mkEmptyWord(atom.getType());
<< "StringsPreprocess::reduce: " << t << std::endl;
Node retNode = t;
NodeManager* nm = NodeManager::currentNM();
- Node zero = nm->mkConst(Rational(0));
- Node one = nm->mkConst(Rational(1));
- Node negOne = nm->mkConst(Rational(-1));
+ Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+ Node negOne = nm->mkConst(CONST_RATIONAL, Rational(-1));
if( t.getKind() == kind::STRING_SUBSTR ) {
// processing term: substr( s, n, m )
Node skk = sc->mkTypedSkolemCached(
nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
- Node negone = nm->mkConst(Rational(-1));
+ Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
// substr( x, n, len( x ) - n )
Node st = nm->mkNode(STRING_SUBSTR,
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
- Node ten = nm->mkConst(Rational(10));
+ Node ten = nm->mkConst(CONST_RATIONAL, Rational(10));
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
Node leadingZeroPos =
nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
MINUS,
nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
c0);
- Node ten = nm->mkConst(Rational(10));
+ Node ten = nm->mkConst(CONST_RATIONAL, Rational(10));
Node kc3 = nm->mkNode(
OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten));
conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one));
Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one));
- Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
- Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
- Node offset =
- nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32));
+ Node lb = nm->mkConst(CONST_RATIONAL,
+ Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
+ Node ub = nm->mkConst(CONST_RATIONAL,
+ Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
+ Node offset = nm->mkConst(
+ CONST_RATIONAL, Rational(t.getKind() == STRING_TOUPPER ? -32 : 32));
Node res = nm->mkNode(
ITE,
Node mkPrefix(Node t, Node n)
{
NodeManager* nm = NodeManager::currentNM();
- return nm->mkNode(STRING_SUBSTR, t, nm->mkConst(Rational(0)), n);
+ return nm->mkNode(
+ STRING_SUBSTR, t, nm->mkConst(CONST_RATIONAL, Rational(0)), n);
}
Node mkSuffix(Node t, Node n)
{
TypeNode integer = d_nodeManager->integerType();
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
Node x = d_nodeManager->mkBoundVar(integer);
Node a = d_skolemManager->mkDummySkolem("a", integer);
Node cons_1_nil =
d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
cons,
- d_nodeManager->mkConst(Rational(1)),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
Node cons_1_cons_2_nil = d_nodeManager->mkNode(
APPLY_CONSTRUCTOR,
cons,
- d_nodeManager->mkConst(Rational(1)),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
cons,
- d_nodeManager->mkConst(Rational(2)),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)),
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
ASSERT_FALSE(cons_x_nil.isConst());
TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->integerType());
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
ASSERT_TRUE(storeAll.isConst());
Node p = d_nodeManager->mkNode(
EQUAL,
- d_nodeManager->mkConst<Rational>(0),
+ d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0),
d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
TEST_F(TestNodeBlackNodeManager, mkConst_rational)
{
Rational r("3/2");
- Node n = d_nodeManager->mkConst(r);
+ Node n = d_nodeManager->mkConst(CONST_RATIONAL, r);
ASSERT_EQ(n.getConst<Rational>(), r);
}
namespace cvc5 {
using namespace cvc5::expr;
+using namespace cvc5::kind;
namespace test {
TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
{
Rational i("3");
- Node n = d_nodeManager->mkConst(i);
- Node m = d_nodeManager->mkConst(i);
+ Node n = d_nodeManager->mkConst(CONST_RATIONAL, i);
+ Node m = d_nodeManager->mkConst(CONST_RATIONAL, i);
ASSERT_EQ(n.getId(), m.getId());
}
Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
- Node two = d_nodeManager->mkConst(Rational(2));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
TypeNode bvType = d_nodeManager->mkBitVectorType(32);
Node x = d_nodeManager->mkBoundVar("x", realType);
- Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
+ Node xPos = d_nodeManager->mkNode(
+ GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
Node lambda = d_nodeManager->mkVar("lambda", funtype);
std::vector<Node> formals;
#include "test_smt.h"
#include "util/rational.h"
-namespace cvc5 {
-
-using namespace preprocessing::passes;
+using namespace cvc5::kind;
+using namespace cvc5::preprocessing::passes;
+namespace cvc5 {
namespace test {
class TestPPWhiteForeignTheoryRewrite : public TestSmt
std::cout << "len(x) >= 0 is simplified to true" << std::endl;
Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType());
Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x);
- Node zero = d_nodeManager->mkConst<Rational>(0);
+ Node zero = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0);
Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero);
Node tt = d_nodeManager->mkConst<bool>(true);
Node simplified1 = ftr.foreignRewrite(geq1);
TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int)
{
TypeNode intType = d_nodeManager->integerType();
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
Node x = d_nodeManager->mkVar("x", intType);
Node y = d_nodeManager->mkVar("y", intType);
Node z = d_nodeManager->mkVar("z", intType);
TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real)
{
TypeNode realType = d_nodeManager->realType();
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node half = d_nodeManager->mkConst(Rational(1) / Rational(2));
- Node two = d_nodeManager->mkConst(Rational(2));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node half = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1) / Rational(2));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
Node x = d_nodeManager->mkVar("x", realType);
Node y = d_nodeManager->mkVar("y", realType);
#include "theory/rewriter.h"
#include "util/rational.h"
-namespace cvc5 {
-
-using namespace theory;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+namespace cvc5 {
namespace test {
class TestTheoryWhiteEvaluator : public TestSmt
{
Node a = d_nodeManager->mkConst(String("A"));
Node empty = d_nodeManager->mkConst(String(""));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
std::vector<Node> args;
std::vector<Node> vals;
{
Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
+ ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(65)));
}
// (str.code "") ---> -1
{
Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
Node r = eval.eval(n, args, vals);
- ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
+ ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
}
}
} // namespace test
#include "util/rational.h"
#include "util/string.h"
-namespace cvc5 {
-
-using namespace theory;
-using namespace theory::strings;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+using namespace cvc5::theory::strings;
+namespace cvc5 {
namespace test {
class TestTheoryWhiteSequencesRewriter : public TestSmt
Node b = d_nodeManager->mkConst(::cvc5::String("B"));
Node x = d_nodeManager->mkVar("x", strType);
Node y = d_nodeManager->mkVar("y", strType);
- Node negOne = d_nodeManager->mkConst(Rational(-1));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node i = d_nodeManager->mkVar("i", intType);
ASSERT_TRUE(se.checkLengthOne(a));
Node z = d_nodeManager->mkVar("z", strType);
Node n = d_nodeManager->mkVar("n", intType);
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
// 1 >= (str.len (str.substr z n 1)) ---> true
Node substr_z = d_nodeManager->mkNode(
Node y = d_nodeManager->mkVar("y", strType);
Node z = d_nodeManager->mkVar("z", intType);
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node empty = d_nodeManager->mkConst(::cvc5::String(""));
Node a = d_nodeManager->mkConst(::cvc5::String("A"));
ASSERT_TRUE(ae.checkWithAssumption(
x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
- Node five = d_nodeManager->mkConst(Rational(5));
- Node six = d_nodeManager->mkConst(Rational(6));
+ Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
+ Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6));
Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five);
Node x_plus_five_lt_six =
d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
Node a = d_nodeManager->mkConst(::cvc5::String("A"));
Node b = d_nodeManager->mkConst(::cvc5::String("B"));
Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
- Node negone = d_nodeManager->mkConst(Rational(-1));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node negone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node s = d_nodeManager->mkVar("s", strType);
Node s2 = d_nodeManager->mkVar("s2", strType);
n = d_nodeManager->mkNode(
kind::STRING_SUBSTR,
a,
- d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
+ d_nodeManager->mkNode(
+ kind::PLUS, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))),
x);
sameNormalForm(n, empty);
Node empty = d_nodeManager->mkConst(::cvc5::String(""));
Node a = d_nodeManager->mkConst(::cvc5::String("A"));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node i = d_nodeManager->mkVar("i", intType);
Node s = d_nodeManager->mkVar("s", strType);
Node ccc = d_nodeManager->mkConst(::cvc5::String("CCC"));
Node x = d_nodeManager->mkVar("x", strType);
Node y = d_nodeManager->mkVar("y", strType);
- Node negOne = d_nodeManager->mkConst(Rational(-1));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node i = d_nodeManager->mkVar("i", intType);
Node j = d_nodeManager->mkVar("j", intType);
Node x = d_nodeManager->mkVar("x", strType);
Node y = d_nodeManager->mkVar("y", strType);
Node z = d_nodeManager->mkVar("z", strType);
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node n = d_nodeManager->mkVar("n", intType);
// (str.replace (str.replace x "B" x) x "A") -->
Node z = d_nodeManager->mkVar("z", strType);
Node n = d_nodeManager->mkVar("n", intType);
Node m = d_nodeManager->mkVar("m", intType);
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
- Node three = d_nodeManager->mkConst(Rational(3));
- Node four = d_nodeManager->mkConst(Rational(4));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+ Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
Node t = d_nodeManager->mkConst(true);
Node f = d_nodeManager->mkConst(false);
Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a);
Node f = d_nodeManager->mkConst(false);
Node n = d_nodeManager->mkVar("n", intType);
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
// Same normal form for:
//
namespace cvc5::test {
using namespace cvc5;
+using namespace cvc5::kind;
using namespace cvc5::theory;
using namespace cvc5::theory::arith;
using namespace cvc5::theory::arith::nl;
nodeManager = d_nodeManager;
}
- Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); }
+ Node dummy(int i) const
+ {
+ return d_nodeManager->mkConst(CONST_RATIONAL, Rational(i));
+ }
Theory::Effort d_level = Theory::EFFORT_FULL;
std::unique_ptr<TypeNode> d_realType;
Node a = d_nodeManager->mkVar(*d_realType);
Node c = d_nodeManager->mkVar(*d_realType);
Node orig = d_nodeManager->mkAnd(std::vector<Node>{
- d_nodeManager->mkNode(Kind::EQUAL, a, d_nodeManager->mkConst(d_zero)),
+ d_nodeManager->mkNode(
+ Kind::EQUAL, a, d_nodeManager->mkConst(CONST_RATIONAL, d_zero)),
d_nodeManager->mkNode(
Kind::EQUAL,
d_nodeManager->mkNode(
Kind::PLUS,
d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c),
- d_nodeManager->mkConst(d_one)),
- d_nodeManager->mkConst(d_zero))});
+ d_nodeManager->mkConst(CONST_RATIONAL, d_one)),
+ d_nodeManager->mkConst(CONST_RATIONAL, d_zero))});
{
Node rewritten = Rewriter::rewrite(orig);
TEST_F(TestTheoryWhiteArithCAD, test_delta_one)
{
std::vector<Node> a;
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node mone = d_nodeManager->mkConst(Rational(-1));
- Node fifth = d_nodeManager->mkConst(Rational(1, 2));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
+ Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2));
Node g = make_real_variable("g");
Node l = make_real_variable("l");
Node q = make_real_variable("q");
TEST_F(TestTheoryWhiteArithCAD, test_delta_two)
{
std::vector<Node> a;
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node mone = d_nodeManager->mkConst(Rational(-1));
- Node fifth = d_nodeManager->mkConst(Rational(1, 2));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
+ Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2));
Node g = make_real_variable("g");
Node l = make_real_variable("l");
Node q = make_real_variable("q");
d_slvEngine->setOption("produce-models", "true");
d_slvEngine->finishInit();
d_true = d_nodeManager->mkConst<bool>(true);
- d_one = d_nodeManager->mkConst<Rational>(Rational(1));
+ d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1));
}
Node d_true;
Node d_one;
TEST_F(TestTheoryWhiteArith, assert)
{
Node x = d_nodeManager->mkVar(*d_realType);
- Node c = d_nodeManager->mkConst<Rational>(d_zero);
+ Node c = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero);
Node gt = d_nodeManager->mkNode(GT, x, c);
Node leq = Rewriter::rewrite(gt.notNode());
{
Node x = d_nodeManager->mkVar(*d_intType);
Node xr = d_nodeManager->mkVar(*d_realType);
- Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
- Node c1 = d_nodeManager->mkConst<Rational>(d_one);
- Node c2 = d_nodeManager->mkConst<Rational>(Rational(2));
+ Node c0 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero);
+ Node c1 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_one);
+ Node c2 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(2));
Node geq0 = d_nodeManager->mkNode(GEQ, x, c0);
Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(1)));
+ Node negative = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node zero =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+ Node positive =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
// (bag.count "x" (union_disjoint (mkBag "x" 4) (mkBag "y" 5)) = 4
// (bag.count "x" (union_disjoint (mkBag "y" 5) (mkBag "z" 5)) = 0
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node four = d_nodeManager->mkConst(Rational(4));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
Node empty = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
- Node z_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(5)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node y_5 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+ Node z_5 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty);
Node output1 = zero;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
-
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
+ Node x_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node y_5 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
Node input2 = d_nodeManager->mkNode(DUPLICATE_REMOVAL, x_4);
Node output2 = x_1;
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node x_3 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node x_7 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+ Node z_2 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
std::vector<Node> elements = getNStrings(3);
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(2)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(3)));
- Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[2],
- d_nodeManager->mkConst(Rational(4)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node B =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node C =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[2],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
// unionDisjointAB is already in a normal form
ASSERT_EQ(unionDisjointA_BC, NormalForm::evaluate(unionDisjointAB_C));
Node unionDisjointAA = d_nodeManager->mkNode(UNION_DISJOINT, A, A);
- Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(4)));
+ Node AA =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
ASSERT_FALSE(unionDisjointAA.isConst());
ASSERT_TRUE(AA.isConst());
ASSERT_EQ(AA, NormalForm::evaluate(unionDisjointAA));
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node x_3 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node x_7 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+ Node z_2 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node x_3 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node x_7 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+ Node z_2 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node x_3 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node x_7 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+ Node z_2 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node x_3 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(3)));
- Node x_7 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(7)));
- Node z_2 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), z, d_nodeManager->mkConst(Rational(2)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node x_3 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node x_7 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+ Node z_2 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ z,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node A = d_nodeManager->mkNode(UNION_DISJOINT, x_4, z_2);
Node B = d_nodeManager->mkNode(UNION_DISJOINT, x_3, y_1);
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node input1 = d_nodeManager->mkNode(BAG_CARD, empty);
- Node output1 = d_nodeManager->mkConst(Rational(0));
+ Node output1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
ASSERT_EQ(output1, NormalForm::evaluate(input1));
Node input2 = d_nodeManager->mkNode(BAG_CARD, x_4);
- Node output2 = d_nodeManager->mkConst(Rational(4));
+ Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
ASSERT_EQ(output2, NormalForm::evaluate(input2));
Node union_disjoint = d_nodeManager->mkNode(UNION_DISJOINT, x_4, y_1);
Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint);
- Node output3 = d_nodeManager->mkConst(Rational(5));
+ Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
ASSERT_EQ(output3, NormalForm::evaluate(input3));
}
Node x = d_nodeManager->mkConst(String("x"));
Node y = d_nodeManager->mkConst(String("y"));
Node z = d_nodeManager->mkConst(String("z"));
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty);
Node output1 = falseNode;
Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
- Node x_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
- Node y_1 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(1)));
+ Node x_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+ Node y_1 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton);
Node output2 = x_1;
Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
- Node x_4 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(4)));
- Node y_5 = d_nodeManager->mkBag(
- d_nodeManager->stringType(), y, d_nodeManager->mkConst(Rational(5)));
+ Node x_4 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node y_5 =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ y,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4);
Node output2 = xSingleton;
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node emptyString = d_nodeManager->mkConst(String(""));
- Node constantBag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- emptyString,
- d_nodeManager->mkConst(Rational(1)));
+ Node constantBag =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ emptyString,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
// (= A A) = true where A is a bag
Node n1 = A.eqNode(A);
TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(1)));
+ Node negative = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node zero =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+ Node positive =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
{
Node skolem =
d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConst(Rational(-1)));
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- skolem,
- d_nodeManager->mkConst(Rational(-1)));
- Node zero = d_nodeManager->mkBag(
- d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(0)));
- Node positive = d_nodeManager->mkBag(
- d_nodeManager->stringType(), skolem, d_nodeManager->mkConst(Rational(1)));
+ Node variable = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ skolem,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node negative = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ skolem,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node zero =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ skolem,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+ Node positive =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ skolem,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
{
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node three = d_nodeManager->mkConst(Rational(3));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node skolem =
d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node emptyBag = d_nodeManager->mkConst(
TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node bag = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
+ Node bag =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
// (duplicate_removal (mkBag x n)) = (mkBag x 1)
Node n = d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag);
RewriteResponse response = d_rewriter->postRewrite(n);
- Node noDuplicate = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(1)));
+ Node noDuplicate =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
ASSERT_TRUE(response.d_node == noDuplicate
&& response.d_status == REWRITE_AGAIN_FULL);
}
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(n + 1)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
+ Node B = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(3);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(n + 1)));
- Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[2],
- d_nodeManager->mkConst(Rational(n + 2)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
+ Node B = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
+ Node C = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[2],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2)));
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
Node unionDisjointBA = d_nodeManager->mkNode(UNION_DISJOINT, B, A);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(n + 1)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
+ Node B = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(n + 1)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
+ Node B = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
std::vector<Node> elements = getNStrings(2);
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(n)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(n + 1)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
+ Node B = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
Node unionMaxAB = d_nodeManager->mkNode(UNION_MAX, A, B);
Node unionMaxBA = d_nodeManager->mkNode(UNION_MAX, B, A);
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
TEST_F(TestTheoryWhiteBagsRewriter, choose)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node c = d_nodeManager->mkConst(Rational(3));
+ Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
// (bag.choose (mkBag x c)) = x where c is a constant > 0
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node c = d_nodeManager->mkConst(Rational(3));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
std::vector<Node> elements = getNStrings(2);
- Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(4)));
- Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[1],
- d_nodeManager->mkConst(Rational(5)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+ Node B =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[1],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
// TODO(projects#223): enable this test after implementing bags normal form
// (bag.is_singleton (mkBag x c) = (c == 1)
Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag);
RewriteResponse response2 = d_rewriter->postRewrite(n2);
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node equal = c.eqNode(one);
ASSERT_TRUE(response2.d_node == equal
&& response2.d_status == REWRITE_AGAIN_FULL);
// (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
RewriteResponse response = d_rewriter->postRewrite(n);
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one);
ASSERT_TRUE(response.d_node == bag
&& response.d_status == REWRITE_AGAIN_FULL);
TEST_F(TestTheoryWhiteBagsRewriter, to_set)
{
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
- Node bag = d_nodeManager->mkBag(
- d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
+ Node bag =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ x,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
// (bag.to_set (mkBag x n)) = (singleton (singleton_op T) x)
Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
std::vector<Node> elements = getNStrings(2);
Node a = d_nodeManager->mkConst(String("a"));
Node b = d_nodeManager->mkConst(String("b"));
- Node A = d_nodeManager->mkBag(
- d_nodeManager->stringType(), a, d_nodeManager->mkConst(Rational(3)));
- Node B = d_nodeManager->mkBag(
- d_nodeManager->stringType(), b, d_nodeManager->mkConst(Rational(4)));
+ Node A =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ a,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
+ Node B =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ b,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
Node unionDisjointAB = d_nodeManager->mkNode(UNION_DISJOINT, A, B);
ASSERT_TRUE(unionDisjointAB.isConst());
Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
Node rewritten = Rewriter::rewrite(n2);
- Node bag = d_nodeManager->mkBag(
- d_nodeManager->stringType(), empty, d_nodeManager->mkConst(Rational(7)));
+ Node bag =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ empty,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
ASSERT_TRUE(rewritten == bag);
}
TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(100)));
+ Node bag = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(100)));
Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag);
- Node node = d_nodeManager->mkConst(Rational(10));
+ Node node = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10));
// node of type Int is not compatible with bag of type (Bag String)
ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true),
TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(10)));
+ Node bag = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
ASSERT_NO_THROW(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag));
ASSERT_EQ(d_nodeManager->mkNode(DUPLICATE_REMOVAL, bag).getType(),
bag.getType());
TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(-1)));
- Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(0)));
- Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(1)));
+ Node negative = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+ Node zero =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+ Node positive =
+ d_nodeManager->mkBag(d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
// only positive multiplicity are constants
ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative));
TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(10)));
+ Node bag = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag));
ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
}
TEST_F(TestTheoryWhiteBagsTypeRule, map_operator)
{
std::vector<Node> elements = getNStrings(1);
- Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
- elements[0],
- d_nodeManager->mkConst(Rational(10)));
+ Node bag = d_nodeManager->mkBag(
+ d_nodeManager->stringType(),
+ elements[0],
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
Node set =
d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
ASSERT_EQ(d_nodeManager->integerType(),
mappedBag.getType().getBagElementType());
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node x2 = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
std::vector<Node> args2;
args2.push_back(x2);
{
TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->integerType());
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
ASSERT_TRUE(storeAll.isConst());
d_slvEngine->setOption("produce-models", "true");
d_slvEngine->finishInit();
d_true = d_nodeManager->mkConst<bool>(true);
- d_one = d_nodeManager->mkConst<Rational>(Rational(1));
+ d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1));
}
Node d_true;
Node d_one;
IntBlaster intBlaster(
env, options::SolveBVAsIntMode::SUM, 1, false);
Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems);
- Node seven = d_nodeManager->mkConst(Rational(7));
+ Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7));
ASSERT_EQ(seven, result);
// translating integer constants should not change them
Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType());
// make the expression (PLUS x y (MULT z 0))
- Node zero = d_nodeManager->mkConst(Rational("0"));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero);
Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero);
"g",
d_nodeManager->mkFunctionType(d_nodeManager->realType(),
d_nodeManager->integerType()));
- Node one = d_nodeManager->mkConst(Rational("1"));
- Node two = d_nodeManager->mkConst(Rational("2"));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational("1"));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational("2"));
Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one);
Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two);
#include "test_smt.h"
#include "util/rational.h"
-namespace cvc5 {
-
-using namespace theory;
-using namespace smt;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+using namespace cvc5::smt;
+namespace cvc5 {
namespace test {
class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
TEST_F(TestTheoryWhiteIntOpt, max)
{
- Node ub = d_nodeManager->mkConst(Rational("100"));
- Node lb = d_nodeManager->mkConst(Rational("0"));
+ Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
+ Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
// Objectives to be optimized max_cost is max objective
Node max_cost = d_nodeManager->mkVar(*d_intType);
TEST_F(TestTheoryWhiteIntOpt, min)
{
- Node ub = d_nodeManager->mkConst(Rational("100"));
- Node lb = d_nodeManager->mkConst(Rational("0"));
+ Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
+ Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
// Objectives to be optimized max_cost is max objective
Node max_cost = d_nodeManager->mkVar(*d_intType);
TEST_F(TestTheoryWhiteIntOpt, result)
{
- Node ub = d_nodeManager->mkConst(Rational("100"));
- Node lb = d_nodeManager->mkConst(Rational("0"));
+ Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
+ Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
// Objectives to be optimized max_cost is max objective
Node max_cost = d_nodeManager->mkVar(*d_intType);
TEST_F(TestTheoryWhiteIntOpt, open_interval)
{
- Node ub1 = d_nodeManager->mkConst(Rational("100"));
- Node lb1 = d_nodeManager->mkConst(Rational("0"));
- Node lb2 = d_nodeManager->mkConst(Rational("110"));
+ Node ub1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
+ Node lb1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
+ Node lb2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("110"));
Node cost1 = d_nodeManager->mkVar(*d_intType);
Node cost2 = d_nodeManager->mkVar(*d_intType);
#include "theory/sets/singleton_op.h"
#include "util/rational.h"
-namespace cvc5 {
-
using namespace cvc5::api;
+namespace cvc5 {
namespace test {
class TestTheoryWhiteSetsTypeRuleApi : public TestApi
d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->integerType()));
Node singletonReal =
d_nodeManager->mkConst(SetSingletonOp(d_nodeManager->realType()));
- Node intConstant = d_nodeManager->mkConst(Rational(1));
- Node realConstant = d_nodeManager->mkConst(Rational(1, 5));
+ Node intConstant = d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1));
+ Node realConstant =
+ d_nodeManager->mkConst(kind::CONST_RATIONAL, Rational(1, 5));
// (singleton (singleton_op Real) 1)
ASSERT_NO_THROW(
d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant));
#include "util/rational.h"
#include "util/string.h"
-namespace cvc5 {
-
-using namespace theory::strings;
+using namespace cvc5::kind;
+using namespace cvc5::theory::strings;
+namespace cvc5 {
namespace test {
class TestTheoryBlackStringsSkolemCache : public TestSmt
TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
{
- Node zero = d_nodeManager->mkConst(Rational(0));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType());
Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType());
Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType());
{
TypeEnumerator te(d_nodeManager->integerType());
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0)));
+ ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
for (int i = 1; i <= 100; ++i)
{
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(i)));
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-i)));
}
ASSERT_FALSE(te.isFinished());
te = TypeEnumerator(d_nodeManager->realType());
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3)));
+ ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 3)));
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 4)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 4)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 1)));
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(6, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-6, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 2)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 4)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 4)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 6)));
ASSERT_FALSE(te.isFinished());
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7)));
- ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 6)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(7, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-7, 1)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 3)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 5)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 7)));
+ ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 7)));
ASSERT_FALSE(te.isFinished());
}
// ensure that certain items were found
TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->integerType());
- Node zeroes = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0))));
- Node ones = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1))));
- Node twos = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2))));
- Node threes = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3))));
- Node fours = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4))));
- Node tens = d_nodeManager->mkConst(
- ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10))));
+ Node zeroes = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))));
+ Node ones = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))));
+ Node twos = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))));
+ Node threes = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))));
+ Node fours = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))));
+ Node tens = d_nodeManager->mkConst(ArrayStoreAll(
+ arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))));
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
- Node three = d_nodeManager->mkConst(Rational(3));
- Node four = d_nodeManager->mkConst(Rational(4));
- Node five = d_nodeManager->mkConst(Rational(5));
- Node eleven = d_nodeManager->mkConst(Rational(11));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+ Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+ Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+ Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+ Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
+ Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
+ Node eleven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(11));
ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)),
elts.end());
#include "test_smt.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace test {
TypeNode usort = d_nodeManager->mkSort("U");
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->realType()),
- d_nodeManager->mkConst(Rational(9, 2)));
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
d_nodeManager->mkConst(UninterpretedConstant(usort, 0)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
d_nodeManager->realType()),
- d_nodeManager->mkConst(Rational(0)));
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
d_nodeManager->integerType()),
- d_nodeManager->mkConst(Rational(0)));
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
}
TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
d_nodeManager->mkConst(UninterpretedConstant(
d_nodeManager->mkSort("U"), 0))),
IllegalArgumentException);
- ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
- d_nodeManager->mkConst(Rational(9, 2))),
- IllegalArgumentException);
+ ASSERT_THROW(
+ ArrayStoreAll(d_nodeManager->integerType(),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))),
+ IllegalArgumentException);
ASSERT_THROW(
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->mkSort("U")),
- d_nodeManager->mkConst(Rational(9, 2))),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))),
IllegalArgumentException);
}
IllegalArgumentException);
ASSERT_THROW(
ArrayStoreAll(d_nodeManager->integerType(),
- d_nodeManager->mkNode(kind::PLUS,
- d_nodeManager->mkConst(Rational(1)),
- d_nodeManager->mkConst(Rational(0)))),
+ d_nodeManager->mkNode(
+ kind::PLUS,
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
+ d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))),
IllegalArgumentException);
}
} // namespace test
#include "test_smt.h"
#include "util/rational.h"
+using namespace cvc5::kind;
+
namespace cvc5 {
namespace test {
const DType& ldt = listType.getDType();
Node updater = ldt[0][0].getUpdater();
Node gt = listType.mkGroundTerm();
- Node zero = d_nodeManager->mkConst(Rational(0));
+ Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
Node truen = d_nodeManager->mkConst(true);
// construct an update term
Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero);
projects / cvc5.git / commitdiff