Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/assertions.cpp	Lines:	89	102	87.3 %
Date:	2021-11-07	Branches:	102	218	46.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
 *
 * 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.
 * ****************************************************************************
 *
 * The module for storing assertions for an SMT engine.
 */

#include "smt/assertions.h"

#include <sstream>

#include "base/modal_exception.h"
#include "expr/node_algorithm.h"
#include "options/base_options.h"
#include "options/expr_options.h"
#include "options/language.h"
#include "options/smt_options.h"
#include "smt/abstract_values.h"
#include "smt/env.h"
#include "smt/solver_engine.h"
#include "theory/trust_substitutions.h"

using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

Assertions::Assertions(Env& env, AbstractValues& absv)
    : EnvObj(env),
      d_absValues(absv),
      d_produceAssertions(false),
      d_assertionList(userContext()),
      d_assertionListDefs(userContext()),
      d_globalDefineFunLemmasIndex(userContext(), 0),
      d_globalNegation(false),
      d_assertions()
{
}

Assertions::~Assertions()
{
}

void Assertions::refresh()
{
  if (d_globalDefineFunLemmas != nullptr)
  {
    // Global definitions are asserted now to ensure they always exist. This is
    // done at the beginning of preprocessing, to ensure that definitions take
    // priority over, e.g. solving during preprocessing. See issue #7479.
    size_t numGlobalDefs = d_globalDefineFunLemmas->size();
    for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
    {
      addFormula((*d_globalDefineFunLemmas)[i], false, true, false);
    }
    d_globalDefineFunLemmasIndex = numGlobalDefs;
  }
}

void Assertions::finishInit()
{
  // [MGD 10/20/2011] keep around in incremental mode, due to a
  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
  // first, some user-context-dependent TNodes might still exist
  // with rc == 0.
  if (options().smt.produceAssertions || options().base.incrementalSolving)
  {
    // In the case of incremental solving, we appear to need these to
    // ensure the relevant Nodes remain live.
    d_produceAssertions = true;
    d_globalDefineFunLemmas.reset(new std::vector<Node>());
  }
}

void Assertions::clearCurrent()
{
  d_assertions.clear();
  d_assertions.getIteSkolemMap().clear();
}

void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
                                    bool isEntailmentCheck)
{
  NodeManager* nm = NodeManager::currentNM();
  // reset global negation
  d_globalNegation = false;
  // clear the assumptions
  d_assumptions.clear();
  if (isEntailmentCheck)
  {
    size_t size = assumptions.size();
    if (size > 1)
    {
      /* Assume: not (BIGAND assumptions)  */
      d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
    }
    else if (size == 1)
    {
      /* Assume: not expr  */
      d_assumptions.push_back(assumptions[0].notNode());
    }
  }
  else
  {
    /* Assume: BIGAND assumptions  */
    d_assumptions = assumptions;
  }

  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
  for (const Node& e : d_assumptions)
  {
    // Substitute out any abstract values in ex.
    Node n = d_absValues.substituteAbstractValues(e);
    // Ensure expr is type-checked at this point.
    ensureBoolean(n);
    addFormula(n, true, false, false);
  }
}

void Assertions::assertFormula(const Node& n)
{
  ensureBoolean(n);
  bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
  addFormula(n, false, false, maybeHasFv);
}

std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
bool Assertions::isGlobalNegated() const { return d_globalNegation; }
void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }

preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
{
  return d_assertions;
}

const context::CDList<Node>& Assertions::getAssertionList() const
{
  return d_assertionList;
}

const context::CDList<Node>& Assertions::getAssertionListDefinitions() const
{
  return d_assertionListDefs;
}

void Assertions::addFormula(TNode n,
                            bool isAssumption,
                            bool isFunDef,
                            bool maybeHasFv)
{
  // add to assertion list if it exists
  if (d_produceAssertions)
  {
    d_assertionList.push_back(n);
    if (isFunDef)
    {
      d_assertionListDefs.push_back(n);
    }
  }
  if (n.isConst() && n.getConst<bool>())
  {
    // true, nothing to do
    return;
  }
  Trace("smt") << "Assertions::addFormula(" << n
               << ", isAssumption = " << isAssumption
               << ", isFunDef = " << isFunDef << std::endl;
  if (isFunDef)
  {
    // if a non-recursive define-fun, just add as a top-level substitution
    if (n.getKind() == EQUAL && n[0].isVar())
    {
      // A define-fun is an assumption in the overall proof, thus
      // we justify the substitution with ASSUME here.
      d_env.getTopLevelSubstitutions().addSubstitution(
          n[0], n[1], PfRule::ASSUME, {}, {n});
      return;
    }
  }

  // Ensure that it does not contain free variables
  if (maybeHasFv)
  {
    if (expr::hasFreeVar(n))
    {
      std::stringstream se;
      if (isFunDef)
      {
        se << "Cannot process function definition with free variable.";
      }
      else
      {
        se << "Cannot process assertion with free variable.";
        if (language::isLangSygus(options().base.inputLanguage))
        {
          // Common misuse of SyGuS is to use top-level assert instead of
          // constraint when defining the synthesis conjecture.
          se << " Perhaps you meant `constraint` instead of `assert`?";
        }
      }
      throw ModalException(se.str().c_str());
    }
  }

  // Add the normalized formula to the queue
  d_assertions.push_back(n, isAssumption, true);
}

