1 

/********************* */ 
2 

/*! \file inference_manager.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Gereon Kremer 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief The inference manager for the theory of sets. 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H 
18 

#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H 
19 


20 

#include "theory/inference_manager_buffered.h" 
21 

#include "theory/sets/solver_state.h" 
22 


23 

namespace CVC4 { 
24 

namespace theory { 
25 

namespace sets { 
26 


27 

class TheorySetsPrivate; 
28 


29 

/** Inference manager 
30 

* 
31 

* This class manages inferences produced by the theory of sets. It manages 
32 

* whether inferences are processed as external lemmas on the output channel 
33 

* of theory of sets or internally as literals asserted to the equality engine 
34 

* of theory of sets. The latter literals are referred to as "facts". 
35 

*/ 
36 
8994 
class InferenceManager : public InferenceManagerBuffered 
37 

{ 
38 

typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; 
39 


40 

public: 
41 

InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); 
42 

/** 
43 

* Add facts corresponding to ( exp => fact ) via calls to the assertFact 
44 

* method of TheorySetsPrivate. 
45 

* 
46 

* The portions of fact that were unable to be processed as facts are added 
47 

* to the data member d_pendingLemmas. 
48 

* 
49 

* The argument inferType is used for overriding the policy on whether 
50 

* fact is processed as a lemma, where inferType=1 forces fact to be 
51 

* set as a lemma, and inferType=1 forces fact to be processed as a fact 
52 

* (if possible). 
53 

*/ 
54 

void assertInference(Node fact, 
55 

InferenceId id, 
56 

Node exp, 
57 

int inferType = 0); 
58 

/** same as above, where exp is interpreted as a conjunction */ 
59 

void assertInference(Node fact, 
60 

InferenceId id, 
61 

std::vector<Node>& exp, 
62 

int inferType = 0); 
63 

/** same as above, where conc is interpreted as a conjunction */ 
64 

void assertInference(std::vector<Node>& conc, 
65 

InferenceId id, 
66 

Node exp, 
67 

int inferType = 0); 
68 

/** same as above, where both exp and conc are interpreted as conjunctions */ 
69 

void assertInference(std::vector<Node>& conc, 
70 

InferenceId id, 
71 

std::vector<Node>& exp, 
72 

int inferType = 0); 
73 


74 

/** flush the splitting lemma ( n OR (NOT n) ) 
75 

* 
76 

* If reqPol is not 0, then a phase requirement for n is requested with 
77 

* polarity ( reqPol>0 ). 
78 

*/ 
79 

void split(Node n, InferenceId id, int reqPol = 0); 
80 


81 

private: 
82 

/** constants */ 
83 

Node d_true; 
84 

Node d_false; 
85 

/** 
86 

* Reference to the state object for the theory of sets. We store the 
87 

* (derived) state here, since it has additional methods required in this 
88 

* class. 
89 

*/ 
90 

SolverState& d_state; 
91 

/** Assert fact recursive 
92 

* 
93 

* This is a helper function for assertInference, which calls assertFact 
94 

* in theory of sets and adds to d_pendingLemmas based on fact. 
95 

* The argument inferType determines the policy on whether fact is processed 
96 

* as a fact or as a lemma (see assertInference above). 
97 

*/ 
98 

bool assertFactRec(Node fact, InferenceId id, Node exp, int inferType = 0); 
99 

}; 
100 


101 

} // namespace sets 
102 

} // namespace theory 
103 

} // namespace CVC4 
104 


105 

#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */ 