Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/infer_bounds.cpp	Lines:	33	138	23.9 %
Date:	2021-09-10	Branches:	7	215	3.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/arith/infer_bounds.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace arith {

using namespace inferbounds;

InferBoundAlgorithm::InferBoundAlgorithm()
  : d_alg(None)
{}

InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
  : d_alg(a)
{
  Assert(a != Simplex);
}

InferBoundAlgorithm::InferBoundAlgorithm(
    const std::optional<int>& simplexRounds)
    : d_alg(Simplex)
{}

Algorithms InferBoundAlgorithm::getAlgorithm() const{
  return d_alg;
}

const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const
{
  Assert(getAlgorithm() == Simplex);
  return d_simplexRounds;
}

InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
  return InferBoundAlgorithm(Lookup);
}

InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
  return InferBoundAlgorithm(RowSum);
}

InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
    const std::optional<int>& rounds)
{
  return InferBoundAlgorithm(rounds);
}

ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
    : d_algorithms()
{}

ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
{}


void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
  addAlgorithm(InferBoundAlgorithm::mkLookup());
  addAlgorithm(InferBoundAlgorithm::mkRowSum());
}

void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
  d_algorithms.push_back(alg);
}

ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
  return d_algorithms.begin();
}

ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
  return d_algorithms.end();
}

InferBoundsResult::InferBoundsResult()
  : d_foundBound(false)
  , d_budgetExhausted(false)
  , d_boundIsProvenOpt(false)
  , d_inconsistentState(false)
  , d_reachedThreshold(false)
  , d_value(false)
  , d_term(Node::null())
  , d_upperBound(true)
  , d_explanation(Node::null())
{}

InferBoundsResult::InferBoundsResult(Node term, bool ub)
  : d_foundBound(false)
  , d_budgetExhausted(false)
  , d_boundIsProvenOpt(false)
  , d_inconsistentState(false)
  , d_reachedThreshold(false)
  , d_value(false)
  , d_term(term)
  , d_upperBound(ub)
  , d_explanation(Node::null())
{}

bool InferBoundsResult::foundBound() const {
  return d_foundBound;
}
bool InferBoundsResult::boundIsOptimal() const {
  return d_boundIsProvenOpt;
}
bool InferBoundsResult::inconsistentState() const {
  return d_inconsistentState;
}

bool InferBoundsResult::boundIsInteger() const{
  return foundBound() && d_value.isIntegral();
}

bool InferBoundsResult::boundIsRational() const {
  return foundBound() && d_value.infinitesimalIsZero();
}

Integer InferBoundsResult::valueAsInteger() const{
  Assert(boundIsInteger());
  return getValue().floor();
}
const Rational& InferBoundsResult::valueAsRational() const{
  Assert(boundIsRational());
  return getValue().getNoninfinitesimalPart();
}

const DeltaRational& InferBoundsResult::getValue() const{
  return d_value;
}

Node InferBoundsResult::getTerm() const { return d_term; }

Node InferBoundsResult::getLiteral() const{
  const Rational& q = getValue().getNoninfinitesimalPart();
  NodeManager* nm = NodeManager::currentNM();
  Node qnode = nm->mkConst(q);

  Kind k;
  if(d_upperBound){
    // x <= q + c*delta
    Assert(getValue().infinitesimalSgn() <= 0);
    k = boundIsRational() ? kind::LEQ : kind::LT;
  }else{
    // x >= q + c*delta
    Assert(getValue().infinitesimalSgn() >= 0);
    k = boundIsRational() ? kind::GEQ : kind::GT;
  }
  Node atom = nm->mkNode(k, getTerm(), qnode);
  Node lit = Rewriter::rewrite(atom);
  return lit;
}

/* If there is a bound, this is a node that explains the bound. */
Node InferBoundsResult::getExplanation() const{
  return d_explanation;
}


void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
  d_foundBound = true;
  d_value = dr;
  d_explanation = exp;
}

void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }

bool InferBoundsResult::thresholdWasReached() const{
  return d_reachedThreshold;
}
bool InferBoundsResult::budgetIsExhausted() const{
  return d_budgetExhausted;
}

