summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/learn_resource_weights.py188
-rw-r--r--src/options/smt_options.toml45
-rw-r--r--src/prop/bvminisat/core/Solver.cc3
-rw-r--r--src/prop/cnf_stream.cpp7
-rw-r--r--src/prop/cnf_stream.h6
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp2
-rw-r--r--src/theory/arith/theory_arith_private.cpp7
-rw-r--r--src/theory/rewriter.cpp6
-rw-r--r--src/theory/rewriter.h2
-rw-r--r--src/util/resource_manager.cpp45
-rw-r--r--src/util/resource_manager.h12
11 files changed, 296 insertions, 27 deletions
diff --git a/contrib/learn_resource_weights.py b/contrib/learn_resource_weights.py
new file mode 100755
index 000000000..8f5213ec2
--- /dev/null
+++ b/contrib/learn_resource_weights.py
@@ -0,0 +1,188 @@
+#!/usr/bin/env python3
+
+import argparse
+import glob
+import gzip
+import json
+import logging
+import re
+from sklearn import linear_model
+import statistics
+
+
+def parse_commandline():
+ """Parse commandline arguments"""
+ epilog = """
+This script can be used to compute good resource weights based on benchmark
+results. The resource weights are used by cvc4 to approximate the running time
+by the spent resources, multiplied with their weights.
+
+In the first stage ("parse") this script reads the output files of a benchmark
+run as generated on our cluster. The output files are expected to be named
+"*.smt2/output.log" and should contain the statistics (by use of "--stats").
+The result is a gziped json file that contains all the relevant information
+in a compact form.
+
+In the second stage ("analyze") this script loads the gziped json file and uses
+a linear regression model to learn resource weights. The resulting weights can
+be used as constants for the resource options ("--*-step=n"). Additionally,
+this script performs some analysis on the results to identify outliers where
+the linear model performs particularly bad, i.e., the runtime estimation is way
+off.
+ """
+ usage = """
+ first stage to parse the solver output:
+ %(prog)s parse <output directory>
+
+ second stage to learn resource weights:
+ %(prog)s analyze
+ """
+ parser = argparse.ArgumentParser(description='export and analyze resources from statistics',
+ formatter_class=argparse.ArgumentDefaultsHelpFormatter,
+ epilog=epilog,
+ usage=usage)
+ parser.add_argument('command', choices=[
+ 'parse', 'analyze'], help='task to perform')
+ parser.add_argument('basedir', default=None, nargs='?',
+ help='path of benchmark results')
+ parser.add_argument('-v', '--verbose',
+ action='store_true', help='be more verbose')
+ parser.add_argument('--json', default='data.json.gz',
+ help='path of json file')
+ parser.add_argument('--threshold', metavar='SEC', type=int, default=1,
+ help='ignore benchmarks with a runtime below this threshold')
+ parser.add_argument('--mult', type=int, default=1000,
+ help='multiply running times with this factor for regression')
+
+ return parser.parse_args()
+
+
+def load_zipped_json(filename):
+ """Load data from a gziped json file"""
+ with gzip.GzipFile(args.json, 'r') as fin:
+ return json.loads(fin.read().decode('utf-8'))
+
+
+def save_zipped_json(filename, data):
+ """Store data to a gziped json file"""
+ with gzip.GzipFile(args.json, 'w') as fout:
+ fout.write(json.dumps(data).encode('utf-8'))
+
+
+def get_sorted_values(data):
+ """Transform [['name', value], ...] to [value, ...] sorted by names"""
+ return [d[1] for d in sorted(data)]
+
+
+def parse(args):
+ if args.basedir is None:
+ raise Exception('Specify basedir for parsing!')
+ filename_re = re.compile('(.*\\.smt2)/output\\.log')
+ resource_re = re.compile('resource::([^,]+), ([0-9]+)')
+ result_re = re.compile('driver::sat/unsat, ([a-z]+)')
+ totaltime_re = re.compile('driver::totalTime, ([0-9\\.]+)')
+
+ logging.info('Parsing files from {}'.format(args.basedir))
+ data = {}
+ failed = 0
+ for file in glob.iglob('{}/**/output.log'.format(args.basedir), recursive=True):
+ content = open(file).read()
+ try:
+ filename = filename_re.match(file).group(1)
+ r = resource_re.findall(content)
+ r = list(map(lambda x: (x[0], int(x[1])), r))
+ data[filename] = {
+ 'resources': r,
+ 'result': result_re.search(content).group(1),
+ 'time': float(totaltime_re.search(content).group(1)),
+ }
+ except Exception as e:
+ logging.debug('Failed to parse {}: {}'.format(file, e))
+ failed += 1
+
+ if failed > 0:
+ logging.info('Failed to parse {} out of {} files'.format(
+ failed, failed + len(data)))
+ logging.info('Dumping data to {}'.format(args.json))
+ save_zipped_json(args.json, data)
+
+
+def analyze(args):
+ logging.info('Loading data from {}'.format(args.json))
+ data = load_zipped_json(args.json)
+
+ logging.info('Extracting resources')
+ resources = set()
+ for f in data:
+ for r in data[f]['resources']:
+ resources.add(r[0])
+ resources = list(sorted(resources))
+
+ vals = {r: [] for r in resources}
+
+ logging.info('Collecting data from {} benchmarks'.format(len(data)))
+ x = []
+ y = []
+ for filename in data:
+ d = data[filename]
+ if d['time'] < args.threshold:
+ continue
+ x.append(get_sorted_values(d['resources']))
+ y.append(d['time'] * args.mult)
+
+ for r in d['resources']:
+ vals[r[0]].append(r[1])
+
+ logging.info('Training regression model')
+ clf = linear_model.LinearRegression()
+ r = clf.fit(x, y)
+ coeffs = zip(resources, r.coef_)
+ for c in sorted(coeffs, key=lambda c: c[1]):
+ minval = min(vals[c[0]])
+ maxval = max(vals[c[0]])
+ avgval = statistics.mean(vals[c[0]])
+ medval = statistics.median(vals[c[0]])
+ impact = c[1] * avgval
+ logging.info('{:23}-> {:15.10f}\t({} .. {:10}, avg {:9.2f}, med {:8}, impact {:7.3f})'.format(
+ *c, minval, maxval, avgval, medval, impact))
+
+ logging.info('Comparing regression model with reality')
+ outliers = {
+ 'over-estimated': [],
+ 'under-estimated': []
+ }
+ for filename in data:
+ d = data[filename]
+ actual = d['time']
+ if actual < args.threshold:
+ continue
+ vals = get_sorted_values(d['resources'])
+ predict = float(r.predict([vals])) / args.mult
+ outliers['over-estimated'].append([predict / actual, predict, actual, filename])
+ outliers['under-estimated'].append([actual / predict, predict, actual, filename])
+
+ for out in outliers:
+ logging.info('Showing outliers for {}'.format(out))
+ filtered = outliers[out]
+ for vals in sorted(filtered)[-5:]:
+ logging.info(
+ ' -> {:6.2f} ({:6.2f}, actual {:6.2f}): {}'.format(*vals))
+
+ cur = 0
+ gnuplot = open('plot.data', 'w')
+ for out in sorted(outliers['under-estimated']):
+ gnuplot.write('{}\t{}\n'.format(cur, out[0]))
+ cur += 1
+
+
+if __name__ == "__main__":
+ logging.basicConfig(format='[%(levelname)s] %(message)s')
+ args = parse_commandline()
+ if args.verbose:
+ logging.getLogger().setLevel(level=logging.DEBUG)
+ else:
+ logging.getLogger().setLevel(level=logging.INFO)
+ if args.command == 'parse':
+ parse(args)
+ elif args.command == 'analyze':
+ analyze(args)
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 55ba43ce9..405abfc4f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -497,6 +497,24 @@ header = "options/smt_options.h"
help = "enable resource limiting per query"
[[option]]
+ name = "arithPivotStep"
+ category = "expert"
+ long = "arith-pivot-step=N"
+ type = "unsigned"
+ default = "1"
+ read_only = true
+ help = "amount of resources spent for each arithmetic pivot step"
+
+[[option]]
+ name = "arithNlLemmaStep"
+ category = "expert"
+ long = "arith-nl-lemma-step=N"
+ type = "unsigned"
+ default = "1"
+ read_only = true
+ help = "amount of resources spent for each arithmetic nonlinear lemma step"
+
+[[option]]
name = "rewriteStep"
category = "expert"
long = "rewrite-step=N"
@@ -569,6 +587,15 @@ header = "options/smt_options.h"
help = "amount of resources spent when adding lemmas"
[[option]]
+ name = "newSkolemStep"
+ category = "expert"
+ long = "new-skolem-step=N"
+ type = "unsigned"
+ default = "1"
+ read_only = true
+ help = "amount of resources spent when adding new skolems"
+
+[[option]]
name = "restartStep"
category = "expert"
long = "restart-step=N"
@@ -623,6 +650,24 @@ header = "options/smt_options.h"
help = "amount of resources spent for each sat conflict (bitvectors)"
[[option]]
+ name = "bvSatPropagateStep"
+ category = "expert"
+ long = "bv-sat-propagate-step=N"
+ type = "unsigned"
+ default = "1"
+ read_only = true
+ help = "amount of resources spent for each sat propagate (bitvectors)"
+
+[[option]]
+ name = "bvSatSimplifyStep"
+ category = "expert"
+ long = "bv-sat-simplify-step=N"
+ type = "unsigned"
+ default = "1"
+ read_only = true
+ help = "amount of resources spent for each sat simplify (bitvectors)"
+
+[[option]]
name = "forceNoLimitCpuWhileDump"
category = "regular"
long = "force-no-limit-cpu-while-dump"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index f7ba14acd..704ea0e20 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -886,6 +886,8 @@ bool Solver::simplify()
if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
return true;
+ d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
+
// Remove satisfied clauses:
removeSatisfied(learnts);
if (remove_satisfied) // Can be turned off.
@@ -922,6 +924,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
starts++;
for (;;){
+ d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
CRef confl = propagate();
if (confl != CRef_Undef){
// CONFLICT
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 8936fb584..7dcd3f910 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -54,7 +54,6 @@ CnfStream::CnfStream(SatSolver* satSolver,
d_nodeToLiteralMap(context),
d_literalToNodeMap(context),
d_fullLitToNodeMap(fullLitToNodeMap),
- d_convertAndAssertCounter(0),
d_registrar(registrar),
d_name(name),
d_cnfProof(nullptr),
@@ -744,11 +743,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
Trace("cnf") << "convertAndAssert(" << node
<< ", negated = " << (negated ? "true" : "false") << ")\n";
- if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
- d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
- d_convertAndAssertCounter = 0;
- }
- ++d_convertAndAssertCounter;
+ d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
switch(node.getKind()) {
case kind::AND: convertAndAssertAnd(node, negated); break;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index dd7fbc15f..74ead0d22 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -202,12 +202,6 @@ class CnfStream {
*/
const bool d_fullLitToNodeMap;
- /**
- * Counter for resource limiting that is used to spend a resource
- * every ResourceManager::resourceCounter calls to convertAndAssert.
- */
- unsigned long d_convertAndAssertCounter;
-
/** The "registrar" for pre-registration of terms */
Registrar* d_registrar;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 5bd02cf19..22a69cadb 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -161,6 +161,8 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
for (const NlLemma& lem : lemmas)
{
sum += filterLemma(lem, out);
+ d_containing.getOutputChannel().spendResource(
+ ResourceManager::Resource::ArithNlLemmaStep);
}
lemmas.clear();
return sum;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e4fa4a82c..ac9ec7e77 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3479,6 +3479,13 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
}
d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
+ size_t nPivots = options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
+ for (std::size_t i = 0; i < d_fcSimplex.getPivots(); ++i)
+ {
+ d_containing.d_out->spendResource(
+ ResourceManager::Resource::ArithPivotStep);
+ }
+
Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
<< "pre approx cuts" << endl;
if(!d_approxCuts.empty()){
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 7ebacee92..3a4941328 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -219,11 +219,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
}
// Rewrite until the stack is empty
for (;;){
-
- if (hasSmtEngine &&
- d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
+ if (hasSmtEngine)
+ {
rm->spendResource(ResourceManager::Resource::RewriteStep);
- d_iterationCount = 0;
}
// Get the top of the recursion stack
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e36426a81..572662483 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -201,8 +201,6 @@ class Rewriter {
/** Theory rewriters used by this rewriter instance */
TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
- unsigned long d_iterationCount = 0;
-
/** Rewriter table for prewrites. Maps kinds to rewriter function. */
std::function<RewriteResponse(RewriteEnvironment*, TNode)>
d_preRewriters[kind::LAST_KIND];
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index f85e06b12..9afa79ef0 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -66,13 +66,18 @@ struct ResourceManager::Statistics
{
ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
IntStat d_spendResourceCalls;
+ IntStat d_numArithPivotStep;
+ IntStat d_numArithNlLemmaStep;
IntStat d_numBitblastStep;
IntStat d_numBvEagerAssertStep;
IntStat d_numBvPropagationStep;
IntStat d_numBvSatConflictsStep;
+ IntStat d_numBvSatPropagateStep;
+ IntStat d_numBvSatSimplifyStep;
IntStat d_numCnfStep;
IntStat d_numDecisionStep;
IntStat d_numLemmaStep;
+ IntStat d_numNewSkolemStep;
IntStat d_numParseStep;
IntStat d_numPreprocessStep;
IntStat d_numQuantifierStep;
@@ -90,13 +95,18 @@ struct ResourceManager::Statistics
ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
: d_resourceUnitsUsed("resource::resourceUnitsUsed"),
d_spendResourceCalls("resource::spendResourceCalls", 0),
+ d_numArithPivotStep("resource::ArithPivotStep", 0),
+ d_numArithNlLemmaStep("resource::ArithNlLemmaStep", 0),
d_numBitblastStep("resource::BitblastStep", 0),
d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
d_numBvPropagationStep("resource::BvPropagationStep", 0),
d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
+ d_numBvSatPropagateStep("resource::BvSatPropagateStep", 0),
+ d_numBvSatSimplifyStep("resource::BvSatSimplifyStep", 0),
d_numCnfStep("resource::CnfStep", 0),
d_numDecisionStep("resource::DecisionStep", 0),
d_numLemmaStep("resource::LemmaStep", 0),
+ d_numNewSkolemStep("resource::NewSkolemStep", 0),
d_numParseStep("resource::ParseStep", 0),
d_numPreprocessStep("resource::PreprocessStep", 0),
d_numQuantifierStep("resource::QuantifierStep", 0),
@@ -108,13 +118,18 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
{
d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
d_statisticsRegistry.registerStat(&d_spendResourceCalls);
+ d_statisticsRegistry.registerStat(&d_numArithPivotStep);
+ d_statisticsRegistry.registerStat(&d_numArithNlLemmaStep);
d_statisticsRegistry.registerStat(&d_numBitblastStep);
d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
+ d_statisticsRegistry.registerStat(&d_numBvSatPropagateStep);
+ d_statisticsRegistry.registerStat(&d_numBvSatSimplifyStep);
d_statisticsRegistry.registerStat(&d_numCnfStep);
d_statisticsRegistry.registerStat(&d_numDecisionStep);
d_statisticsRegistry.registerStat(&d_numLemmaStep);
+ d_statisticsRegistry.registerStat(&d_numNewSkolemStep);
d_statisticsRegistry.registerStat(&d_numParseStep);
d_statisticsRegistry.registerStat(&d_numPreprocessStep);
d_statisticsRegistry.registerStat(&d_numQuantifierStep);
@@ -128,13 +143,18 @@ ResourceManager::Statistics::~Statistics()
{
d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
+ d_statisticsRegistry.unregisterStat(&d_numArithPivotStep);
+ d_statisticsRegistry.unregisterStat(&d_numArithNlLemmaStep);
d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
+ d_statisticsRegistry.unregisterStat(&d_numBvSatPropagateStep);
+ d_statisticsRegistry.unregisterStat(&d_numBvSatSimplifyStep);
d_statisticsRegistry.unregisterStat(&d_numCnfStep);
d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
+ d_statisticsRegistry.unregisterStat(&d_numNewSkolemStep);
d_statisticsRegistry.unregisterStat(&d_numParseStep);
d_statisticsRegistry.unregisterStat(&d_numPreprocessStep);
d_statisticsRegistry.unregisterStat(&d_numQuantifierStep);
@@ -146,8 +166,6 @@ ResourceManager::Statistics::~Statistics()
/*---------------------------------------------------------------------------*/
-const uint64_t ResourceManager::s_resourceCount = 1000;
-
ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
: d_perCallTimer(),
d_timeBudgetPerCall(0),
@@ -219,7 +237,8 @@ void ResourceManager::spendResource(unsigned amount)
if (out())
{
Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
- Trace("limit") << " on call " << d_statistics->d_spendResourceCalls.getData() << std::endl;
+ Trace("limit") << " on call "
+ << d_statistics->d_spendResourceCalls.getData() << std::endl;
if (outOfTime())
{
Trace("limit") << "ResourceManager::spendResource: elapsed time"
@@ -238,6 +257,14 @@ void ResourceManager::spendResource(Resource r)
uint32_t amount = 0;
switch (r)
{
+ case Resource::ArithPivotStep:
+ amount = d_options[options::arithPivotStep];
+ ++d_statistics->d_numArithPivotStep;
+ break;
+ case Resource::ArithNlLemmaStep:
+ amount = d_options[options::arithNlLemmaStep];
+ ++d_statistics->d_numArithNlLemmaStep;
+ break;
case Resource::BitblastStep:
amount = d_options[options::bitblastStep];
++d_statistics->d_numBitblastStep;
@@ -254,6 +281,14 @@ void ResourceManager::spendResource(Resource r)
amount = d_options[options::bvSatConflictStep];
++d_statistics->d_numBvSatConflictsStep;
break;
+ case Resource::BvSatPropagateStep:
+ amount = d_options[options::bvSatPropagateStep];
+ ++d_statistics->d_numBvSatPropagateStep;
+ break;
+ case Resource::BvSatSimplifyStep:
+ amount = d_options[options::bvSatSimplifyStep];
+ ++d_statistics->d_numBvSatSimplifyStep;
+ break;
case Resource::CnfStep:
amount = d_options[options::cnfStep];
++d_statistics->d_numCnfStep;
@@ -266,6 +301,10 @@ void ResourceManager::spendResource(Resource r)
amount = d_options[options::lemmaStep];
++d_statistics->d_numLemmaStep;
break;
+ case Resource::NewSkolemStep:
+ amount = d_options[options::newSkolemStep];
+ ++d_statistics->d_numNewSkolemStep;
+ break;
case Resource::ParseStep:
amount = d_options[options::parseStep];
++d_statistics->d_numParseStep;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index e67598afc..f6cff2e7f 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -10,7 +10,7 @@
** directory for licensing information.\endverbatim
**
** \brief Provides mechanisms to limit resources.
- **
+ **
** This file provides the ResourceManager class. It can be used to impose
** (cumulative and per-call) resource limits on the solver, as well as per-call
** time limits.
@@ -81,13 +81,18 @@ class CVC4_PUBLIC ResourceManager
/** Types of resources. */
enum class Resource
{
+ ArithPivotStep,
+ ArithNlLemmaStep,
BitblastStep,
BvEagerAssertStep,
BvPropagationStep,
BvSatConflictsStep,
+ BvSatPropagateStep,
+ BvSatSimplifyStep,
CnfStep,
DecisionStep,
LemmaStep,
+ NewSkolemStep,
ParseStep,
PreprocessStep,
QuantifierStep,
@@ -159,8 +164,6 @@ class CVC4_PUBLIC ResourceManager
*/
void endCall();
- static uint64_t getFrequencyCount() { return s_resourceCount; }
-
/**
* Registers a listener that is notified on a resource out or (per-call)
* timeout.
@@ -195,9 +198,6 @@ class CVC4_PUBLIC ResourceManager
/** A flag indicating whether resource limitation is active. */
bool d_on;
- /** Counter indicating how often to check resource manager in loops */
- static const uint64_t s_resourceCount;
-
/** Receives a notification on reaching a limit. */
std::vector<Listener*> d_listeners;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback