summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/bitblast/bitblast_strategies_template.h12
-rw-r--r--src/theory/bv/bitblast/bitblaster.h6
-rw-r--r--src/theory/bv/bv_solver_lazy.cpp4
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp7
-rw-r--r--src/theory/bv/kinds9
-rw-r--r--src/theory/bv/theory_bv.cpp55
-rw-r--r--src/theory/bv/theory_bv.h15
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h8
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h8
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h21
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp19
11 files changed, 35 insertions, 129 deletions
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 8bab969c5..2cc1b7e68 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -517,7 +517,7 @@ void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb)
{
Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node
<< "\n";
- Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0);
+ Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0);
std::vector<T> a, b;
bb->bbTerm(node[0], a);
@@ -540,8 +540,8 @@ void DefaultUdivBB(TNode node, std::vector<T>& q, TBitblaster<T>* bb)
}
// cache the remainder in case we need it later
- Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
- kind::BITVECTOR_UREM_TOTAL, node[0], node[1]));
+ Node remainder = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_UREM, node[0], node[1]));
bb->storeBBTerm(remainder, r);
}
@@ -550,7 +550,7 @@ void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb)
{
Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node
<< "\n";
- Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0);
+ Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0);
std::vector<T> a, b;
bb->bbTerm(node[0], a);
@@ -573,8 +573,8 @@ void DefaultUremBB(TNode node, std::vector<T>& rem, TBitblaster<T>* bb)
}
// cache the quotient in case we need it later
- Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
- kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]));
+ Node quotient = Rewriter::rewrite(
+ NodeManager::currentNM()->mkNode(kind::BITVECTOR_UDIV, node[0], node[1]));
bb->storeBBTerm(quotient, q);
}
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index a1763d081..1e9db1597 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -160,10 +160,8 @@ void TBitblaster<T>::initTermBBStrategies()
d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB<T>;
d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB<T>;
d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB<T>;
- d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy<T>;
- d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB<T>;
- d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_UDIV] = DefaultUdivBB<T>;
+ d_termBBStrategies[kind::BITVECTOR_UREM] = DefaultUremBB<T>;
d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy<T>;
d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy<T>;
d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy<T>;
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 3cadac621..fbf295a85 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -208,7 +208,7 @@ void BVSolverLazy::checkForLemma(TNode fact)
if (fact.getKind() == kind::EQUAL)
{
NodeManager* nm = NodeManager::currentNM();
- if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL)
+ if (fact[0].getKind() == kind::BITVECTOR_UREM)
{
TNode urem = fact[0];
TNode result = fact[1];
@@ -220,7 +220,7 @@ void BVSolverLazy::checkForLemma(TNode fact)
kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div);
lemma(split);
}
- if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL)
+ if (fact[1].getKind() == kind::BITVECTOR_UREM)
{
TNode urem = fact[1];
TNode result = fact[0];
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e1230a56c..003e9dd1a 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -781,9 +781,10 @@ AlgebraicSolver::Statistics::~Statistics() {
}
bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
- if (fact.getKind() == kind::BITVECTOR_MULT ||
- fact.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
- fact.getKind() == kind::BITVECTOR_UREM_TOTAL) {
+ if (fact.getKind() == kind::BITVECTOR_MULT
+ || fact.getKind() == kind::BITVECTOR_UDIV
+ || fact.getKind() == kind::BITVECTOR_UREM)
+ {
return true;
}
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index f9caf119a..32e0e9e85 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -56,14 +56,12 @@ operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
-operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)"
-operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)"
+operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
+operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
operator BITVECTOR_SDIV 2 "2's complement signed division"
operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
# total division kinds
-operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
-operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
## shift kinds
operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
@@ -183,9 +181,6 @@ typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-# total division kinds
-typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
## shift kinds
typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 47974fc03..52bb55757 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -36,8 +36,6 @@ TheoryBV::TheoryBV(context::Context* c,
std::string name)
: Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
d_internal(nullptr),
- d_ufDivByZero(),
- d_ufRemByZero(),
d_rewriter(),
d_state(c, u, valuation),
d_im(*this, d_state, nullptr, "theory::bv"),
@@ -126,46 +124,6 @@ void TheoryBV::finishInit()
}
}
-Node TheoryBV::getUFDivByZero(Kind k, unsigned width)
-{
- NodeManager* nm = NodeManager::currentNM();
- if (k == kind::BITVECTOR_UDIV)
- {
- if (d_ufDivByZero.find(width) == d_ufDivByZero.end())
- {
- // lazily create the function symbols
- std::ostringstream os;
- os << "BVUDivByZero_" << width;
- Node divByZero =
- nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width),
- nm->mkBitVectorType(width)),
- "partial bvudiv",
- NodeManager::SKOLEM_EXACT_NAME);
- d_ufDivByZero[width] = divByZero;
- }
- return d_ufDivByZero[width];
- }
- else if (k == kind::BITVECTOR_UREM)
- {
- if (d_ufRemByZero.find(width) == d_ufRemByZero.end())
- {
- std::ostringstream os;
- os << "BVURemByZero_" << width;
- Node divByZero =
- nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width),
- nm->mkBitVectorType(width)),
- "partial bvurem",
- NodeManager::SKOLEM_EXACT_NAME);
- d_ufRemByZero[width] = divByZero;
- }
- return d_ufRemByZero[width];
- }
-
- Unreachable();
-}
-
TrustNode TheoryBV::expandDefinition(Node node)
{
Debug("bitvector-expandDefinition")
@@ -180,19 +138,6 @@ TrustNode TheoryBV::expandDefinition(Node node)
ret = TheoryBVRewriter::eliminateBVSDiv(node);
break;
- case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM:
- {
- NodeManager* nm = NodeManager::currentNM();
-
- Kind kind = node.getKind() == kind::BITVECTOR_UDIV
- ? kind::BITVECTOR_UDIV_TOTAL
- : kind::BITVECTOR_UREM_TOTAL;
- ret = nm->mkNode(kind, node[0], node[1]);
- break;
- }
- break;
-
default: break;
}
if (!ret.isNull() && node != ret)
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fafde0601..685f25a92 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -107,24 +107,9 @@ class TheoryBV : public Theory
private:
void notifySharedTerm(TNode t) override;
- /**
- * Return the UF symbol corresponding to division-by-zero for this particular
- * bit-width.
- * @param k should be UREM or UDIV
- * @param width bit-width
- */
- Node getUFDivByZero(Kind k, unsigned width);
-
/** Internal BV solver. */
std::unique_ptr<BVSolver> d_internal;
- /**
- * Maps from bit-vector width to division-by-zero uninterpreted
- * function symbols.
- */
- std::unordered_map<unsigned, Node> d_ufDivByZero;
- std::unordered_map<unsigned, Node> d_ufRemByZero;
-
/** The theory rewriter for this theory. */
TheoryBVRewriter d_rewriter;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index dfcc4f052..2334d96f2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -198,9 +198,7 @@ Node RewriteRule<EvalNeg>::apply(TNode node) {
}
template<> inline
bool RewriteRule<EvalUdiv>::applies(TNode node) {
- return (utils::isBvConstTerm(node) &&
- (node.getKind() == kind::BITVECTOR_UDIV_TOTAL ||
- (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst())));
+ return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UDIV;
}
template<> inline
@@ -214,9 +212,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
}
template<> inline
bool RewriteRule<EvalUrem>::applies(TNode node) {
- return (utils::isBvConstTerm(node) &&
- (node.getKind() == kind::BITVECTOR_UREM_TOTAL ||
- (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst())));
+ return utils::isBvConstTerm(node) && node.getKind() == kind::BITVECTOR_UREM;
}
template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 2fff03c10..dda5c0420 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -464,7 +464,7 @@ inline Node RewriteRule<SdivEliminate>::apply(TNode node)
Node abs_b =
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b);
+ Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b);
Node condition = nm->mkNode(kind::XOR, a_lt_0, b_lt_0);
@@ -502,7 +502,7 @@ inline Node RewriteRule<SdivEliminateFewerBitwiseOps>::apply(TNode node)
Node abs_b =
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV_TOTAL, abs_a, abs_b);
+ Node a_udiv_b = nm->mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_udiv_b);
Node result = nm->mkNode(kind::ITE, a_lt_0.xorNode(b_lt_0), neg_result, a_udiv_b);
@@ -536,7 +536,7 @@ inline Node RewriteRule<SremEliminate>::apply(TNode node)
Node abs_b =
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b);
+ Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b);
Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
@@ -571,7 +571,7 @@ inline Node RewriteRule<SremEliminateFewerBitwiseOps>::apply(TNode node)
nm->mkNode(kind::ITE, a_lt_0, nm->mkNode(kind::BITVECTOR_NEG, a), a);
Node abs_b =
nm->mkNode(kind::ITE, b_lt_0, nm->mkNode(kind::BITVECTOR_NEG, b), b);
- Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM_TOTAL, abs_a, abs_b);
+ Node a_urem_b = nm->mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
Node neg_result = nm->mkNode(kind::BITVECTOR_NEG, a_urem_b);
Node result = nm->mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index ca26577bf..d5a230098 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1393,7 +1393,7 @@ template <>
inline bool RewriteRule<UdivPow2>::applies(TNode node)
{
bool isNeg = false;
- if (node.getKind() == kind::BITVECTOR_UDIV_TOTAL
+ if (node.getKind() == kind::BITVECTOR_UDIV
&& utils::isPow2Const(node[1], isNeg))
{
return !isNeg;
@@ -1439,8 +1439,8 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node)
template <>
inline bool RewriteRule<UdivZero>::applies(TNode node) {
- return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
- node[1] == utils::mkConst(utils::getSize(node), 0));
+ return (node.getKind() == kind::BITVECTOR_UDIV
+ && node[1] == utils::mkConst(utils::getSize(node), 0));
}
template <>
@@ -1459,8 +1459,8 @@ inline Node RewriteRule<UdivZero>::apply(TNode node) {
template <>
inline bool RewriteRule<UdivOne>::applies(TNode node) {
- return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
- node[1] == utils::mkConst(utils::getSize(node), 1));
+ return (node.getKind() == kind::BITVECTOR_UDIV
+ && node[1] == utils::mkConst(utils::getSize(node), 1));
}
template <>
@@ -1481,7 +1481,7 @@ template <>
inline bool RewriteRule<UremPow2>::applies(TNode node)
{
bool isNeg;
- if (node.getKind() == kind::BITVECTOR_UREM_TOTAL
+ if (node.getKind() == kind::BITVECTOR_UREM
&& utils::isPow2Const(node[1], isNeg))
{
return !isNeg;
@@ -1521,8 +1521,8 @@ inline Node RewriteRule<UremPow2>::apply(TNode node)
template<> inline
bool RewriteRule<UremOne>::applies(TNode node) {
- return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
- node[1] == utils::mkConst(utils::getSize(node), 1));
+ return (node.getKind() == kind::BITVECTOR_UREM
+ && node[1] == utils::mkConst(utils::getSize(node), 1));
}
template<> inline
@@ -1541,8 +1541,7 @@ Node RewriteRule<UremOne>::apply(TNode node) {
template<> inline
bool RewriteRule<UremSelf>::applies(TNode node) {
- return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
- node[0] == node[1]);
+ return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]);
}
template<> inline
@@ -1590,7 +1589,7 @@ template <>
inline bool RewriteRule<UgtUrem>::applies(TNode node)
{
return (node.getKind() == kind::BITVECTOR_UGT
- && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL
+ && node[0].getKind() == kind::BITVECTOR_UREM
&& node[0][1] == node[1]);
}
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index b883ab537..4651b9256 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -440,18 +440,6 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){
Node resultNode = node;
- return RewriteUdivTotal(node, prerewrite);
-}
-
-RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite){
- Node resultNode = node;
-
- return RewriteUremTotal(node, prerewrite);
-}
-
-RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){
- Node resultNode = node;
-
if(RewriteRule<UdivPow2>::applies(node)) {
resultNode = RewriteRule<UdivPow2>::run <false> (node);
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
@@ -464,7 +452,8 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){
return RewriteResponse(REWRITE_DONE, resultNode);
}
-RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) {
+RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool prerewrite)
+{
Node resultNode = node;
if(RewriteRule<UremPow2>::applies(node)) {
@@ -477,7 +466,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite)
RewriteRule<UremOne>,
RewriteRule<UremSelf>
>::apply(node);
- return RewriteResponse(REWRITE_DONE, resultNode);
+ return RewriteResponse(REWRITE_DONE, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) {
@@ -705,8 +694,6 @@ void TheoryBVRewriter::initializeRewrites() {
d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
- d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal;
- d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal;
d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod;
d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv;
d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback