/* assumptions.h */

/*
 * SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
 * For more information, please refer to <https://unlicense.org/>
 * SPDX-License-Identifier: Unlicense
 */

#ifndef ASSUMPTIONS_H
#define ASSUMPTIONS_H 1

#include "formula.h"

struct assumptions {
    int label;
    struct formula *formula;
    struct assumptions *next;
};

struct assumptions *assume(int, struct formula *, struct assumptions *);
struct formula *lookup(int, struct assumptions *);
struct assumptions *discharge(int, struct assumptions *);
struct assumptions *merge(struct assumptions *, struct assumptions *);

void assumptions_fprint(FILE *, struct assumptions *);

#endif /* ndef ASSUMPTIONS_H */