Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/process_assertions.cpp	Lines:	195	210	92.9 %
Date:	2021-11-07	Branches:	362	688	52.6 %


/******************************************************************************
 * 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_registry.h"
#include "printer/printer.h"
#include "smt/assertions.h"
#include "smt/expand_definitions.h"
#include "smt/print_benchmark.h"
#include "smt/solver_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(Env& env, SolverEngineStatistics& stats)
    : EnvObj(env), d_slvStats(stats), d_preprocessingPassContext(nullptr)
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

ProcessAssertions::~ProcessAssertions()
{
}

void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
{
  // note that we may be replacing a stale preprocessing pass context here
  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)
{
  resourceManager()->spendResource(r);
}

bool ProcessAssertions::apply(Assertions& as)
{
  // must first refresh the assertions, in the case global declarations is true
  as.refresh();
  AssertionPipeline& assertions = as.getAssertionPipeline();
  Assert(d_preprocessingPassContext != nullptr);
  // Dump the assertions
  dumpAssertions("assertions::pre-everything", as);
  Trace("assertions::pre-everything") << std::endl;

  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().bv.bvGaussElim)
  {
    applyPass("bv-gauss", as);
  }

  // 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;
  // 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.
  applyPass("apply-substs", as);
  Trace("smt-proc")
      << "ProcessAssertions::processAssertions() : post-definition-expansion"
      << endl;

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

  if (options().quantifiers.globalNegate)
  {
    // global negation of the formula
    applyPass("global-negate", as);
    as.flipGlobalNegated();
  }

  if (options().arith.nlExtPurify)
  {
    applyPass("nl-ext-purify", as);
  }

  if (options().smt.solveRealAsInt)
  {
    applyPass("real-to-int", as);
  }

  if (options().smt.solveIntAsBV > 0)
  {
    applyPass("int-to-bv", as);
  }

  if (options().smt.ackermann)
  {
    applyPass("ackermann", as);
  }

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

  bool noConflict = true;

  if (options().smt.extRewPrep)
  {
    applyPass("ext-rew-pre", as);
  }

  // Unconstrained simplification
  if (options().smt.unconstrainedSimp)
  {
    applyPass("rewrite", as);
    applyPass("unconstrained-simplifier", as);
  }

  if (options().bv.bvIntroducePow2)
  {
    applyPass("bv-intro-pow2", as);
  }

  // Lift bit-vectors of size 1 to bool
  if (options().bv.bitvectorToBool)
  {
    applyPass("bv-to-bool", as);
  }
  if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
  {
    applyPass("bv-to-int", as);
  }
  if (options().smt.foreignTheoryRewrite)
  {
    applyPass("foreign-theory-rewrite", as);
  }

  // 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
  applyPass("apply-substs", as);

  // Assertions MUST BE guaranteed to be rewritten by this point
  applyPass("rewrite", as);

  // Convert non-top-level Booleans to bit-vectors of size 1
  if (options().bv.boolToBitvector != options::BoolToBVMode::OFF)
  {
    applyPass("bool-to-bv", as);
  }
  if (options().sep.sepPreSkolemEmp)
  {
    applyPass("sep-skolem-emp", as);
  }

  if (logicInfo().isQuantified())
  {
    // remove rewrite rules, apply pre-skolemization to existential quantifiers
    applyPass("quantifiers-preprocess", as);

    // fmf-fun : assume admissible functions, applying preprocessing reduction
    // to FMF
    if (options().quantifiers.fmfFunWellDefined)
    {
      applyPass("fun-def-fmf", as);
    }
  }
  if (!options().strings.stringLazyPreproc)
  {
    applyPass("strings-eager-pp", as);
  }
  if (options().smt.sortInference || options().uf.ufssFairnessMonotone)
  {
    applyPass("sort-inference", as);
  }

  if (options().arith.pbRewrites)
  {
    applyPass("pseudo-boolean-processor", as);
  }

  // rephrasing normal inputs as sygus problems
  if (options().quantifiers.sygusInference)
  {
    applyPass("sygus-infer", as);
  }
  else if (options().quantifiers.sygusRewSynthInput)
  {
    // do candidate rewrite rule synthesis
    applyPass("synth-rr", as);
  }

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

  if (options().smt.doStaticLearning)
  {
    applyPass("static-learning", as);
  }
  Debug("smt") << " assertions     : " << assertions.size() << endl;

  if (options().smt.learnedRewrite)
  {
    applyPass("learned-rewrite", as);
  }

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

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

  if (logicInfo().isHigherOrder())
  {
    applyPass("ho-elim", as);
  }

  // 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
  applyPass("rewrite", as);
  // rewrite equalities based on theory-specific rewriting
  applyPass("theory-rewrite-eq", as);
  // apply theory preprocess, which includes ITE removal
  applyPass("theory-preprocess", as);
  // notice that we do not apply substitutions as a last step here, since
  // the range of substitutions is not theory-preprocessed.

  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
  {
    applyPass("bv-eager-atoms", as);
  }

  Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
  dumpAssertions("assertions::post-everything", as);
  Trace("assertions::post-everything") << std::endl;

  return noConflict;
}

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

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

    if (options().smt.simplificationMode != options::SimplificationMode::NONE)
    {
      // Perform non-clausal simplification
      PreprocessingPassResult res = applyPass("non-clausal-simp", as);
      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().arith.arithMLTrick &&
          // only useful in arith
          logicInfo().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())
      {
        applyPass("miplib-trick", as);
      }
      else
      {
        Trace("simplify") << "ProcessAssertions::simplify(): "
                          << "skipping miplib pseudobooleans pass..." << endl;
      }
    }

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

    // ITE simplification
    if (options().smt.doITESimp
        && (d_simplifyAssertionsDepth <= 1 || options().smt.doITESimpOnRepeat))
    {
      PreprocessingPassResult res = applyPass("ite-simp", as);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        verbose(2) << "...ITE simplification found unsat..." << std::endl;
        return false;
      }
    }

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

    // Unconstrained simplification
    if (options().smt.unconstrainedSimp)
    {
      applyPass("unconstrained-simplifier", as);
    }

    if (options().smt.repeatSimp
        && options().smt.simplificationMode
               != options::SimplificationMode::NONE)
    {
      PreprocessingPassResult res = applyPass("non-clausal-simp", as);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        return false;
      }
    }

    dumpAssertions("post-repeatsimp", as);
    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 std::string& key, Assertions& as)
{
  bool isTraceOn = Trace.isOn(key);
  if (!isTraceOn)
  {
    return;
  }
  // Cannot print unless produce assertions is enabled. Otherwise, the printing
  // is misleading, since it does not capture what symbols were provided
  // as definitions.
  if (!options().smt.produceAssertions)
  {
    warning()
        << "Assertions not available for dumping (use --produce-assertions)."
        << std::endl;
    return;
  }
  PrintBenchmark pb(&d_env.getPrinter());
  std::vector<Node> assertions;
  // Notice that the following list covers define-fun and define-fun-rec
  // from input. The former does not impact the assertions since define-fun are
  // added as top-level substitutions. The latter do get added to the list
  // of assertions. Since we are interested in printing the result of
  // preprocessed quantified formulas corresponding to recursive function
  // definitions and not the original definitions, we discard the latter
  // in the loop below.
  //
  // In summary, this means that define-fun-rec are expanded to
  // (declare-fun ...) + (assert (forall ...)) in the printing below, whereas
  // define-fun are preserved.
  const context::CDList<Node>& asld = as.getAssertionListDefinitions();
  std::vector<Node> defs;
  for (const Node& d : asld)
  {
    if (d.getKind() != FORALL)
    {
      defs.push_back(d);
    }
  }
  AssertionPipeline& ap = as.getAssertionPipeline();
  for (size_t i = 0, size = ap.size(); i < size; i++)
  {
    assertions.push_back(ap[i]);
  }
  std::stringstream ss;
  pb.printBenchmark(ss, logicInfo().getLogicString(), defs, assertions);
  Trace(key) << ";;; " << key << " start" << std::endl;
  Trace(key) << ss.str();
  Trace(key) << ";;; " << key << " end " << std::endl;
}

PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname,
                                                     Assertions& as)
{
  dumpAssertions("assertions::pre-" + pname, as);
  AssertionPipeline& assertions = as.getAssertionPipeline();
  PreprocessingPassResult res = d_passes[pname]->apply(&assertions);
  dumpAssertions("assertions::post-" + pname, as);
  return res;
}

}  // 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_registry.h"
31		#include "printer/printer.h"
32		#include "smt/assertions.h"
33		#include "smt/expand_definitions.h"
34		#include "smt/print_benchmark.h"
35		#include "smt/solver_engine_stats.h"
36		#include "theory/logic_info.h"
37		#include "theory/theory_engine.h"
38
39		using namespace std;
40		using namespace cvc5::preprocessing;
41		using namespace cvc5::theory;
42		using namespace cvc5::kind;
43
44		namespace cvc5 {
45		namespace smt {
46
47		/** Useful for counting the number of recursive calls. */
48		class ScopeCounter
49		{
50		public:
51	19609	ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
52	19609	~ScopeCounter() { --d_depth; }
53
54		private:
55		unsigned& d_depth;
56		};
57
58	18633	ProcessAssertions::ProcessAssertions(Env& env, SolverEngineStatistics& stats)
59	18633	: EnvObj(env), d_slvStats(stats), d_preprocessingPassContext(nullptr)
60		{
61	18633	d_true = NodeManager::currentNM()->mkConst(true);
62	18633	}
63
64	15884	ProcessAssertions::~ProcessAssertions()
65		{
66	15884	}
67
68	15340	void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
69		{
70		// note that we may be replacing a stale preprocessing pass context here
71	15340	d_preprocessingPassContext = pc;
72
73	15340	PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
74		// TODO: this will likely change when we add support for actually assembling
75		// preprocessing pipelines. For now, we just create an instance of each
76		// available preprocessing pass.
77	30680	std::vector<std::string> passNames = ppReg.getAvailablePasses();
78	521560	for (const std::string& passName : passNames)
79		{
80	506220	d_passes[passName].reset(
81		ppReg.createPass(d_preprocessingPassContext, passName));
82		}
83	15340	}
84
85	15884	void ProcessAssertions::cleanup() { d_passes.clear(); }
86
87	19358	void ProcessAssertions::spendResource(Resource r)
88		{
89	19358	resourceManager()->spendResource(r);
90	19358	}
91
92	19110	bool ProcessAssertions::apply(Assertions& as)
93		{
94		// must first refresh the assertions, in the case global declarations is true
95	19110	as.refresh();
96	19110	AssertionPipeline& assertions = as.getAssertionPipeline();
97	19110	Assert(d_preprocessingPassContext != nullptr);
98		// Dump the assertions
99	19110	dumpAssertions("assertions::pre-everything", as);
100	19110	Trace("assertions::pre-everything") << std::endl;
101
102	19110	Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
103	19110	Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
104
105	19110	Debug("smt") << "#Assertions : " << assertions.size() << endl;
106	19110	Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
107
108	19110	if (assertions.size() == 0)
109		{
110		// nothing to do
111		return true;
112		}
113
114	19110	if (options().bv.bvGaussElim)
115		{
116		applyPass("bv-gauss", as);
117		}
118
119		// Add dummy assertion in last position - to be used as a
120		// placeholder for any new assertions to get added
121	19110	assertions.push_back(d_true);
122		// any assertions added beyond realAssertionsEnd must NOT affect the
123		// equisatisfiability
124	19110	assertions.updateRealAssertionsEnd();
125
126		// Assertions are NOT guaranteed to be rewritten by this point
127
128	38220	Trace("smt-proc")
129	19110	<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
130	19110	<< endl;
131		// Apply substitutions first. If we are non-incremental, this has only the
132		// effect of replacing defined functions with their definitions.
133		// We do not call theory-specific expand definitions here, since we want
134		// to give the opportunity to rewrite/preprocess terms before expansion.
135	19112	applyPass("apply-substs", as);
136	38216	Trace("smt-proc")
137	19108	<< "ProcessAssertions::processAssertions() : post-definition-expansion"
138	19108	<< endl;
139
140	19108	Debug("smt") << " assertions : " << assertions.size() << endl;
141
142	19108	if (options().quantifiers.globalNegate)
143		{
144		// global negation of the formula
145	6	applyPass("global-negate", as);
146	6	as.flipGlobalNegated();
147		}
148
149	19108	if (options().arith.nlExtPurify)
150		{
151	6	applyPass("nl-ext-purify", as);
152		}
153
154	19108	if (options().smt.solveRealAsInt)
155		{
156	13	applyPass("real-to-int", as);
157		}
158
159	19108	if (options().smt.solveIntAsBV > 0)
160		{
161	18	applyPass("int-to-bv", as);
162		}
163
164	19107	if (options().smt.ackermann)
165		{
166	68	applyPass("ackermann", as);
167		}
168
169	19107	Debug("smt") << " assertions : " << assertions.size() << endl;
170
171	19107	bool noConflict = true;
172
173	19107	if (options().smt.extRewPrep)
174		{
175	24	applyPass("ext-rew-pre", as);
176		}
177
178		// Unconstrained simplification
179	19107	if (options().smt.unconstrainedSimp)
180		{
181	182	applyPass("rewrite", as);
182	182	applyPass("unconstrained-simplifier", as);
183		}
184
185	19107	if (options().bv.bvIntroducePow2)
186		{
187	2	applyPass("bv-intro-pow2", as);
188		}
189
190		// Lift bit-vectors of size 1 to bool
191	19107	if (options().bv.bitvectorToBool)
192		{
193	139	applyPass("bv-to-bool", as);
194		}
195	19107	if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
196		{
197	193	applyPass("bv-to-int", as);
198		}
199	19107	if (options().smt.foreignTheoryRewrite)
200		{
201	2	applyPass("foreign-theory-rewrite", as);
202		}
203
204		// Since this pass is not robust for the information tracking necessary for
205		// unsat cores, it's only applied if we are not doing unsat core computation
206	19107	applyPass("apply-substs", as);
207
208		// Assertions MUST BE guaranteed to be rewritten by this point
209	19107	applyPass("rewrite", as);
210
211		// Convert non-top-level Booleans to bit-vectors of size 1
212	19107	if (options().bv.boolToBitvector != options::BoolToBVMode::OFF)
213		{
214	12	applyPass("bool-to-bv", as);
215		}
216	19107	if (options().sep.sepPreSkolemEmp)
217		{
218	1	applyPass("sep-skolem-emp", as);
219		}
220
221	19107	if (logicInfo().isQuantified())
222		{
223		// remove rewrite rules, apply pre-skolemization to existential quantifiers
224	13439	applyPass("quantifiers-preprocess", as);
225
226		// fmf-fun : assume admissible functions, applying preprocessing reduction
227		// to FMF
228	13439	if (options().quantifiers.fmfFunWellDefined)
229		{
230	123	applyPass("fun-def-fmf", as);
231		}
232		}
233	19107	if (!options().strings.stringLazyPreproc)
234		{
235	42	applyPass("strings-eager-pp", as);
236		}
237	19107	if (options().smt.sortInference \|\| options().uf.ufssFairnessMonotone)
238		{
239	24	applyPass("sort-inference", as);
240		}
241
242	19107	if (options().arith.pbRewrites)
243		{
244	2	applyPass("pseudo-boolean-processor", as);
245		}
246
247		// rephrasing normal inputs as sygus problems
248	19107	if (options().quantifiers.sygusInference)
249		{
250	57	applyPass("sygus-infer", as);
251		}
252	19050	else if (options().quantifiers.sygusRewSynthInput)
253		{
254		// do candidate rewrite rule synthesis
255		applyPass("synth-rr", as);
256		}
257
258	38214	Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
259	19107	<< endl;
260	19107	dumpAssertions("assertions::pre-simplify", as);
261	19107	Trace("assertions::pre-simplify") << std::endl;
262	19107	verbose(2) << "simplifying assertions..." << std::endl;
263	19107	noConflict = simplifyAssertions(as);
264	19107	if (!noConflict)
265		{
266	2814	++(d_slvStats.d_simplifiedToFalse);
267		}
268	38214	Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
269	19107	<< endl;
270	19107	dumpAssertions("assertions::post-simplify", as);
271	19107	Trace("assertions::post-simplify") << std::endl;
272
273	19107	if (options().smt.doStaticLearning)
274		{
275	19107	applyPass("static-learning", as);
276		}
277	19107	Debug("smt") << " assertions : " << assertions.size() << endl;
278
279	19107	if (options().smt.learnedRewrite)
280		{
281	2	applyPass("learned-rewrite", as);
282		}
283
284	19107	if (options().smt.earlyIteRemoval)
285		{
286	1	d_slvStats.d_numAssertionsPre += assertions.size();
287	1	applyPass("ite-removal", as);
288		// This is needed because when solving incrementally, removeITEs may
289		// introduce skolems that were solved for earlier and thus appear in the
290		// substitution map.
291	1	applyPass("apply-substs", as);
292	1	d_slvStats.d_numAssertionsPost += assertions.size();
293		}
294
295	19107	dumpAssertions("assertions::pre-repeat-simplify", as);
296	19107	Trace("assertions::pre-repeat-simplify") << std::endl;
297	19107	if (options().smt.repeatSimp)
298		{
299	502	Trace("smt-proc")
300	251	<< "ProcessAssertions::processAssertions() : pre-repeat-simplify"
301	251	<< endl;
302	251	verbose(2) << "re-simplifying assertions..." << std::endl;
303	502	ScopeCounter depth(d_simplifyAssertionsDepth);
304	251	noConflict &= simplifyAssertions(as);
305	502	Trace("smt-proc")
306	251	<< "ProcessAssertions::processAssertions() : post-repeat-simplify"
307	251	<< endl;
308		}
309	19107	dumpAssertions("assertions::post-repeat-simplify", as);
310	19107	Trace("assertions::post-repeat-simplify") << std::endl;
311
312	19107	if (logicInfo().isHigherOrder())
313		{
314	232	applyPass("ho-elim", as);
315		}
316
317		// begin: INVARIANT to maintain: no reordering of assertions or
318		// introducing new ones
319
320	19107	Debug("smt") << " assertions : " << assertions.size() << endl;
321
322	38214	Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
323	19107	<< endl;
324	19107	Debug("smt") << " assertions : " << assertions.size() << endl;
325
326		// ensure rewritten
327	19107	applyPass("rewrite", as);
328		// rewrite equalities based on theory-specific rewriting
329	19107	applyPass("theory-rewrite-eq", as);
330		// apply theory preprocess, which includes ITE removal
331	19119	applyPass("theory-preprocess", as);
332		// notice that we do not apply substitutions as a last step here, since
333		// the range of substitutions is not theory-preprocessed.
334
335	19095	if (options().bv.bitblastMode == options::BitblastMode::EAGER)
336		{
337	60	applyPass("bv-eager-atoms", as);
338		}
339
340	19095	Trace("smt-proc") << "ProcessAssertions::apply() end" << endl;
341	19095	dumpAssertions("assertions::post-everything", as);
342	19095	Trace("assertions::post-everything") << std::endl;
343
344	19095	return noConflict;
345		}
346
347		// returns false if simplification led to "false"
348	19358	bool ProcessAssertions::simplifyAssertions(Assertions& as)
349		{
350	19358	spendResource(Resource::PreprocessStep);
351		try
352		{
353	19358	AssertionPipeline& assertions = as.getAssertionPipeline();
354	35893	ScopeCounter depth(d_simplifyAssertionsDepth);
355
356	19358	Trace("simplify") << "ProcessAssertions::simplify()" << endl;
357
358	19358	if (options().smt.simplificationMode != options::SimplificationMode::NONE)
359		{
360		// Perform non-clausal simplification
361	15829	PreprocessingPassResult res = applyPass("non-clausal-simp", as);
362	15829	if (res == PreprocessingPassResult::CONFLICT)
363		{
364	2819	return false;
365		}
366
367		// We piggy-back off of the BackEdgesMap in the CircuitPropagator to
368		// do the miplib trick.
369	13010	if ( // check that option is on
370	13022	options().arith.arithMLTrick &&
371		// only useful in arith
372	13022	logicInfo().isTheoryEnabled(THEORY_ARITH) &&
373		// we add new assertions and need this (in practice, this
374		// restriction only disables miplib processing during
375		// re-simplification, which we don't expect to be useful anyway)
376	12	assertions.getRealAssertionsEnd() == assertions.size())
377		{
378	12	applyPass("miplib-trick", as);
379		}
380		else
381		{
382	25996	Trace("simplify") << "ProcessAssertions::simplify(): "
383	12998	<< "skipping miplib pseudobooleans pass..." << endl;
384		}
385		}
386
387	16539	Debug("smt") << " assertions : " << assertions.size() << endl;
388
389		// ITE simplification
390	33078	if (options().smt.doITESimp
391	16539	&& (d_simplifyAssertionsDepth <= 1 \|\| options().smt.doITESimpOnRepeat))
392		{
393	1	PreprocessingPassResult res = applyPass("ite-simp", as);
394	1	if (res == PreprocessingPassResult::CONFLICT)
395		{
396		verbose(2) << "...ITE simplification found unsat..." << std::endl;
397		return false;
398		}
399		}
400
401	16539	Debug("smt") << " assertions : " << assertions.size() << endl;
402
403		// Unconstrained simplification
404	16539	if (options().smt.unconstrainedSimp)
405		{
406	333	applyPass("unconstrained-simplifier", as);
407		}
408
409	33078	if (options().smt.repeatSimp
410	16539	&& options().smt.simplificationMode
411		!= options::SimplificationMode::NONE)
412		{
413	474	PreprocessingPassResult res = applyPass("non-clausal-simp", as);
414	474	if (res == PreprocessingPassResult::CONFLICT)
415		{
416	4	return false;
417		}
418		}
419
420	16535	dumpAssertions("post-repeatsimp", as);
421	16535	Trace("smt") << "POST repeatSimp" << endl;
422	16535	Debug("smt") << " assertions : " << assertions.size() << endl;
423		}
424		catch (TypeCheckingExceptionPrivate& tcep)
425		{
426		// Calls to this function should have already weeded out any
427		// typechecking exceptions via (e.g.) ensureBoolean(). But a
428		// theory could still create a new expression that isn't
429		// well-typed, and we don't want the C++ runtime to abort our
430		// process without any error notice.
431		InternalError()
432		<< "A bad expression was produced. Original exception follows:\n"
433		<< tcep;
434		}
435	16535	return true;
436		}
437
438	461615	void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as)
439		{
440	461615	bool isTraceOn = Trace.isOn(key);
441	461615	if (!isTraceOn)
442		{
443	923228	return;
444		}
445		// Cannot print unless produce assertions is enabled. Otherwise, the printing
446		// is misleading, since it does not capture what symbols were provided
447		// as definitions.
448	1	if (!options().smt.produceAssertions)
449		{
450		warning()
451		<< "Assertions not available for dumping (use --produce-assertions)."
452		<< std::endl;
453		return;
454		}
455	1	PrintBenchmark pb(&d_env.getPrinter());
456	2	std::vector<Node> assertions;
457		// Notice that the following list covers define-fun and define-fun-rec
458		// from input. The former does not impact the assertions since define-fun are
459		// added as top-level substitutions. The latter do get added to the list
460		// of assertions. Since we are interested in printing the result of
461		// preprocessed quantified formulas corresponding to recursive function
462		// definitions and not the original definitions, we discard the latter
463		// in the loop below.
464		//
465		// In summary, this means that define-fun-rec are expanded to
466		// (declare-fun ...) + (assert (forall ...)) in the printing below, whereas
467		// define-fun are preserved.
468	1	const context::CDList<Node>& asld = as.getAssertionListDefinitions();
469	2	std::vector<Node> defs;
470	1	for (const Node& d : asld)
471		{
472		if (d.getKind() != FORALL)
473		{
474		defs.push_back(d);
475		}
476		}
477	1	AssertionPipeline& ap = as.getAssertionPipeline();
478	5	for (size_t i = 0, size = ap.size(); i < size; i++)
479		{
480	4	assertions.push_back(ap[i]);
481		}
482	2	std::stringstream ss;
483	1	pb.printBenchmark(ss, logicInfo().getLogicString(), defs, assertions);
484	1	Trace(key) << ";;; " << key << " start" << std::endl;
485	1	Trace(key) << ss.str();
486	1	Trace(key) << ";;; " << key << " end " << std::endl;
487		}
488
489	165231	PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname,
490		Assertions& as)
491		{
492	165231	dumpAssertions("assertions::pre-" + pname, as);
493	165231	AssertionPipeline& assertions = as.getAssertionPipeline();
494	165231	PreprocessingPassResult res = d_passes[pname]->apply(&assertions);
495	165216	dumpAssertions("assertions::post-" + pname, as);
496	165216	return res;
497		}
498
499		} // namespace smt
500	31137	} // namespace cvc5