summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/arith_static_learner.cpp3
-rw-r--r--src/theory/arith/theory_arith_private.cpp31
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp5
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h5
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp4
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp42
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp74
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp9
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.cpp17
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp7
-rw-r--r--src/theory/quantifiers/term_util.cpp5
-rw-r--r--src/theory/sets/theory_sets_private.cpp18
-rw-r--r--src/theory/substitutions.cpp10
-rw-r--r--src/theory/theory.cpp10
14 files changed, 154 insertions, 86 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index f26f45449..4bfc1a4f9 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -111,7 +111,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
if (expr::hasBoundVar(n))
{
// Unsafe with non-ground ITEs; do nothing
- Debug("arith::static") << "(potentially) non-ground ITE, ignoring..." << endl;
+ Debug("arith::static")
+ << "(potentially) non-ground ITE, ignoring..." << endl;
break;
}
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 777e99912..968970049 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1355,26 +1355,37 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
// Add the substitution if not recursive
Assert(elim == Rewriter::rewrite(elim));
-
- if(right.size() > options::ppAssertMaxSubSize()){
- Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl;
+ if (right.size() > options::ppAssertMaxSubSize())
+ {
+ Debug("simplify")
+ << "TheoryArithPrivate::solve(): did not substitute due to the "
+ "right hand side containing too many terms: "
+ << minVar << ":" << elim << endl;
Debug("simplify") << right.size() << endl;
}
else if (expr::hasSubterm(elim, minVar))
{
- Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
-
- }else if (!minVar.getType().isInteger() || right.isIntegral()) {
+ Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
+ "due to recursive pattern with sharing: "
+ << minVar << ":" << elim << endl;
+ }
+ else if (!minVar.getType().isInteger() || right.isIntegral())
+ {
Assert(!expr::hasSubterm(elim, minVar));
// cannot eliminate integers here unless we know the resulting
// substitution is integral
- Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl;
+ Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
+ << minVar << " |-> " << elim << endl;
outSubstitutions.addSubstitution(minVar, elim);
return Theory::PP_ASSERT_STATUS_SOLVED;
- } else {
- Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
-
+ }
+ else
+ {
+ Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
+ "b/c it's integer: "
+ << minVar << ":" << minVar.getType() << " |-> "
+ << elim << ":" << elim.getType() << endl;
}
}
}
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 8c95abe01..0150264fd 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -493,7 +493,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
if (left.isVar() && !expr::hasSubterm(right, left))
{
- bool changed = subst.addSubstitution(left, right, reason);
+ bool changed = subst.addSubstitution(left, right, reason);
return changed;
}
if (right.isVar() && !expr::hasSubterm(left, right))
@@ -590,7 +590,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
return false;
}
-bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) {
+bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in)
+{
if (node.getMetaKind() == kind::metakind::VARIABLE
&& !expr::hasSubterm(in, node))
return true;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 65cb53e7e..1293f8311 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -602,8 +602,9 @@ inline Node RewriteRule<ConcatToMult>::apply(TNode node)
return NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, factor, coef);
}
-template<> inline
-bool RewriteRule<SolveEq>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SolveEq>::applies(TNode node)
+{
if (node.getKind() != kind::EQUAL
|| (node[0].isVar() && !expr::hasSubterm(node[1], node[0]))
|| (node[1].isVar() && !expr::hasSubterm(node[0], node[1])))
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 44f37a30e..3615ef6f4 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -309,7 +309,9 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
&& !expr::hasSubterm(n1, n2))
{
return true;
- }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
+ }
+ else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
+ {
return true;
}
}
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 8dd609e42..f0789a503 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -437,18 +437,23 @@ void BoundedIntegers::checkOwnership(Node f)
<< bound_lit_map[2][v] << std::endl;
}
}else if( it->second==BOUND_FIXED_SET ){
- setBoundedVar( f, v, BOUND_FIXED_SET );
+ setBoundedVar(f, v, BOUND_FIXED_SET);
setBoundVar = true;
- for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){
+ for (unsigned i = 0; i < bound_fixed_set[v].size(); i++)
+ {
Node t = bound_fixed_set[v][i];
if (expr::hasBoundVar(t))
{
- d_fixed_set_ngr_range[f][v].push_back( t );
- }else{
- d_fixed_set_gr_range[f][v].push_back( t );
+ d_fixed_set_ngr_range[f][v].push_back(t);
+ }
+ else
+ {
+ d_fixed_set_gr_range[f][v].push_back(t);
}
- }
- Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl;
+ }
+ Trace("bound-int") << "Variable " << v
+ << " is bound because of disequality conjunction "
+ << bound_lit_map[3][v] << std::endl;
}
if( setBoundVar ){
success = true;
@@ -547,8 +552,9 @@ void BoundedIntegers::checkOwnership(Node f)
bool isProxy = false;
if (expr::hasBoundVar(r))
{
- //introduce a new bound
- Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" );
+ // introduce a new bound
+ Node new_range = NodeManager::currentNM()->mkSkolem(
+ "bir", r.getType(), "bound for term");
d_nground_range[f][v] = r;
d_range[f][v] = new_range;
r = new_range;
@@ -648,14 +654,21 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
return;
}
-bool BoundedIntegers::isGroundRange( Node q, Node v ) {
- if( isBoundVar(q,v) ){
- if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+bool BoundedIntegers::isGroundRange(Node q, Node v)
+{
+ if (isBoundVar(q, v))
+ {
+ if (d_bound_type[q][v] == BOUND_INT_RANGE)
+ {
return !expr::hasBoundVar(getLowerBound(q, v))
&& !expr::hasBoundVar(getUpperBound(q, v));
- }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){
+ }
+ else if (d_bound_type[q][v] == BOUND_SET_MEMBER)
+ {
return !expr::hasBoundVar(d_setm_range[q][v]);
- }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){
+ }
+ else if (d_bound_type[q][v] == BOUND_FIXED_SET)
+ {
return !d_fixed_set_ngr_range[q][v].empty();
}
}
@@ -919,4 +932,3 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
return true;
}
}
-
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 8df24d626..3006a07bf 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -182,22 +182,32 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
if( !MatchGen::isHandledBoolConnective( n ) ){
if (expr::hasBoundVar(n))
{
- //literals
- if( n.getKind()==EQUAL ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- flatten( n[i], beneathQuant );
+ // literals
+ if (n.getKind() == EQUAL)
+ {
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ flatten(n[i], beneathQuant);
}
- }else if( MatchGen::isHandledUfTerm( n ) ){
- flatten( n, beneathQuant );
- }else if( n.getKind()==ITE ){
- for( unsigned i=1; i<=2; i++ ){
- flatten( n[i], beneathQuant );
+ }
+ else if (MatchGen::isHandledUfTerm(n))
+ {
+ flatten(n, beneathQuant);
+ }
+ else if (n.getKind() == ITE)
+ {
+ for (unsigned i = 1; i <= 2; i++)
+ {
+ flatten(n[i], beneathQuant);
}
- registerNode( n[0], false, pol, beneathQuant );
- }else if( options::qcfTConstraint() ){
- //a theory-specific predicate
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- flatten( n[i], beneathQuant );
+ registerNode(n[0], false, pol, beneathQuant);
+ }
+ else if (options::qcfTConstraint())
+ {
+ // a theory-specific predicate
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ flatten(n[i], beneathQuant);
}
}
}
@@ -1016,22 +1026,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
Assert( d_n.getType().isBoolean() );
d_type = typ_bool_var;
}else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
- for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+ for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+ {
if (expr::hasBoundVar(d_n[i]))
{
- if( !qi->isVar( d_n[i] ) ){
- Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;
+ if (!qi->isVar(d_n[i]))
+ {
+ Trace("qcf-qregister-debug")
+ << "ERROR : not var " << d_n[i] << std::endl;
}
- Assert( qi->isVar( d_n[i] ) );
- if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
- d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
+ Assert(qi->isVar(d_n[i]));
+ if (d_n.getKind() != EQUAL && qi->isVar(d_n[i]))
+ {
+ d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
}
- }else{
+ }
+ else
+ {
d_qni_gterm[i] = d_n[i];
- qi->setGroundSubterm( d_n[i] );
+ qi->setGroundSubterm(d_n[i]);
}
}
- d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
+ d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint;
Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
}
}
@@ -1185,13 +1201,17 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
}
}
}else if( d_type==typ_eq ){
- for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
+ for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+ {
if (!expr::hasBoundVar(d_n[i]))
{
- TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] );
- if( t.isNull() ){
+ TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]);
+ if (t.isNull())
+ {
d_ground_eval[i] = d_n[i];
- }else{
+ }
+ else
+ {
d_ground_eval[i] = t;
}
}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 9ed6e766d..37451b776 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -775,8 +775,10 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
}
}
}else if( n.getKind()==EQUAL ){
- for( unsigned i=0; i<2; i++ ){
- if( n[i].getKind()==BOUND_VARIABLE ){
+ for (unsigned i = 0; i < 2; i++)
+ {
+ if (n[i].getKind() == BOUND_VARIABLE)
+ {
if (!expr::hasSubterm(n[1 - i], n[i]))
{
return true;
@@ -875,7 +877,8 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
return body;
}
-bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
+bool QuantifiersRewriter::isVariableElim(Node v, Node s)
+{
return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
}
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index d374f25d0..5f5a84a6b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -727,12 +727,14 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
// check if it is a variable equality
TNode v;
Node s;
- for( unsigned r=0; r<2; r++ ){
- if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){
+ for (unsigned r = 0; r < 2; r++)
+ {
+ if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
+ {
if (!expr::hasSubterm(slit[1 - r], slit[r]))
{
v = slit[r];
- s = slit[1-r];
+ s = slit[1 - r];
break;
}
}
@@ -742,8 +744,12 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
std::map< Node, Node > msum;
if (ArithMSum::getMonomialSumLit(slit, msum))
{
- for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
- if( std::find( vars.begin(), vars.end(), itm->first )!=vars.end() ){
+ for (std::map<Node, Node>::iterator itm = msum.begin();
+ itm != msum.end();
+ ++itm)
+ {
+ if (std::find(vars.begin(), vars.end(), itm->first) != vars.end())
+ {
Node veq_c;
Node val;
int ires =
@@ -1079,4 +1085,3 @@ Node TransitionInference::constructFormulaTrace( DetTrace& dt ) {
}
} //namespace CVC4
-
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 43465270d..2ee120211 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -297,9 +297,10 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >&
Node eqro = eq[r==0 ? 1 : 0 ];
if (!expr::hasSubterm(eqro, eq[r]))
{
- Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
- new_vars.push_back( eq[r] );
- new_subs.push_back( eqro );
+ Trace("csi-simp-debug")
+ << "---equality " << eq[r] << " = " << eqro << std::endl;
+ new_vars.push_back(eq[r]);
+ new_subs.push_back(eqro);
return true;
}
}
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index afa4935d6..7d91e9812 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -596,7 +596,7 @@ Node TermUtil::rewriteVtsSymbols( Node n ) {
subs_lhs.push_back( rew_vts_inf );
n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
n = Rewriter::rewrite( n );
- //may have cancelled
+ // may have cancelled
if (!expr::hasSubterm(n, rew_vts_inf))
{
rew_vts_inf = Node::null();
@@ -604,7 +604,8 @@ Node TermUtil::rewriteVtsSymbols( Node n ) {
}
}
}
- if( rew_vts_inf.isNull() ){
+ if (rew_vts_inf.isNull())
+ {
if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta))
{
rew_delta = true;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 3c75bd98f..9346970d1 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -2201,11 +2201,13 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
//this is based off of Theory::ppAssert
Node var;
- if (in.getKind() == kind::EQUAL) {
+ if (in.getKind() == kind::EQUAL)
+ {
if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
&& (in[1].getType()).isSubtypeOf(in[0].getType()))
{
- if( !in[0].getType().isSet() || !options::setsExt() ){
+ if (!in[0].getType().isSet() || !options::setsExt())
+ {
outSubstitutions.addSubstitution(in[0], in[1]);
var = in[0];
status = Theory::PP_ASSERT_STATUS_SOLVED;
@@ -2214,18 +2216,22 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou
else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
&& (in[0].getType()).isSubtypeOf(in[1].getType()))
{
- if( !in[1].getType().isSet() || !options::setsExt() ){
+ if (!in[1].getType().isSet() || !options::setsExt())
+ {
outSubstitutions.addSubstitution(in[1], in[0]);
var = in[1];
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
- }else if (in[0].isConst() && in[1].isConst()) {
- if (in[0] != in[1]) {
+ }
+ else if (in[0].isConst() && in[1].isConst())
+ {
+ if (in[0] != in[1])
+ {
status = Theory::PP_ASSERT_STATUS_CONFLICT;
}
}
}
-
+
if( status==Theory::PP_ASSERT_STATUS_SOLVED ){
Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl;
/*
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 01a3c3572..036bb4ada 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -210,13 +210,15 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC
}
}
-
-static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
-static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
+static bool check(TNode node,
+ const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
+static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions)
+{
SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
Debug("substitution") << "checking " << node << endl;
- for (; it != it_end; ++ it) {
+ for (; it != it_end; ++it)
+ {
Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl;
if (expr::hasSubterm(node, (*it).first))
{
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index e2a61de26..eedf0ff52 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -284,11 +284,11 @@ void Theory::computeRelevantTerms(set<Node>& termSet,
}
}
-
Theory::PPAssertStatus Theory::ppAssert(TNode in,
SubstitutionMap& outSubstitutions)
{
- if (in.getKind() == kind::EQUAL) {
+ if (in.getKind() == kind::EQUAL)
+ {
// (and (= x t) phi) can be replaced by phi[x/t] if
// 1) x is a variable
// 2) x is not in the term t
@@ -305,8 +305,10 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
outSubstitutions.addSubstitution(in[1], in[0]);
return PP_ASSERT_STATUS_SOLVED;
}
- if (in[0].isConst() && in[1].isConst()) {
- if (in[0] != in[1]) {
+ if (in[0].isConst() && in[1].isConst())
+ {
+ if (in[0] != in[1])
+ {
return PP_ASSERT_STATUS_CONFLICT;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback