decision/decision_strategy.h \
decision/justification_heuristic.cpp \
decision/justification_heuristic.h \
+ preprocessing/assertion_pipeline.cpp \
+ preprocessing/assertion_pipeline.h \
preprocessing/passes/apply_substs.cpp \
preprocessing/passes/apply_substs.h \
preprocessing/passes/apply_to_const.cpp \
preprocessing/passes/pseudo_boolean_processor.h \
preprocessing/passes/miplib_trick.cpp \
preprocessing/passes/miplib_trick.h \
- preprocessing/passes/quantifiers_preprocess.cpp \
- preprocessing/passes/quantifiers_preprocess.h \
preprocessing/passes/quantifier_macros.cpp \
preprocessing/passes/quantifier_macros.h \
+ preprocessing/passes/quantifiers_preprocess.cpp \
+ preprocessing/passes/quantifiers_preprocess.h \
preprocessing/passes/real_to_int.cpp \
preprocessing/passes/real_to_int.h \
preprocessing/passes/rewrite.cpp \
namespace {
-bool isDefinedKind(Kind k)
-{
- return k > UNDEFINED_KIND && k < LAST_KIND;
-}
+bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
bool isDefinedIntKind(CVC4::Kind k)
{
}
}
-void DecisionEngine::addAssertions(const vector<Node> &assertions)
-{
- Assert(false); // doing this so that we revisit what to do
- // here. Currently not being used.
-
- // d_result = SAT_VALUE_UNKNOWN;
- // d_assertions.reserve(assertions.size());
- // for(unsigned i = 0; i < assertions.size(); ++i)
- // d_assertions.push_back(assertions[i]);
-}
-
-void DecisionEngine::addAssertions(const vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap)
+void DecisionEngine::addAssertions(
+ const preprocessing::AssertionPipeline& assertions)
{
// new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
- // d_assertions.reserve(assertions.size());
- for(unsigned i = 0; i < assertions.size(); ++i)
- d_assertions.push_back(assertions[i]);
+ for (const Node& assertion : assertions)
+ {
+ d_assertions.push_back(assertion);
+ }
for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
- d_needIteSkolemMap[i]->
- addAssertions(assertions, assertionsEnd, iteSkolemMap);
+ {
+ d_needIteSkolemMap[i]->addAssertions(assertions);
+ }
}
}/* CVC4 namespace */
#include "base/output.h"
#include "decision/decision_strategy.h"
#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "prop/sat_solver_types.h"
-#include "smt/term_formula_removal.h"
#include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
using namespace std;
using namespace CVC4::prop;
/* return d_needIteSkolemMap.size() > 0; */
/* } */
- /* add a set of assertions */
- void addAssertions(const vector<Node> &assertions);
-
/**
- * add a set of assertions, while providing a mapping between skolem
- * variables and corresponding assertions. It is assumed that all
- * assertions after assertionEnd were generated by ite
- * removal. Hence, iteSkolemMap maps into only these.
+ * Add a list of assertions from an AssertionPipeline.
*/
- void addAssertions(const vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap);
-
- /* add a single assertion */
- void addAssertion(Node n);
+ void addAssertions(const preprocessing::AssertionPipeline& assertions);
// Interface for Strategies to use stuff stored in Decision Engine
// (which was possibly requested by them on initialization)
#ifndef __CVC4__DECISION__DECISION_STRATEGY_H
#define __CVC4__DECISION__DECISION_STRATEGY_H
+#include "preprocessing/assertion_pipeline.h"
#include "prop/sat_solver_types.h"
#include "smt/term_formula_removal.h"
bool needIteSkolemMap() override { return true; }
- virtual void addAssertions(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) = 0;
+ virtual void addAssertions(
+ const preprocessing::AssertionPipeline& assertions) = 0;
};/* class ITEDecisionStrategy */
class RelevancyStrategy : public ITEDecisionStrategy {
}
}
-
-
-void JustificationHeuristic::addAssertions
-(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) {
+void JustificationHeuristic::addAssertions(
+ const preprocessing::AssertionPipeline &assertions)
+{
+ size_t assertionsEnd = assertions.getRealAssertionsEnd();
Trace("decision")
<< "JustificationHeuristic::addAssertions()"
<< std::endl;
// Save the 'real' assertions locally
- for(unsigned i = 0; i < assertionsEnd; ++i)
+ for (size_t i = 0; i < assertionsEnd; i++)
+ {
d_assertions.push_back(assertions[i]);
+ }
// Save mapping between ite skolems and ite assertions
- for(IteSkolemMap::iterator i = iteSkolemMap.begin();
- i != iteSkolemMap.end(); ++i) {
-
- Trace("decision::jh::ite")
- << " jh-ite: " << (i->first) << " maps to "
- << assertions[(i->second)] << std::endl;
- Assert(i->second >= assertionsEnd && i->second < assertions.size());
+ for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+ {
+ Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
+ << assertions[(i.second)] << std::endl;
+ Assert(i.second >= assertionsEnd && i.second < assertions.size());
- d_iteAssertions[i->first] = assertions[i->second];
+ d_iteAssertions[i.first] = assertions[i.second];
}
// Automatic weight computation
#include "decision/decision_engine.h"
#include "decision/decision_strategy.h"
#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
#include "prop/sat_solver_types.h"
namespace CVC4 {
prop::SatLiteral getNext(bool &stopSearch) override;
- void addAssertions(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) override;
+ void addAssertions(
+ const preprocessing::AssertionPipeline &assertions) override;
private:
/* getNext with an option to specify threshold */
#ifndef __CVC4_PRIVATE_LIBRARY_H
#define __CVC4_PRIVATE_LIBRARY_H
-#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER))
+#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \
+ || defined(__BUILDING_CVC4PARSERLIB) \
+ || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) \
+ || defined(__BUILDING_CVC4DRIVER))
# error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */
--- /dev/null
+/********************* */
+/*! \file assertion_pipeline.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "preprocessing/assertion_pipeline.h"
+
+#include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "proof/proof_manager.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {}
+
+void AssertionPipeline::replace(size_t i, Node n)
+{
+ PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
+ d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i,
+ Node n,
+ const std::vector<Node>& addnDeps)
+{
+ PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+ for (const auto& addnDep
+ : addnDeps) {
+ ProofManager::currentPM()->addDependence(n, addnDep);
+ });
+ d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
+{
+ PROOF(
+ for (const auto& n
+ : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
+ d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
+
+ for (const auto& n : ns)
+ {
+ d_nodes.push_back(n);
+ }
+}
+
+} // namespace preprocessing
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file assertion_pipeline.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/term_formula_removal.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+/**
+ * Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes. It is assumed that all assertions after d_realAssertionsEnd were
+ * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
+ */
+class AssertionPipeline
+{
+ public:
+ AssertionPipeline();
+
+ size_t size() const { return d_nodes.size(); }
+
+ void resize(size_t n) { d_nodes.resize(n); }
+
+ void clear()
+ {
+ d_nodes.clear();
+ d_realAssertionsEnd = 0;
+ }
+
+ Node& operator[](size_t i) { return d_nodes[i]; }
+ const Node& operator[](size_t i) const { return d_nodes[i]; }
+ void push_back(Node n) { d_nodes.push_back(n); }
+
+ std::vector<Node>& ref() { return d_nodes; }
+ const std::vector<Node>& ref() const { return d_nodes; }
+
+ std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
+ std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
+
+ /*
+ * Replaces assertion i with node n and records the dependency between the
+ * original assertion and its replacement.
+ */
+ void replace(size_t i, Node n);
+
+ /*
+ * Replaces assertion i with node n and records that this replacement depends
+ * on assertion i and the nodes listed in addnDeps. The dependency
+ * information is used for unsat cores and proofs.
+ */
+ void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
+
+ /*
+ * Replaces an assertion with a vector of assertions and records the
+ * dependencies.
+ */
+ void replace(size_t i, const std::vector<Node>& ns);
+
+ IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+ const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
+
+ size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
+
+ void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
+
+ private:
+ std::vector<Node> d_nodes;
+
+ /**
+ * Map from skolem variables to index in d_assertions containing
+ * corresponding introduced Boolean ite
+ */
+ IteSkolemMap d_iteSkolemMap;
+
+ /** Size of d_nodes when preprocessing starts */
+ size_t d_realAssertionsEnd;
+}; /* class AssertionPipeline */
+
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
// When solving incrementally, all substitutions are piled into the
// assertion at d_substitutionsIndex: we don't want to apply substitutions
// to this assertion or information will be lost.
- context::CDO<unsigned>& substs_index =
- assertionsToPreprocess->getSubstitutionsIndex();
+ unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
+ theory::SubstitutionMap& substMap =
+ d_preprocContext->getTopLevelSubstitutions();
unsigned size = assertionsToPreprocess->size();
unsigned substitutionAssertion = substs_index > 0 ? substs_index : size;
for (unsigned i = 0; i < size; ++i)
Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
<< std::endl;
d_preprocContext->spendResource(options::preprocessStep());
- assertionsToPreprocess->replace(
- i,
- theory::Rewriter::rewrite(
- assertionsToPreprocess->getTopLevelSubstitutions().apply(
- (*assertionsToPreprocess)[i])));
+ assertionsToPreprocess->replace(i,
+ theory::Rewriter::rewrite(substMap.apply(
+ (*assertionsToPreprocess)[i])));
Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i]
<< std::endl;
}
propagator->getBackEdges();
unordered_set<unsigned long> removeAssertions;
SubstitutionMap& top_level_substs =
- assertionsToPreprocess->getTopLevelSubstitutions();
+ d_preprocContext->getTopLevelSubstitutions();
NodeManager* nm = NodeManager::currentNM();
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
// Assert all the assertions to the propagator
Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
- context::CDO<unsigned>& substs_index =
- assertionsToPreprocess->getSubstitutionsIndex();
+ unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
<< " learned literals." << std::endl;
// No conflict, go through the literals and solve them
SubstitutionMap& top_level_substs =
- assertionsToPreprocess->getTopLevelSubstitutions();
+ d_preprocContext->getTopLevelSubstitutions();
SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
SubstitutionMap::iterator pos;
#include "preprocessing/preprocessing_pass.h"
-#include "expr/node_manager.h"
-#include "proof/proof.h"
#include "smt/dump.h"
#include "smt/smt_statistics_registry.h"
namespace CVC4 {
namespace preprocessing {
-AssertionPipeline::AssertionPipeline(context::Context* context)
- : d_substitutionsIndex(context, 0),
- d_topLevelSubstitutions(context),
- d_realAssertionsEnd(0)
-{
-}
-
-void AssertionPipeline::replace(size_t i, Node n) {
- PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
- d_nodes[i] = n;
-}
-
-void AssertionPipeline::replace(size_t i,
- Node n,
- const std::vector<Node>& addnDeps)
-{
- PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
- for (const auto& addnDep
- : addnDeps) {
- ProofManager::currentPM()->addDependence(n, addnDep);
- });
- d_nodes[i] = n;
-}
-
-void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
-{
- PROOF(
- for (const auto& n
- : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
- d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
-
- for (const auto& n : ns)
- {
- d_nodes.push_back(n);
- }
-}
-
PreprocessingPassResult PreprocessingPass::apply(
AssertionPipeline* assertionsToPreprocess) {
TimerStat::CodeTimer codeTimer(d_timer);
#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
#include <string>
-#include <vector>
-#include "context/cdo.h"
-#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/smt_engine_scope.h"
-#include "smt/term_formula_removal.h"
#include "theory/logic_info.h"
-#include "theory/substitutions.h"
namespace CVC4 {
namespace preprocessing {
-/**
- * Assertion Pipeline stores a list of assertions modified by preprocessing
- * passes.
- */
-class AssertionPipeline
-{
- public:
- AssertionPipeline(context::Context* context);
-
- size_t size() const { return d_nodes.size(); }
-
- void resize(size_t n) { d_nodes.resize(n); }
-
- void clear()
- {
- d_nodes.clear();
- d_realAssertionsEnd = 0;
- }
-
- Node& operator[](size_t i) { return d_nodes[i]; }
- const Node& operator[](size_t i) const { return d_nodes[i]; }
- void push_back(Node n) { d_nodes.push_back(n); }
-
- std::vector<Node>& ref() { return d_nodes; }
- const std::vector<Node>& ref() const { return d_nodes; }
-
- std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
- std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
-
- /*
- * Replaces assertion i with node n and records the dependency between the
- * original assertion and its replacement.
- */
- void replace(size_t i, Node n);
-
- /*
- * Replaces assertion i with node n and records that this replacement depends
- * on assertion i and the nodes listed in addnDeps. The dependency
- * information is used for unsat cores and proofs.
- */
- void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
-
- /*
- * Replaces an assertion with a vector of assertions and records the
- * dependencies.
- */
- void replace(size_t i, const std::vector<Node>& ns);
-
- IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
-
- context::CDO<unsigned>& getSubstitutionsIndex()
- {
- return d_substitutionsIndex;
- }
-
- theory::SubstitutionMap& getTopLevelSubstitutions()
- {
- return d_topLevelSubstitutions;
- }
-
- size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
-
- void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
-
- private:
- std::vector<Node> d_nodes;
-
- /**
- * Map from skolem variables to index in d_assertions containing
- * corresponding introduced Boolean ite
- */
- IteSkolemMap d_iteSkolemMap;
-
- /* Index for where to store substitutions */
- context::CDO<unsigned> d_substitutionsIndex;
-
- /* The top level substitutions */
- theory::SubstitutionMap d_topLevelSubstitutions;
-
- /** Size of d_nodes when preprocessing starts */
- size_t d_realAssertionsEnd;
-}; /* class AssertionPipeline */
-
/**
* Preprocessing passes return a result which indicates whether a conflict has
* been detected during preprocessing.
: d_smt(smt),
d_resourceManager(resourceManager),
d_iteRemover(iteRemover),
+ d_substitutionsIndex(smt->d_userContext, 0),
+ d_topLevelSubstitutions(smt->d_userContext),
d_circuitPropagator(circuitPropagator),
d_symsInAssertions(smt->d_userContext)
{
#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#include "context/cdo.h"
#include "context/context.h"
#include "decision/decision_engine.h"
#include "preprocessing/util/ite_utilities.h"
/* Widen the logic to include the given theory. */
void widenLogic(theory::TheoryId id);
+ unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); }
+
+ void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; }
+
+ /** Gets a reference to the top-level substitution map */
+ theory::SubstitutionMap& getTopLevelSubstitutions()
+ {
+ return d_topLevelSubstitutions;
+ }
+
/* Enable Integers. */
void enableIntegers();
/** Instance of the ITE remover */
RemoveTermFormulas* d_iteRemover;
+ /* Index for where to store substitutions */
+ context::CDO<unsigned> d_substitutionsIndex;
+
+ /* The top level substitutions */
+ theory::SubstitutionMap d_topLevelSubstitutions;
+
/** Instance of the circuit propagator */
theory::booleans::CircuitPropagator* d_circuitPropagator;
d_managedReplayLog(),
d_listenerRegistrations(new ListenerRegistrationList()),
d_propagator(true, true),
- d_assertions(d_smt.d_userContext),
+ d_assertions(),
d_assertionsProcessed(smt.d_userContext, false),
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
Node applySubstitutions(TNode node)
{
return Rewriter::rewrite(
- d_assertions.getTopLevelSubstitutions().apply(node));
+ d_preprocessingPassContext->getTopLevelSubstitutions().apply(node));
}
/**
spendResource(options::preprocessStep());
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
- SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions();
+ SubstitutionMap& top_level_substs =
+ d_preprocessingPassContext->getTopLevelSubstitutions();
// Dump the assertions
dumpAssertions("pre-everything", d_assertions);
// proper data structure.
// Placeholder for storing substitutions
- d_assertions.getSubstitutionsIndex() = d_assertions.size();
+ d_preprocessingPassContext->setSubstitutionsIndex(d_assertions.size());
d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
}
if(noConflict) {
Chat() << "pushing to decision engine..." << endl;
Assert(iteRewriteAssertionsEnd == d_assertions.size());
- d_smt.d_decisionEngine->addAssertions(d_assertions.ref(),
- d_assertions.getRealAssertionsEnd(),
- getIteSkolemMap());
+ d_smt.d_decisionEngine->addAssertions(d_assertions);
}
// end: INVARIANT to maintain: no reordering of assertions or
d_check_vts_lemma_lc = false;
}
-InstStrategyCegqi::~InstStrategyCegqi()
-{
-
-}
+InstStrategyCegqi::~InstStrategyCegqi() {}
bool InstStrategyCegqi::needsCheck(Theory::Effort e)
{
d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
}
if( d_type==typ_ground ){
- //int e = p->evaluate( d_n );
- //if( e==1 ){
+ // int e = p->evaluate( d_n );
+ // if( e==1 ){
// d_ground_eval[0] = p->d_true;
//}else if( e==-1 ){
// d_ground_eval[0] = p->d_false;
//}
- //modified
+ // modified
TermDb* tdb = p->getTermDatabase();
QuantifiersEngine* qe = p->getQuantifiersEngine();
- for( unsigned i=0; i<2; i++ ){
+ for (unsigned i = 0; i < 2; i++)
+ {
if (tdb->isEntailed(d_n, i == 0))
{
d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
{
if (!expr::hasBoundVar(d_n[i]))
{
- TNode t = tdb->getEntailedTerm(d_n[i]);
+ TNode t = tdb->getEntailedTerm(d_n[i]);
if (qe->inConflict())
{
return false;
}
Trace("cegqi-engine") << "...success:" << std::endl;
Trace("cegqi-engine") << ss.str();
- Trace("sygus-repair-const") << "Repaired constants in solution : "
- << std::endl;
+ Trace("sygus-repair-const")
+ << "Repaired constants in solution : " << std::endl;
Trace("sygus-repair-const") << ss.str();
return true;
}
#include "options/options.h"
#include "options/proof_options.h"
#include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
#include "proof/cnf_proof.h"
#include "proof/lemma_proof.h"
#include "proof/proof_manager.h"
using namespace std;
+using namespace CVC4::preprocessing;
using namespace CVC4::theory;
namespace CVC4 {
d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
}
- std::vector<Node> additionalLemmas;
- IteSkolemMap iteSkolemMap;
+ AssertionPipeline additionalLemmas;
// Run theory preprocessing, maybe
Node ppNode = preprocess ? this->preprocess(node) : Node(node);
// Remove the ITEs
Debug("ite") << "Remove ITE from " << ppNode << std::endl;
additionalLemmas.push_back(ppNode);
- d_tform_remover.run(additionalLemmas, iteSkolemMap);
+ additionalLemmas.updateRealAssertionsEnd();
+ d_tform_remover.run(additionalLemmas.ref(),
+ additionalLemmas.getIteSkolemMap());
Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
- additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
+ additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0]));
if(Debug.isOn("lemma-ites")) {
Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
// assert to prop engine
d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
- additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
+ additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i]));
d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
}
// WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
if(negated) {
- additionalLemmas[0] = additionalLemmas[0].notNode();
+ additionalLemmas.replace(0, additionalLemmas[0].notNode());
negated = false;
}
// assert to decision engine
if(!removable) {
- d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
+ d_decisionEngine->addAssertions(additionalLemmas);
}
// Mark that we added some lemmas
Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3);
- context::Context context;
- AssertionPipeline apipe(&context);
+ AssertionPipeline apipe;
apipe.push_back(a);
passes::BVGauss bgauss(nullptr);
std::unordered_map<Node, Node, NodeHashFunction> res;
Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3);
- context::Context context;
- AssertionPipeline apipe(&context);
+ AssertionPipeline apipe;
apipe.push_back(a);
apipe.push_back(eq4);
apipe.push_back(eq5);
d_p),
d_nine);
- context::Context context;
- AssertionPipeline apipe(&context);
+ AssertionPipeline apipe;
apipe.push_back(eq1);
apipe.push_back(eq2);
passes::BVGauss bgauss(nullptr);
projects / cvc5.git / commitdiff