From 8c794ae1009bf8515b965c1023de188f50b35d60 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 29 Jun 2020 21:55:51 -0500 Subject: [PATCH] Add internal support for integer and operator (#4668) Towards merging iand branch to master. This adds internal support for an "integer AND" operator. --- src/CMakeLists.txt | 1 + src/bindings/java/CMakeLists.txt | 1 + src/cvc4.i | 2 + src/theory/arith/arith_rewriter.cpp | 50 ++++++++++++++++++++-- src/theory/arith/arith_rewriter.h | 4 +- src/theory/arith/congruence_manager.cpp | 1 + src/theory/arith/kinds | 14 ++++++ src/theory/arith/normal_form.cpp | 6 +++ src/theory/arith/normal_form.h | 2 + src/theory/arith/theory_arith.cpp | 1 + src/theory/arith/theory_arith_type_rules.h | 43 +++++++++++++++++++ src/util/CMakeLists.txt | 1 + src/util/iand.h | 47 ++++++++++++++++++++ src/util/iand.i | 9 ++++ 14 files changed, 177 insertions(+), 5 deletions(-) create mode 100644 src/util/iand.h create mode 100644 src/util/iand.i diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6850ef450..0774d60af 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1001,6 +1001,7 @@ install(FILES util/divisible.h util/gmp_util.h util/hash.h + util/iand.h util/integer_cln_imp.h util/integer_gmp_imp.h util/maybe.h diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 8e919db86..8159b8ee0 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -81,6 +81,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java + ${CMAKE_CURRENT_BINARY_DIR}/IntAnd.java ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java ${CMAKE_CURRENT_BINARY_DIR}/Integer.java ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java diff --git a/src/cvc4.i b/src/cvc4.i index 4fc0b092a..9fc8ed60e 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -40,6 +40,7 @@ using namespace CVC4; #include "smt/command.h" #include "util/bitvector.h" #include "util/floatingpoint.h" +#include "util/iand.h" #include "util/integer.h" #include "util/sexpr.h" #include "util/unsafe_interrupt_exception.h" @@ -206,6 +207,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "util/integer.i" %include "util/rational.i" %include "util/bitvector.i" +%include "util/iand.i" %include "util/floatingpoint.i" // Tim: The remainder of util/. 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().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().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 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 */ diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index eba5fb8c9..028288dbc 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -17,6 +17,7 @@ libcvc4_add_sources( floatingpoint.cpp gmp_util.h hash.h + iand.h index.cpp index.h maybe.h diff --git a/src/util/iand.h b/src/util/iand.h new file mode 100644 index 000000000..b5bc92960 --- /dev/null +++ b/src/util/iand.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file iand.h + ** \verbatim + ** Top contributors (to current version): + ** Anrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The integer AND operator. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__IAND_H +#define CVC4__IAND_H + +#include +#include + +#include "base/exception.h" +#include "util/integer.h" + +namespace CVC4 { + +struct CVC4_PUBLIC IntAnd +{ + unsigned d_size; + IntAnd(unsigned size) : d_size(size) {} + operator unsigned() const { return d_size; } +}; /* struct IntAnd */ + +/* ----------------------------------------------------------------------- + ** Output stream + * ----------------------------------------------------------------------- */ + +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) +{ + return os << "[" << ia.d_size << "]"; +} + +} // namespace CVC4 + +#endif /* CVC4__IAND_H */ diff --git a/src/util/iand.i b/src/util/iand.i new file mode 100644 index 000000000..92c5a1223 --- /dev/null +++ b/src/util/iand.i @@ -0,0 +1,9 @@ +%{ +#include "util/iand.h" +%} + +%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const; + +%ignore CVC4::operator<<(std::ostream&, const IntAnd&); + +%include "util/iand.h" -- 2.30.2