std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
  os << "{InferBoundsResult " << std::endl;
  os << "on " << ibr.getTerm() << ", ";
  if(ibr.findUpperBound()){
    os << "find upper bound, ";
  }else{
    os << "find lower bound, ";
  }
  if(ibr.foundBound()){
    os << "found a bound: ";
    if(ibr.boundIsInteger()){
      os << ibr.valueAsInteger() << "(int), ";
    }else if(ibr.boundIsRational()){
      os << ibr.valueAsRational() << "(rat), ";
    }else{
      os << ibr.getValue() << "(extended), ";
    }

    os << "as term " << ibr.getLiteral() << ", ";
    os << "explanation " << ibr.getExplanation() << ", ";
  }else {
    os << "did not find a bound, ";
  }

  if(ibr.boundIsOptimal()){
    os << "(opt), ";
  }

  if(ibr.inconsistentState()){
    os << "(inconsistent), ";
  }
  if(ibr.budgetIsExhausted()){
    os << "(budget exhausted), ";
  }
  if(ibr.thresholdWasReached()){
    os << "(reached threshold), ";
  }
  os << "}";
  return os;
}

ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
    : d_simplexSideEffects(NULL)
{}

ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
  if(d_simplexSideEffects != NULL){
    delete d_simplexSideEffects;
    d_simplexSideEffects = NULL;
  }
}

InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
  if(d_simplexSideEffects == NULL){
    d_simplexSideEffects = new InferBoundsResult;
  }
  return *d_simplexSideEffects;
}

