# #include "resolve.h"

This page has information from files resolve.h and resolve.c.

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File resolve.c

#### Index

| copy_inference | merge_literals | resolve3
binary_factors | hyper_resolution | res_instance_prunes | ur_resolution
binary_resolution | instantiate_clause | resolve2 | xx_resolve2

#### Details

    void resolution_options(BOOL ordered,
    			BOOL check_instances,
    			BOOL initial_nuclei,
    			int ur_nucleus_limit);

    void binary_factors(Topform c, void (*proc_proc) (Topform));

    void binary_resolution(Topform c,
    		       int res_type,  /* POS_RES, NEG_RES, ANY_RES */
    		       Lindex idx,
    		       void (*proc_proc) (Topform));

Binary resolution.

    Topform copy_inference(Topform c);

This makes a "copy" inference; that is, a copy of the clause in which the justification is "copy". All attributes are copied (not just the inheritible attributes). An ID is not assigned.

    void hyper_resolution(Topform c, int pos_or_neg, Lindex idx,
    		      void (*proc_proc) (Topform));

Hyperresolution.

    Topform instantiate_clause(Topform c, Context subst);

    void merge_literals(Topform c);

    int res_instance_prunes();

    Topform resolve2(Topform c1, int n1, Topform c2, int n2, BOOL renumber_vars);

Resolve, if possible, two clauses on the literals (specified by literals, counting from 1). Include justification, transfer inheritable attributes, but do not assign an ID. Renumbering of variables is optional.

if n2 < 0, then the literal is abs(n2), and it should be flipped.

    Topform resolve3(Topform c1, Literals l1, Topform c2, Literals l2, BOOL renumber_vars);

Similar to resolve2(), but literals are given instead of integers.

    void ur_resolution(Topform c, int target_constraint, Lindex idx,
    		   void (*proc_proc) (Topform));

Unit-resulting resolution.

    Topform xx_resolve2(Topform c, int n, BOOL renumber_vars);

Resolve, if possible, a clause with x=x. Renumber vars, include justification, transfer inheritable attributes, but do not assign an ID.

## Public Definitions in File resolve.h

    enum {  /* literal selection */
      LIT_SELECTION_NONE,
      LIT_SELECTION_MAXIMAL,
      LIT_SELECTION_ALL
    };

    enum {  /* types of resolution (binary, hyper, UR) */
      POS_RES,  /* positive */
      NEG_RES,  /* negative */
      ANY_RES   /* unrestricted by sign */
    };

## Introduction