Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/callbacks.cpp	Lines:	103	117	88.0 %
Date:	2021-11-08	Branches:	100	436	22.9 %


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

#include "theory/arith/callbacks.h"

#include "expr/skolem_manager.h"
#include "proof/proof_node.h"
#include "theory/arith/theory_arith_private.h"

namespace cvc5 {
namespace theory {
namespace arith {

SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
  : d_arith(ta)
{}
void SetupLiteralCallBack::operator()(TNode lit){
  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
  if(!d_arith.isSetup(atom)){
    d_arith.setupAtom(atom);
  }
}

DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
  : d_ta(ta)
{}
Rational DeltaComputeCallback::operator()() const{
  return d_ta.deltaValueForTotalOrder();
}

TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
: d_ta(ta)
{}
ArithVar TempVarMalloc::request(){
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
  return d_ta.requestArithVar(skolem, false, true);
}
void TempVarMalloc::release(ArithVar v){
  d_ta.releaseArithVar(v);
}

BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
  : d_ta(ta)
{}
void BasicVarModelUpdateCallBack::operator()(ArithVar x){
  d_ta.signal(x);
}

RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
  : d_ta(ta)
{}

void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
  Assert(c->inConflict());
  d_ta.raiseConflict(c, id);
}

FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs)
    : d_farkas(),
      d_constraints(),
      d_consequent(NullConstraint),
      d_consequentSet(false),
      d_produceProofs(produceProofs)
{
  reset();
}

bool FarkasConflictBuilder::underConstruction() const{
  return d_consequent != NullConstraint;
}

bool FarkasConflictBuilder::consequentIsSet() const{
  return d_consequentSet;
}

void FarkasConflictBuilder::reset(){
  d_consequent = NullConstraint;
  d_constraints.clear();
  d_consequentSet = false;
  if (d_produceProofs)
  {
    d_farkas.clear();
  }
  Assert(!underConstruction());
}

/* Adds a constraint to the constraint under construction. */
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
  Assert(
      !d_produceProofs
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
  Assert(d_produceProofs || d_farkas.empty());
  Assert(c->isTrue());

  if(d_consequent == NullConstraint){
    d_consequent = c;
  } else {
    d_constraints.push_back(c);
  }
  if (d_produceProofs)
  {
    d_farkas.push_back(fc);
  }
  Assert(!d_produceProofs || d_constraints.size() + 1 == d_farkas.size());
  Assert(d_produceProofs || d_farkas.empty());
}

void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
  Assert(!mult.isZero());
  if (d_produceProofs && !mult.isOne())
  {
    Rational prod = fc * mult;
    addConstraint(c, prod);
  }
  else
  {
    addConstraint(c, fc);
  }
}

void FarkasConflictBuilder::makeLastConsequent(){
  Assert(!d_consequentSet);
  Assert(underConstruction());

  if(d_constraints.empty()){
    // no-op
    d_consequentSet = true;
  } else {
    Assert(d_consequent != NullConstraint);
    ConstraintCP last = d_constraints.back();
    d_constraints.back() = d_consequent;
    d_consequent = last;
    if (d_produceProofs)
    {
      std::swap(d_farkas.front(), d_farkas.back());
    }
    d_consequentSet = true;
  }

  Assert(!d_consequent->negationHasProof());
  Assert(d_consequentSet);
}

/* Turns the vector under construction into a conflict */
ConstraintCP FarkasConflictBuilder::commitConflict(){
  Assert(underConstruction());
  Assert(!d_constraints.empty());
  Assert(
      !d_produceProofs
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
  Assert(d_produceProofs || d_farkas.empty());
  Assert(d_consequentSet);

  ConstraintP not_c = d_consequent->getNegation();
  RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr;
  not_c->impliedByFarkas(d_constraints, coeffs, true );

  reset();
  Assert(!underConstruction());
  Assert(not_c->inConflict());
  Assert(!d_consequentSet);
  return not_c;
}

RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
  : d_ta(ta)
{}

/* If you are not an equality engine, don't use this! */
void RaiseEqualityEngineConflict::raiseEEConflict(
    Node n, std::shared_ptr<ProofNode> pf) const
{
  d_ta.raiseBlackBoxConflict(n, pf);
}

BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
: d_ta(ta)
{}

const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
  return d_ta.boundsInfo(basic);
}

BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
  return boundsInfo(basic).atBounds();
}
BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
  return boundsInfo(basic).hasBounds();
}

}  // 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, Haniel Barbosa, 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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "theory/arith/callbacks.h"
20
21		#include "expr/skolem_manager.h"
22		#include "proof/proof_node.h"
23		#include "theory/arith/theory_arith_private.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace arith {
28
29	15275	SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
30	15275	: d_arith(ta)
31	15275	{}
32	21964	void SetupLiteralCallBack::operator()(TNode lit){
33	43928	TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
34	21964	if(!d_arith.isSetup(atom)){
35	21964	d_arith.setupAtom(atom);
36		}
37	21964	}
38
39	15275	DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
40	15275	: d_ta(ta)
41	15275	{}
42	61162	Rational DeltaComputeCallback::operator()() const{
43	61162	return d_ta.deltaValueForTotalOrder();
44		}
45
46	61100	TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
47	61100	: d_ta(ta)
48	61100	{}
49		ArithVar TempVarMalloc::request(){
50		NodeManager* nm = NodeManager::currentNM();
51		SkolemManager* sm = nm->getSkolemManager();
52		Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
53		return d_ta.requestArithVar(skolem, false, true);
54		}
55		void TempVarMalloc::release(ArithVar v){
56		d_ta.releaseArithVar(v);
57		}
58
59	15275	BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
60	15275	: d_ta(ta)
61	15275	{}
62	8324602	void BasicVarModelUpdateCallBack::operator()(ArithVar x){
63	8324602	d_ta.signal(x);
64	8324602	}
65
66	76375	RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
67	76375	: d_ta(ta)
68	76375	{}
69
70	87350	void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
71	87350	Assert(c->inConflict());
72	87350	d_ta.raiseConflict(c, id);
73	87350	}
74
75	61100	FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs)
76		: d_farkas(),
77		d_constraints(),
78		d_consequent(NullConstraint),
79		d_consequentSet(false),
80	61100	d_produceProofs(produceProofs)
81		{
82	61100	reset();
83	61100	}
84
85	1017954	bool FarkasConflictBuilder::underConstruction() const{
86	1017954	return d_consequent != NullConstraint;
87		}
88
89	87350	bool FarkasConflictBuilder::consequentIsSet() const{
90	87350	return d_consequentSet;
91		}
92
93	148450	void FarkasConflictBuilder::reset(){
94	148450	d_consequent = NullConstraint;
95	148450	d_constraints.clear();
96	148450	d_consequentSet = false;
97	148450	if (d_produceProofs)
98		{
99	63580	d_farkas.clear();
100		}
101	148450	Assert(!underConstruction());
102	148450	}
103
104		/* Adds a constraint to the constraint under construction. */
105	1092109	void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
106	1092109	Assert(
107		!d_produceProofs
108		\|\| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
109		\|\| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
110	1092109	Assert(d_produceProofs \|\| d_farkas.empty());
111	1092109	Assert(c->isTrue());
112
113	1092109	if(d_consequent == NullConstraint){
114	87350	d_consequent = c;
115		} else {
116	1004759	d_constraints.push_back(c);
117		}
118	1092109	if (d_produceProofs)
119		{
120	244244	d_farkas.push_back(fc);
121		}
122	1092109	Assert(!d_produceProofs \|\| d_constraints.size() + 1 == d_farkas.size());
123	1092109	Assert(d_produceProofs \|\| d_farkas.empty());
124	1092109	}
125
126	1092109	void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
127	1092109	Assert(!mult.isZero());
128	1092109	if (d_produceProofs && !mult.isOne())
129		{
130	246602	Rational prod = fc * mult;
131	123301	addConstraint(c, prod);
132		}
133		else
134		{
135	968808	addConstraint(c, fc);
136		}
137	1092109	}
138
139	87350	void FarkasConflictBuilder::makeLastConsequent(){
140	87350	Assert(!d_consequentSet);
141	87350	Assert(underConstruction());
142
143	87350	if(d_constraints.empty()){
144		// no-op
145	3894	d_consequentSet = true;
146		} else {
147	83456	Assert(d_consequent != NullConstraint);
148	83456	ConstraintCP last = d_constraints.back();
149	83456	d_constraints.back() = d_consequent;
150	83456	d_consequent = last;
151	83456	if (d_produceProofs)
152		{
153	30660	std::swap(d_farkas.front(), d_farkas.back());
154		}
155	83456	d_consequentSet = true;
156		}
157
158	87350	Assert(!d_consequent->negationHasProof());
159	87350	Assert(d_consequentSet);
160	87350	}
161
162		/* Turns the vector under construction into a conflict */
163	87350	ConstraintCP FarkasConflictBuilder::commitConflict(){
164	87350	Assert(underConstruction());
165	87350	Assert(!d_constraints.empty());
166	87350	Assert(
167		!d_produceProofs
168		\|\| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
169		\|\| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
170	87350	Assert(d_produceProofs \|\| d_farkas.empty());
171	87350	Assert(d_consequentSet);
172
173	87350	ConstraintP not_c = d_consequent->getNegation();
174	87350	RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr;
175	87350	not_c->impliedByFarkas(d_constraints, coeffs, true );
176
177	87350	reset();
178	87350	Assert(!underConstruction());
179	87350	Assert(not_c->inConflict());
180	87350	Assert(!d_consequentSet);
181	87350	return not_c;
182		}
183
184	15275	RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
185	15275	: d_ta(ta)
186	15275	{}
187
188		/* If you are not an equality engine, don't use this! */
189	2728	void RaiseEqualityEngineConflict::raiseEEConflict(
190		Node n, std::shared_ptr<ProofNode> pf) const
191		{
192	2728	d_ta.raiseBlackBoxConflict(n, pf);
193	2728	}
194
195	15275	BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
196	15275	: d_ta(ta)
197	15275	{}
198
199		const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
200		return d_ta.boundsInfo(basic);
201		}
202
203		BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
204		return boundsInfo(basic).atBounds();
205		}
206		BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
207		return boundsInfo(basic).hasBounds();
208		}
209
210		} // namespace arith
211		} // namespace theory
212	31140	} // namespace cvc5