From: yoni206 Date: Thu, 23 Aug 2018 04:13:46 +0000 (-0700) Subject: global-negate preprocessing pass (#2317) X-Git-Tag: cvc5-1.0.0~4736 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ac7db6796f2255678d3b2e2e87940211f162223e;p=cvc5.git global-negate preprocessing pass (#2317) --- 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/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp new file mode 100644 index 000000000..ddebf961f --- /dev/null +++ b/src/preprocessing/passes/global_negate.cpp @@ -0,0 +1,116 @@ +/********************* */ +/*! \file global_negate.cpp + ** \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 Implementation of global_negate + **/ + +#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 preprocessing { +namespace passes { + +Node GlobalNegate::simplify(std::vector& assertions, NodeManager* nm) +{ + Assert(!assertions.empty()); + Trace("cbqi-gn") << "Global negate : " << std::endl; + // collect free variables in all assertions + std::vector free_vars; + std::vector visit; + std::unordered_set visited; + for (const Node& as : assertions) + { + Trace("cbqi-gn") << " " << as << std::endl; + TNode cur = as; + // compute free variables + visit.push_back(cur); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar() && cur.getKind() != BOUND_VARIABLE) + { + free_vars.push_back(cur); + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + } + + Node body; + if (assertions.size() == 1) + { + body = assertions[0]; + } + else + { + body = nm->mkNode(AND, assertions); + } + + // do the negation + body = body.negate(); + + if (!free_vars.empty()) + { + std::vector bvs; + for (const Node& v : free_vars) + { + Node bv = nm->mkBoundVar(v.getType()); + bvs.push_back(bv); + } + + body = body.substitute( + free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end()); + + Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs); + + body = nm->mkNode(FORALL, bvl, body); + } + + 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; +} + +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) + { + assertionsToPreprocess->replace(i, trueNode); + } + assertionsToPreprocess->push_back(simplifiedNode); + return PreprocessingPassResult::NO_CONFLICT; +} + +} // 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.cpp b/src/theory/quantifiers/global_negate.cpp deleted file mode 100644 index 0670b5c5b..000000000 --- a/src/theory/quantifiers/global_negate.cpp +++ /dev/null @@ -1,110 +0,0 @@ -/********************* */ -/*! \file global_negate.cpp - ** \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 Implementation of global_negate - **/ - -#include "theory/quantifiers/global_negate.h" -#include "theory/rewriter.h" - -using namespace std; -using namespace CVC4::kind; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -void GlobalNegate::simplify(std::vector& assertions) -{ - NodeManager* nm = NodeManager::currentNM(); - Assert(!assertions.empty()); - - Trace("cbqi-gn") << "Global negate : " << std::endl; - // collect free variables in all assertions - std::vector free_vars; - std::vector visit; - std::unordered_set visited; - for (const Node& as : assertions) - { - Trace("cbqi-gn") << " " << as << std::endl; - TNode cur = as; - // compute free variables - visit.push_back(cur); - do - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur.isVar() && cur.getKind() != BOUND_VARIABLE) - { - free_vars.push_back(cur); - } - for (const TNode& cn : cur) - { - visit.push_back(cn); - } - } - } while (!visit.empty()); - } - - Node body; - if (assertions.size() == 1) - { - body = assertions[0]; - } - else - { - body = nm->mkNode(AND, assertions); - } - - // do the negation - body = body.negate(); - - if (!free_vars.empty()) - { - std::vector bvs; - for (const Node& v : free_vars) - { - Node bv = nm->mkBoundVar(v.getType()); - bvs.push_back(bv); - } - - body = body.substitute( - free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end()); - - Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs); - - body = nm->mkNode(FORALL, bvl, body); - } - - Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; - body = Rewriter::rewrite(body); - Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; - - Node truen = nm->mkConst(true); - for (unsigned i = 0, size = assertions.size(); i < size; i++) - { - if (i == 0) - { - assertions[i] = body; - } - else - { - assertions[i] = truen; - } - } -} - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ 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 */