diff options
Diffstat (limited to 'src/preprocessing')
45 files changed, 890 insertions, 428 deletions
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index aea2554bd..cc9d1c2af 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H -#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H +#ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H +#define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H #include <vector> @@ -117,4 +117,4 @@ class AssertionPipeline } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ +#endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */ diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index ea8585506..f20ffa61e 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H -#define __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#ifndef CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/apply_to_const.h b/src/preprocessing/passes/apply_to_const.h index 3ff8dec75..4c1df22ca 100644 --- a/src/preprocessing/passes/apply_to_const.h +++ b/src/preprocessing/passes/apply_to_const.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H -#define __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H +#ifndef CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H +#define CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H #include <unordered_map> @@ -48,4 +48,4 @@ class ApplyToConst : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */ +#endif /* CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */ diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 57f69a6e3..11cb551fa 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H -#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -70,4 +70,4 @@ class BoolToBV : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */ diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index 963e99570..b5840b355 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H -#define __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -47,4 +47,4 @@ class BvAbstraction : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h index 645dd72aa..98d1080bd 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/bv_ackermann.h @@ -23,8 +23,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H -#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#define CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H #include <unordered_map> #include "expr/node.h" diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index c83a16491..4ed685855 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H -#define __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H +#define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -41,4 +41,4 @@ class BvEagerAtoms : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */ diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index fccdfa2f9..09d963ba3 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -37,47 +37,6 @@ namespace passes { namespace { -/** - * Represents the result of Gaussian Elimination where the solution - * of the given equation system is - * - * INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b, - * where ci, b and p are - * - bit-vector constants - * - extracts or zero extensions on bit-vector constants - * - of arbitrary nesting level - * and p is co-prime to all bit-vector constants for which - * a multiplicative inverse has to be computed. - * - * UNIQUE ... determined for all unknowns, e.g., x = 4 - * - * PARTIAL ... e.g., x = 4 - 2z - * - * NONE ... no solution - * - * Given a matrix A representing an equation system, the resulting - * matrix B after applying GE represents, e.g.: - * - * B = 1 0 0 2 <- UNIQUE - * 0 1 0 3 <- - * 0 0 1 1 <- - * - * B = 1 0 2 4 <- PARTIAL - * 0 1 3 2 <- - * 0 0 1 1 - * - * B = 1 0 0 1 NONE - * 0 1 1 2 - * 0 0 0 2 <- - */ -enum class Result -{ - INVALID, - UNIQUE, - PARTIAL, - NONE -}; - bool is_bv_const(Node n) { if (n.isConst()) { return true; } @@ -96,6 +55,8 @@ Integer get_bv_const_value(Node n) return get_bv_const(n).getConst<BitVector>().getValue(); } +} // namespace + /** * Determines if an overflow may occur in given 'expr'. * @@ -112,7 +73,7 @@ Integer get_bv_const_value(Node n) * will be handled via the default case, which is not incorrect but also not * necessarily the minimum. */ -unsigned getMinBwExpr(Node expr) +unsigned BVGauss::getMinBwExpr(Node expr) { std::vector<Node> visit; /* Maps visited nodes to the determined minimum bit-width required. */ @@ -280,10 +241,9 @@ unsigned getMinBwExpr(Node expr) * form) is stored in 'rhs' and 'lhs', i.e., the given matrix is overwritten * with the resulting matrix. */ -Result gaussElim( - Integer prime, - std::vector<Integer>& rhs, - std::vector<std::vector<Integer>>& lhs) +BVGauss::Result BVGauss::gaussElim(Integer prime, + std::vector<Integer>& rhs, + std::vector<std::vector<Integer>>& lhs) { Assert(prime > 0); Assert(lhs.size()); @@ -296,7 +256,7 @@ Result gaussElim( rhs = std::vector<Integer>(rhs.size(), Integer(0)); lhs = std::vector<std::vector<Integer>>( lhs.size(), std::vector<Integer>(lhs[0].size(), Integer(0))); - return Result::UNIQUE; + return BVGauss::Result::UNIQUE; } size_t nrows = lhs.size(); @@ -361,7 +321,7 @@ Result gaussElim( Integer inv = lhs[j][pcol].modInverse(prime); if (inv == -1) { - return Result::INVALID; /* not coprime */ + return BVGauss::Result::INVALID; /* not coprime */ } for (size_t k = pcol; k < ncols; ++k) { @@ -409,7 +369,7 @@ Result gaussElim( if (rhs[i] != 0) { /* no solution */ - return Result::NONE; + return BVGauss::Result::NONE; } continue; } @@ -426,9 +386,12 @@ Result gaussElim( } } - if (ispart) { return Result::PARTIAL; } + if (ispart) + { + return BVGauss::Result::PARTIAL; + } - return Result::UNIQUE; + return BVGauss::Result::UNIQUE; } /** @@ -452,7 +415,7 @@ Result gaussElim( * to result (modulo prime). These mapped results are added as constraints * of the form 'unknown = mapped result' in applyInternal. */ -Result gaussElimRewriteForUrem( +BVGauss::Result BVGauss::gaussElimRewriteForUrem( const std::vector<Node>& equations, std::unordered_map<Node, Node, NodeHashFunction>& res) { @@ -493,7 +456,7 @@ Result gaussElimRewriteForUrem( << "Minimum required bit-width exceeds given bit-width, " "will not apply Gaussian Elimination." << std::endl; - return Result::INVALID; + return BVGauss::Result::INVALID; } rhs.push_back(get_bv_const_value(eqrhs)); @@ -613,7 +576,7 @@ Result gaussElimRewriteForUrem( if (nrows < 1) { - return Result::INVALID; + return BVGauss::Result::INVALID; } for (size_t i = 0; i < nrows; ++i) @@ -631,13 +594,13 @@ Result gaussElimRewriteForUrem( if (lhs.size() > lhs[0].size()) { - return Result::INVALID; + return BVGauss::Result::INVALID; } Trace("bv-gauss-elim") << "Applying Gaussian Elimination..." << std::endl; - Result ret = gaussElim(iprime, rhs, lhs); + BVGauss::Result ret = gaussElim(iprime, rhs, lhs); - if (ret != Result::NONE && ret != Result::INVALID) + if (ret != BVGauss::Result::NONE && ret != BVGauss::Result::INVALID) { std::vector<Node> vvars; for (const auto& p : vars) { vvars.push_back(p.first); } @@ -645,7 +608,7 @@ Result gaussElimRewriteForUrem( Assert(nrows == lhs.size()); Assert(nrows == rhs.size()); NodeManager *nm = NodeManager::currentNM(); - if (ret == Result::UNIQUE) + if (ret == BVGauss::Result::UNIQUE) { for (size_t i = 0; i < nvars; ++i) { @@ -655,7 +618,7 @@ Result gaussElimRewriteForUrem( } else { - Assert(ret == Result::PARTIAL); + Assert(ret == BVGauss::Result::PARTIAL); for (size_t pcol = 0, prow = 0; pcol < nvars && prow < nrows; ++pcol, ++prow) @@ -712,10 +675,6 @@ Result gaussElimRewriteForUrem( return ret; } -} // namespace - - - BVGauss::BVGauss(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bv-gauss") { @@ -772,20 +731,20 @@ PreprocessingPassResult BVGauss::applyInternal( if (eq.second.size() <= 1) { continue; } std::unordered_map<Node, Node, NodeHashFunction> res; - Result ret = gaussElimRewriteForUrem(eq.second, res); + BVGauss::Result ret = gaussElimRewriteForUrem(eq.second, res); Trace("bv-gauss-elim") << "result: " - << (ret == Result::INVALID + << (ret == BVGauss::Result::INVALID ? "INVALID" - : (ret == Result::UNIQUE + : (ret == BVGauss::Result::UNIQUE ? "UNIQUE" - : (ret == Result::PARTIAL + : (ret == BVGauss::Result::PARTIAL ? "PARTIAL" : "NONE"))) << std::endl; - if (ret != Result::INVALID) + if (ret != BVGauss::Result::INVALID) { NodeManager *nm = NodeManager::currentNM(); - if (ret == Result::NONE) + if (ret == BVGauss::Result::NONE) { atpp.clear(); atpp.push_back(nm->mkConst<bool>(false)); diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index e991b17c4..93d61be9e 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H -#define __CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -30,7 +30,7 @@ namespace passes { class BVGauss : public PreprocessingPass { public: - BVGauss(PreprocessingPassContext* preprocContext); + BVGauss(PreprocessingPassContext* preprocContext); protected: /** @@ -42,8 +42,63 @@ class BVGauss : public PreprocessingPass * succeed modulo a prime number, which is not necessarily the case if a * given set of equations is modulo a non-prime number. */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /* Note: The following functionality is only exposed for unit testing in + * pass_bv_gauss_white.h. */ + + /** + * Represents the result of Gaussian Elimination where the solution + * of the given equation system is + * + * INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b, + * where ci, b and p are + * - bit-vector constants + * - extracts or zero extensions on bit-vector constants + * - of arbitrary nesting level + * and p is co-prime to all bit-vector constants for which + * a multiplicative inverse has to be computed. + * + * UNIQUE ... determined for all unknowns, e.g., x = 4 + * + * PARTIAL ... e.g., x = 4 - 2z + * + * NONE ... no solution + * + * Given a matrix A representing an equation system, the resulting + * matrix B after applying GE represents, e.g.: + * + * B = 1 0 0 2 <- UNIQUE + * 0 1 0 3 <- + * 0 0 1 1 <- + * + * B = 1 0 2 4 <- PARTIAL + * 0 1 3 2 <- + * 0 0 1 1 + * + * B = 1 0 0 1 NONE + * 0 1 1 2 + * 0 0 0 2 <- + */ + enum class Result + { + INVALID, + UNIQUE, + PARTIAL, + NONE + }; + + static Result gaussElim(Integer prime, + std::vector<Integer>& rhs, + std::vector<std::vector<Integer>>& lhs); + + static Result gaussElimRewriteForUrem( + const std::vector<Node>& equations, + std::unordered_map<Node, Node, NodeHashFunction>& res); + + static unsigned getMinBwExpr(Node expr); }; } // namespace passes diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index c0238b01e..86d5ebfef 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H -#define __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H +#define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -42,4 +42,4 @@ class BvIntroPow2 : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */ diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 83502e3d8..dc0494943 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H -#define __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -76,4 +76,4 @@ class BVToBool : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ +#endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */ diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index aa379329b..dbaaa05ad 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H -#define __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#ifndef CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H +#define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,4 +40,4 @@ class ExtRewPre : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */ diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 84d78d959..89c3a3e3e 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -22,8 +22,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H -#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_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" @@ -49,4 +49,4 @@ class GlobalNegate : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ +#endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp new file mode 100644 index 000000000..65945f0d7 --- /dev/null +++ b/src/preprocessing/passes/ho_elim.cpp @@ -0,0 +1,543 @@ +/********************* */ +/*! \file ho_elim.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 HoElim preprocessing pass + ** + ** Eliminates higher-order constraints. + **/ + +#include "preprocessing/passes/ho_elim.h" + +#include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" +#include "theory/rewriter.h" +#include "theory/uf/theory_uf_rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +HoElim::HoElim(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "ho-elim"){}; + +Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + + if (it == d_visited.end()) + { + if (cur.getKind() == LAMBDA) + { + Trace("ho-elim-ll") << "Lambda lift: " << cur << std::endl; + // must also get free variables in lambda + std::vector<Node> lvars; + std::vector<TypeNode> ftypes; + std::unordered_set<Node, NodeHashFunction> fvs; + expr::getFreeVariables(cur, fvs); + std::vector<Node> nvars; + std::vector<Node> vars; + Node sbd = cur[1]; + if (!fvs.empty()) + { + Trace("ho-elim-ll") + << "Has " << fvs.size() << " free variables" << std::endl; + for (const Node& v : fvs) + { + TypeNode vt = v.getType(); + ftypes.push_back(vt); + Node vs = nm->mkBoundVar(vt); + vars.push_back(v); + nvars.push_back(vs); + lvars.push_back(vs); + } + sbd = sbd.substitute( + vars.begin(), vars.end(), nvars.begin(), nvars.end()); + } + for (const Node& bv : cur[0]) + { + TypeNode bvt = bv.getType(); + ftypes.push_back(bvt); + lvars.push_back(bv); + } + Node nlambda = cur; + if (!fvs.empty()) + { + nlambda = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lvars), sbd); + Trace("ho-elim-ll") + << "...new lambda definition: " << nlambda << std::endl; + } + TypeNode rangeType = cur.getType().getRangeType(); + TypeNode nft = nm->mkFunctionType(ftypes, rangeType); + Node nf = nm->mkSkolem("ll", nft); + Trace("ho-elim-ll") + << "...introduce: " << nf << " of type " << nft << std::endl; + newLambda[nf] = nlambda; + Assert(nf.getType() == nlambda.getType()); + if (!vars.empty()) + { + for (const Node& v : vars) + { + nf = nm->mkNode(HO_APPLY, nf, v); + } + Trace("ho-elim-ll") << "...partial application: " << nf << std::endl; + } + d_visited[cur] = nf; + Trace("ho-elim-ll") << "...return types : " << nf.getType() << " " + << cur.getType() << std::endl; + Assert(nf.getType() == cur.getType()); + } + else + { + d_visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = d_visited.find(cn); + Assert(it != d_visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + d_visited[cur] = ret; + } + } while (!visit.empty()); + Assert(d_visited.find(n) != d_visited.end()); + Assert(!d_visited.find(n)->second.isNull()); + return d_visited[n]; +} + +Node HoElim::eliminateHo(Node n) +{ + Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::map<Node, Node> preReplace; + std::map<Node, Node>::iterator itr; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_visited.find(cur); + Trace("ho-elim-visit") << "Process: " << cur << std::endl; + + if (it == d_visited.end()) + { + TypeNode tn = cur.getType(); + // lambdas are already eliminated by now + Assert(cur.getKind() != LAMBDA); + if (tn.isFunction()) + { + d_funTypes.insert(tn); + } + if (cur.isVar()) + { + Node ret = cur; + if (options::hoElim()) + { + if (tn.isFunction()) + { + TypeNode ut = getUSort(tn); + if (cur.getKind() == BOUND_VARIABLE) + { + ret = nm->mkBoundVar(ut); + } + else + { + ret = nm->mkSkolem("k", ut); + } + // must get the ho apply to ensure extensionality is applied + Node hoa = getHoApplyUf(tn); + Trace("ho-elim-visit") << "Hoa is " << hoa << std::endl; + } + } + d_visited[cur] = ret; + } + else + { + d_visited[cur] = Node::null(); + if (cur.getKind() == APPLY_UF && options::hoElim()) + { + Node op = cur.getOperator(); + // convert apply uf with variable arguments eagerly to ho apply + // chains, so they are processed uniformly. + visit.push_back(cur); + Node newCur = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(cur); + preReplace[cur] = newCur; + cur = newCur; + d_visited[cur] = Node::null(); + } + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + itr = preReplace.find(cur); + if (itr != preReplace.end()) + { + Trace("ho-elim-visit") + << "return (pre-repl): " << d_visited[itr->second] << std::endl; + d_visited[cur] = d_visited[itr->second]; + } + else + { + bool childChanged = false; + std::vector<Node> children; + std::vector<TypeNode> childrent; + bool typeChanged = false; + for (const Node& cn : ret) + { + it = d_visited.find(cn); + Assert(it != d_visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + TypeNode ct = it->second.getType(); + childrent.push_back(ct); + typeChanged = typeChanged || ct != cn.getType(); + } + if (ret.getMetaKind() == metakind::PARAMETERIZED) + { + // child of an argument changed type, must change type + Node op = ret.getOperator(); + Node retOp = op; + Trace("ho-elim-visit") + << "Process op " << op << ", typeChanged = " << typeChanged + << std::endl; + if (typeChanged) + { + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator ito = + d_visited_op.find(op); + if (ito == d_visited_op.end()) + { + Assert(!childrent.empty()); + TypeNode newFType = nm->mkFunctionType(childrent, cur.getType()); + retOp = nm->mkSkolem("rf", newFType); + d_visited_op[op] = retOp; + } + else + { + retOp = ito->second; + } + } + children.insert(children.begin(), retOp); + } + // process ho apply + if (ret.getKind() == HO_APPLY && options::hoElim()) + { + TypeNode tnr = ret.getType(); + tnr = getUSort(tnr); + Node hoa = + getHoApplyUf(children[0].getType(), children[1].getType(), tnr); + std::vector<Node> hchildren; + hchildren.push_back(hoa); + hchildren.push_back(children[0]); + hchildren.push_back(children[1]); + ret = nm->mkNode(APPLY_UF, hchildren); + } + else if (childChanged) + { + ret = nm->mkNode(ret.getKind(), children); + } + Trace("ho-elim-visit") << "return (pre-repl): " << ret << std::endl; + d_visited[cur] = ret; + } + } + } while (!visit.empty()); + Assert(d_visited.find(n) != d_visited.end()); + Assert(!d_visited.find(n)->second.isNull()); + Trace("ho-elim-assert") << "...got : " << d_visited[n] << std::endl; + return d_visited[n]; +} + +PreprocessingPassResult HoElim::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + // step [1]: apply lambda lifting to eliminate all lambdas + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> axioms; + std::map<Node, Node> newLambda; + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + Node res = eliminateLambdaComplete(prev, newLambda); + if (res != prev) + { + res = theory::Rewriter::rewrite(res); + Assert(!expr::hasFreeVar(res)); + assertionsToPreprocess->replace(i, res); + } + } + // do lambda lifting on new lambda definitions + // this will do fixed point to eliminate lambdas within lambda lifting axioms. + while (!newLambda.empty()) + { + std::map<Node, Node> lproc = newLambda; + newLambda.clear(); + for (const std::pair<Node, Node>& l : lproc) + { + Node lambda = l.second; + std::vector<Node> vars; + std::vector<Node> nvars; + for (const Node& v : lambda[0]) + { + Node bv = nm->mkBoundVar(v.getType()); + vars.push_back(v); + nvars.push_back(bv); + } + + Node bd = lambda[1].substitute( + vars.begin(), vars.end(), nvars.begin(), nvars.end()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, nvars); + + nvars.insert(nvars.begin(), l.first); + Node curr = nm->mkNode(APPLY_UF, nvars); + + Node llfax = nm->mkNode(FORALL, bvl, curr.eqNode(bd)); + Trace("ho-elim-ax") << "Lambda lifting axiom (pre-elim) " << llfax + << " for " << lambda << std::endl; + Assert(!expr::hasFreeVar(llfax)); + Node llfaxe = eliminateLambdaComplete(llfax, newLambda); + Trace("ho-elim-ax") << "Lambda lifting axiom " << llfaxe << " for " + << lambda << std::endl; + axioms.push_back(llfaxe); + } + } + + d_visited.clear(); + // add lambda lifting axioms as a conjunction to the first assertion + if (!axioms.empty()) + { + Node orig = (*assertionsToPreprocess)[0]; + axioms.push_back(orig); + Node conj = nm->mkNode(AND, axioms); + conj = theory::Rewriter::rewrite(conj); + Assert(!expr::hasFreeVar(conj)); + assertionsToPreprocess->replace(0, conj); + } + axioms.clear(); + + // step [2]: eliminate all higher-order constraints + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + Node prev = (*assertionsToPreprocess)[i]; + Node res = eliminateHo(prev); + if (res != prev) + { + res = theory::Rewriter::rewrite(res); + Assert(!expr::hasFreeVar(res)); + assertionsToPreprocess->replace(i, res); + } + } + // extensionality: process all function types + for (const TypeNode& ftn : d_funTypes) + { + if (options::hoElim()) + { + Node h = getHoApplyUf(ftn); + Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl; + TypeNode ft = h.getType(); + TypeNode uf = getUSort(ft[0]); + TypeNode ut = getUSort(ft[1]); + // extensionality + Node x = nm->mkBoundVar("x", uf); + Node y = nm->mkBoundVar("y", uf); + Node z = nm->mkBoundVar("z", ut); + Node eq = + nm->mkNode(APPLY_UF, h, x, z).eqNode(nm->mkNode(APPLY_UF, h, y, z)); + Node antec = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, z), eq); + Node conc = x.eqNode(y); + Node ax = nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, x, y), + nm->mkNode(OR, antec.negate(), conc)); + axioms.push_back(ax); + Trace("ho-elim-ax") << "...ext axiom : " << ax << std::endl; + // Make the "store" axiom, which asserts for every function, there + // exists another function that acts like the "store" operator for + // arrays, e.g. it is the same function with one I/O pair updated. + // Without this axiom, the translation is model unsound. + if (options::hoElimStoreAx()) + { + Node u = nm->mkBoundVar("u", uf); + Node v = nm->mkBoundVar("v", uf); + Node i = nm->mkBoundVar("i", ut); + Node ii = nm->mkBoundVar("ii", ut); + Node huii = nm->mkNode(APPLY_UF, h, u, ii); + Node e = nm->mkBoundVar("e", huii.getType()); + Node store = nm->mkNode( + FORALL, + nm->mkNode(BOUND_VAR_LIST, u, e, i), + nm->mkNode(EXISTS, + nm->mkNode(BOUND_VAR_LIST, v), + nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, ii), + nm->mkNode(APPLY_UF, h, v, ii) + .eqNode(nm->mkNode( + ITE, ii.eqNode(i), e, huii))))); + axioms.push_back(store); + Trace("ho-elim-ax") << "...store axiom : " << store << std::endl; + } + } + else if (options::hoElimStoreAx()) + { + Node u = nm->mkBoundVar("u", ftn); + Node v = nm->mkBoundVar("v", ftn); + std::vector<TypeNode> argTypes = ftn.getArgTypes(); + Node i = nm->mkBoundVar("i", argTypes[0]); + Node ii = nm->mkBoundVar("ii", argTypes[0]); + Node huii = nm->mkNode(HO_APPLY, u, ii); + Node e = nm->mkBoundVar("e", huii.getType()); + Node store = nm->mkNode( + FORALL, + nm->mkNode(BOUND_VAR_LIST, u, e, i), + nm->mkNode( + EXISTS, + nm->mkNode(BOUND_VAR_LIST, v), + nm->mkNode(FORALL, + nm->mkNode(BOUND_VAR_LIST, ii), + nm->mkNode(HO_APPLY, v, ii) + .eqNode(nm->mkNode(ITE, ii.eqNode(i), e, huii))))); + axioms.push_back(store); + Trace("ho-elim-ax") << "...store (ho_apply) axiom : " << store + << std::endl; + } + } + // add new axioms as a conjunction to the first assertion + if (!axioms.empty()) + { + Node orig = (*assertionsToPreprocess)[0]; + axioms.push_back(orig); + Node conj = nm->mkNode(AND, axioms); + conj = theory::Rewriter::rewrite(conj); + Assert(!expr::hasFreeVar(conj)); + assertionsToPreprocess->replace(0, conj); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +Node HoElim::getHoApplyUf(TypeNode tn) +{ + TypeNode tnu = getUSort(tn); + TypeNode rangeType = tn.getRangeType(); + std::vector<TypeNode> argTypes = tn.getArgTypes(); + TypeNode tna = getUSort(argTypes[0]); + + TypeNode tr = rangeType; + if (argTypes.size() > 1) + { + std::vector<TypeNode> remArgTypes; + remArgTypes.insert(remArgTypes.end(), argTypes.begin() + 1, argTypes.end()); + tr = NodeManager::currentNM()->mkFunctionType(remArgTypes, tr); + } + TypeNode tnr = getUSort(tr); + + return getHoApplyUf(tnu, tna, tnr); +} + +Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr) +{ + std::map<TypeNode, Node>::iterator it = d_hoApplyUf.find(tnf); + if (it == d_hoApplyUf.end()) + { + NodeManager* nm = NodeManager::currentNM(); + + std::vector<TypeNode> hoTypeArgs; + hoTypeArgs.push_back(tnf); + hoTypeArgs.push_back(tna); + TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr); + Node k = NodeManager::currentNM()->mkSkolem("ho", tnh); + d_hoApplyUf[tnf] = k; + return k; + } + return it->second; +} + +TypeNode HoElim::getUSort(TypeNode tn) +{ + if (!tn.isFunction()) + { + return tn; + } + std::map<TypeNode, TypeNode>::iterator it = d_ftypeMap.find(tn); + if (it == d_ftypeMap.end()) + { + // flatten function arguments + std::vector<TypeNode> argTypes = tn.getArgTypes(); + TypeNode rangeType = tn.getRangeType(); + bool typeChanged = false; + for (unsigned i = 0; i < argTypes.size(); i++) + { + if (argTypes[i].isFunction()) + { + argTypes[i] = getUSort(argTypes[i]); + typeChanged = true; + } + } + TypeNode s; + if (typeChanged) + { + TypeNode ntn = + NodeManager::currentNM()->mkFunctionType(argTypes, rangeType); + s = getUSort(ntn); + } + else + { + std::stringstream ss; + ss << "u_" << tn; + s = NodeManager::currentNM()->mkSort(ss.str()); + } + d_ftypeMap[tn] = s; + return s; + } + return it->second; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h new file mode 100644 index 000000000..f0de321c4 --- /dev/null +++ b/src/preprocessing/passes/ho_elim.h @@ -0,0 +1,151 @@ +/********************* */ +/*! \file ho_elim.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 HoElim preprocessing pass + ** + ** Eliminates higher-order constraints. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H +#define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** Higher-order elimination. + * + * This preprocessing pass eliminates all occurrences of higher-order + * constraints in the input, and replaces the entire input problem with + * an equisatisfiable one. This is based on the following steps. + * + * [1] Eliminate all occurrences of lambdas via lambda lifting. This includes + * lambdas with free variables that occur in quantifier bodies (see + * documentation for eliminateLambdaComplete). + * + * [2] Eliminate all occurrences of partial applications and constraints + * involving functions as first-class members. This is done by first + * turning all function applications into an applicative encoding involving the + * parametric binary operator @ (of kind HO_APPLY). Then we introduce: + * - An uninterpreted sort U(T) for each function type T, + * - A function H(f) of sort U(T1) x .. x U(Tn) -> U(T) for each function f + * of sort T1 x ... x Tn -> T. + * - A function App_{T1 x T2 ... x Tn -> T} of type + * U(T1 x T2 ... x Tn -> T) x U(T1) -> U(T2 ... x Tn -> T) + * for each occurrence of @ applied to arguments of types T1 x T2 ... x Tn -> T + * and T1. + * + * [3] Add additional axioms to ensure the correct interpretation of + * the sorts U(...), and functions App_{...}. This includes: + * + * - The "extensionality" axiom for App_{...} terms, stating that functions + * that behave the same according to App for all inputs must be equal: + * forall x : U(T1->T2), y : U(T1->T2). + * ( forall z : T1. App_{T1->T2}( x, z ) = App_{T1->T2}( y, z ) ) => + * x = y + * + * - The "store" axiom, which effectively states that for all (encoded) + * functions f, there exists a function g that behaves identically to f, except + * that g for argument i is e: + * forall x : U(T1->T2), i : U(T1), e : U(T2). + * exists g : U(T1->T2). + * forall z: T1. + * App_{T1->T2}( g, z ) = ite( z = i, e, App_{T1->T2}( f, z ) ). + * + * + * Based on options, this preprocessing pass may apply a subset o the above + * steps. In particular: + * * If options::hoElim() is true, then step [2] is taken and extensionality + * axioms are added in step [3]. + * * If options::hoElimStoreAx() is true, then store axioms are added in step 3. + * The form of these axioms depends on whether options::hoElim() is true. If it + * is true, the axiom is given in terms of the uninterpreted functions that + * encode function sorts. If it is false, then the store axiom is given in terms + * of the original function sorts. + */ +class HoElim : public PreprocessingPass +{ + public: + HoElim(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + /** + * Eliminate all occurrences of lambdas in term n, return the result. This + * is step [1] mentioned at the header of this class. + * + * The map newLambda maps newly introduced function skolems with their + * (lambda) definition, which is a closed term. + * + * Notice that to ensure that all lambda definitions are closed, we + * introduce extra bound arguments to the lambda, for example: + * forall x. (lambda y. x+y) != f + * becomes + * forall x. g(x) != f + * where g is mapped to the (closed) term ( lambda xy. x+y ). + * + * Notice that the definitions in newLambda may themselves contain lambdas, + * hence, this method is run until a fix point is reached. + */ + Node eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda); + + /** + * Eliminate all higher-order constraints in n, return the result. This is + * step [2] mentioned at the header of this class. + */ + Node eliminateHo(Node n); + /** + * Stores the set of nodes we have current visited and their results + * in steps [1] and [2] of this pass. + */ + std::unordered_map<TNode, Node, TNodeHashFunction> d_visited; + /** + * Stores the mapping from functions f to their corresponding function H(f) + * in the encoding for step [2] of this pass. + */ + std::unordered_map<TNode, Node, TNodeHashFunction> d_visited_op; + /** The set of all function types encountered in assertions. */ + std::unordered_set<TypeNode, TypeNodeHashFunction> d_funTypes; + + /** + * Get ho apply uf, this returns App_{@_{T1 x T2 ... x Tn -> T}} + */ + Node getHoApplyUf(TypeNode tn); + /** + * Get ho apply uf, where: + * tn is T1 x T2 ... x Tn -> T, + * tna is T1, + * tnr is T2 ... x Tn -> T + * This returns App_{@_{T1 x T2 ... x Tn -> T}}. + */ + Node getHoApplyUf(TypeNode tn, TypeNode tna, TypeNode tnr); + /** cache of getHoApplyUf */ + std::map<TypeNode, Node> d_hoApplyUf; + /** + * Get uninterpreted sort for function sort. This returns U(T) for function + * type T for step [2] of this pass. + */ + TypeNode getUSort(TypeNode tn); + /** cache of the above function */ + std::map<TypeNode, TypeNode> d_ftypeMap; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */ diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 225f9945f..95f31621a 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H -#define __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H +#ifndef CVC4__PREPROCESSING__PASSES__INT_TO_BV_H +#define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -42,4 +42,4 @@ class IntToBV : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ +#endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */ diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index cdc104dbe..5620b4afb 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H -#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H #include <unordered_set> #include <vector> @@ -43,4 +43,4 @@ class IteRemoval : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H +#endif // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 8d7ad648a..44976bded 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H -#define __CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H +#define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 93fa701d1..f1748d635 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H -#define __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -59,4 +59,4 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ +#endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */ diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index dcaf12b5e..7744df824 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H -#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#ifndef CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#define CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H #include <unordered_map> #include <vector> @@ -54,4 +54,4 @@ class NlExtPurify : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ +#endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 61706e382..cb4ece4a9 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H -#define __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H #include <vector> diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index efbcb502e..e73b721ff 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H -#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H #include <unordered_set> #include <vector> @@ -114,4 +114,4 @@ class PseudoBooleanProcessor : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index d92d8599c..6b62c4d31 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H -#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H #include <map> #include <string> @@ -86,4 +86,4 @@ class QuantifierMacros : public PreprocessingPass } // preprocessing } // CVC4 -#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ +#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index bb5d8f8e7..991b3dd05 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H -#define __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H +#define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -43,4 +43,4 @@ class QuantifiersPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */ diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index a3d95b549..7949fb051 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H -#define __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H +#define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H #include <unordered_map> #include <vector> @@ -49,4 +49,4 @@ class RealToInt : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ +#endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */ diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index a3d42d660..e83cafb85 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__REWRITE_H -#define __CVC4__PREPROCESSING__PASSES__REWRITE_H +#ifndef CVC4__PREPROCESSING__PASSES__REWRITE_H +#define CVC4__PREPROCESSING__PASSES__REWRITE_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,5 +40,5 @@ class Rewrite : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__REWRITE_H */ +#endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */ diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index e787fe08c..a81dbb4b5 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -2,7 +2,7 @@ /*! \file sep_skolem_emp.cpp ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar, Andrew Reynolds, Paul Meng + ** Yoni Zohar, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index a8ea8db1c..1a5e36c40 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H -#define __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_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" @@ -39,4 +39,4 @@ class SepSkolemEmp : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ +#endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */ diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index e0ecd50c5..ae722529d 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -12,8 +12,8 @@ ** \brief Sort inference preprocessing pass **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ -#define __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ #include <map> #include <string> @@ -46,4 +46,4 @@ class SortInferencePass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index 27fb6f86b..f200755c5 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H -#define __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H +#ifndef CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H +#define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -39,4 +39,4 @@ class StaticLearning : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ +#endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */ diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp deleted file mode 100644 index 346915b51..000000000 --- a/src/preprocessing/passes/sygus_abduct.cpp +++ /dev/null @@ -1,174 +0,0 @@ -/********************* */ -/*! \file sygus_abduct.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 sygus abduction preprocessing pass, which - ** transforms an arbitrary input into an abduction problem. - **/ - -#include "preprocessing/passes/sygus_abduct.h" - -#include "expr/node_algorithm.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/term_util.h" -#include "theory/rewriter.h" - -using namespace std; -using namespace CVC4::kind; - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "sygus-abduct"){}; - -PreprocessingPassResult SygusAbduct::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - NodeManager* nm = NodeManager::currentNM(); - Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; - - Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; - std::unordered_set<Node, NodeHashFunction> symset; - std::vector<Node>& asserts = assertionsToPreprocess->ref(); - // do we have any assumptions, e.g. via check-sat-assuming? - bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); - // The following is our set of "axioms". We construct this set only when the - // usingAssumptions (above) is true. In this case, our input formula is - // partitioned into Fa ^ Fc as described in the header of this class, where: - // - The conjunction of assertions marked as assumptions are the negated - // conjecture Fc, and - // - The conjunction of all other assertions are the axioms Fa. - std::vector<Node> axioms; - for (size_t i = 0, size = asserts.size(); i < size; i++) - { - expr::getSymbols(asserts[i], symset); - // if we are not an assumption, add it to the set of axioms - if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart()) - { - axioms.push_back(asserts[i]); - } - } - Trace("sygus-abduct-debug") - << "...finish, got " << symset.size() << " symbols." << std::endl; - - Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; - std::vector<Node> syms; - std::vector<Node> vars; - std::vector<Node> varlist; - std::vector<TypeNode> varlistTypes; - for (const Node& s : symset) - { - TypeNode tn = s.getType(); - if (tn.isFirstClass()) - { - std::stringstream ss; - ss << s; - Node var = nm->mkBoundVar(tn); - syms.push_back(s); - vars.push_back(var); - Node vlv = nm->mkBoundVar(ss.str(), tn); - varlist.push_back(vlv); - varlistTypes.push_back(tn); - } - } - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl; - // make the abduction predicate to synthesize - TypeNode abdType = varlistTypes.empty() ? nm->booleanType() - : nm->mkPredicateType(varlistTypes); - Node abd = nm->mkBoundVar("A", abdType); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl; - std::vector<Node> achildren; - achildren.push_back(abd); - achildren.insert(achildren.end(), vars.begin(), vars.end()); - Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - Trace("sygus-abduct-debug") << "Set attributes..." << std::endl; - // set the sygus bound variable list - Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); - abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl; - Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts); - input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); - // A(x) => ~input( x ) - input = nm->mkNode(OR, abdApp.negate(), input.negate()); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl; - Node res = input.negate(); - if (!vars.empty()) - { - Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); - // exists x. ~( A( x ) => ~input( x ) ) - res = nm->mkNode(EXISTS, bvl, res); - } - // sygus attribute - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - theory::SygusAttribute ca; - sygusVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - std::vector<Node> iplc; - iplc.push_back(instAttr); - if (!axioms.empty()) - { - Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms); - aconj = - aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); - Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; - Node sc = nm->mkNode(AND, aconj, abdApp); - Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); - sc = nm->mkNode(EXISTS, vbvl, sc); - Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); - sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); - instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); - // build in the side condition - // exists x. A( x ) ^ input_axioms( x ) - // as an additional annotation on the sygus conjecture. In other words, - // the abducts A we procedure must be consistent with our axioms. - iplc.push_back(instAttr); - } - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); - - Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); - - // forall A. exists x. ~( A( x ) => ~input( x ) ) - res = nm->mkNode(FORALL, fbvl, res, instAttrList); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - res = theory::Rewriter::rewrite(res); - - Trace("sygus-abduct") << "Generate: " << res << std::endl; - - Node trueNode = nm->mkConst(true); - - assertionsToPreprocess->replace(0, res); - for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) - { - assertionsToPreprocess->replace(i, trueNode); - } - - return PreprocessingPassResult::NO_CONFLICT; -} - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h deleted file mode 100644 index 8e83bf1d7..000000000 --- a/src/preprocessing/passes/sygus_abduct.h +++ /dev/null @@ -1,72 +0,0 @@ -/********************* */ -/*! \file sygus_abduct.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 Sygus abduction preprocessing pass, which transforms an arbitrary - ** input into an abduction problem. - **/ - -#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H -#define __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H - -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -/** SygusAbduct - * - * A preprocessing utility that turns a set of quantifier-free assertions into - * a sygus conjecture that encodes an abduction problem. In detail, if our - * input formula is F( x ) for free symbols x, then we construct the sygus - * conjecture: - * - * exists A. forall x. ( A( x ) => ~F( x ) ) - * - * where A( x ) is a predicate over the free symbols of our input. In other - * words, A( x ) is a sufficient condition for showing ~F( x ). - * - * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x ) - * is unsatisfiable. - * - * A common use case is to find the weakest such A that meets the above - * specification. We do this by streaming solutions (sygus-stream) for A - * while filtering stronger solutions (sygus-filter-sol=strong). These options - * are enabled by default when this preprocessing class is used (sygus-abduct). - * - * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc - * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is: - * - * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) ) - * - * In other words, A( y ) must be consistent with our axioms Fa and imply - * ~F( x ). We encode this conjecture using SygusSideConditionAttribute. - */ -class SygusAbduct : public PreprocessingPass -{ - public: - SygusAbduct(PreprocessingPassContext* preprocContext); - - protected: - /** - * Replaces the set of assertions by an abduction sygus problem described - * above. - */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; -}; - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 - -#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */ diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 78e9e639a..471d68ff8 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -256,10 +256,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, // quantify the body Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl; + body = body.negate(); if (!qvars.empty()) { Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); - body = nm->mkNode(EXISTS, bvl, body.negate()); + body = nm->mkNode(EXISTS, bvl, body); } // sygus attribute to mark the conjecture as a sygus conjecture diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 9350a15c7..91deb445c 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -12,8 +12,8 @@ ** \brief SygusInference **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ -#define __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ #include <map> #include <string> @@ -68,4 +68,4 @@ class SygusInference : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h index 6f3cd5e0b..6bb10ebb8 100644 --- a/src/preprocessing/passes/symmetry_breaker.h +++ b/src/preprocessing/passes/symmetry_breaker.h @@ -12,8 +12,8 @@ ** \brief Symmetry breaker for theories **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ -#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ +#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ +#define CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ #include <map> #include <string> @@ -106,4 +106,4 @@ class SymBreakerPass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */ +#endif /* CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */ diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h index 1bc354419..deb1accd7 100644 --- a/src/preprocessing/passes/symmetry_detect.h +++ b/src/preprocessing/passes/symmetry_detect.h @@ -14,14 +14,14 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H -#define __CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H +#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H +#define CVC4__PREPROCESSING__PASSES__SYMMETRY_DETECT_H #include <map> #include <string> #include <vector> #include "expr/node.h" -#include "theory/quantifiers/term_canonize.h" +#include "expr/term_canonize.h" namespace CVC4 { namespace preprocessing { @@ -242,7 +242,7 @@ class SymmetryDetect Node d_falseNode; /** term canonizer (for quantified formulas) */ - theory::quantifiers::TermCanonize d_tcanon; + expr::TermCanonize d_tcanon; /** Cache for partitions */ std::map<Node, Partition> d_term_partition; diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index f83cb7f31..6d6e8fb27 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -15,6 +15,7 @@ #include "preprocessing/passes/synth_rew_rules.h" +#include "expr/term_canonize.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -22,7 +23,6 @@ #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_util.h" using namespace std; @@ -79,8 +79,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( { Trace("srs-input-debug") << "...preprocess " << cur << std::endl; visited[cur] = false; - Kind k = cur.getKind(); - bool isQuant = k == FORALL || k == EXISTS || k == LAMBDA || k == CHOICE; + bool isQuant = cur.isClosure(); // we recurse on this node if it is not a quantified formula if (!isQuant) { @@ -219,7 +218,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::vector<Node> cterms; // canonical terms for each type std::map<TypeNode, std::vector<Node> > t_cterms; - theory::quantifiers::TermCanonize tcanon; + expr::TermCanonize tcanon; for (unsigned i = 0, nterms = terms.size(); i < nterms; i++) { Node n = terms[i]; diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 4319c0243..38ef98b35 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -13,8 +13,8 @@ ** where t1 and t2 are subterms of the input. **/ -#ifndef __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H -#define __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#ifndef CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -74,4 +74,4 @@ class SynthRewRulesPass : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ +#endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index d8f75e4ba..cfa9ab0b5 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H -#define __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#ifndef CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H +#define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" @@ -40,4 +40,4 @@ class TheoryPreprocess : public PreprocessingPass } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ +#endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */ diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index f56b86489..ac4fd0a03 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H #include <unordered_map> #include <unordered_set> diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 7ffd5dc67..4a2e71488 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -28,8 +28,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_H #include <string> @@ -82,4 +82,4 @@ class PreprocessingPass { } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */ diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index d6a3b9f0f..e37680538 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H #include "context/cdo.h" #include "context/context.h" @@ -121,4 +121,4 @@ class PreprocessingPassContext } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 15618f575..36b3c6392 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -34,6 +34,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/extended_rewriter_pass.h" #include "preprocessing/passes/global_negate.h" +#include "preprocessing/passes/ho_elim.h" #include "preprocessing/passes/int_to_bv.h" #include "preprocessing/passes/ite_removal.h" #include "preprocessing/passes/ite_simp.h" @@ -48,7 +49,6 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" -#include "preprocessing/passes/sygus_abduct.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -127,7 +127,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>); registerPassInfo("real-to-int", callCtor<RealToInt>); registerPassInfo("sygus-infer", callCtor<SygusInference>); - registerPassInfo("sygus-abduct", callCtor<SygusAbduct>); registerPassInfo("bv-to-bool", callCtor<BVToBool>); registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>); registerPassInfo("sort-inference", callCtor<SortInferencePass>); @@ -150,6 +149,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>); registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>); registerPassInfo("bool-to-bv", callCtor<BoolToBV>); + registerPassInfo("ho-elim", callCtor<HoElim>); } } // namespace preprocessing diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index 786e59135..9cc109897 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -16,8 +16,8 @@ **/ #include "cvc4_private.h" -#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H -#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H +#ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H +#define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H #include <memory> #include <string> @@ -97,4 +97,4 @@ class PreprocessingPassRegistry { } // namespace preprocessing } // namespace CVC4 -#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */ +#endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */ diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index 383a087c1..ad195e62e 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -20,8 +20,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__ITE_UTILITIES_H -#define __CVC4__ITE_UTILITIES_H +#ifndef CVC4__ITE_UTILITIES_H +#define CVC4__ITE_UTILITIES_H #include <unordered_map> #include <vector> |