From ac7db6796f2255678d3b2e2e87940211f162223e Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 22 Aug 2018 21:13:46 -0700 Subject: [PATCH] global-negate preprocessing pass (#2317) --- src/Makefile.am | 4 +- .../passes}/global_negate.cpp | 44 ++++++++------- src/preprocessing/passes/global_negate.h | 52 ++++++++++++++++++ src/smt/smt_engine.cpp | 9 ++-- src/theory/quantifiers/global_negate.h | 53 ------------------- 5 files changed, 85 insertions(+), 77 deletions(-) rename src/{theory/quantifiers => preprocessing/passes}/global_negate.cpp (71%) create mode 100644 src/preprocessing/passes/global_negate.h delete mode 100644 src/theory/quantifiers/global_negate.h diff --git a/src/Makefile.am b/src/Makefile.am index 40aa1a5af..6a21566e0 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/bv_intro_pow2.h \ preprocessing/passes/extended_rewriter_pass.cpp \ preprocessing/passes/extended_rewriter_pass.h \ + preprocessing/passes/global_negate.cpp \ + preprocessing/passes/global_negate.h \ preprocessing/passes/int_to_bv.cpp \ preprocessing/passes/int_to_bv.h \ preprocessing/passes/ite_removal.cpp \ @@ -462,8 +464,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fmf/model_engine.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/fun_def_process.h \ - theory/quantifiers/global_negate.cpp \ - theory/quantifiers/global_negate.h \ theory/quantifiers/instantiate.cpp \ theory/quantifiers/instantiate.h \ theory/quantifiers/inst_match.cpp \ diff --git a/src/theory/quantifiers/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp similarity index 71% rename from src/theory/quantifiers/global_negate.cpp rename to src/preprocessing/passes/global_negate.cpp index 0670b5c5b..ddebf961f 100644 --- a/src/theory/quantifiers/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -12,21 +12,22 @@ ** \brief Implementation of global_negate **/ -#include "theory/quantifiers/global_negate.h" +#include "preprocessing/passes/global_negate.h" +#include +#include "expr/node.h" #include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; +using namespace CVC4::theory; namespace CVC4 { -namespace theory { -namespace quantifiers { +namespace preprocessing { +namespace passes { -void GlobalNegate::simplify(std::vector& assertions) +Node GlobalNegate::simplify(std::vector& assertions, NodeManager* nm) { - NodeManager* nm = NodeManager::currentNM(); Assert(!assertions.empty()); - Trace("cbqi-gn") << "Global negate : " << std::endl; // collect free variables in all assertions std::vector free_vars; @@ -90,21 +91,26 @@ void GlobalNegate::simplify(std::vector& assertions) Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; body = Rewriter::rewrite(body); Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + return body; +} - Node truen = nm->mkConst(true); - for (unsigned i = 0, size = assertions.size(); i < size; i++) +GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "global-negate"){}; + +PreprocessingPassResult GlobalNegate::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm); + Node trueNode = nm->mkConst(true); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - if (i == 0) - { - assertions[i] = body; - } - else - { - assertions[i] = truen; - } + assertionsToPreprocess->replace(i, trueNode); } + assertionsToPreprocess->push_back(simplifiedNode); + return PreprocessingPassResult::NO_CONFLICT; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h new file mode 100644 index 000000000..0330aa10e --- /dev/null +++ b/src/preprocessing/passes/global_negate.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file global_negate.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 global_negate preprocessing pass + * Updates a set of assertions to the negation of + * these assertions. In detail, if assertions is: + * F1, ..., Fn + * then we update this vector to: + * forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true + * where x1...xm are the free variables of F1...Fn. + * When this is done, d_globalNegation flag is marked, so that the solver checks + *for unsat instead of sat. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class GlobalNegate : public PreprocessingPass +{ + public: + GlobalNegate(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node simplify(std::vector& assertions, NodeManager* nm); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9ea2f1ac..33ca6eb3d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,6 +79,7 @@ #include "preprocessing/passes/bv_intro_pow2.h" #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/pseudo_boolean_processor.h" @@ -115,7 +116,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" @@ -2660,6 +2660,8 @@ void SmtEnginePrivate::finishInit() new BVToBool(d_preprocessingPassContext.get())); std::unique_ptr extRewPre( new ExtRewPre(d_preprocessingPassContext.get())); + std::unique_ptr globalNegate( + new GlobalNegate(d_preprocessingPassContext.get())); std::unique_ptr intToBV( new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr quantifiersPreprocess( @@ -2701,6 +2703,8 @@ void SmtEnginePrivate::finishInit() std::move(bvIntroPow2)); d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); + d_preprocessingPassRegistry.registerPass("global-negate", + std::move(globalNegate)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", std::move(quantifiersPreprocess)); @@ -4085,8 +4089,7 @@ void SmtEnginePrivate::processAssertions() { if (options::globalNegate()) { // global negation of the formula - quantifiers::GlobalNegate gn; - gn.simplify(d_assertions.ref()); + d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions); d_smt.d_globalNegation = !d_smt.d_globalNegation; } diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h deleted file mode 100644 index f5d92c478..000000000 --- a/src/theory/quantifiers/global_negate.h +++ /dev/null @@ -1,53 +0,0 @@ -/********************* */ -/*! \file global_negate.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** 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 global_negate - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H -#define __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H - -#include -#include "expr/node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** GlobalNegate - * - * This class updates a set of assertions to be equivalent to the negation of - * these assertions. In detail, if assertions is: - * F1, ..., Fn - * then we update this vector to: - * forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true - * where x1...xm are the free variables of F1...Fn. - */ -class GlobalNegate -{ - public: - GlobalNegate() {} - ~GlobalNegate() {} - /** simplify assertions - * - * Replaces assertions with a set of assertions that is equivalent to its - * negation. - */ - void simplify(std::vector& assertions); -}; - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */ -- 2.30.2