daniel-j-h

On Logic Solvers

From SAT to SMT and back.

There is a Gist, see references [@gist].

Satisfiability (SAT)

Is a given formula (i.e. $\lnot A \land (B \lor C)$) satisfiable?

daniel-j-h

#!/usr/bin/env python2
# -*- coding: utf-8 -*-

# http://docs.sqlalchemy.org/en/latest/orm/self_referential.html

import json

from sqlalchemy import create_engine, Column, Integer, String, ForeignKey, CheckConstraint
from sqlalchemy.orm import sessionmaker, relationship, backref
from sqlalchemy.ext.declarative import declarative_base

daniel-j-h

#include <iostream>
#include <z3++.h>
 
int main() {
 
  z3::config config;
  z3::context context{config};
  z3::optimize optimizer{context};
 
  auto x = context.int_const("x");

daniel-j-h

    bool operator()(const InternalExtractorEdge &lhs, const InternalExtractorEdge &rhs) const
    {
        return (lhs.result.source <  rhs.result.source) ||
              ((lhs.result.source == rhs.result.source) &&
               (lhs.result.target <  rhs.result.target));
    }

daniel-j-h

set disassembly-flavor intel

daniel-j-h

#!/usr/bin/env bash

git ls-files '*.cpp' | \
  xargs -I{} -P $(nproc) clang-modernize -p build -final-syntax-check -format -style=file -summary -for-compilers=clang-3.4,gcc-4.8 -include . -exclude third_party {}

daniel-j-h

unexposed_decl: '^.*$'
struct_decl: '^.*$'
union_decl: '^.*$'
class_decl: '^.*$'
enum_decl: '^.*$'
field_decl: '^.*$'
enum_constant_decl: '^.*$'
function_decl: '^.*$'
var_decl: '^.*$'
parm_decl: '^.*$'

daniel-j-h

#include <iostream>
#include <ostream>
#include <algorithm>
#include <iterator>
#include <functional>
#include <type_traits>

struct Person {
  int age;

daniel-j-h

CMake Warning (dev) in /tmp/osrm-backend/CMakeLists.txt:
  unused variable (changing definition) 'CMAKE_CURRENT_SOURCE_DIR'
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning (dev) in /tmp/osrm-backend/CMakeLists.txt:
  unused variable (changing definition) 'CMAKE_CURRENT_BINARY_DIR'
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning (dev) at /tmp/osrm-backend/CMakeLists.txt:9 (project):
  unused variable (out of scope) 'CMAKE_BINARY_DIR'

daniel-j-h

#include <iostream>
#include <ostream>
#include <algorithm>
#include <iterator>
#include <functional>
#include <type_traits>

struct Person {
  int id;
  int age;