--- /dev/null
+/********************* */
+/*! \file nl_ext_purify.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** 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 The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms
+ **/
+
+#include "preprocessing/passes/nl_ext_purify.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+Node NlExtPurify::purifyNlTerms(TNode n,
+ NodeMap& cache,
+ NodeMap& bcache,
+ std::vector<Node>& var_eq,
+ bool beneathMult)
+{
+ if (beneathMult)
+ {
+ NodeMap::iterator find = bcache.find(n);
+ if (find != bcache.end())
+ {
+ return (*find).second;
+ }
+ }
+ else
+ {
+ NodeMap::iterator find = cache.find(n);
+ if (find != cache.end())
+ {
+ return (*find).second;
+ }
+ }
+ Node ret = n;
+ if (n.getNumChildren() > 0)
+ {
+ if (beneathMult
+ && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
+ {
+ // don't do it if it rewrites to a constant
+ Node nr = Rewriter::rewrite(n);
+ if (nr.isConst())
+ {
+ // return the rewritten constant
+ ret = nr;
+ }
+ else
+ {
+ // new variable
+ ret = NodeManager::currentNM()->mkSkolem(
+ "__purifyNl_var",
+ n.getType(),
+ "Variable introduced in purifyNl pass");
+ Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
+ var_eq.push_back(np.eqNode(ret));
+ Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
+ << std::endl;
+ }
+ }
+ else
+ {
+ bool beneathMultNew = beneathMult || n.getKind() == kind::MULT;
+ bool childChanged = false;
+ std::vector<Node> children;
+ for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
+ {
+ Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew);
+ childChanged = childChanged || nc != n[i];
+ children.push_back(nc);
+ }
+ if (childChanged)
+ {
+ ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ }
+ }
+ }
+ if (beneathMult)
+ {
+ bcache[n] = ret;
+ }
+ else
+ {
+ cache[n] = ret;
+ }
+ return ret;
+}
+
+NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "nl-ext-purify"){};
+
+PreprocessingPassResult NlExtPurify::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> bcache;
+ std::vector<Node> var_eq;
+ unsigned size = assertionsToPreprocess->size();
+ 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";
+ }
+ 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));
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file nl_ext_purify.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** 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 The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms by replacing sums under multiplications by fresh
+ ** variables
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class NlExtPurify : public PreprocessingPass
+{
+ public:
+ NlExtPurify(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ Node purifyNlTerms(TNode n,
+ NodeMap& cache,
+ NodeMap& bcache,
+ std::vector<Node>& var_eq,
+ bool beneathMult = false);
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/ite_removal.h"
#include "preprocessing/passes/ite_simp.h"
+#include "preprocessing/passes/nl_ext_purify.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/quantifiers_preprocess.h"
#include "preprocessing/passes/real_to_int.h"
*/
bool nonClausalSimplify();
- /**
- * Performs static learning on the assertions.
- */
- void staticLearning();
-
- Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
- Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
-
/**
* Helper function to fix up assertion list to restore invariants needed after
* ite removal.
/** Process a user push.
*/
void notifyPush() {
-
+
}
/**
std::ostream* getReplayLog() const {
return d_managedReplayLog.getReplayLog();
}
-
+
//------------------------------- expression names
// implements setExpressionName, as described in smt_engine.h
void setExpressionName(Expr e, std::string name) {
d_exprNames[Node::fromExpr(e)] = name;
}
-
+
// implements getExpressionName, as described in smt_engine.h
bool getExpressionName(Expr e, std::string& name) const {
context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
new IntToBV(d_preprocessingPassContext.get()));
std::unique_ptr<ITESimp> iteSimp(
new ITESimp(d_preprocessingPassContext.get()));
+ std::unique_ptr<NlExtPurify> nlExtPurify(
+ new NlExtPurify(d_preprocessingPassContext.get()));
std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
new QuantifiersPreprocess(d_preprocessingPassContext.get()));
std::unique_ptr<PseudoBooleanProcessor> pbProc(
std::move(globalNegate));
d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
+ d_preprocessingPassRegistry.registerPass("nl-ext-purify",
+ std::move(nlExtPurify));
d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
std::move(quantifiersPreprocess));
d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
std::move(sepSkolemEmp));
d_preprocessingPassRegistry.registerPass("sort-inference",
std::move(sortInfer));
- d_preprocessingPassRegistry.registerPass("static-learning",
+ d_preprocessingPassRegistry.registerPass("static-learning",
std::move(staticLearning));
d_preprocessingPassRegistry.registerPass("sygus-infer",
std::move(sygusInfer));
return result.top();
}
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-
-Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) {
- if( beneathMult ){
- NodeMap::iterator find = bcache.find(n);
- if (find != bcache.end()) {
- return (*find).second;
- }
- }else{
- NodeMap::iterator find = cache.find(n);
- if (find != cache.end()) {
- return (*find).second;
- }
- }
- Node ret = n;
- if( n.getNumChildren()>0 ){
- if (beneathMult
- && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
- {
- // don't do it if it rewrites to a constant
- Node nr = Rewriter::rewrite(n);
- if (nr.isConst())
- {
- // return the rewritten constant
- ret = nr;
- }
- else
- {
- // new variable
- ret = NodeManager::currentNM()->mkSkolem(
- "__purifyNl_var",
- n.getType(),
- "Variable introduced in purifyNl pass");
- Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
- var_eq.push_back(np.eqNode(ret));
- Trace("nl-ext-purify")
- << "Purify : " << ret << " -> " << np << std::endl;
- }
- }
- else
- {
- bool beneathMultNew = beneathMult || n.getKind()==kind::MULT;
- bool childChanged = false;
- std::vector< Node > children;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew );
- childChanged = childChanged || nc!=n[i];
- children.push_back( nc );
- }
- if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- }
- if( beneathMult ){
- bcache[n] = ret;
- }else{
- cache[n] = ret;
- }
- return ret;
-}
-
// do dumping (before/after any preprocessing pass)
static void dumpAssertions(const char* key,
const AssertionPipeline& assertionList) {
}
if( options::nlExtPurify() ){
- unordered_map<Node, Node, NodeHashFunction> cache;
- unordered_map<Node, Node, NodeHashFunction> bcache;
- std::vector< Node > var_eq;
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Node a = d_assertions[i];
- d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq));
- Trace("nl-ext-purify")
- << "Purify : " << a << " -> " << d_assertions[i] << std::endl;
- }
- if( !var_eq.empty() ){
- unsigned lastIndex = d_assertions.size()-1;
- var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
- d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
- }
+ d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions);
}
if( options::ceGuidedInst() ){
Assert( inst_qs.size()<=1 );
Node ret_n;
if( inst_qs.size()==1 ){
- Node top_q = inst_qs[0];
+ Node top_q = inst_qs[0];
//Node top_q = Rewriter::rewrite( nn_e ).negate();
Assert( top_q.getKind()==kind::FORALL );
Trace("smt-qe") << "Get qe for " << top_q << std::endl;
AlwaysAssert(!d_fullyInited,
"Cannot set replay stream once fully initialized");
d_replayStream = replayStream;
-}
+}
bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
return d_private->getExpressionName(e, name);
projects / cvc5.git / commitdiff