void Assertions::addDefineFunDefinition(Node n, bool global)
{
  n = d_absValues.substituteAbstractValues(n);
  if (global && d_globalDefineFunLemmas != nullptr)
  {
    // Global definitions are asserted at check-sat-time because we have to
    // make sure that they are always present
    Assert(!language::isLangSygus(options().base.inputLanguage));
    d_globalDefineFunLemmas->emplace_back(n);
  }
  else
  {
    // We don't permit functions-to-synthesize within recursive function
    // definitions currently. Thus, we should check for free variables if the
    // input language is SyGuS.
    bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
    addFormula(n, false, true, maybeHasFv);
  }
}

void Assertions::ensureBoolean(const Node& n)
{
  TypeNode type = n.getType(options().expr.typeChecking);
  if (!type.isBoolean())
  {
    std::stringstream ss;
    ss << "Expected Boolean type\n"
       << "The assertion : " << n << "\n"
       << "Its type      : " << type;
    throw TypeCheckingExceptionPrivate(n, ss.str());
  }
}

void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
{
  d_assertions.setProofGenerator(pppg);
}

bool Assertions::isProofEnabled() const
{
  return d_assertions.isProofEnabled();
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Haniel Barbosa
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		* The module for storing assertions for an SMT engine.
14		*/
15
16		#include "smt/assertions.h"
17
18		#include <sstream>
19
20		#include "base/modal_exception.h"
21		#include "expr/node_algorithm.h"
22		#include "options/base_options.h"
23		#include "options/expr_options.h"
24		#include "options/language.h"
25		#include "options/smt_options.h"
26		#include "smt/abstract_values.h"
27		#include "smt/env.h"
28		#include "smt/solver_engine.h"
29		#include "theory/trust_substitutions.h"
30
31		using namespace cvc5::theory;
32		using namespace cvc5::kind;
33
34		namespace cvc5 {
35		namespace smt {
36
37	18633	Assertions::Assertions(Env& env, AbstractValues& absv)
38		: EnvObj(env),
39		d_absValues(absv),
40		d_produceAssertions(false),
41	18633	d_assertionList(userContext()),
42	18633	d_assertionListDefs(userContext()),
43	18633	d_globalDefineFunLemmasIndex(userContext(), 0),
44		d_globalNegation(false),
45	74532	d_assertions()
46		{
47	18633	}
48
49	31768	Assertions::~Assertions()
50		{
51	31768	}
52
53	19110	void Assertions::refresh()
54		{
55	19110	if (d_globalDefineFunLemmas != nullptr)
56		{
57		// Global definitions are asserted now to ensure they always exist. This is
58		// done at the beginning of preprocessing, to ensure that definitions take
59		// priority over, e.g. solving during preprocessing. See issue #7479.
60	16168	size_t numGlobalDefs = d_globalDefineFunLemmas->size();
61	16247	for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
62		{
63	79	addFormula((*d_globalDefineFunLemmas)[i], false, true, false);
64		}
65	16168	d_globalDefineFunLemmasIndex = numGlobalDefs;
66		}
67	19110	}
68
69	15273	void Assertions::finishInit()
70		{
71		// [MGD 10/20/2011] keep around in incremental mode, due to a
72		// cleanup ordering issue and Nodes/TNodes. If SAT is popped
73		// first, some user-context-dependent TNodes might still exist
74		// with rc == 0.
75	15273	if (options().smt.produceAssertions \|\| options().base.incrementalSolving)
76		{
77		// In the case of incremental solving, we appear to need these to
78		// ensure the relevant Nodes remain live.
79	12287	d_produceAssertions = true;
80	12287	d_globalDefineFunLemmas.reset(new std::vector<Node>());
81		}
82	15273	}
83
84	22716	void Assertions::clearCurrent()
85		{
86	22716	d_assertions.clear();
87	22716	d_assertions.getIteSkolemMap().clear();
88	22716	}
89
90	20579	void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
91		bool isEntailmentCheck)
92		{
93	20579	NodeManager* nm = NodeManager::currentNM();
94		// reset global negation
95	20579	d_globalNegation = false;
96		// clear the assumptions
97	20579	d_assumptions.clear();
98	20579	if (isEntailmentCheck)
99		{
100	81	size_t size = assumptions.size();
101	81	if (size > 1)
102		{
103		/* Assume: not (BIGAND assumptions) */
104	4	d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
105		}
106	77	else if (size == 1)
107		{
108		/* Assume: not expr */
109	77	d_assumptions.push_back(assumptions[0].notNode());
110		}
111		}
112		else
113		{
114		/* Assume: BIGAND assumptions */
115	20498	d_assumptions = assumptions;
116		}
117
118	41158	Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
119	23187	for (const Node& e : d_assumptions)
120		{
121		// Substitute out any abstract values in ex.
122	5216	Node n = d_absValues.substituteAbstractValues(e);
123		// Ensure expr is type-checked at this point.
124	2608	ensureBoolean(n);
125	2608	addFormula(n, true, false, false);
126		}
127	20579	}
128
129	96617	void Assertions::assertFormula(const Node& n)
130		{
131	96617	ensureBoolean(n);
132	96617	bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
133	96617	addFormula(n, false, false, maybeHasFv);
134	96617	}
135
136	16	std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
137	20537	bool Assertions::isGlobalNegated() const { return d_globalNegation; }
138	6	void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
139
140	252508	preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
141		{
142	252508	return d_assertions;
143		}
144
145	15674	const context::CDList<Node>& Assertions::getAssertionList() const
146		{
147	15674	return d_assertionList;
148		}
149
150	1	const context::CDList<Node>& Assertions::getAssertionListDefinitions() const
151		{
152	1	return d_assertionListDefs;
153		}
154
155	106950	void Assertions::addFormula(TNode n,
156		bool isAssumption,
157		bool isFunDef,
158		bool maybeHasFv)
159		{
160		// add to assertion list if it exists
161	106950	if (d_produceAssertions)
162		{
163	73611	d_assertionList.push_back(n);
164	73611	if (isFunDef)
165		{
166	5228	d_assertionListDefs.push_back(n);
167		}
168		}
169	106950	if (n.isConst() && n.getConst<bool>())
170		{
171		// true, nothing to do
172	541	return;
173		}
174	212818	Trace("smt") << "Assertions::addFormula(" << n
175	106409	<< ", isAssumption = " << isAssumption
176	106409	<< ", isFunDef = " << isFunDef << std::endl;
177	106409	if (isFunDef)
178		{
179		// if a non-recursive define-fun, just add as a top-level substitution
180	7725	if (n.getKind() == EQUAL && n[0].isVar())
181		{
182		// A define-fun is an assumption in the overall proof, thus
183		// we justify the substitution with ASSUME here.
184	15076	d_env.getTopLevelSubstitutions().addSubstitution(
185	7538	n[0], n[1], PfRule::ASSUME, {}, {n});
186	7538	return;
187		}
188		}
189
190		// Ensure that it does not contain free variables
191	98871	if (maybeHasFv)
192		{
193	698	if (expr::hasFreeVar(n))
194		{
195		std::stringstream se;
196		if (isFunDef)
197		{
198		se << "Cannot process function definition with free variable.";
199		}
200		else
201		{
202		se << "Cannot process assertion with free variable.";
203		if (language::isLangSygus(options().base.inputLanguage))
204		{
205		// Common misuse of SyGuS is to use top-level assert instead of
206		// constraint when defining the synthesis conjecture.
207		se << " Perhaps you meant `constraint` instead of `assert`?";
208		}
209		}
210		throw ModalException(se.str().c_str());
211		}
212		}
213
214		// Add the normalized formula to the queue
215	98871	d_assertions.push_back(n, isAssumption, true);
216		}
217
218	7679	void Assertions::addDefineFunDefinition(Node n, bool global)
219		{
220	7679	n = d_absValues.substituteAbstractValues(n);
221	7679	if (global && d_globalDefineFunLemmas != nullptr)
222		{
223		// Global definitions are asserted at check-sat-time because we have to
224		// make sure that they are always present
225	33	Assert(!language::isLangSygus(options().base.inputLanguage));
226	33	d_globalDefineFunLemmas->emplace_back(n);
227		}
228		else
229		{
230		// We don't permit functions-to-synthesize within recursive function
231		// definitions currently. Thus, we should check for free variables if the
232		// input language is SyGuS.
233	7646	bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
234	7646	addFormula(n, false, true, maybeHasFv);
235		}
236	7679	}
237
238	99225	void Assertions::ensureBoolean(const Node& n)
239		{
240	198450	TypeNode type = n.getType(options().expr.typeChecking);
241	99225	if (!type.isBoolean())
242		{
243		std::stringstream ss;
244		ss << "Expected Boolean type\n"
245		<< "The assertion : " << n << "\n"
246		<< "Its type : " << type;
247		throw TypeCheckingExceptionPrivate(n, ss.str());
248		}
249	99225	}
250
251	7989	void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
252		{
253	7989	d_assertions.setProofGenerator(pppg);
254	7989	}
255
256		bool Assertions::isProofEnabled() const
257		{
258		return d_assertions.isProofEnabled();
259		}
260
261		} // namespace smt
262	31137	} // namespace cvc5