summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/assertion_pipeline.h8
-rw-r--r--src/preprocessing/passes/ackermann.cpp10
-rw-r--r--src/preprocessing/passes/bv_gauss.cpp20
-rw-r--r--src/preprocessing/passes/global_negate.cpp3
-rw-r--r--src/preprocessing/passes/global_negate.h2
-rw-r--r--src/preprocessing/passes/ho_elim.cpp12
-rw-r--r--src/preprocessing/passes/ite_removal.cpp4
-rw-r--r--src/preprocessing/passes/ite_simp.cpp8
-rw-r--r--src/preprocessing/passes/nl_ext_purify.cpp15
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp16
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp8
-rw-r--r--src/preprocessing/passes/quantifier_macros.h12
-rw-r--r--src/preprocessing/passes/sygus_inference.cpp2
-rw-r--r--src/preprocessing/passes/sygus_inference.h2
-rw-r--r--src/preprocessing/passes/synth_rew_rules.cpp2
-rw-r--r--src/preprocessing/passes/unconstrained_simplifier.cpp9
-rw-r--r--src/preprocessing/util/ite_utilities.cpp14
-rw-r--r--src/preprocessing/util/ite_utilities.h7
18 files changed, 88 insertions, 66 deletions
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 6ca430ac4..5c50903c5 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -49,9 +49,6 @@ class AssertionPipeline
*/
void clear();
- /** TODO (projects #75): remove this */
- Node& operator[](size_t i) { return d_nodes[i]; }
- /** Get the assertion at index i */
const Node& operator[](size_t i) const { return d_nodes[i]; }
/**
@@ -72,9 +69,6 @@ class AssertionPipeline
/** Same as above, with TrustNode */
void pushBackTrusted(theory::TrustNode trn);
- /** TODO (projects #75): remove this */
- std::vector<Node>& ref() { return d_nodes; }
-
/**
* Get the constant reference to the underlying assertions. It is only
* possible to modify these via the replace methods below.
@@ -134,7 +128,7 @@ class AssertionPipeline
* @param n The substitution node
* @param pg The proof generator that can provide a proof of n.
*/
- void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr);
+ void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr);
/**
* Conjoin n to the assertion vector at position i. This replaces
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a7b33ae26..af6cae796 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -276,9 +276,13 @@ void usortsToBitVectors(const LogicInfo& d_logic,
for (size_t i = 0, size = assertions->size(); i < size; ++i)
{
Node old = (*assertions)[i];
- assertions->replace(i, usVarsToBVVars.apply((*assertions)[i]));
- Trace("uninterpretedSorts-to-bv")
- << " " << old << " => " << (*assertions)[i] << "\n";
+ Node newA = usVarsToBVVars.apply((*assertions)[i]);
+ if (newA != old)
+ {
+ assertions->replace(i, newA);
+ Trace("uninterpretedSorts-to-bv")
+ << " " << old << " => " << (*assertions)[i] << "\n";
+ }
}
}
}
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 05fee230e..eaba90561 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -737,8 +737,8 @@ PreprocessingPassResult BVGauss::applyInternal(
}
std::unordered_map<Node, Node, NodeHashFunction> subst;
- std::vector<Node>& atpp = assertionsToPreprocess->ref();
+ NodeManager* nm = NodeManager::currentNM();
for (const auto& eq : equations)
{
if (eq.second.size() <= 1) { continue; }
@@ -756,11 +756,12 @@ PreprocessingPassResult BVGauss::applyInternal(
<< std::endl;
if (ret != BVGauss::Result::INVALID)
{
- NodeManager *nm = NodeManager::currentNM();
if (ret == BVGauss::Result::NONE)
{
- atpp.clear();
- atpp.push_back(nm->mkConst<bool>(false));
+ assertionsToPreprocess->clear();
+ Node n = nm->mkConst<bool>(false);
+ assertionsToPreprocess->push_back(n);
+ return PreprocessingPassResult::CONFLICT;
}
else
{
@@ -773,7 +774,8 @@ PreprocessingPassResult BVGauss::applyInternal(
{
Node a = nm->mkNode(kind::EQUAL, p.first, p.second);
Trace("bv-gauss-elim") << "added assertion: " << a << std::endl;
- atpp.push_back(a);
+ // add new assertion
+ assertionsToPreprocess->push_back(a);
}
}
}
@@ -782,9 +784,13 @@ PreprocessingPassResult BVGauss::applyInternal(
if (!subst.empty())
{
/* delete (= substitute with true) obsolete assertions */
- for (auto& a : atpp)
+ const std::vector<Node>& aref = assertionsToPreprocess->ref();
+ for (size_t i = 0, asize = aref.size(); i < asize; ++i)
{
- a = a.substitute(subst.begin(), subst.end());
+ Node a = aref[i];
+ Node as = a.substitute(subst.begin(), subst.end());
+ // replace the assertion
+ assertionsToPreprocess->replace(i, as);
}
}
return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 5d29add3c..00ca1efd3 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -27,7 +27,8 @@ namespace CVC4 {
namespace preprocessing {
namespace passes {
-Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
+Node GlobalNegate::simplify(const std::vector<Node>& assertions,
+ NodeManager* nm)
{
Assert(!assertions.empty());
Trace("cegqi-gn") << "Global negate : " << std::endl;
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index 853e5a4dd..208b8d990 100644
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -42,7 +42,7 @@ class GlobalNegate : public PreprocessingPass
AssertionPipeline* assertionsToPreprocess) override;
private:
- Node simplify(std::vector<Node>& assertions, NodeManager* nm);
+ Node simplify(const std::vector<Node>& assertions, NodeManager* nm);
};
} // namespace passes
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 2b8b6f3bd..34645b441 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -353,12 +353,10 @@ PreprocessingPassResult HoElim::applyInternal(
// add lambda lifting axioms as a conjunction to the first assertion
if (!axioms.empty())
{
- Node orig = (*assertionsToPreprocess)[0];
- axioms.push_back(orig);
- Node conj = nm->mkNode(AND, axioms);
+ Node conj = nm->mkAnd(axioms);
conj = theory::Rewriter::rewrite(conj);
Assert(!expr::hasFreeVar(conj));
- assertionsToPreprocess->replace(0, conj);
+ assertionsToPreprocess->conjoin(0, conj);
}
axioms.clear();
@@ -450,12 +448,10 @@ PreprocessingPassResult HoElim::applyInternal(
// add new axioms as a conjunction to the first assertion
if (!axioms.empty())
{
- Node orig = (*assertionsToPreprocess)[0];
- axioms.push_back(orig);
- Node conj = nm->mkNode(AND, axioms);
+ Node conj = nm->mkAnd(axioms);
conj = theory::Rewriter::rewrite(conj);
Assert(!expr::hasFreeVar(conj));
- assertionsToPreprocess->replace(0, conj);
+ assertionsToPreprocess->conjoin(0, conj);
}
return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 11ad27364..a75b6f5ad 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -43,12 +43,12 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
TrustNode trn = d_preprocContext->getIteRemover()->run(
(*assertions)[i], newAsserts, newSkolems, true);
// process
- assertions->replace(i, trn.getNode());
+ assertions->replaceTrusted(i, trn);
Assert(newSkolems.size() == newAsserts.size());
for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
{
imap[newSkolems[j]] = assertions->size();
- assertions->ref().push_back(newAsserts[j].getNode());
+ assertions->pushBackTrusted(newAsserts[j]);
}
}
for (unsigned i = 0, size = assertions->size(); i < size; ++i)
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 49a6fe603..8c99493ba 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -127,7 +127,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
if (options::compressItes())
{
- result = d_iteUtilities.compress(assertionsToPreprocess->ref());
+ result = d_iteUtilities.compress(assertionsToPreprocess);
}
if (result)
@@ -175,7 +175,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
{
Node more = aiteu.reduceConstantIteByGCD(res);
Debug("arith::ite::red") << " gcd->" << more << endl;
- (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+ Node morer = Rewriter::rewrite(more);
+ assertionsToPreprocess->replace(i, morer);
}
}
}
@@ -214,7 +215,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
<< " ->" << res << endl;
Node more = aiteu.reduceConstantIteByGCD(res);
Debug("arith::ite::red") << " gcd->" << more << endl;
- (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+ Node morer = Rewriter::rewrite(more);
+ assertionsToPreprocess->replace(i, morer);
}
}
}
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index e4d79d614..88bdf2e5c 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -117,16 +117,19 @@ PreprocessingPassResult NlExtPurify::applyInternal(
for (unsigned i = 0; i < size; ++i)
{
Node a = (*assertionsToPreprocess)[i];
- assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq));
- Trace("nl-ext-purify") << "Purify : " << a << " -> "
- << (*assertionsToPreprocess)[i] << "\n";
+ Node ap = purifyNlTerms(a, cache, bcache, var_eq);
+ if (a != ap)
+ {
+ assertionsToPreprocess->replace(i, ap);
+ Trace("nl-ext-purify")
+ << "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n";
+ }
}
if (!var_eq.empty())
{
unsigned lastIndex = size - 1;
- var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]);
- assertionsToPreprocess->replace(
- lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq));
+ Node veq = NodeManager::currentNM()->mkAnd(var_eq);
+ assertionsToPreprocess->conjoin(lastIndex, veq);
}
return PreprocessingPassResult::NO_CONFLICT;
}
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 2ca9f783f..fcb6dd171 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -375,11 +375,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
}
}
- NodeBuilder<> learnedBuilder(kind::AND);
Assert(assertionsToPreprocess->getRealAssertionsEnd()
<= assertionsToPreprocess->size());
- learnedBuilder << (*assertionsToPreprocess)
- [assertionsToPreprocess->getRealAssertionsEnd() - 1];
+ std::vector<Node> learnedLitsToConjoin;
for (size_t i = 0; i < learned_literals.size(); ++i)
{
@@ -406,7 +404,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
continue;
}
s.insert(learned);
- learnedBuilder << learned;
+ learnedLitsToConjoin.push_back(learned);
Trace("non-clausal-simplify")
<< "non-clausal learned : " << learned << std::endl;
}
@@ -428,7 +426,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
continue;
}
s.insert(cProp);
- learnedBuilder << cProp;
+ learnedLitsToConjoin.push_back(cProp);
Trace("non-clausal-simplify")
<< "non-clausal constant propagation : " << cProp << std::endl;
}
@@ -439,11 +437,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
// substituting
top_level_substs.addSubstitutions(newSubstitutions);
- if (learnedBuilder.getNumChildren() > 1)
+ if (!learnedLitsToConjoin.empty())
{
- assertionsToPreprocess->replace(
- assertionsToPreprocess->getRealAssertionsEnd() - 1,
- Rewriter::rewrite(Node(learnedBuilder)));
+ size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
+ Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
+ assertionsToPreprocess->conjoin(replIndex, newConj);
}
propagator->setNeedsFinish(true);
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 7713dbc1b..8fea4cbac 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -49,7 +49,7 @@ PreprocessingPassResult QuantifierMacros::applyInternal(
bool success;
do
{
- success = simplify(assertionsToPreprocess->ref(), true);
+ success = simplify(assertionsToPreprocess, true);
} while (success);
finalizeDefinitions();
clearMaps();
@@ -67,7 +67,9 @@ void QuantifierMacros::clearMaps()
d_ground_macros = false;
}
-bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
+bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
+{
+ const std::vector<Node>& assertions = ap->ref();
unsigned rmax =
options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1;
for( unsigned r=0; r<rmax; r++ ){
@@ -116,7 +118,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
}
}
}
- assertions[i] = curr;
+ ap->replace(i, curr);
retVal = true;
}
}
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index 59a4bee2d..c5e557a9e 100644
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -64,7 +64,17 @@ class QuantifierMacros : public PreprocessingPass
bool reqComplete);
void addMacro(Node op, Node n, std::vector<Node>& opc);
void debugMacroDefinition(Node oo, Node n);
- bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+ /**
+ * This applies macro elimination to the given pipeline, which discovers
+ * whether there are any quantified formulas corresponding to macros.
+ *
+ * @param ap The pipeline to apply macros to.
+ * @param doRewrite Whether we also wish to rewrite the assertions based on
+ * the discovered macro definitions.
+ * @return Whether new definitions were inferred and we rewrote the assertions
+ * based on them.
+ */
+ bool simplify(AssertionPipeline* ap, bool doRewrite = false);
Node simplify(Node n);
void finalizeDefinitions();
void clearMaps();
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 0b27d0c17..cdacd740a 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -80,7 +80,7 @@ PreprocessingPassResult SygusInference::applyInternal(
return PreprocessingPassResult::NO_CONFLICT;
}
-bool SygusInference::solveSygus(std::vector<Node>& assertions,
+bool SygusInference::solveSygus(const std::vector<Node>& assertions,
std::vector<Node>& funs,
std::vector<Node>& sols)
{
diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index 02965c8ed..31d94efd2 100644
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -59,7 +59,7 @@ class SygusInference : public PreprocessingPass
* If this function returns true, then we add all uninterpreted symbols s in
* assertions to funs and their corresponding solution to sols.
*/
- bool solveSygus(std::vector<Node>& assertions,
+ bool solveSygus(const std::vector<Node>& assertions,
std::vector<Node>& funs,
std::vector<Node>& sols);
};
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 2ca11eb81..8465a63a0 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -40,7 +40,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
{
Trace("srs-input") << "Synthesize rewrite rules from assertions..."
<< std::endl;
- std::vector<Node>& assertions = assertionsToPreprocess->ref();
+ const std::vector<Node>& assertions = assertionsToPreprocess->ref();
if (assertions.empty())
{
return PreprocessingPassResult::NO_CONFLICT;
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 64080987b..9b4d02032 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -842,7 +842,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
{
d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
- std::vector<Node>& assertions = assertionsToPreprocess->ref();
+ const std::vector<Node>& assertions = assertionsToPreprocess->ref();
d_context->push();
@@ -855,9 +855,12 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
{
processUnconstrained();
// d_substitutions.print(Message.getStream());
- for (Node& assertion : assertions)
+ for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
{
- assertion = Rewriter::rewrite(d_substitutions.apply(assertion));
+ Node a = assertions[i];
+ Node as = Rewriter::rewrite(d_substitutions.apply(a));
+ // replace the assertion
+ assertionsToPreprocess->replace(i, as);
}
}
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index c72da1621..c9bf283ac 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -130,13 +130,13 @@ bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
}
/* returns false if an assertion is discovered to be equal to false. */
-bool ITEUtilities::compress(std::vector<Node>& assertions)
+bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess)
{
if (d_compressor == NULL)
{
d_compressor = new ITECompressor(d_containsVisitor.get());
}
- return d_compressor->compress(assertions);
+ return d_compressor->compress(assertionsToPreprocess);
}
Node ITEUtilities::simplifyWithCare(TNode e)
@@ -527,17 +527,18 @@ Node ITECompressor::compressBoolean(Node toCompress)
}
}
-bool ITECompressor::compress(std::vector<Node>& assertions)
+bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
{
reset();
- d_assertions = &assertions;
- d_incoming.computeReachability(assertions);
+ d_assertions = assertionsToPreprocess;
+ d_incoming.computeReachability(assertionsToPreprocess->ref());
++(d_statistics.d_compressCalls);
Chat() << "Computed reachability" << endl;
bool nofalses = true;
+ const std::vector<Node>& assertions = assertionsToPreprocess->ref();
size_t original_size = assertions.size();
Chat() << "compressing " << original_size << endl;
for (size_t i = 0; i < original_size && nofalses; ++i)
@@ -545,7 +546,8 @@ bool ITECompressor::compress(std::vector<Node>& assertions)
Node assertion = assertions[i];
Node compressed = compressBoolean(assertion);
Node rewritten = theory::Rewriter::rewrite(compressed);
- assertions[i] = rewritten;
+ // replace
+ assertionsToPreprocess->replace(i, rewritten);
Assert(!d_contains->containsTermITE(rewritten));
nofalses = (rewritten != d_false);
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index fbddf7169..c82bf7958 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -27,6 +27,7 @@
#include <vector>
#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
#include "util/hash.h"
#include "util/statistics_registry.h"
@@ -74,7 +75,7 @@ class ITEUtilities
bool simpIteDidALotOfWorkHeuristic() const;
/* returns false if an assertion is discovered to be equal to false. */
- bool compress(std::vector<Node>& assertions);
+ bool compress(AssertionPipeline* assertionsToPreprocess);
Node simplifyWithCare(TNode e);
@@ -167,7 +168,7 @@ class ITECompressor
~ITECompressor();
/* returns false if an assertion is discovered to be equal to false. */
- bool compress(std::vector<Node>& assertions);
+ bool compress(AssertionPipeline* assertionsToPreprocess);
/* garbage Collects the compressor. */
void garbageCollect();
@@ -176,7 +177,7 @@ class ITECompressor
Node d_true; /* Copy of true. */
Node d_false; /* Copy of false. */
ContainsTermITEVisitor* d_contains;
- std::vector<Node>* d_assertions;
+ AssertionPipeline* d_assertions;
IncomingArcCounter d_incoming;
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback