Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/strategy.cpp	Lines:	58	82	70.7 %
Date:	2021-08-01	Branches:	87	248	35.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of the strategy of the theory of strings.
 */

#include "theory/strings/strategy.h"

#include "options/strings_options.h"

namespace cvc5 {
namespace theory {
namespace strings {

std::ostream& operator<<(std::ostream& out, InferStep s)
{
  switch (s)
  {
    case BREAK: out << "break"; break;
    case CHECK_INIT: out << "check_init"; break;
    case CHECK_CONST_EQC: out << "check_const_eqc"; break;
    case CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
    case CHECK_CYCLES: out << "check_cycles"; break;
    case CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
    case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break;
    case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break;
    case CHECK_CODES: out << "check_codes"; break;
    case CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
    case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
    case CHECK_MEMBERSHIP: out << "check_membership"; break;
    case CHECK_CARDINALITY: out << "check_cardinality"; break;
    default: out << "?"; break;
  }
  return out;
}

Strategy::Strategy() : d_strategy_init(false) {}

Strategy::~Strategy() {}

bool Strategy::isStrategyInit() const { return d_strategy_init; }

bool Strategy::hasStrategyEffort(Theory::Effort e) const
{
  return d_strat_steps.find(e) != d_strat_steps.end();
}

std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin(
    Theory::Effort e)
{
  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
      d_strat_steps.find(e);
  Assert(it != d_strat_steps.end());
  return d_infer_steps.begin() + it->second.first;
}

std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd(
    Theory::Effort e)
{
  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
      d_strat_steps.find(e);
  Assert(it != d_strat_steps.end());
  return d_infer_steps.begin() + it->second.second;
}

void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak)
{
  // must run check init first
  Assert((s == CHECK_INIT) == d_infer_steps.empty());
  d_infer_steps.push_back(std::pair<InferStep, int>(s, effort));
  if (addBreak)
  {
    d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0));
  }
}

void Strategy::initializeStrategy()
{
  // initialize the strategy if not already done so
  if (!d_strategy_init)
  {
    std::map<Theory::Effort, unsigned> step_begin;
    std::map<Theory::Effort, unsigned> step_end;
    d_strategy_init = true;
    // beginning indices
    step_begin[Theory::EFFORT_FULL] = 0;
    if (options::stringEager())
    {
      step_begin[Theory::EFFORT_STANDARD] = 0;
    }
    // add the inference steps
    addStrategyStep(CHECK_INIT);
    addStrategyStep(CHECK_CONST_EQC);
    addStrategyStep(CHECK_EXTF_EVAL, 0);
    // we must check cycles before using flat forms
    addStrategyStep(CHECK_CYCLES);
    if (options::stringFlatForms())
    {
      addStrategyStep(CHECK_FLAT_FORMS);
    }
    addStrategyStep(CHECK_EXTF_REDUCTION, 1);
    if (options::stringEager())
    {
      // do only the above inferences at standard effort, if applicable
      step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1;
    }
    if (!options::stringEagerLen())
    {
      addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
    }
    addStrategyStep(CHECK_NORMAL_FORMS_EQ);
    addStrategyStep(CHECK_EXTF_EVAL, 1);
    if (!options::stringEagerLen() && options::stringLenNorm())
    {
      addStrategyStep(CHECK_LENGTH_EQC, 0, false);
      addStrategyStep(CHECK_REGISTER_TERMS_NF);
    }
    addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
    addStrategyStep(CHECK_CODES);
    if (options::stringEagerLen() && options::stringLenNorm())
    {
      addStrategyStep(CHECK_LENGTH_EQC);
    }
    if (options::stringExp() && !options::stringGuessModel())
    {
      addStrategyStep(CHECK_EXTF_REDUCTION, 2);
    }
    addStrategyStep(CHECK_MEMBERSHIP);
    addStrategyStep(CHECK_CARDINALITY);
    step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
    if (options::stringExp() && options::stringGuessModel())
    {
      step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
      // these two steps are run in parallel
      addStrategyStep(CHECK_EXTF_REDUCTION, 2, false);
      addStrategyStep(CHECK_EXTF_EVAL, 3);
      step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
    }
    // set the beginning/ending ranges
    for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin)
    {
      Theory::Effort e = it_begin.first;
      std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
      Assert(it_end != step_end.end());
      d_strat_steps[e] =
          std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
    }
  }
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Implementation of the strategy of the theory of strings.
14		*/
15
16		#include "theory/strings/strategy.h"
17
18		#include "options/strings_options.h"
19
20		namespace cvc5 {
21		namespace theory {
22		namespace strings {
23
24		std::ostream& operator<<(std::ostream& out, InferStep s)
25		{
26		switch (s)
27		{
28		case BREAK: out << "break"; break;
29		case CHECK_INIT: out << "check_init"; break;
30		case CHECK_CONST_EQC: out << "check_const_eqc"; break;
31		case CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
32		case CHECK_CYCLES: out << "check_cycles"; break;
33		case CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
34		case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break;
35		case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break;
36		case CHECK_CODES: out << "check_codes"; break;
37		case CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
38		case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
39		case CHECK_MEMBERSHIP: out << "check_membership"; break;
40		case CHECK_CARDINALITY: out << "check_cardinality"; break;
41		default: out << "?"; break;
42		}
43		return out;
44		}
45
46	9838	Strategy::Strategy() : d_strategy_init(false) {}
47
48	9838	Strategy::~Strategy() {}
49
50	361292	bool Strategy::isStrategyInit() const { return d_strategy_init; }
51
52	92086	bool Strategy::hasStrategyEffort(Theory::Effort e) const
53		{
54	92086	return d_strat_steps.find(e) != d_strat_steps.end();
55		}
56
57	33565	std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin(
58		Theory::Effort e)
59		{
60		std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
61	33565	d_strat_steps.find(e);
62	33565	Assert(it != d_strat_steps.end());
63	33565	return d_infer_steps.begin() + it->second.first;
64		}
65
66	33565	std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd(
67		Theory::Effort e)
68		{
69		std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
70	33565	d_strat_steps.find(e);
71	33565	Assert(it != d_strat_steps.end());
72	33565	return d_infer_steps.begin() + it->second.second;
73		}
74
75	123169	void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak)
76		{
77		// must run check init first
78	123169	Assert((s == CHECK_INIT) == d_infer_steps.empty());
79	123169	d_infer_steps.push_back(std::pair<InferStep, int>(s, effort));
80	123169	if (addBreak)
81		{
82	123169	d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0));
83		}
84	123169	}
85
86	15189	void Strategy::initializeStrategy()
87		{
88		// initialize the strategy if not already done so
89	15189	if (!d_strategy_init)
90		{
91	18778	std::map<Theory::Effort, unsigned> step_begin;
92	18778	std::map<Theory::Effort, unsigned> step_end;
93	9389	d_strategy_init = true;
94		// beginning indices
95	9389	step_begin[Theory::EFFORT_FULL] = 0;
96	28167	if (options::stringEager())
97		{
98	2	step_begin[Theory::EFFORT_STANDARD] = 0;
99		}
100		// add the inference steps
101	9389	addStrategyStep(CHECK_INIT);
102	9389	addStrategyStep(CHECK_CONST_EQC);
103	9389	addStrategyStep(CHECK_EXTF_EVAL, 0);
104		// we must check cycles before using flat forms
105	9389	addStrategyStep(CHECK_CYCLES);
106	18778	if (options::stringFlatForms())
107		{
108	9389	addStrategyStep(CHECK_FLAT_FORMS);
109		}
110	9389	addStrategyStep(CHECK_EXTF_REDUCTION, 1);
111	9389	if (options::stringEager())
112		{
113		// do only the above inferences at standard effort, if applicable
114	2	step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1;
115		}
116	62178	if (!options::stringEagerLen())
117		{
118		addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
119		}
120	9389	addStrategyStep(CHECK_NORMAL_FORMS_EQ);
121	9389	addStrategyStep(CHECK_EXTF_EVAL, 1);
122	18778	if (!options::stringEagerLen() && options::stringLenNorm())
123		{
124		addStrategyStep(CHECK_LENGTH_EQC, 0, false);
125		addStrategyStep(CHECK_REGISTER_TERMS_NF);
126		}
127	9389	addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
128	9389	addStrategyStep(CHECK_CODES);
129	9389	if (options::stringEagerLen() && options::stringLenNorm())
130		{
131	9389	addStrategyStep(CHECK_LENGTH_EQC);
132		}
133	18204	if (options::stringExp() && !options::stringGuessModel())
134		{
135	1112	addStrategyStep(CHECK_EXTF_REDUCTION, 2);
136		}
137	9389	addStrategyStep(CHECK_MEMBERSHIP);
138	9389	addStrategyStep(CHECK_CARDINALITY);
139	9389	step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
140	9389	if (options::stringExp() && options::stringGuessModel())
141		{
142		step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
143		// these two steps are run in parallel
144		addStrategyStep(CHECK_EXTF_REDUCTION, 2, false);
145		addStrategyStep(CHECK_EXTF_EVAL, 3);
146		step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
147		}
148		// set the beginning/ending ranges
149	18780	for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin)
150		{
151	9391	Theory::Effort e = it_begin.first;
152	9391	std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
153	9391	Assert(it_end != step_end.end());
154	9391	d_strat_steps[e] =
155	18782	std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
156		}
157		}
158	15189	}
159
160		} // namespace strings
161		} // namespace theory
162	128440	} // namespace cvc5