Also fixes a debug failure for the nightlies.
This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples).
integers and reals. Type rules for other operators like `APPLY_UF` now
require their arguments to match the type of the function being applied, and
do not assume integer/real subtyping.
+- The API method `mkTuple` no longer supports casting integers to reals when
+ constructing tuples.
cvc5 1.0
return Term(this, fun);
}
-Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
-{
- // Note: Term and sort are checked in the caller to avoid double checks
- CVC5_API_CHECK(term.getSort() == sort
- || (term.getSort().isInteger() && sort.isReal()))
- << "Expected conversion from Int to Real";
- //////// all checks before this line
-
- Sort t = term.getSort();
- if (term.getSort() == sort)
- {
- return term;
- }
-
- // Integers are reals, too
- Assert(t.d_type->isReal());
- Term res = term;
- if (t.isInteger())
- {
- // Must cast to Real to ensure correct type is passed to parametric type
- // constructors. We do this cast using division with 1. This has the
- // advantage wrt using TO_REAL since (constant) division is always included
- // in the theory.
- res = Term(this,
- d_nodeMgr->mkNode(extToIntKind(DIVISION),
- *res.d_node,
- d_nodeMgr->mkConstInt(internal::Rational(1))));
- }
- Assert(res.getSort() == sort);
- return res;
-}
-
bool Solver::isValidInteger(const std::string& s) const
{
//////// all checks before this line
<< "Expected the same number of sorts and elements";
CVC5_API_SOLVER_CHECK_SORTS(sorts);
CVC5_API_SOLVER_CHECK_TERMS(terms);
+ for (size_t i = 0, size = sorts.size(); i < size; i++)
+ {
+ CVC5_API_CHECK(terms[i].getSort() == sorts[i])
+ << "Type mismatch in mkTuple";
+ }
//////// all checks before this line
std::vector<internal::Node> args;
for (size_t i = 0, size = sorts.size(); i < size; i++)
{
- args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node);
+ args.push_back(*terms[i].d_node);
}
Sort s = mkTupleSortHelper(sorts);
CVC5_API_SOLVER_CHECK_TERM(term);
//////// all checks before this line
Term res = Term(this, d_slv->simplify(*term.d_node));
- Assert(res.getSort().d_type->isSubtypeOf(*term.getSort().d_type));
+ Assert(*res.getSort().d_type == *term.getSort().d_type);
return res;
////////
CVC5_API_TRY_CATCH_END;
// SMT-LIB inputs in the Reals theory, where NUMERAL can be used to specify
// reals. Instead of making our parser for numerals dependent on the logic,
// we instead allow integers here in this case.
- CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type))
+ CVC5_API_CHECK(term.d_node->getType() == *sort.d_type)
<< "Invalid sort of function body '" << term << "', expected '" << sort
<< "'";
CVC5_API_SOLVER_CHECK_TERM(term);
CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
// we are permissive with subtypes, similar to defineFun
- CVC5_API_CHECK(term.d_node->getType().isSubtypeOf(*sort.d_type))
+ CVC5_API_CHECK(term.d_node->getType() == *sort.d_type)
<< "Invalid sort of function body '" << term << "', expected '" << sort
<< "'";
CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
Sort codomain = fun.getSort().getFunctionCodomainSort();
// we are permissive with subtypes, similar to defineFun
- CVC5_API_CHECK(codomain.d_type->isSubtypeOf(term.d_node->getType()))
+ CVC5_API_CHECK(*codomain.d_type == term.d_node->getType())
<< "Invalid sort of function body '" << term << "', expected '"
<< codomain << "'";
}
Term mkTerm(const Op& op, const std::vector<Term>& children = {}) const;
/**
- * Create a tuple term. Terms are automatically converted if sorts are
- * compatible.
+ * Create a tuple term, where terms have the provided sorts.
* @param sorts The sorts of the elements in the tuple.
* @param terms The elements in the tuple.
* @return The tuple Term.
/** Check whether string s is a valid decimal integer. */
bool isValidInteger(const std::string& s) const;
- /**
- * If needed, convert this term to a given sort.
- *
- * The sort of the term must be convertible into the target sort.
- * Currently only Int to Real conversions are supported.
- *
- * @param t The term.
- * @param s The target sort.
- * @return The term wrapped into a sort conversion if needed.
- */
- Term ensureTermSort(const Term& t, const Sort& s) const;
-
/**
* Check that the given term is a valid closed term, which can be used as an
* argument to, e.g., assert, get-value, block-model-values, etc.
type.toString().c_str());
PrettyCheckArgument(
- value.getType().isComparableTo(type.getArrayConstituentType()),
+ value.getType() == type.getArrayConstituentType(),
value,
"expr type `%s' does not match constituent type of array type `%s'",
value.getType().toString().c_str(),
// x = (p - ax - c) * -1/a
// Add the substitution if not recursive
Assert(elim == rewrite(elim));
-
+ if (elim.getType().isInteger() && !minVar.getType().isInteger())
+ {
+ elim = NodeManager::currentNM()->mkNode(kind::TO_REAL, elim);
+ }
if (right.size() > options().arith.ppAssertMaxSubSize)
{
Trace("simplify")
// substitution is integral
Trace("simplify") << "TheoryArithPrivate::solve(): substitution "
<< minVar << " |-> " << elim << endl;
- if (elim.getType().isInteger() && !minVar.getType().isInteger())
- {
- elim = NodeManager::currentNM()->mkNode(kind::TO_REAL, elim);
- }
Assert(elim.getType() == minVar.getType());
outSubstitutions.addSubstitutionSolved(minVar, elim, tin);
return Theory::PP_ASSERT_STATUS_SOLVED;
Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
{
NodeManager* nm = NodeManager::currentNM();
- Assert(a.getType().isComparableTo(b.getType()));
+ Assert(a.getType().isRealOrInt() && b.getType().isRealOrInt());
if (status == 0)
{
Node a_eq_b = mkEquality(a, b);
return n;
}
-Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn)
-{
- std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
- if (it == d_tc_skolem[n].end())
- {
- SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
- Node k = sm->mkDummySkolem("tc_k", tn);
- d_tc_skolem[n][tn] = k;
- return k;
- }
- return it->second;
-}
-
void TermRegistry::debugPrintSet(Node s, const char* c) const
{
if (s.getNumChildren() == 0)
InferenceManager& im,
SkolemCache& skc,
ProofNodeManager* pnm);
- /** Get type constraint skolem
- *
- * The sets theory solver outputs equality lemmas of the form:
- * n = d_tc_skolem[n][tn]
- * where the type of d_tc_skolem[n][tn] is tn, and the type
- * of n is not a subtype of tn. This is required to handle benchmarks like
- * test/regress/regress0/sets/sets-of-sets-subtypes.smt2
- * where for s : (Set Int) and t : (Set Real), we have that
- * ( s = t ^ y in t ) implies ( exists k : Int. y = k )
- * The type constraint Skolem for (y, Int) is the skolemization of k above.
- */
- Node getTypeConstraintSkolem(Node n, TypeNode tn);
/** get the proxy variable for set n
*
* Proxy variables are used to communicate information that otherwise would
NodeMap d_proxy;
/** Backwards map of above */
NodeMap d_proxy_to_term;
- /** Cache of type constraint skolems (see getTypeConstraintSkolem) */
- std::map<Node, std::map<TypeNode, Node> > d_tc_skolem;
/** Map from types to empty set of that type */
std::map<TypeNode, Node> d_emptyset;
/** Map from types to universe set of that type */
{
ASSERT_NO_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(3)},
{d_solver.mkBitVector(3, "101", 2)}));
- ASSERT_NO_THROW(
- d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}));
+ ASSERT_THROW(
+ d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}),
+ CVC5ApiException);
ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector(3, "101", 2)}),
CVC5ApiException);
assertDoesNotThrow(()
-> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)},
new Term[] {d_solver.mkBitVector(3, "101", 2)}));
- assertDoesNotThrow(()
- -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()},
- new Term[] {d_solver.mkInteger("5")}));
+ assertThrows(CVC5ApiException.class,
+ ()
+ -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()},
+ new Term[] {d_solver.mkInteger("5")}));
assertThrows(CVC5ApiException.class,
() -> d_solver.mkTuple(new Sort[] {}, new Term[] {d_solver.mkBitVector(3, "101", 2)}));
def test_mk_tuple(solver):
solver.mkTuple([solver.mkBitVectorSort(3)],
[solver.mkBitVector(3, "101", 2)])
- solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")])
+ with pytest.raises(RuntimeError):
+ solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")])
with pytest.raises(RuntimeError):
solver.mkTuple([], [solver.mkBitVector(3, "101", 2)])
ASSERT_EQ(Rewriter::rewrite(absX), absX);
// (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1))
+ Node cr0 = d_nodeManager->mkConstReal(d_zero);
Node t =
d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(ADD, c2, xr))
- .eqNode(c0);
+ .eqNode(cr0);
ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t));
}
} // namespace test
d_nodeManager->mkConst(UninterpretedSortValue(usort, 0)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
d_nodeManager->realType()),
- d_nodeManager->mkConstInt(Rational(0)));
+ d_nodeManager->mkConstReal(Rational(0)));
ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
d_nodeManager->integerType()),
d_nodeManager->mkConstInt(Rational(0)));
d_nodeManager->mkSort("U")),
d_nodeManager->mkConstReal(Rational(9, 2))),
IllegalArgumentException);
+ ASSERT_THROW(ArrayStoreAll(
+ d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
+ d_nodeManager->realType()),
+ d_nodeManager->mkConstInt(Rational(0))),
+ IllegalArgumentException);
}
TEST_F(TestUtilWhiteArrayStoreAll, const_error)
projects / cvc5.git / commitdiff