diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-29 21:55:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 19:55:51 -0700 |
commit | 8c794ae1009bf8515b965c1023de188f50b35d60 (patch) | |
tree | 7dcf7bed2aa581fb806c8b23efe77c33f6632754 /src/theory/arith | |
parent | 19054b3b1d427e662d30d4322df2b2f2361353da (diff) |
Add internal support for integer and operator (#4668)
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 50 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/kinds | 14 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 43 |
8 files changed, 116 insertions, 5 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index e50b79bbc..188ef47e6 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -25,6 +25,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/theory.h" +#include "util/iand.h" namespace CVC4 { namespace theory { @@ -101,8 +102,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::PLUS: return preRewritePlus(t); case kind::MULT: - case kind::NONLINEAR_MULT: - return preRewriteMult(t); + case kind::NONLINEAR_MULT: return preRewriteMult(t); + case kind::IAND: return RewriteResponse(REWRITE_DONE, t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -165,8 +166,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::PLUS: return postRewritePlus(t); case kind::MULT: - case kind::NONLINEAR_MULT: - return postRewriteMult(t); + case kind::NONLINEAR_MULT: return postRewriteMult(t); + case kind::IAND: return postRewriteIAnd(t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -371,6 +372,47 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ return RewriteResponse(REWRITE_DONE, res.getNode()); } +RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) +{ + Assert(t.getKind() == kind::IAND); + NodeManager* nm = NodeManager::currentNM(); + // if constant, we eliminate + if (t[0].isConst() && t[1].isConst()) + { + size_t bsize = t.getOperator().getConst<IntAnd>().d_size; + Node iToBvop = nm->mkConst(IntToBitVector(bsize)); + Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]); + Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]); + Node bvand = nm->mkNode(kind::BITVECTOR_AND, arg1, arg2); + Node ret = nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } + else if (t[0] > t[1]) + { + // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering + Node ret = nm->mkNode(kind::IAND, t.getOperator(), t[1], t[0]); + return RewriteResponse(REWRITE_AGAIN, ret); + } + else if (t[0] == t[1]) + { + // ((_ iand k) x x) ---> x + return RewriteResponse(REWRITE_DONE, t[0]); + } + // simplifications involving constants + for (unsigned i = 0; i < 2; i++) + { + if (!t[i].isConst()) + { + continue; + } + if (t[i].getConst<Rational>().sgn() == 0) + { + // ((_ iand k) 0 y) ---> 0 + return RewriteResponse(REWRITE_DONE, t[i]); + } + } + return RewriteResponse(REWRITE_DONE, t); +} RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) { return RewriteResponse(REWRITE_DONE, t); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 0563aa1de..1dc756514 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -52,7 +52,9 @@ class ArithRewriter : public TheoryRewriter static RewriteResponse preRewriteMult(TNode t); static RewriteResponse postRewriteMult(TNode t); - + + static RewriteResponse postRewriteIAnd(TNode t); + static RewriteResponse preRewriteTranscendental(TNode t); static RewriteResponse postRewriteTranscendental(TNode t); diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 4c35e5d19..858098b70 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -47,6 +47,7 @@ ArithCongruenceManager::ArithCongruenceManager( d_ee.addFunctionKind(kind::NONLINEAR_MULT); d_ee.addFunctionKind(kind::EXPONENTIAL); d_ee.addFunctionKind(kind::SINE); + d_ee.addFunctionKind(kind::IAND); } ArithCongruenceManager::~ArithCongruenceManager() {} diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 409534050..e563d8f66 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -133,4 +133,18 @@ nullaryoperator PI "pi" typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule +# Integer AND, which is parameterized by a (positive) bitwidth k. +# ((_ iand k) i1 i2) is equivalent to: +# (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2))) +# for all integers i1, i2. +constant IAND_OP \ + ::CVC4::IntAnd \ + "::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >" \ + "util/iand.h" \ + "operator for integer AND; payload is an instance of the CVC4::IntAnd class" +parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms" + +typerule IAND_OP ::CVC4::theory::arith::IAndOpTypeRule +typerule IAND ::CVC4::theory::arith::IAndTypeRule + endtheory diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index c7b4b3625..f964f1628 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -71,6 +71,12 @@ bool Variable::isLeafMember(Node n){ VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); } +bool Variable::isIAndMember(Node n) +{ + return n.getKind() == kind::IAND && Polynomial::isMember(n[0]) + && Polynomial::isMember(n[1]); +} + bool Variable::isDivMember(Node n){ switch(n.getKind()){ case kind::DIVISION: diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 3ab5d907a..484bdbf44 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -239,6 +239,7 @@ public: case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: case kind::DIVISION_TOTAL: return isDivMember(n); + case kind::IAND: return isIAndMember(n); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -264,6 +265,7 @@ public: } static bool isLeafMember(Node n); + static bool isIAndMember(Node n); static bool isDivMember(Node n); bool isDivLike() const{ return isDivMember(getNode()); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 30b8ed01d..8b4747927 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -48,6 +48,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, getExtTheory()->addFunctionKind(kind::EXPONENTIAL); getExtTheory()->addFunctionKind(kind::SINE); getExtTheory()->addFunctionKind(kind::PI); + getExtTheory()->addFunctionKind(kind::IAND); } } diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 2d3d8a28b..77efcfff7 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -87,6 +87,49 @@ public: } };/* class RealNullaryOperatorTypeRule */ +class IAndOpTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (n.getKind() != kind::IAND_OP) + { + InternalError() << "IAND_OP typerule invoked for IAND_OP kind"; + } + TypeNode iType = nodeManager->integerType(); + std::vector<TypeNode> argTypes; + argTypes.push_back(iType); + argTypes.push_back(iType); + return nodeManager->mkFunctionType(argTypes, iType); + } +}; /* class IAndOpTypeRule */ + +class IAndTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (n.getKind() != kind::IAND) + { + InternalError() << "IAND typerule invoked for IAND kind"; + } + if (check) + { + TypeNode arg1 = n[0].getType(check); + TypeNode arg2 = n[1].getType(check); + if (!arg1.isInteger() || !arg2.isInteger()) + { + throw TypeCheckingExceptionPrivate(n, "expecting integer terms"); + } + } + return nodeManager->integerType(); + } +}; /* class BitVectorConversionTypeRule */ + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |