1 

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

/*! \file arith_preprocess.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds 
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 Arithmetic preprocess 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__ARITH__ARITH_PREPROCESS_H 
18 

#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H 
19 


20 

#include "context/cdhashmap.h" 
21 

#include "theory/arith/operator_elim.h" 
22 

#include "theory/logic_info.h" 
23 


24 

namespace CVC4 { 
25 

namespace theory { 
26 


27 

class SkolemLemma; 
28 


29 

namespace arith { 
30 


31 

class ArithState; 
32 

class InferenceManager; 
33 


34 

/** 
35 

* This module can be used for (on demand) elimination of extended arithmetic 
36 

* operators like div, mod, to_int, is_int, sqrt, and so on. It uses the 
37 

* operator elimination utility for determining how to reduce formulas. It 
38 

* extends that utility with the ability to generate lemmas on demand via 
39 

* the provided inference manager. 
40 

*/ 
41 

class ArithPreprocess 
42 

{ 
43 

public: 
44 

ArithPreprocess(ArithState& state, 
45 

InferenceManager& im, 
46 

ProofNodeManager* pnm, 
47 

const LogicInfo& info); 
48 
8992 
~ArithPreprocess() {} 
49 

/** 
50 

* Call eliminate operators on formula n, return the resulting trust node, 
51 

* which is of TrustNodeKind REWRITE and whose node is the result of 
52 

* eliminating extended operators from n. 
53 

* 
54 

* @param n The node to eliminate operators from 
55 

* @param partialOnly Whether we are eliminating partial operators only. 
56 

* @return the trust node proving (= n nr) where nr is the return of 
57 

* eliminating operators in n, or the null trust node if n was unchanged. 
58 

*/ 
59 

TrustNode eliminate(TNode n, 
60 

std::vector<SkolemLemma>& lems, 
61 

bool partialOnly = false); 
62 

/** 
63 

* Reduce assertion. This sends a lemma via the inference manager if atom 
64 

* contains any extended operators. When applicable, the lemma is of the form: 
65 

* atom == d_opElim.eliminate(atom) 
66 

* This method returns true if a lemma of the above form was added to 
67 

* the inference manager. Note this returns true even if this lemma was added 
68 

* on a previous call. 
69 

*/ 
70 

bool reduceAssertion(TNode atom); 
71 

/** 
72 

* Is the atom reduced? Returns true if a call to method reduceAssertion was 
73 

* made for the given atom and returned a lemma. In this case, the atom 
74 

* can be ignored. 
75 

*/ 
76 

bool isReduced(TNode atom) const; 
77 


78 

private: 
79 

/** Reference to the inference manager */ 
80 

InferenceManager& d_im; 
81 

/** The operator elimination utility */ 
82 

OperatorElim d_opElim; 
83 

/** The set of assertions that were reduced */ 
84 

context::CDHashMap<Node, bool, NodeHashFunction> d_reduced; 
85 

}; 
86 


87 

} // namespace arith 
88 

} // namespace theory 
89 

} // namespace CVC4 
90 


91 

#endif 