sat.cc File Reference

#include "kernel/register.h"
#include "kernel/celltypes.h"
#include "kernel/consteval.h"
#include "kernel/sigtools.h"
#include "kernel/log.h"
#include "kernel/satgen.h"
#include <stdlib.h>
#include <stdio.h>
#include <algorithm>
#include <errno.h>
#include <string.h>

Include dependency graph for sat.cc:

Go to the source code of this file.

Data Structures
struct	SatHelper
struct	SatHelper::ModelBlockInfo
struct	SatPass

Functions
void	print_proof_failed ()
void	print_timeout ()
void	print_qed ()

Variables
SatPass	SatPass

Function Documentation

void print_proof_failed

(

)

Definition at line 770 of file sat.cc.

{
    log("\n");
    log("   ______                   ___       ___       _ _            _ _ \n");
    log("  (_____ \\                 / __)     / __)     (_) |          | | |\n");
    log("   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\n");
    log("  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\n");
    log("  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \n");
    log("  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\n");
    log("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void print_qed

(

)

Definition at line 793 of file sat.cc.

{
    log("\n");
    log("                  /$$$$$$      /$$$$$$$$     /$$$$$$$    \n");
    log("                 /$$__  $$    | $$_____/    | $$__  $$   \n");
    log("                | $$  \\ $$    | $$          | $$  \\ $$   \n");
    log("                | $$  | $$    | $$$$$       | $$  | $$   \n");
    log("                | $$  | $$    | $$__/       | $$  | $$   \n");
    log("                | $$/$$ $$    | $$          | $$  | $$   \n");
    log("                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
    log("                 \\____ $$$|__/|________/|__/|_______/|__/\n");
    log("                       \\__/                              \n");
    log("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void print_timeout

(

)

Definition at line 782 of file sat.cc.

{
    log("\n");
    log("        _____  _  _      _____ ____  _     _____\n");
    log("       /__ __\\/ \\/ \\__/|/  __//  _ \\/ \\ /\\/__ __\\\n");
    log("         / \\  | || |\\/|||  \\  | / \\|| | ||  / \\\n");
    log("         | |  | || |  |||  /_ | \\_/|| \\_/|  | |\n");
    log("         \\_/  \\_/\\_/  \\|\\____\\\\____/\\____/  \\_/\n");
    log("\n");
}

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

SatPass SatPass