namespace inferbounds { /* namespace arith */

std::ostream& operator<<(std::ostream& os,  const Algorithms a){
  switch(a){
  case None:    os << "AlgNone"; break;
  case Lookup:  os << "AlgLookup"; break;
  case RowSum:  os << "AlgRowSum"; break;
  case Simplex: os << "AlgSimplex"; break;
  default:
    Unhandled();
  }

  return os;
}

} /* namespace inferbounds */

} /* namespace arith */
} /* namespace theory */
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, 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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "theory/arith/infer_bounds.h"
20		#include "theory/rewriter.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arith {
25
26		using namespace inferbounds;
27
28		InferBoundAlgorithm::InferBoundAlgorithm()
29		: d_alg(None)
30		{}
31
32	17034	InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
33	17034	: d_alg(a)
34		{
35	17034	Assert(a != Simplex);
36	17034	}
37
38		InferBoundAlgorithm::InferBoundAlgorithm(
39		const std::optional<int>& simplexRounds)
40		: d_alg(Simplex)
41		{}
42
43	50046	Algorithms InferBoundAlgorithm::getAlgorithm() const{
44	50046	return d_alg;
45		}
46
47		const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const
48		{
49		Assert(getAlgorithm() == Simplex);
50		return d_simplexRounds;
51		}
52
53	8517	InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
54	8517	return InferBoundAlgorithm(Lookup);
55		}
56
57	8517	InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
58	8517	return InferBoundAlgorithm(RowSum);
59		}
60
61		InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
62		const std::optional<int>& rounds)
63		{
64		return InferBoundAlgorithm(rounds);
65		}
66
67	8517	ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
68	8517	: d_algorithms()
69	8517	{}
70
71	8517	ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
72	8517	{}
73
74
75	8517	void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
76	8517	addAlgorithm(InferBoundAlgorithm::mkLookup());
77	8517	addAlgorithm(InferBoundAlgorithm::mkRowSum());
78	8517	}
79
80	17034	void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
81	17034	d_algorithms.push_back(alg);
82	17034	}
83
84	8517	ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
85	8517	return d_algorithms.begin();
86		}
87
88	8517	ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
89	8517	return d_algorithms.end();
90		}
91
92		InferBoundsResult::InferBoundsResult()
93		: d_foundBound(false)
94		, d_budgetExhausted(false)
95		, d_boundIsProvenOpt(false)
96		, d_inconsistentState(false)
97		, d_reachedThreshold(false)
98		, d_value(false)
99		, d_term(Node::null())
100		, d_upperBound(true)
101		, d_explanation(Node::null())
102		{}
103
104		InferBoundsResult::InferBoundsResult(Node term, bool ub)
105		: d_foundBound(false)
106		, d_budgetExhausted(false)
107		, d_boundIsProvenOpt(false)
108		, d_inconsistentState(false)
109		, d_reachedThreshold(false)
110		, d_value(false)
111		, d_term(term)
112		, d_upperBound(ub)
113		, d_explanation(Node::null())
114		{}
115
116		bool InferBoundsResult::foundBound() const {
117		return d_foundBound;
118		}
119		bool InferBoundsResult::boundIsOptimal() const {
120		return d_boundIsProvenOpt;
121		}
122		bool InferBoundsResult::inconsistentState() const {
123		return d_inconsistentState;
124		}
125
126		bool InferBoundsResult::boundIsInteger() const{
127		return foundBound() && d_value.isIntegral();
128		}
129
130		bool InferBoundsResult::boundIsRational() const {
131		return foundBound() && d_value.infinitesimalIsZero();
132		}
133
134		Integer InferBoundsResult::valueAsInteger() const{
135		Assert(boundIsInteger());
136		return getValue().floor();
137		}
138		const Rational& InferBoundsResult::valueAsRational() const{
139		Assert(boundIsRational());
140		return getValue().getNoninfinitesimalPart();
141		}
142
143		const DeltaRational& InferBoundsResult::getValue() const{
144		return d_value;
145		}
146
147		Node InferBoundsResult::getTerm() const { return d_term; }
148
149		Node InferBoundsResult::getLiteral() const{
150		const Rational& q = getValue().getNoninfinitesimalPart();
151		NodeManager* nm = NodeManager::currentNM();
152		Node qnode = nm->mkConst(q);
153
154		Kind k;
155		if(d_upperBound){
156		// x <= q + c*delta
157		Assert(getValue().infinitesimalSgn() <= 0);
158		k = boundIsRational() ? kind::LEQ : kind::LT;
159		}else{
160		// x >= q + c*delta
161		Assert(getValue().infinitesimalSgn() >= 0);
162		k = boundIsRational() ? kind::GEQ : kind::GT;
163		}
164		Node atom = nm->mkNode(k, getTerm(), qnode);
165		Node lit = Rewriter::rewrite(atom);
166		return lit;
167		}
168
169		/* If there is a bound, this is a node that explains the bound. */
170		Node InferBoundsResult::getExplanation() const{
171		return d_explanation;
172		}
173
174
175		void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
176		d_foundBound = true;
177		d_value = dr;
178		d_explanation = exp;
179		}
180
181		void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
182		void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
183		void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
184		void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }
185
186		bool InferBoundsResult::thresholdWasReached() const{
187		return d_reachedThreshold;
188		}
189		bool InferBoundsResult::budgetIsExhausted() const{
190		return d_budgetExhausted;
191		}
192
193		std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
194		os << "{InferBoundsResult " << std::endl;
195		os << "on " << ibr.getTerm() << ", ";
196		if(ibr.findUpperBound()){
197		os << "find upper bound, ";
198		}else{
199		os << "find lower bound, ";
200		}
201		if(ibr.foundBound()){
202		os << "found a bound: ";
203		if(ibr.boundIsInteger()){
204		os << ibr.valueAsInteger() << "(int), ";
205		}else if(ibr.boundIsRational()){
206		os << ibr.valueAsRational() << "(rat), ";
207		}else{
208		os << ibr.getValue() << "(extended), ";
209		}
210
211		os << "as term " << ibr.getLiteral() << ", ";
212		os << "explanation " << ibr.getExplanation() << ", ";
213		}else {
214		os << "did not find a bound, ";
215		}
216
217		if(ibr.boundIsOptimal()){
218		os << "(opt), ";
219		}
220
221		if(ibr.inconsistentState()){
222		os << "(inconsistent), ";
223		}
224		if(ibr.budgetIsExhausted()){
225		os << "(budget exhausted), ";
226		}
227		if(ibr.thresholdWasReached()){
228		os << "(reached threshold), ";
229		}
230		os << "}";
231		return os;
232		}
233
234	8517	ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
235	8517	: d_simplexSideEffects(NULL)
236	8517	{}
237
238	17034	ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
239	8517	if(d_simplexSideEffects != NULL){
240		delete d_simplexSideEffects;
241		d_simplexSideEffects = NULL;
242		}
243	8517	}
244
245		InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
246		if(d_simplexSideEffects == NULL){
247		d_simplexSideEffects = new InferBoundsResult;
248		}
249		return *d_simplexSideEffects;
250		}
251
252		namespace inferbounds { /* namespace arith */
253
254		std::ostream& operator<<(std::ostream& os, const Algorithms a){
255		switch(a){
256		case None: os << "AlgNone"; break;
257		case Lookup: os << "AlgLookup"; break;
258		case RowSum: os << "AlgRowSum"; break;
259		case Simplex: os << "AlgSimplex"; break;
260		default:
261		Unhandled();
262		}
263
264		return os;
265		}
266
267		} /* namespace inferbounds */
268
269		} /* namespace arith */
270		} /* namespace theory */
271	29502	} // namespace cvc5