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 \
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 \
--- /dev/null
+/********************* */
+/*! \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 <vector>
+#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<Node>& assertions, NodeManager* nm)
+{
+ Assert(!assertions.empty());
+ Trace("cbqi-gn") << "Global negate : " << std::endl;
+ // collect free variables in all assertions
+ std::vector<Node> free_vars;
+ std::vector<TNode> visit;
+ std::unordered_set<TNode, TNodeHashFunction> 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<Node> 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
--- /dev/null
+/********************* */
+/*! \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<Node>& assertions, NodeManager* nm);
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
#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"
#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"
new BVToBool(d_preprocessingPassContext.get()));
std::unique_ptr<ExtRewPre> extRewPre(
new ExtRewPre(d_preprocessingPassContext.get()));
+ std::unique_ptr<GlobalNegate> globalNegate(
+ new GlobalNegate(d_preprocessingPassContext.get()));
std::unique_ptr<IntToBV> intToBV(
new IntToBV(d_preprocessingPassContext.get()));
std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
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));
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;
}
+++ /dev/null
-/********************* */
-/*! \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<Node>& assertions)
-{
- NodeManager* nm = NodeManager::currentNM();
- Assert(!assertions.empty());
-
- Trace("cbqi-gn") << "Global negate : " << std::endl;
- // collect free variables in all assertions
- std::vector<Node> free_vars;
- std::vector<TNode> visit;
- std::unordered_set<TNode, TNodeHashFunction> 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<Node> 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 */
+++ /dev/null
-/********************* */
-/*! \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 <vector>
-#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<Node>& assertions);
-};
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */
projects / cvc5.git / commitdiff