Changes since 1.2
=================
+* SMT-LIB support for abs, to_real, to_int, is_int
+* Support in linear logics for /, div, and mod by constants.
* We no longer permit model or proof generation if there's been an
intervening push/pop.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
This kind of problem can be identified by checking TCCs. Though CVC4 does not
(yet) support TCCs, CVC3 can be used to produce TCCs for this input (with the
-+dump-tcc option). The TCC can be checked by CVC3 or another solver. (CVC3 can
-also check TCCs while solving with +tcc.)
++dump-tcc option). The TCC can then be checked by CVC4 or another solver.
+(CVC3 can also check TCCs at the same time it creates them, with +tcc.)
** Changes in CVC's Presentation Language
CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
support decimals.
-CVC4 does not have support for the IS_INTEGER predicate, or for predicate
-subtypes, although these are planned for future releases.
+CVC4 does not have support for predicate subtypes, although these are
+planned for future releases.
** SMT-LIB compliance
args.size() > 2 ) {
/* "chainable", but CVC4 internally only supports 2 args */
expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
+ } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
+ args.size() == 1 && !args[0].getType().isInteger() ) {
+ /* first, check that ABS is even defined in this logic */
+ PARSER_STATE->checkOperator(kind, args.size());
+ PARSER_STATE->parseError("abs can only be applied to Int, not Real, while in strict SMT-LIB compliance mode");
} else {
PARSER_STATE->checkOperator(kind, args.size());
expr = MK_EXPR(kind, args);
| /* An indexed function application */
LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK
- { expr = MK_EXPR(op, args); }
-
+ { expr = MK_EXPR(op, args);
+ PARSER_STATE->checkOperator(expr.getKind(), args.size());
+ }
| /* a let binding */
LPAREN_TOK LET_TOK LPAREN_TOK
{ PARSER_STATE->pushScope(true); }
{ op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
| 'rotate_right' n=INTEGER_LITERAL
{ op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
+ | DIVISIBLE_TOK n=INTEGER_LITERAL
+ { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
| badIndexedFunctionName
)
RPAREN_TOK
| DIV_TOK { $kind = CVC4::kind::DIVISION; }
| INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; }
| INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; }
+ | ABS_TOK { $kind = CVC4::kind::ABS; }
+ | IS_INT_TOK { $kind = CVC4::kind::IS_INTEGER; }
+ | TO_INT_TOK { $kind = CVC4::kind::TO_INTEGER; }
+ | TO_REAL_TOK { $kind = CVC4::kind::TO_REAL; }
| SELECT_TOK { $kind = CVC4::kind::SELECT; }
| STORE_TOK { $kind = CVC4::kind::STORE; }
GREATER_THAN_TOK : '>';
GREATER_THAN_EQUAL_TOK : '>=';
IMPLIES_TOK : '=>';
+IS_INT_TOK : 'is_int';
LESS_THAN_TOK : '<';
LESS_THAN_EQUAL_TOK : '<=';
MINUS_TOK : '-';
STAR_TOK : '*';
STORE_TOK : 'store';
// TILDE_TOK : '~';
+TO_INT_TOK : 'to_int';
+TO_REAL_TOK : 'to_real';
XOR_TOK : 'xor';
INTS_DIV_TOK : 'div';
INTS_MOD_TOK : 'mod';
+ABS_TOK : 'abs';
+
+DIVISIBLE_TOK : 'divisible';
CONCAT_TOK : 'concat';
BVNOT_TOK : 'bvnot';
case THEORY_REALS_INTS:
defineType("Real", getExprManager()->realType());
addOperator(kind::DIVISION);
+ addOperator(kind::TO_INTEGER);
+ addOperator(kind::IS_INTEGER);
+ addOperator(kind::TO_REAL);
// falling through on purpose, to add Ints part of Reals_Ints
case THEORY_INTS:
addArithmeticOperators();
addOperator(kind::INTS_DIVISION);
addOperator(kind::INTS_MODULUS);
+ addOperator(kind::ABS);
+ addOperator(kind::DIVISIBLE);
break;
case THEORY_REALS:
if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
if(d_logic.areIntegersUsed()) {
- addTheory(THEORY_INTS);
- }
-
- if(d_logic.areRealsUsed()) {
+ if(d_logic.areRealsUsed()) {
+ addTheory(THEORY_REALS_INTS);
+ } else {
+ addTheory(THEORY_INTS);
+ }
+ } else if(d_logic.areRealsUsed()) {
addTheory(THEORY_REALS);
}
}
case kind::INTS_DIVISION:
case kind::INTS_DIVISION_TOTAL:
case kind::INTS_MODULUS:
- case kind::INTS_MODULUS_TOTAL: out << smtKindString(k) << " "; break;
+ case kind::INTS_MODULUS_TOTAL:
+ case kind::ABS: out << smtKindString(k) << " "; break;
+ case kind::IS_INTEGER:
+ case kind::TO_INTEGER:
+ case kind::TO_REAL: out << smtKindString(k) << " "; break;
+
+ case kind::DIVISIBLE:
+ out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
+ stillNeedToPrintParams = false;
+ break;
// arrays theory
case kind::SELECT:
case kind::INTS_DIVISION_TOTAL: return "div";
case kind::INTS_MODULUS:
case kind::INTS_MODULUS_TOTAL: return "mod";
+ case kind::ABS: return "abs";
+ case kind::IS_INTEGER: return "is_int";
+ case kind::TO_INTEGER: return "to_int";
+ case kind::TO_REAL: return "to_real";
// arrays theory
case kind::SELECT: return "select";
k != kind::TUPLE_SELECT &&
k != kind::TUPLE_UPDATE &&
k != kind::RECORD_SELECT &&
- k != kind::RECORD_UPDATE) {
+ k != kind::RECORD_UPDATE &&
+ k != kind::DIVISIBLE) {
Debug("bt") << "rewriting: " << top.getOperator() << endl;
result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
Debug("bt") << "got: " << result.top().getOperator() << endl;
node = expandBVDivByZero(node);
break;
}
+
case kind::DIVISION: {
// partial function: division
if(d_divByZero.isNull()) {
break;
}
+ case kind::ABS: {
+ Node out = nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
+ cache[n] = out;
+ return out;
+ }
+
case kind::APPLY: {
// application of a user-defined symbol
TNode func = n.getOperator();
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
hash_map<Node, Node, NodeHashFunction> cache;
- for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+ for(unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
d_assertionsToPreprocess[i] =
expandDefinitions(d_assertionsToPreprocess[i], cache);
}
namespace arith {
bool ArithRewriter::isAtom(TNode n) {
- return arith::isRelationOperator(n.getKind());
+ Kind k = n.getKind();
+ return arith::isRelationOperator(k) || k == kind::IS_INTEGER || k == kind::DIVISIBLE;
}
RewriteResponse ArithRewriter::rewriteConstant(TNode t){
return preRewritePlus(t);
case kind::MULT:
return preRewriteMult(t);
- //case kind::INTS_DIVISION:
- //case kind::INTS_MODULUS:
+ case kind::INTS_DIVISION:
+ case kind::INTS_MODULUS:
+ return RewriteResponse(REWRITE_DONE, t);
case kind::INTS_DIVISION_TOTAL:
case kind::INTS_MODULUS_TOTAL:
return rewriteIntsDivModTotal(t,true);
+ case kind::ABS:
+ if(t[0].isConst()) {
+ const Rational& rat = t[0].getConst<Rational>();
+ if(rat >= 0) {
+ return RewriteResponse(REWRITE_DONE, t[0]);
+ } else {
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(-rat));
+ }
+ }
+ return RewriteResponse(REWRITE_DONE, t);
+ case kind::IS_INTEGER:
+ case kind::TO_INTEGER:
+ return RewriteResponse(REWRITE_DONE, t);
+ case kind::TO_REAL:
+ return RewriteResponse(REWRITE_DONE, t[0]);
default:
Unhandled(k);
}
return postRewritePlus(t);
case kind::MULT:
return postRewriteMult(t);
- //case kind::INTS_DIVISION:
- //case kind::INTS_MODULUS:
+ case kind::INTS_DIVISION:
+ case kind::INTS_MODULUS:
+ return RewriteResponse(REWRITE_DONE, t);
case kind::INTS_DIVISION_TOTAL:
case kind::INTS_MODULUS_TOTAL:
return rewriteIntsDivModTotal(t, false);
+ case kind::ABS:
+ if(t[0].isConst()) {
+ const Rational& rat = t[0].getConst<Rational>();
+ if(rat >= 0) {
+ return RewriteResponse(REWRITE_DONE, t[0]);
+ } else {
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(-rat));
+ }
+ }
+ case kind::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())));
+ }
+ if(t[0].getType().isInteger()) {
+ return RewriteResponse(REWRITE_DONE, t[0]);
+ }
+ //Unimplemented("TO_INTEGER, nonconstant");
+ //return rewriteToInteger(t);
+ return RewriteResponse(REWRITE_DONE, t);
+ case kind::IS_INTEGER:
+ if(t[0].isConst()) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst<Rational>().getDenominator() == 1));
+ }
+ if(t[0].getType().isInteger()) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+ }
+ //Unimplemented("IS_INTEGER, nonconstant");
+ //return rewriteIsInteger(t);
+ return RewriteResponse(REWRITE_DONE, t);
default:
Unreachable();
}
}
RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
+ if(atom.getKind() == kind::IS_INTEGER) {
+ if(atom[0].isConst()) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst<Rational>().isIntegral()));
+ }
+ if(atom[0].getType().isInteger()) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+ }
+ // not supported, but this isn't the right place to complain
+ return RewriteResponse(REWRITE_DONE, atom);
+ } else if(atom.getKind() == kind::DIVISIBLE) {
+ if(atom[0].isConst()) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst<Rational>() / atom.getOperator().getConst<Divisible>().k).isIntegral())));
+ }
+ 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))));
+ }
+
// left |><| right
TNode left = atom[0];
TNode right = atom[1];
}else if(atom.getKind() == kind::LT){
Node geq = currNM->mkNode(kind::GEQ, atom[0], atom[1]);
return RewriteResponse(REWRITE_DONE, currNM->mkNode(kind::NOT, geq));
+ }else if(atom.getKind() == kind::IS_INTEGER){
+ if(atom[0].getType().isInteger()){
+ return RewriteResponse(REWRITE_DONE, currNM->mkConst(true));
+ }
+ }else if(atom.getKind() == kind::DIVISIBLE){
+ if(atom.getOperator().getConst<Divisible>().k.isOne()){
+ return RewriteResponse(REWRITE_DONE, currNM->mkConst(true));
+ }
}
return RewriteResponse(REWRITE_DONE, atom);
Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
return RewriteResponse(REWRITE_AGAIN, n);
}
+ }else if(dIsConstant && d.getConst<Rational>().isNegativeOne()){
+ if(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL){
+ return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+ }else{
+ Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
+ return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::UMINUS, n));
+ }
}else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){
Assert(d.getConst<Rational>().isIntegral());
Assert(n.getConst<Rational>().isIntegral());
operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)"
operator INTS_MODULUS 2 "ints modulus (user symbol)"
operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)"
+operator ABS 1 "absolute value"
+parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate"
operator POW 2 "arithmetic power"
+constant DIVISIBLE_OP \
+ ::CVC4::Divisible \
+ ::CVC4::DivisibleHashFunction \
+ "util/divisible.h" \
+ "operator for the divisibility-by-k predicate"
+
sort REAL_TYPE \
Cardinality::REALS \
well-founded \
operator GT 2 "greater than, x > y"
operator GEQ 2 "greater than or equal, x >= y"
+operator IS_INTEGER 1 "term is integer"
+operator TO_INTEGER 1 "cast term to integer"
+operator TO_REAL 1 "cast term to real"
+
typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule
typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
+
+typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
+typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
endtheory
case kind::INTS_MODULUS_TOTAL:
case kind::DIVISION_TOTAL:
return isDivMember(n);
+ case kind::ABS:
+ case kind::TO_INTEGER:
+ // Treat to_int as a variable; it is replaced in early preprocessing
+ // by a variable.
+ return true;
default:
return (!isRelationOperator(k)) &&
(Theory::isLeafOf(n, theory::THEORY_ARITH));
option soiQuickExplain --soi-qe bool :default false :read-write
Use quick explain to minimize the sum of infeasibility conflicts.
+option rewriteDivk rewrite-divk --rewrite-divk bool :default false
+ rewrite division and mod when by a constant into linear terms
endmodule
}
Node TheoryArith::ppRewrite(TNode atom) {
+ CodeTimer timer(d_ppRewriteTimer);
return d_internal->ppRewrite(atom);
}
TheoryArithPrivate* d_internal;
+ KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
public:
TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
}
}
+namespace attr {
+ struct ToIntegerTag { };
+ struct LinearIntDivTag { };
+}/* CVC4::theory::arith::attr namespace */
+
+/**
+ * This attribute maps the child of a to_int / is_int to the
+ * corresponding integer skolem.
+ */
+typedef expr::Attribute<attr::ToIntegerTag, Node> ToIntegerAttr;
+
+/**
+ * This attribute maps division-by-constant-k terms to a variable
+ * used to eliminate them.
+ */
+typedef expr::Attribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
+
+Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
+ if(Theory::theoryOf(n) != THEORY_ARITH) {
+ return n;
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ switch(Kind k = n.getKind()) {
+
+ case kind::TO_INTEGER:
+ case kind::IS_INTEGER: {
+ Node intVar;
+ if(!n[0].getAttribute(ToIntegerAttr(), intVar)) {
+ intVar = nm->mkSkolem("toInt", nm->integerType(), "a conversion of a Real term to its Integer part");
+ n[0].setAttribute(ToIntegerAttr(), intVar);
+ d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LT, nm->mkNode(kind::MINUS, n[0], nm->mkConst(Rational(1))), intVar), nm->mkNode(kind::LEQ, intVar, n[0])));
+ }
+ if(n.getKind() == kind::TO_INTEGER) {
+ Node node = intVar;
+ return node;
+ } else {
+ Node node = nm->mkNode(kind::EQUAL, node[0], intVar);
+ return node;
+ }
+ Unreachable();
+ }
+
+ case kind::INTS_DIVISION:
+ case kind::INTS_DIVISION_TOTAL: {
+ if(!options::rewriteDivk()) {
+ return n;
+ }
+ Node num = Rewriter::rewrite(n[0]);
+ Node den = Rewriter::rewrite(n[1]);
+ if(den.isConst()) {
+ const Rational& rat = den.getConst<Rational>();
+ Assert(!num.isConst());
+ if(rat != 0) {
+ Node intVar;
+ Node rw = nm->mkNode(k, num, den);
+ if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
+ intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
+ rw.setAttribute(LinearIntDivAttr(), intVar);
+ if(rat > 0) {
+ d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
+ } else {
+ d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
+ }
+ }
+ return intVar;
+ }
+ }
+ break;
+ }
+
+ case kind::INTS_MODULUS:
+ case kind::INTS_MODULUS_TOTAL: {
+ if(!options::rewriteDivk()) {
+ return n;
+ }
+ Node num = Rewriter::rewrite(n[0]);
+ Node den = Rewriter::rewrite(n[1]);
+ if(den.isConst()) {
+ const Rational& rat = den.getConst<Rational>();
+ Assert(!num.isConst());
+ if(rat != 0) {
+ Node intVar;
+ Node rw = nm->mkNode(k, num, den);
+ if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
+ intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
+ rw.setAttribute(LinearIntDivAttr(), intVar);
+ if(rat > 0) {
+ d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
+ } else {
+ d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
+ }
+ }
+ Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar));
+ return node;
+ }
+ }
+ break;
+ }
+
+ default:
+ ;
+ }
+
+ for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) {
+ Node rewritten = ppRewriteTerms(*i);
+ if(rewritten != *i) {
+ NodeBuilder<> b(n.getKind());
+ b.append(n.begin(), i);
+ b << rewritten;
+ for(++i; i != n.end(); ++i) {
+ b << ppRewriteTerms(*i);
+ }
+ rewritten = b;
+ return rewritten;
+ }
+ }
+
+ return n;
+}
+
Node TheoryArithPrivate::ppRewrite(TNode atom) {
Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
-
if (atom.getKind() == kind::EQUAL && options::arithRewriteEq()) {
Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+ leq = ppRewriteTerms(leq);
+ geq = ppRewriteTerms(geq);
Node rewritten = Rewriter::rewrite(leq.andNode(geq));
Debug("arith::preprocess") << "arith::preprocess() : returning "
<< rewritten << endl;
return rewritten;
} else {
- return atom;
+ return ppRewriteTerms(atom);
}
}
// vl is the product of at least 2 variables
// vl : (* v1 v2 ...)
if(getLogicInfo().isLinear()){
- throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+ throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
}
setIncomplete();
Assert(v.isDivLike());
if(getLogicInfo().isLinear()){
- throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+ throw LogicException("A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic;\nif you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.");
}
Node vnode = v.getNode();
void TheoryArithPrivate::preRegisterTerm(TNode n) {
Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
- if(isRelationOperator(n.getKind())){
- if(!isSetup(n)){
- setupAtom(n);
+ try {
+ if(isRelationOperator(n.getKind())){
+ if(!isSetup(n)){
+ setupAtom(n);
+ }
+ Constraint c = d_constraintDatabase.lookup(n);
+ Assert(c != NullConstraint);
+
+ Debug("arith::preregister") << "setup constraint" << c << endl;
+ Assert(!c->canBePropagated());
+ c->setPreregistered();
}
- Constraint c = d_constraintDatabase.lookup(n);
- Assert(c != NullConstraint);
-
- Debug("arith::preregister") << "setup constraint" << c << endl;
- Assert(!c->canBePropagated());
- c->setPreregistered();
+ } catch(LogicException& le) {
+ std::stringstream ss;
+ ss << le.getMessage() << endl << "The fact in question: " << n << endl;
+ throw LogicException(ss.str());
}
Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
//TODO : The VarList trick is good enough?
Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
- throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+ stringstream ss;
+ ss << "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: " << x << endl
+ << "if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.";
+ throw LogicException(ss.str());
}
Assert(!d_partialModel.hasArithVar(x));
Assert(x.getType().isReal()); // real or integer
Node axiomIteForTotalDivision(Node div_tot);
Node axiomIteForTotalIntDivision(Node int_div_like);
-
+ // handle linear /, div, mod, and also is_int, to_int
+ Node ppRewriteTerms(TNode atom);
public:
TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
}
}
}
- Kind k = n.getKind();
- bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
- return (isInteger && !isDivision ? integerType : realType);
+ switch(Kind k = n.getKind()) {
+ case kind::TO_REAL:
+ return realType;
+ case kind::TO_INTEGER:
+ return integerType;
+ default: {
+ bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
+ return (isInteger && !isDivision ? integerType : realType);
+ }
+ }
}
};/* class ArithOperatorTypeRule */
+class IntOperatorTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TNode::iterator child_it = n.begin();
+ TNode::iterator child_it_end = n.end();
+ if(check) {
+ for(; child_it != child_it_end; ++child_it) {
+ TypeNode childType = (*child_it).getType(check);
+ if (!childType.isInteger()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
+ }
+ }
+ }
+ return nodeManager->integerType();
+ }
+};/* class IntOperatorTypeRule */
+
class ArithPredicateTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
}
};/* class ArithPredicateTypeRule */
+class ArithUnaryPredicateTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ if( check ) {
+ TypeNode t = n[0].getType(check);
+ if (!t.isReal()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* class ArithUnaryPredicateTypeRule */
+
+class IntUnaryPredicateTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ if( check ) {
+ TypeNode t = n[0].getType(check);
+ if (!t.isInteger()) {
+ throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* class IntUnaryPredicateTypeRule */
+
class SubrangeProperties {
public:
inline static Cardinality computeCardinality(TypeNode type) {
datatype.h \
datatype.cpp \
tuple.h \
- maybe.h \
record.h \
record.cpp \
+ divisible.h \
+ divisible.cpp \
+ maybe.h \
matcher.h \
gmp_util.h \
sexpr.h \
datatype.i \
tuple.i \
record.i \
+ divisible.i \
output.i \
cardinality.i \
result.i \
div.06.smt2 \
div.07.smt2 \
div.08.smt2 \
- div.09.smt2 \
mult.01.smt2 \
mult.02.smt2 \
bug443.delta01.smt \
miplib-pp08a-3000.smt \
miplib-pp08a-3000.smt2 \
miplib-opt1217--27.smt.expect \
- miplib-pp08a-3000.smt.expect
+ miplib-pp08a-3000.smt.expect \
+ div.09.smt2
#if CVC4_BUILD_PROFILE_COMPETITION
#else
-; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.")
+; EXPECT: (error "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: (/ n n)
+; EXPECT: if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.
+; EXPECT: The fact in question: (>= (+ (* (- 1) (/ n n)) termITE_132) 0)
+; EXPECT: ")
; EXIT: 1
(set-logic QF_LRA)
(set-info :status unknown)
-; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.")
+; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
+; EXPECT: The fact in question: (>= (* (- 1) (* n n)) (- 1))
+; EXPECT: ")
; EXIT: 1
(set-logic QF_LRA)
(set-info :status unknown)
projects / cvc5.git / commitdiff