mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add headers, remove pragma in cpp before Agatha Christie character prepended by N notices
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c43852a266
commit
15ae942118
|
@ -11,7 +11,6 @@
|
|||
|
||||
--*/
|
||||
|
||||
#pragma once;
|
||||
|
||||
#include "util/hashtable.h"
|
||||
#include "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"
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue