summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS2
-rw-r--r--RELEASE-NOTES8
-rw-r--r--src/parser/smt2/Smt2.g22
-rw-r--r--src/parser/smt2/smt2.cpp15
-rw-r--r--src/printer/smt2/smt2_printer.cpp15
-rw-r--r--src/smt/boolean_terms.cpp3
-rw-r--r--src/smt/smt_engine.cpp9
-rw-r--r--src/theory/arith/arith_rewriter.cpp95
-rw-r--r--src/theory/arith/kinds26
-rw-r--r--src/theory/arith/normal_form.h5
-rw-r--r--src/theory/arith/options2
-rw-r--r--src/theory/arith/theory_arith.cpp1
-rw-r--r--src/theory/arith/theory_arith.h1
-rw-r--r--src/theory/arith/theory_arith_private.cpp160
-rw-r--r--src/theory/arith/theory_arith_private.h3
-rw-r--r--src/theory/arith/theory_arith_type_rules.h59
-rw-r--r--src/util/Makefile.am5
-rw-r--r--test/regress/regress0/arith/Makefile.am4
-rw-r--r--test/regress/regress0/arith/div.09.smt25
-rw-r--r--test/regress/regress0/arith/mult.02.smt24
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<Divisible>().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_map<Node, Node, NodeHashF
node = expandBVDivByZero(node);
break;
}
+
case kind::DIVISION: {
// partial function: division
if(d_divByZero.isNull()) {
@@ -1423,6 +1424,12 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
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();
@@ -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<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);
}
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<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);
}
@@ -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<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();
}
@@ -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<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];
@@ -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<Divisible>().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<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());
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<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);
}
}
@@ -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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback