GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/global_negate.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file global_negate.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Mathias Preiner, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief the global_negate preprocessing pass
13
 **
14
 ** Updates a set of assertions to the negation of these assertions.
15
 ** In detail, if assertions is:
16
 **    F1, ..., Fn
17
 ** then we update this vector to:
18
 **    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
19
 ** where x1...xm are the free variables of F1...Fn.
20
 ** When this is done, d_globalNegation flag is marked, so that the solver
21
 ** checks for unsat instead of sat.
22
 **/
23
24
#include "cvc4_private.h"
25
26
#ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
27
#define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
28
29
#include "expr/node.h"
30
#include "preprocessing/preprocessing_pass.h"
31
32
namespace CVC4 {
33
namespace preprocessing {
34
namespace passes {
35
36
17984
class GlobalNegate : public PreprocessingPass
37
{
38
 public:
39
  GlobalNegate(PreprocessingPassContext* preprocContext);
40
41
 protected:
42
  PreprocessingPassResult applyInternal(
43
      AssertionPipeline* assertionsToPreprocess) override;
44
45
 private:
46
  Node simplify(const std::vector<Node>& assertions, NodeManager* nm);
47
};
48
49
}  // namespace passes
50
}  // namespace preprocessing
51
}  // namespace CVC4
52
53
#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */