From 15ae942118281b8b969e62db5ab341644bdd742b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Jan 2020 17:58:19 -0800 Subject: [PATCH] add headers, remove pragma in cpp before Agatha Christie character prepended by N notices Signed-off-by: Nikolaj Bjorner --- src/sat/sat_cutset.cpp | 1 - src/sat/sat_cutset.h | 12 ++++++++++++ src/sat/sat_cutset_compute_shift.h | 21 +++++++++++++++++++++ 3 files changed, 33 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp index e2f94f1c5..ab5005862 100644 --- a/src/sat/sat_cutset.cpp +++ b/src/sat/sat_cutset.cpp @@ -11,7 +11,6 @@ --*/ -#pragma once; #include "util/hashtable.h" #include "sat/sat_cutset.h" diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index 9773eaf17..fd8b24548 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -1,3 +1,15 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Module Name: + + sat_cutset.cpp + + Author: + + Nikolaj Bjorner 2020-01-02 + + --*/ #pragma once; #include "util/region.h" diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h index 09ca551bf..5222e704f 100644 --- a/src/sat/sat_cutset_compute_shift.h +++ b/src/sat/sat_cutset_compute_shift.h @@ -1,3 +1,24 @@ +/*++ + Copyright (c) 2020 Microsoft Corporation + + Module Name: + + sat_cutset_compute_shift.h + + Author: + + Nikolaj Bjorner 2020-01-02 + + Notes: + + shifts truth table x using 'code'. + code encodes a mapping from bit-positions of the + input truth table encoded with x into bit-positions + in the output truth table. + The truth table covers up to 6 inputs, which fits in 64 bits. + + --*/ + static uint64_t compute_shift(uint64_t x, unsigned code) { switch (code) { #define _x0 (x & 1)