summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/bindings/java/CMakeLists.txt1
-rw-r--r--src/cvc4.i2
-rw-r--r--src/theory/arith/arith_rewriter.cpp50
-rw-r--r--src/theory/arith/arith_rewriter.h4
-rw-r--r--src/theory/arith/congruence_manager.cpp1
-rw-r--r--src/theory/arith/kinds14
-rw-r--r--src/theory/arith/normal_form.cpp6
-rw-r--r--src/theory/arith/normal_form.h2
-rw-r--r--src/theory/arith/theory_arith.cpp1
-rw-r--r--src/theory/arith/theory_arith_type_rules.h43
-rw-r--r--src/util/CMakeLists.txt1
-rw-r--r--src/util/iand.h47
-rw-r--r--src/util/iand.i9
14 files changed, 177 insertions, 5 deletions
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<JavaInputStreamAdapter*> 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<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 */
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 <cstdint>
+#include <iosfwd>
+
+#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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback