preprocessing/passes/real_to_int.h \
preprocessing/passes/rewrite.cpp \
preprocessing/passes/rewrite.h \
+ preprocessing/passes/sep_skolem_emp.cpp \
+ preprocessing/passes/sep_skolem_emp.h \
preprocessing/passes/static_learning.cpp \
preprocessing/passes/static_learning.h \
preprocessing/passes/symmetry_breaker.cpp \
--- /dev/null
+/**********************/
+/*! \file sep_skolem_emp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Mathias Preiner, Yoni Zohar
+ ** 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 sep-pre-skolem-emp preprocessing pass
+ **
+ **/
+
+#include "preprocessing/passes/sep_skolem_emp.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+namespace {
+
+Node preSkolemEmp(Node n,
+ bool pol,
+ std::map<bool, std::map<Node, Node>>& visited)
+{
+ std::map<Node, Node>::iterator it = visited[pol].find(n);
+ if (it == visited[pol].end())
+ {
+ Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
+ << std::endl;
+ Node ret = n;
+ if (n.getKind() == kind::SEP_EMP)
+ {
+ if (!pol)
+ {
+ TypeNode tnx = n[0].getType();
+ TypeNode tny = n[1].getType();
+ Node x = NodeManager::currentNM()->mkSkolem(
+ "ex", tnx, "skolem location for negated emp");
+ Node y = NodeManager::currentNM()->mkSkolem(
+ "ey", tny, "skolem data for negated emp");
+ return NodeManager::currentNM()
+ ->mkNode(kind::SEP_STAR,
+ NodeManager::currentNM()->mkNode(kind::SEP_PTO, x, y),
+ NodeManager::currentNM()->mkConst(true))
+ .negate();
+ }
+ }
+ else if (n.getKind() != kind::FORALL && n.getNumChildren() > 0)
+ {
+ std::vector<Node> children;
+ bool childChanged = false;
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(n.getOperator());
+ }
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ bool newPol, newHasPol;
+ QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol);
+ Node nc = n[i];
+ if (newHasPol)
+ {
+ nc = preSkolemEmp(n[i], newPol, visited);
+ childChanged = childChanged || nc != n[i];
+ }
+ children.push_back(nc);
+ }
+ if (childChanged)
+ {
+ return NodeManager::currentNM()->mkNode(n.getKind(), children);
+ }
+ }
+ visited[pol][n] = ret;
+ return n;
+ }
+ else
+ {
+ return it->second;
+ }
+}
+
+} // namespace
+
+SepSkolemEmp::SepSkolemEmp(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "sep-skolem-emp"){};
+
+PreprocessingPassResult SepSkolemEmp::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ std::map<bool, std::map<Node, Node>> visited;
+ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+ {
+ Node prev = (*assertionsToPreprocess)[i];
+ bool pol = true;
+ Node next = preSkolemEmp(prev, pol, visited);
+ if (next != prev)
+ {
+ assertionsToPreprocess->replace(i, Rewriter::rewrite(next));
+ Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
+ Trace("sep-preprocess") << " ...got " << (*assertionsToPreprocess)[i]
+ << endl;
+ }
+ visited.clear();
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sep_skolem_emp.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Mathias Preiner, Yoni Zohar
+ ** 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 sep-pre-skolem-emp eprocessing pass
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+#define __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class SepSkolemEmp : public PreprocessingPass
+{
+ public:
+ SepSkolemEmp(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/real_to_int.h"
#include "preprocessing/passes/rewrite.h"
+#include "preprocessing/passes/sep_skolem_emp.h"
#include "preprocessing/passes/static_learning.h"
#include "preprocessing/passes/symmetry_breaker.h"
#include "preprocessing/passes/symmetry_detect.h"
new SymBreakerPass(d_preprocessingPassContext.get()));
std::unique_ptr<SynthRewRulesPass> srrProc(
new SynthRewRulesPass(d_preprocessingPassContext.get()));
- d_preprocessingPassRegistry.registerPass("apply-substs",
+ std::unique_ptr<SepSkolemEmp> sepSkolemEmp(
+ new SepSkolemEmp(d_preprocessingPassContext.get()));
+ d_preprocessingPassRegistry.registerPass("apply-substs",
std::move(applySubsts));
d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
d_preprocessingPassRegistry.registerPass("bv-abstraction",
std::move(pbProc));
d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
+ d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
+ std::move(sepSkolemEmp));
d_preprocessingPassRegistry.registerPass("static-learning",
std::move(staticLearning));
d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
Trace("smt") << "POST boolToBv" << endl;
}
if(options::sepPreSkolemEmp()) {
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Node prev = d_assertions[i];
- Node next = sep::TheorySepRewriter::preprocess( prev );
- if( next!=prev ){
- d_assertions.replace( i, Rewriter::rewrite( next ) );
- Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
- Trace("sep-preprocess") << " ...got " << d_assertions[i] << endl;
- }
- }
+ d_preprocessingPassRegistry.getPass("sep-skolem-emp")->apply(&d_assertions);
}
if( d_smt.d_logic.isQuantified() ){
return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
}
-Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) {
- std::map< Node, Node >::iterator it = visited[pol].find( n );
- if( it==visited[pol].end() ){
- Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
- Node ret = n;
- if( n.getKind()==kind::SEP_EMP ){
- if( !pol ){
- TypeNode tnx = n[0].getType();
- TypeNode tny = n[1].getType();
- Node x = NodeManager::currentNM()->mkSkolem( "ex", tnx, "skolem location for negated emp" );
- Node y = NodeManager::currentNM()->mkSkolem( "ey", tny, "skolem data for negated emp" );
- return NodeManager::currentNM()->mkNode( kind::SEP_STAR,
- NodeManager::currentNM()->mkNode( kind::SEP_PTO, x, y ),
- NodeManager::currentNM()->mkConst( true ) ).negate();
- }
- }else if( n.getKind()!=kind::FORALL && n.getNumChildren()>0 ){
- std::vector< Node > children;
- bool childChanged = false;
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newPol, newHasPol;
- QuantPhaseReq::getPolarity( n, i, true, pol, newHasPol, newPol );
- Node nc = n[i];
- if( newHasPol ){
- nc = preSkolemEmp( n[i], newPol, visited );
- childChanged = childChanged || nc!=n[i];
- }
- children.push_back( nc );
- }
- if( childChanged ){
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }
- }
- visited[pol][n] = ret;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node TheorySepRewriter::preprocess( Node n ) {
- if( options::sepPreSkolemEmp() ){
- bool pol = true;
- std::map< bool, std::map< Node, Node > > visited;
- n = preSkolemEmp( n, pol, visited );
- }
- return n;
-}
-
-
}/* CVC4::theory::sep namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
static inline void init() {}
static inline void shutdown() {}
-private:
- static Node preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited );
-public:
- static Node preprocess( Node n );
};/* class TheorySepRewriter */
}/* CVC4::theory::sep namespace */
regress0/sep/sep-01.smt2 \
regress0/sep/sep-plus1.smt2 \
regress0/sep/sep-simp-unsat-emp.smt2 \
+ regress0/sep/skolem_emp.smt2 \
regress0/sep/trees-1.smt2 \
regress0/sep/wand-crash.smt2 \
regress0/sets/abt-min.smt2 \
--- /dev/null
+; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(assert (not (emp 0 0)))
+(check-sat)
projects / cvc5.git / commitdiff