Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/process_assertions.cpp	Lines:	171	184	92.9 %
Date:	2021-05-22	Branches:	378	766	49.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Aina Niemetz
 *
 * 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 module for processing assertions for an SMT engine.
 */

#include "smt/process_assertions.h"

#include <utility>

#include "expr/node_manager_attributes.h"
#include "options/arith_options.h"
#include "options/base_options.h"
#include "options/bv_options.h"
#include "options/quantifiers_options.h"
#include "options/sep_options.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "options/uf_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_registry.h"
#include "printer/printer.h"
#include "smt/assertions.h"
#include "smt/dump.h"
#include "smt/expand_definitions.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_stats.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"

using namespace std;
using namespace cvc5::preprocessing;
using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

/** Useful for counting the number of recursive calls. */
class ScopeCounter
{
 public:
  ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
  ~ScopeCounter() { --d_depth; }

 private:
  unsigned& d_depth;
};

ProcessAssertions::ProcessAssertions(SmtEngine& smt,
                                     ResourceManager& rm,
                                     SmtEngineStatistics& stats)
    : d_smt(smt),
      d_resourceManager(rm),
      d_smtStats(stats),
      d_preprocessingPassContext(nullptr)
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

ProcessAssertions::~ProcessAssertions()
{
}

void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
{
  Assert(d_preprocessingPassContext == nullptr);
  d_preprocessingPassContext = pc;

  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
  // TODO: this will likely change when we add support for actually assembling
  // preprocessing pipelines. For now, we just create an instance of each
  // available preprocessing pass.
  std::vector<std::string> passNames = ppReg.getAvailablePasses();
  for (const std::string& passName : passNames)
  {
    d_passes[passName].reset(
        ppReg.createPass(d_preprocessingPassContext, passName));
  }
}

void ProcessAssertions::cleanup() { d_passes.clear(); }

void ProcessAssertions::spendResource(Resource r)
{
  d_resourceManager.spendResource(r);
}

bool ProcessAssertions::apply(Assertions& as)
{
  AssertionPipeline& assertions = as.getAssertionPipeline();
  Assert(d_preprocessingPassContext != nullptr);
  // Dump the assertions
  dumpAssertions("pre-everything", assertions);

  Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
  Trace("smt") << "ProcessAssertions::processAssertions()" << endl;

  Debug("smt") << "#Assertions : " << assertions.size() << endl;
  Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;

  if (assertions.size() == 0)
  {
    // nothing to do
    return true;
  }

  if (options::bvGaussElim())
  {
    d_passes["bv-gauss"]->apply(&assertions);
  }

  // Add dummy assertion in last position - to be used as a
  // placeholder for any new assertions to get added
  assertions.push_back(d_true);
  // any assertions added beyond realAssertionsEnd must NOT affect the
  // equisatisfiability
  assertions.updateRealAssertionsEnd();

  // Assertions are NOT guaranteed to be rewritten by this point

  Trace("smt-proc")
      << "ProcessAssertions::processAssertions() : pre-definition-expansion"
      << endl;
  dumpAssertions("pre-definition-expansion", assertions);
  // Apply substitutions first. If we are non-incremental, this has only the
  // effect of replacing defined functions with their definitions.
  // We do not call theory-specific expand definitions here, since we want
  // to give the opportunity to rewrite/preprocess terms before expansion.
  d_passes["apply-substs"]->apply(&assertions);
  Trace("smt-proc")
      << "ProcessAssertions::processAssertions() : post-definition-expansion"
      << endl;
  dumpAssertions("post-definition-expansion", assertions);

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  if (options::globalNegate())
  {
    // global negation of the formula
    d_passes["global-negate"]->apply(&assertions);
    as.flipGlobalNegated();
  }

  if (options::nlExtPurify())
  {
    d_passes["nl-ext-purify"]->apply(&assertions);
  }

  if (options::solveRealAsInt())
  {
    d_passes["real-to-int"]->apply(&assertions);
  }

  if (options::solveIntAsBV() > 0)
  {
    d_passes["int-to-bv"]->apply(&assertions);
  }

  if (options::ackermann())
  {
    d_passes["ackermann"]->apply(&assertions);
  }

  if (options::bvAbstraction())
  {
    d_passes["bv-abstraction"]->apply(&assertions);
  }

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  bool noConflict = true;

  if (options::extRewPrep())
  {
    d_passes["ext-rew-pre"]->apply(&assertions);
  }

  // Unconstrained simplification
  if (options::unconstrainedSimp())
  {
    d_passes["rewrite"]->apply(&assertions);
    d_passes["unconstrained-simplifier"]->apply(&assertions);
  }

  if (options::bvIntroducePow2())
  {
    d_passes["bv-intro-pow2"]->apply(&assertions);
  }

  // Lift bit-vectors of size 1 to bool
  if (options::bitvectorToBool())
  {
    d_passes["bv-to-bool"]->apply(&assertions);
  }
  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
  {
    d_passes["bv-to-int"]->apply(&assertions);
  }
  if (options::foreignTheoryRewrite())
  {
    d_passes["foreign-theory-rewrite"]->apply(&assertions);
  }

  // Since this pass is not robust for the information tracking necessary for
  // unsat cores, it's only applied if we are not doing unsat core computation
  d_passes["apply-substs"]->apply(&assertions);

  // Assertions MUST BE guaranteed to be rewritten by this point
  d_passes["rewrite"]->apply(&assertions);

  // Convert non-top-level Booleans to bit-vectors of size 1
  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
  {
    d_passes["bool-to-bv"]->apply(&assertions);
  }
  if (options::sepPreSkolemEmp())
  {
    d_passes["sep-skolem-emp"]->apply(&assertions);
  }

  if (d_smt.getLogicInfo().isQuantified())
  {
    // remove rewrite rules, apply pre-skolemization to existential quantifiers
    d_passes["quantifiers-preprocess"]->apply(&assertions);

    // fmf-fun : assume admissible functions, applying preprocessing reduction
    // to FMF
    if (options::fmfFunWellDefined())
    {
      d_passes["fun-def-fmf"]->apply(&assertions);
    }
  }
  if (!options::stringLazyPreproc())
  {
    d_passes["strings-eager-pp"]->apply(&assertions);
  }
  if (options::sortInference() || options::ufssFairnessMonotone())
  {
    d_passes["sort-inference"]->apply(&assertions);
  }

  if (options::pbRewrites())
  {
    d_passes["pseudo-boolean-processor"]->apply(&assertions);
  }

  // rephrasing normal inputs as sygus problems
  if (!d_smt.isInternalSubsolver())
  {
    if (options::sygusInference())
    {
      d_passes["sygus-infer"]->apply(&assertions);
    }
    else if (options::sygusRewSynthInput())
    {
      // do candidate rewrite rule synthesis
      d_passes["synth-rr"]->apply(&assertions);
    }
  }

  Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
                    << endl;
  dumpAssertions("pre-simplify", assertions);
  Chat() << "simplifying assertions..." << endl;
  noConflict = simplifyAssertions(assertions);
  if (!noConflict)
  {
    ++(d_smtStats.d_simplifiedToFalse);
  }
  Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
                    << endl;
  dumpAssertions("post-simplify", assertions);

  if (options::doStaticLearning())
  {
    d_passes["static-learning"]->apply(&assertions);
  }
  Debug("smt") << " assertions     : " << assertions.size() << endl;

  if (options::earlyIteRemoval())
  {
    d_smtStats.d_numAssertionsPre += assertions.size();
    d_passes["ite-removal"]->apply(&assertions);
    // This is needed because when solving incrementally, removeITEs may
    // introduce skolems that were solved for earlier and thus appear in the
    // substitution map.
    d_passes["apply-substs"]->apply(&assertions);
    d_smtStats.d_numAssertionsPost += assertions.size();
  }

  dumpAssertions("pre-repeat-simplify", assertions);
  if (options::repeatSimp())
  {
    Trace("smt-proc")
        << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
        << endl;
    Chat() << "re-simplifying assertions..." << endl;
    ScopeCounter depth(d_simplifyAssertionsDepth);
    noConflict &= simplifyAssertions(assertions);
    Trace("smt-proc")
        << "ProcessAssertions::processAssertions() : post-repeat-simplify"
        << endl;
  }
  dumpAssertions("post-repeat-simplify", assertions);

  if (options::ufHo())
  {
    d_passes["ho-elim"]->apply(&assertions);
  }

  // begin: INVARIANT to maintain: no reordering of assertions or
  // introducing new ones

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
               << endl;
  Debug("smt") << " assertions     : " << assertions.size() << endl;

  // ensure rewritten
  d_passes["rewrite"]->apply(&assertions);
  // rewrite equalities based on theory-specific rewriting
  d_passes["theory-rewrite-eq"]->apply(&assertions);
  // apply theory preprocess, which includes ITE removal
  d_passes["theory-preprocess"]->apply(&assertions);
  // notice that we do not apply substitutions as a last step here, since
  // the range of substitutions is not theory-preprocessed.

  if (options::bitblastMode() == options::BitblastMode::EAGER)
  {
    d_passes["bv-eager-atoms"]->apply(&assertions);
  }

  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
  dumpAssertions("post-everything", assertions);

  return noConflict;
}

// returns false if simplification led to "false"
bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
{
  spendResource(Resource::PreprocessStep);
  try
  {
    ScopeCounter depth(d_simplifyAssertionsDepth);

    Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;

    if (options::simplificationMode() != options::SimplificationMode::NONE)
    {
      // Perform non-clausal simplification
      PreprocessingPassResult res =
          d_passes["non-clausal-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        return false;
      }

      // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
      // do the miplib trick.
      if (  // check that option is on
          options::arithMLTrick() &&
          // only useful in arith
          d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
          // we add new assertions and need this (in practice, this
          // restriction only disables miplib processing during
          // re-simplification, which we don't expect to be useful anyway)
          assertions.getRealAssertionsEnd() == assertions.size())
      {
        d_passes["miplib-trick"]->apply(&assertions);
      }
      else
      {
        Trace("simplify") << "SmtEnginePrivate::simplify(): "
                          << "skipping miplib pseudobooleans pass..." << endl;
      }
    }

    Debug("smt") << " assertions     : " << assertions.size() << endl;

    // ITE simplification
    if (options::doITESimp()
        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
    {
      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        Chat() << "...ITE simplification found unsat..." << endl;
        return false;
      }
    }

    Debug("smt") << " assertions     : " << assertions.size() << endl;

    // Unconstrained simplification
    if (options::unconstrainedSimp())
    {
      d_passes["unconstrained-simplifier"]->apply(&assertions);
    }

    if (options::repeatSimp()
        && options::simplificationMode() != options::SimplificationMode::NONE)
    {
      PreprocessingPassResult res =
          d_passes["non-clausal-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        return false;
      }
    }

    dumpAssertions("post-repeatsimp", assertions);
    Trace("smt") << "POST repeatSimp" << endl;
    Debug("smt") << " assertions     : " << assertions.size() << endl;
  }
  catch (TypeCheckingExceptionPrivate& tcep)
  {
    // Calls to this function should have already weeded out any
    // typechecking exceptions via (e.g.) ensureBoolean().  But a
    // theory could still create a new expression that isn't
    // well-typed, and we don't want the C++ runtime to abort our
    // process without any error notice.
    InternalError()
        << "A bad expression was produced.  Original exception follows:\n"
        << tcep;
  }
  return true;
}

void ProcessAssertions::dumpAssertions(const char* key,
                                       const AssertionPipeline& assertionList)
{
  if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
  {
    // Push the simplified assertions to the dump output stream
    for (unsigned i = 0; i < assertionList.size(); ++i)
    {
      TNode n = assertionList[i];
      d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
          d_smt.getOutputManager().getDumpOut(), n);
    }
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Aina Niemetz
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 module for processing assertions for an SMT engine.
14		*/
15
16		#include "smt/process_assertions.h"
17
18		#include <utility>
19
20		#include "expr/node_manager_attributes.h"
21		#include "options/arith_options.h"
22		#include "options/base_options.h"
23		#include "options/bv_options.h"
24		#include "options/quantifiers_options.h"
25		#include "options/sep_options.h"
26		#include "options/smt_options.h"
27		#include "options/strings_options.h"
28		#include "options/uf_options.h"
29		#include "preprocessing/assertion_pipeline.h"
30		#include "preprocessing/preprocessing_pass.h"
31		#include "preprocessing/preprocessing_pass_registry.h"
32		#include "printer/printer.h"
33		#include "smt/assertions.h"
34		#include "smt/dump.h"
35		#include "smt/expand_definitions.h"
36		#include "smt/smt_engine.h"
37		#include "smt/smt_engine_stats.h"
38		#include "theory/logic_info.h"
39		#include "theory/theory_engine.h"
40
41		using namespace std;
42		using namespace cvc5::preprocessing;
43		using namespace cvc5::theory;
44		using namespace cvc5::kind;
45
46		namespace cvc5 {
47		namespace smt {
48
49		/** Useful for counting the number of recursive calls. */
50		class ScopeCounter
51		{
52		public:
53	13371	ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
54	13371	~ScopeCounter() { --d_depth; }
55
56		private:
57		unsigned& d_depth;
58		};
59
60	10092	ProcessAssertions::ProcessAssertions(SmtEngine& smt,
61		ResourceManager& rm,
62	10092	SmtEngineStatistics& stats)
63		: d_smt(smt),
64		d_resourceManager(rm),
65		d_smtStats(stats),
66	10092	d_preprocessingPassContext(nullptr)
67		{
68	10092	d_true = NodeManager::currentNM()->mkConst(true);
69	10092	}
70
71	10092	ProcessAssertions::~ProcessAssertions()
72		{
73	10092	}
74
75	9459	void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
76		{
77	9459	Assert(d_preprocessingPassContext == nullptr);
78	9459	d_preprocessingPassContext = pc;
79
80	9459	PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
81		// TODO: this will likely change when we add support for actually assembling
82		// preprocessing pipelines. For now, we just create an instance of each
83		// available preprocessing pass.
84	18918	std::vector<std::string> passNames = ppReg.getAvailablePasses();
85	321606	for (const std::string& passName : passNames)
86		{
87	312147	d_passes[passName].reset(
88		ppReg.createPass(d_preprocessingPassContext, passName));
89		}
90	9459	}
91
92	10092	void ProcessAssertions::cleanup() { d_passes.clear(); }
93
94	13126	void ProcessAssertions::spendResource(Resource r)
95		{
96	13126	d_resourceManager.spendResource(r);
97	13126	}
98
99	12883	bool ProcessAssertions::apply(Assertions& as)
100		{
101	12883	AssertionPipeline& assertions = as.getAssertionPipeline();
102	12883	Assert(d_preprocessingPassContext != nullptr);
103		// Dump the assertions
104	12883	dumpAssertions("pre-everything", assertions);
105
106	12883	Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
107	12883	Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
108
109	12883	Debug("smt") << "#Assertions : " << assertions.size() << endl;
110	12883	Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
111
112	12883	if (assertions.size() == 0)
113		{
114		// nothing to do
115		return true;
116		}
117
118	25766	if (options::bvGaussElim())
119		{
120		d_passes["bv-gauss"]->apply(&assertions);
121		}
122
123		// Add dummy assertion in last position - to be used as a
124		// placeholder for any new assertions to get added
125	12883	assertions.push_back(d_true);
126		// any assertions added beyond realAssertionsEnd must NOT affect the
127		// equisatisfiability
128	12883	assertions.updateRealAssertionsEnd();
129
130		// Assertions are NOT guaranteed to be rewritten by this point
131
132	25766	Trace("smt-proc")
133	12883	<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
134	12883	<< endl;
135	12883	dumpAssertions("pre-definition-expansion", assertions);
136		// Apply substitutions first. If we are non-incremental, this has only the
137		// effect of replacing defined functions with their definitions.
138		// We do not call theory-specific expand definitions here, since we want
139		// to give the opportunity to rewrite/preprocess terms before expansion.
140	12885	d_passes["apply-substs"]->apply(&assertions);
141	25762	Trace("smt-proc")
142	12881	<< "ProcessAssertions::processAssertions() : post-definition-expansion"
143	12881	<< endl;
144	12881	dumpAssertions("post-definition-expansion", assertions);
145
146	12881	Debug("smt") << " assertions : " << assertions.size() << endl;
147
148	53402	if (options::globalNegate())
149		{
150		// global negation of the formula
151	6	d_passes["global-negate"]->apply(&assertions);
152	6	as.flipGlobalNegated();
153		}
154
155	25766	if (options::nlExtPurify())
156		{
157	6	d_passes["nl-ext-purify"]->apply(&assertions);
158		}
159
160	40065	if (options::solveRealAsInt())
161		{
162	13	d_passes["real-to-int"]->apply(&assertions);
163		}
164
165	12881	if (options::solveIntAsBV() > 0)
166		{
167	8	d_passes["int-to-bv"]->apply(&assertions);
168		}
169
170	44749	if (options::ackermann())
171		{
172	64	d_passes["ackermann"]->apply(&assertions);
173		}
174
175	2003626	if (options::bvAbstraction())
176		{
177	4	d_passes["bv-abstraction"]->apply(&assertions);
178		}
179
180	12881	Debug("smt") << " assertions : " << assertions.size() << endl;
181
182	12881	bool noConflict = true;
183
184	25781	if (options::extRewPrep())
185		{
186	24	d_passes["ext-rew-pre"]->apply(&assertions);
187		}
188
189		// Unconstrained simplification
190	62397	if (options::unconstrainedSimp())
191		{
192	182	d_passes["rewrite"]->apply(&assertions);
193	182	d_passes["unconstrained-simplifier"]->apply(&assertions);
194		}
195
196	28178	if (options::bvIntroducePow2())
197		{
198	2	d_passes["bv-intro-pow2"]->apply(&assertions);
199		}
200
201		// Lift bit-vectors of size 1 to bool
202	28483	if (options::bitvectorToBool())
203		{
204	155	d_passes["bv-to-bool"]->apply(&assertions);
205		}
206	12881	if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
207		{
208	187	d_passes["bv-to-int"]->apply(&assertions);
209		}
210	25764	if (options::foreignTheoryRewrite())
211		{
212	2	d_passes["foreign-theory-rewrite"]->apply(&assertions);
213		}
214
215		// Since this pass is not robust for the information tracking necessary for
216		// unsat cores, it's only applied if we are not doing unsat core computation
217	12881	d_passes["apply-substs"]->apply(&assertions);
218
219		// Assertions MUST BE guaranteed to be rewritten by this point
220	12881	d_passes["rewrite"]->apply(&assertions);
221
222		// Convert non-top-level Booleans to bit-vectors of size 1
223	12881	if (options::boolToBitvector() != options::BoolToBVMode::OFF)
224		{
225	12	d_passes["bool-to-bv"]->apply(&assertions);
226		}
227	25763	if (options::sepPreSkolemEmp())
228		{
229	1	d_passes["sep-skolem-emp"]->apply(&assertions);
230		}
231
232	12881	if (d_smt.getLogicInfo().isQuantified())
233		{
234		// remove rewrite rules, apply pre-skolemization to existential quantifiers
235	7321	d_passes["quantifiers-preprocess"]->apply(&assertions);
236
237		// fmf-fun : assume admissible functions, applying preprocessing reduction
238		// to FMF
239	24172	if (options::fmfFunWellDefined())
240		{
241	117	d_passes["fun-def-fmf"]->apply(&assertions);
242		}
243		}
244	34225	if (!options::stringLazyPreproc())
245		{
246	36	d_passes["strings-eager-pp"]->apply(&assertions);
247		}
248	12881	if (options::sortInference() \|\| options::ufssFairnessMonotone())
249		{
250	24	d_passes["sort-inference"]->apply(&assertions);
251		}
252
253	28178	if (options::pbRewrites())
254		{
255	2	d_passes["pseudo-boolean-processor"]->apply(&assertions);
256		}
257
258		// rephrasing normal inputs as sygus problems
259	12881	if (!d_smt.isInternalSubsolver())
260		{
261	29551	if (options::sygusInference())
262		{
263	58	d_passes["sygus-infer"]->apply(&assertions);
264		}
265	27516	else if (options::sygusRewSynthInput())
266		{
267		// do candidate rewrite rule synthesis
268		d_passes["synth-rr"]->apply(&assertions);
269		}
270		}
271
272	25762	Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
273	12881	<< endl;
274	12881	dumpAssertions("pre-simplify", assertions);
275	12881	Chat() << "simplifying assertions..." << endl;
276	12881	noConflict = simplifyAssertions(assertions);
277	12881	if (!noConflict)
278		{
279	1045	++(d_smtStats.d_simplifiedToFalse);
280		}
281	25762	Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
282	12881	<< endl;
283	12881	dumpAssertions("post-simplify", assertions);
284
285	25762	if (options::doStaticLearning())
286		{
287	12881	d_passes["static-learning"]->apply(&assertions);
288		}
289	12881	Debug("smt") << " assertions : " << assertions.size() << endl;
290
291	25768	if (options::earlyIteRemoval())
292		{
293	2	d_smtStats.d_numAssertionsPre += assertions.size();
294	2	d_passes["ite-removal"]->apply(&assertions);
295		// This is needed because when solving incrementally, removeITEs may
296		// introduce skolems that were solved for earlier and thus appear in the
297		// substitution map.
298	2	d_passes["apply-substs"]->apply(&assertions);
299	2	d_smtStats.d_numAssertionsPost += assertions.size();
300		}
301
302	12881	dumpAssertions("pre-repeat-simplify", assertions);
303	59170	if (options::repeatSimp())
304		{
305	490	Trace("smt-proc")
306	245	<< "ProcessAssertions::processAssertions() : pre-repeat-simplify"
307	245	<< endl;
308	245	Chat() << "re-simplifying assertions..." << endl;
309	490	ScopeCounter depth(d_simplifyAssertionsDepth);
310	245	noConflict &= simplifyAssertions(assertions);
311	490	Trace("smt-proc")
312	245	<< "ProcessAssertions::processAssertions() : post-repeat-simplify"
313	245	<< endl;
314		}
315	12881	dumpAssertions("post-repeat-simplify", assertions);
316
317	12881	if (options::ufHo())
318		{
319	198	d_passes["ho-elim"]->apply(&assertions);
320		}
321
322		// begin: INVARIANT to maintain: no reordering of assertions or
323		// introducing new ones
324
325	12881	Debug("smt") << " assertions : " << assertions.size() << endl;
326
327	25762	Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
328	12881	<< endl;
329	12881	Debug("smt") << " assertions : " << assertions.size() << endl;
330
331		// ensure rewritten
332	12881	d_passes["rewrite"]->apply(&assertions);
333		// rewrite equalities based on theory-specific rewriting
334	12881	d_passes["theory-rewrite-eq"]->apply(&assertions);
335		// apply theory preprocess, which includes ITE removal
336	12888	d_passes["theory-preprocess"]->apply(&assertions);
337		// notice that we do not apply substitutions as a last step here, since
338		// the range of substitutions is not theory-preprocessed.
339
340	12874	if (options::bitblastMode() == options::BitblastMode::EAGER)
341		{
342	56	d_passes["bv-eager-atoms"]->apply(&assertions);
343		}
344
345	12874	Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
346	12874	dumpAssertions("post-everything", assertions);
347
348	12874	return noConflict;
349		}
350
351		// returns false if simplification led to "false"
352	13126	bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
353		{
354	13126	spendResource(Resource::PreprocessStep);
355		try
356		{
357	25198	ScopeCounter depth(d_simplifyAssertionsDepth);
358
359	13126	Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
360
361	45445	if (options::simplificationMode() != options::SimplificationMode::NONE)
362		{
363		// Perform non-clausal simplification
364		PreprocessingPassResult res =
365	9815	d_passes["non-clausal-simp"]->apply(&assertions);
366	9815	if (res == PreprocessingPassResult::CONFLICT)
367		{
368	1050	return false;
369		}
370
371		// We piggy-back off of the BackEdgesMap in the CircuitPropagator to
372		// do the miplib trick.
373	8765	if ( // check that option is on
374	29053	options::arithMLTrick() &&
375		// only useful in arith
376	8773	d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
377		// we add new assertions and need this (in practice, this
378		// restriction only disables miplib processing during
379		// re-simplification, which we don't expect to be useful anyway)
380	8	assertions.getRealAssertionsEnd() == assertions.size())
381		{
382	8	d_passes["miplib-trick"]->apply(&assertions);
383		}
384		else
385		{
386	17514	Trace("simplify") << "SmtEnginePrivate::simplify(): "
387	8757	<< "skipping miplib pseudobooleans pass..." << endl;
388		}
389		}
390
391	12076	Debug("smt") << " assertions : " << assertions.size() << endl;
392
393		// ITE simplification
394	48105	if (options::doITESimp()
395	12076	&& (d_simplifyAssertionsDepth <= 1 \|\| options::doITESimpOnRepeat()))
396		{
397	2	PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
398	2	if (res == PreprocessingPassResult::CONFLICT)
399		{
400		Chat() << "...ITE simplification found unsat..." << endl;
401		return false;
402		}
403		}
404
405	12076	Debug("smt") << " assertions : " << assertions.size() << endl;
406
407		// Unconstrained simplification
408	12076	if (options::unconstrainedSimp())
409		{
410	333	d_passes["unconstrained-simplifier"]->apply(&assertions);
411		}
412
413	24152	if (options::repeatSimp()
414	12076	&& options::simplificationMode() != options::SimplificationMode::NONE)
415		{
416		PreprocessingPassResult res =
417	462	d_passes["non-clausal-simp"]->apply(&assertions);
418	462	if (res == PreprocessingPassResult::CONFLICT)
419		{
420	4	return false;
421		}
422		}
423
424	12072	dumpAssertions("post-repeatsimp", assertions);
425	12072	Trace("smt") << "POST repeatSimp" << endl;
426	12072	Debug("smt") << " assertions : " << assertions.size() << endl;
427		}
428		catch (TypeCheckingExceptionPrivate& tcep)
429		{
430		// Calls to this function should have already weeded out any
431		// typechecking exceptions via (e.g.) ensureBoolean(). But a
432		// theory could still create a new expression that isn't
433		// well-typed, and we don't want the C++ runtime to abort our
434		// process without any error notice.
435		InternalError()
436		<< "A bad expression was produced. Original exception follows:\n"
437		<< tcep;
438		}
439	12072	return true;
440		}
441
442	115117	void ProcessAssertions::dumpAssertions(const char* key,
443		const AssertionPipeline& assertionList)
444		{
445	115117	if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
446		{
447		// Push the simplified assertions to the dump output stream
448		for (unsigned i = 0; i < assertionList.size(); ++i)
449		{
450		TNode n = assertionList[i];
451		d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
452		d_smt.getOutputManager().getDumpOut(), n);
453		}
454		}
455	115117	}
456
457		} // namespace smt
458	2502813	} // namespace cvc5