From 0a3422299da7e882bae22c5fa3e5ec3c80b42046 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 24 Jun 2013 19:35:58 -0400 Subject: [PATCH] Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant. --- NEWS | 2 + RELEASE-NOTES | 8 +- src/parser/smt2/Smt2.g | 22 ++- src/parser/smt2/smt2.cpp | 15 +- src/printer/smt2/smt2_printer.cpp | 15 +- src/smt/boolean_terms.cpp | 3 +- src/smt/smt_engine.cpp | 9 +- src/theory/arith/arith_rewriter.cpp | 95 +++++++++++- src/theory/arith/kinds | 26 +++- src/theory/arith/normal_form.h | 5 + src/theory/arith/options | 2 + src/theory/arith/theory_arith.cpp | 1 + src/theory/arith/theory_arith.h | 1 + src/theory/arith/theory_arith_private.cpp | 160 +++++++++++++++++++-- src/theory/arith/theory_arith_private.h | 3 +- src/theory/arith/theory_arith_type_rules.h | 59 +++++++- src/util/Makefile.am | 5 +- test/regress/regress0/arith/Makefile.am | 4 +- test/regress/regress0/arith/div.09.smt2 | 5 +- test/regress/regress0/arith/mult.02.smt2 | 4 +- 20 files changed, 399 insertions(+), 45 deletions(-) diff --git a/NEWS b/NEWS index 0532716a9..bd54ae81a 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,8 @@ This file contains a summary of important user-visible changes. 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 diff --git a/RELEASE-NOTES b/RELEASE-NOTES index b45602d87..136051d0b 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -36,8 +36,8 @@ For example: 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 @@ -69,8 +69,8 @@ QUERY commands. 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index cb9a13c20..190eb19ba 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -787,6 +787,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] 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); @@ -876,8 +881,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | /* 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); } @@ -1092,6 +1098,8 @@ indexedFunctionName[CVC4::Expr& op] { 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 @@ -1164,6 +1172,10 @@ builtinOp[CVC4::Kind& kind] | 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; } @@ -1502,6 +1514,7 @@ FORALL_TOK : 'forall'; GREATER_THAN_TOK : '>'; GREATER_THAN_EQUAL_TOK : '>='; IMPLIES_TOK : '=>'; +IS_INT_TOK : 'is_int'; LESS_THAN_TOK : '<'; LESS_THAN_EQUAL_TOK : '<='; MINUS_TOK : '-'; @@ -1514,10 +1527,15 @@ SELECT_TOK : 'select'; 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'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 42324fe1e..7a1fdf174 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -111,6 +111,9 @@ void Smt2::addTheory(Theory theory) { 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: @@ -118,6 +121,8 @@ void Smt2::addTheory(Theory theory) { addArithmeticOperators(); addOperator(kind::INTS_DIVISION); addOperator(kind::INTS_MODULUS); + addOperator(kind::ABS); + addOperator(kind::DIVISIBLE); break; case THEORY_REALS: @@ -157,10 +162,12 @@ void Smt2::setLogic(const std::string& name) { 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); } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f4abee292..007b4ea82 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -256,7 +256,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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().k << ")"; + stillNeedToPrintParams = false; + break; // arrays theory case kind::SELECT: @@ -442,6 +451,10 @@ static string smtKindString(Kind k) throw() { 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"; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index b3e69619f..80518fcdf 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -736,7 +736,8 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa 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; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ca89ce36d..2d2e8e099 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1366,6 +1366,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkNode(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(); @@ -2691,7 +2698,7 @@ void SmtEnginePrivate::processAssertions() { Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); hash_map 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); } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index aa5049ed4..247c09294 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -29,7 +29,8 @@ namespace theory { 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){ @@ -98,11 +99,28 @@ RewriteResponse ArithRewriter::preRewriteTerm(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(); + 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); } @@ -126,11 +144,44 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ 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(); + 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().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().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(); } @@ -190,6 +241,25 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ } 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().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() / atom.getOperator().getConst().k).isIntegral()))); + } + if(atom.getOperator().getConst().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().k))), NodeManager::currentNM()->mkConst(Rational(0)))); + } + // left |><| right TNode left = atom[0]; TNode right = atom[1]; @@ -217,6 +287,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ }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().k.isOne()){ + return RewriteResponse(REWRITE_DONE, currNM->mkConst(true)); + } } return RewriteResponse(REWRITE_DONE, atom); @@ -329,6 +407,13 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); return RewriteResponse(REWRITE_AGAIN, n); } + }else if(dIsConstant && d.getConst().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().isIntegral()); Assert(n.getConst().isIntegral()); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 07cfcc9e5..a8a4047ca 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -23,8 +23,16 @@ operator INTS_DIVISION 2 "ints division (user symbol)" 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 \ @@ -72,6 +80,10 @@ operator LEQ 2 "less than or equal, x <= y" 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 @@ -86,11 +98,17 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule 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 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index c6af7010f..1dddb5a5b 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -241,6 +241,11 @@ public: 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)); diff --git a/src/theory/arith/options b/src/theory/arith/options index 7d92f5351..57ef3d1b9 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -100,5 +100,7 @@ option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-wri 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 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c0442da90..120ac0154 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -47,6 +47,7 @@ void TheoryArith::addSharedTerm(TNode n){ } Node TheoryArith::ppRewrite(TNode atom) { + CodeTimer timer(d_ppRewriteTimer); return d_internal->ppRewrite(atom); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 10c79b293..6b9fd5515 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -42,6 +42,7 @@ private: 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); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index dd5e404c6..a01397973 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -737,19 +737,142 @@ void TheoryArithPrivate::addSharedTerm(TNode n){ } } +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 ToIntegerAttr; + +/** + * This attribute maps division-by-constant-k terms to a variable + * used to eliminate them. + */ +typedef expr::Attribute 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(); + 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(); + 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); } } @@ -902,7 +1025,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ // 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(); @@ -939,7 +1062,7 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ 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(); @@ -1161,16 +1284,22 @@ void TheoryArithPrivate::setupAtom(TNode atom) { 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; @@ -1187,7 +1316,10 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){ //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 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 86c8e213e..7370cfc15 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -346,7 +346,8 @@ private: 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); diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index cc8451f8b..45e18fe0d 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -62,12 +62,37 @@ public: } } } - 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) @@ -87,6 +112,34 @@ public: } };/* 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) { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 4f93f5a61..51eb5cb1a 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -39,9 +39,11 @@ libutil_la_SOURCES = \ 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 \ @@ -122,6 +124,7 @@ EXTRA_DIST = \ datatype.i \ tuple.i \ record.i \ + divisible.i \ output.i \ cardinality.i \ result.i \ diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 40f04b239..6c5eded7c 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ div.06.smt2 \ div.07.smt2 \ div.08.smt2 \ - div.09.smt2 \ mult.01.smt2 \ mult.02.smt2 \ bug443.delta01.smt \ @@ -52,7 +51,8 @@ EXTRA_DIST = $(TESTS) \ 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 diff --git a/test/regress/regress0/arith/div.09.smt2 b/test/regress/regress0/arith/div.09.smt2 index 2f1bca63a..9bcb93476 100644 --- a/test/regress/regress0/arith/div.09.smt2 +++ b/test/regress/regress0/arith/div.09.smt2 @@ -1,4 +1,7 @@ -; 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) diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 index d690e38e8..54b876d38 100644 --- a/test/regress/regress0/arith/mult.02.smt2 +++ b/test/regress/regress0/arith/mult.02.smt2 @@ -1,4 +1,6 @@ -; 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) -- 2.30.2