Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/bv_eager_atoms.cpp	Lines:	12	12	100.0 %
Date:	2021-08-16	Branches:	16	26	61.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Wrap assertions in BITVECTOR_EAGER_ATOM nodes.
 *
 * This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes
 * and allows to use eager bit-blasting in the BV solver.
 */

#include "preprocessing/passes/bv_eager_atoms.h"

#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"

namespace cvc5 {
namespace preprocessing {
namespace passes {

BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "bv-eager-atoms"){};

PreprocessingPassResult BvEagerAtoms::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  NodeManager* nm = NodeManager::currentNM();
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    TNode atom = (*assertionsToPreprocess)[i];
    if (atom.isConst())
    {
      // don't bother making true/false into atoms
      continue;
    }
    Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
    assertionsToPreprocess->replace(i, eager_atom);
  }
  return PreprocessingPassResult::NO_CONFLICT;
}


}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Wrap assertions in BITVECTOR_EAGER_ATOM nodes.
14		*
15		* This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes
16		* and allows to use eager bit-blasting in the BV solver.
17		*/
18
19		#include "preprocessing/passes/bv_eager_atoms.h"
20
21		#include "preprocessing/assertion_pipeline.h"
22		#include "preprocessing/preprocessing_pass_context.h"
23		#include "theory/theory_engine.h"
24		#include "theory/theory_model.h"
25
26		namespace cvc5 {
27		namespace preprocessing {
28		namespace passes {
29
30	9853	BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext)
31	9853	: PreprocessingPass(preprocContext, "bv-eager-atoms"){};
32
33	58	PreprocessingPassResult BvEagerAtoms::applyInternal(
34		AssertionPipeline* assertionsToPreprocess)
35		{
36	58	NodeManager* nm = NodeManager::currentNM();
37	488	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
38		{
39	735	TNode atom = (*assertionsToPreprocess)[i];
40	430	if (atom.isConst())
41		{
42		// don't bother making true/false into atoms
43	125	continue;
44		}
45	610	Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
46	305	assertionsToPreprocess->replace(i, eager_atom);
47		}
48	58	return PreprocessingPassResult::NO_CONFLICT;
49		}
50
51
52		} // namespace passes
53		} // namespace preprocessing
54	29340	} // namespace cvc5