From: Haniel Barbosa Date: Thu, 16 Aug 2018 16:18:11 +0000 (-0500) Subject: Refactor apply2const (#2316) X-Git-Tag: cvc5-1.0.0~4777 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80be200c84494a4f82ab30cb743b7758c67db5b5;p=cvc5.git Refactor apply2const (#2316) --- diff --git a/src/Makefile.am b/src/Makefile.am index 43aa70174..c7dc311b6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -63,6 +63,8 @@ libcvc4_la_SOURCES = \ decision/justification_heuristic.h \ preprocessing/passes/apply_substs.cpp \ preprocessing/passes/apply_substs.h \ + preprocessing/passes/apply_to_const.cpp \ + preprocessing/passes/apply_to_const.h \ preprocessing/passes/bv_abstraction.cpp \ preprocessing/passes/bv_abstraction.h \ preprocessing/passes/bv_ackermann.cpp \ diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp new file mode 100644 index 000000000..bbe4439ec --- /dev/null +++ b/src/preprocessing/passes/apply_to_const.cpp @@ -0,0 +1,108 @@ +/********************* */ +/*! \file apply_to_const.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** 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 ApplyToConst preprocessing pass + ** + ** Rewrites applies to constants + **/ + +#include "preprocessing/passes/apply_to_const.h" + +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +ApplyToConst::ApplyToConst(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "apply-to-const"){}; + +Node ApplyToConst::rewriteApplyToConst(TNode n, NodeMap& cache) +{ + Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl; + + if (n.getMetaKind() == kind::metakind::CONSTANT + || n.getMetaKind() == kind::metakind::VARIABLE + || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR) + { + return n; + } + + if (cache.find(n) != cache.end()) + { + Trace("rewriteApplyToConst") << "in cache :: " << cache[n] << std::endl; + return cache[n]; + } + + if (n.getKind() == kind::APPLY_UF) + { + if (n.getNumChildren() == 1 && n[0].isConst() && n[0].getType().isInteger()) + { + stringstream ss; + ss << n.getOperator() << "_"; + if (n[0].getConst() < 0) + { + ss << "m" << -n[0].getConst(); + } + else + { + ss << n[0]; + } + Node newvar = + NodeManager::currentNM()->mkSkolem(ss.str(), + n.getType(), + "rewriteApplyToConst skolem", + NodeManager::SKOLEM_EXACT_NAME); + cache[n] = newvar; + Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl; + return newvar; + } + stringstream ss; + ss << "The rewrite-apply-to-const preprocessor is currently limited;\n" + << "it only works if all function symbols are unary and with Integer\n" + << "domain, and all applications are to integer values.\n" + << "Found application: " << n; + Unhandled(ss.str()); + } + + NodeBuilder<> builder(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + builder << n.getOperator(); + } + for (unsigned i = 0; i < n.getNumChildren(); ++i) + { + builder << rewriteApplyToConst(n[i], cache); + } + Node rewr = builder; + cache[n] = rewr; + Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl; + return rewr; +} + +PreprocessingPassResult ApplyToConst::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeMap cache; + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, + Rewriter::rewrite(rewriteApplyToConst( + (*assertionsToPreprocess)[i], cache))); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/apply_to_const.h b/src/preprocessing/passes/apply_to_const.h new file mode 100644 index 000000000..9d5072023 --- /dev/null +++ b/src/preprocessing/passes/apply_to_const.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file apply_to_const.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** 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 ApplyToConst preprocessing pass + ** + ** Rewrites applies to constants + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H +#define __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H + +#include + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map; + +class ApplyToConst : public PreprocessingPass +{ + public: + ApplyToConst(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node rewriteApplyToConst(TNode n, NodeMap& cache); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index db4efe89f..41b113b94 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,6 +70,7 @@ #include "options/theory_options.h" #include "options/uf_options.h" #include "preprocessing/passes/apply_substs.h" +#include "preprocessing/passes/apply_to_const.h" #include "preprocessing/passes/bool_to_bv.h" #include "preprocessing/passes/bv_abstraction.h" #include "preprocessing/passes/bv_ackermann.h" @@ -897,66 +898,6 @@ public: return retval; } - NodeToNodeHashMap d_rewriteApplyToConstCache; - Node rewriteApplyToConst(TNode n) { - Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl; - - if(n.getMetaKind() == kind::metakind::CONSTANT || - n.getMetaKind() == kind::metakind::VARIABLE || - n.getMetaKind() == kind::metakind::NULLARY_OPERATOR) - { - return n; - } - - if(d_rewriteApplyToConstCache.find(n) != d_rewriteApplyToConstCache.end()) { - Trace("rewriteApplyToConst") << "in cache :: " - << d_rewriteApplyToConstCache[n] - << std::endl; - return d_rewriteApplyToConstCache[n]; - } - - if(n.getKind() == kind::APPLY_UF) { - if(n.getNumChildren() == 1 && n[0].isConst() && - n[0].getType().isInteger()) - { - stringstream ss; - ss << n.getOperator() << "_"; - if(n[0].getConst() < 0) { - ss << "m" << -n[0].getConst(); - } else { - ss << n[0]; - } - Node newvar = NodeManager::currentNM()->mkSkolem( - ss.str(), n.getType(), "rewriteApplyToConst skolem", - NodeManager::SKOLEM_EXACT_NAME); - d_rewriteApplyToConstCache[n] = newvar; - Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl; - return newvar; - } else { - stringstream ss; - ss << "The rewrite-apply-to-const preprocessor is currently limited;" - << std::endl - << "it only works if all function symbols are unary and with Integer" - << std::endl - << "domain, and all applications are to integer values." << std::endl - << "Found application: " << n; - Unhandled(ss.str()); - } - } - - NodeBuilder<> builder(n.getKind()); - if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << n.getOperator(); - } - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - builder << rewriteApplyToConst(n[i]); - } - Node rewr = builder; - d_rewriteApplyToConstCache[n] = rewr; - Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl; - return rewr; - } - void addUseTheoryListListener(TheoryEngine* theoryEngine){ Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); d_listenerRegistrations->add( @@ -2717,6 +2658,8 @@ void SmtEnginePrivate::finishInit() // actually assembling preprocessing pipelines). std::unique_ptr applySubsts( new ApplySubsts(d_preprocessingPassContext.get())); + std::unique_ptr applyToConst( + new ApplyToConst(d_preprocessingPassContext.get())); std::unique_ptr boolToBv( new BoolToBV(d_preprocessingPassContext.get())); std::unique_ptr bvAbstract( @@ -2750,6 +2693,8 @@ void SmtEnginePrivate::finishInit() new SepSkolemEmp(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("apply-substs", std::move(applySubsts)); + d_preprocessingPassRegistry.registerPass("apply-to-const", + std::move(applyToConst)); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-abstraction", std::move(bvAbstract)); @@ -4476,9 +4421,7 @@ void SmtEnginePrivate::processAssertions() { if(options::rewriteApplyToConst()) { Chat() << "Rewriting applies to constants..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i])); - } + d_preprocessingPassRegistry.getPass("apply-to-const")->apply(&d_assertions); } dumpAssertions("post-rewrite-apply-to-const", d_assertions); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index cd79fe050..496551462 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -2,6 +2,7 @@ equals = = REG0_TESTS = \ + regress0/arith/apply2const-test.smt2 \ regress0/arith/arith.01.cvc \ regress0/arith/arith.02.cvc \ regress0/arith/arith.03.cvc \ diff --git a/test/regress/regress0/arith/apply2const-test.smt2 b/test/regress/regress0/arith/apply2const-test.smt2 new file mode 100644 index 000000000..e11878a74 --- /dev/null +++ b/test/regress/regress0/arith/apply2const-test.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --rewrite-apply-to-const +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun hash_1 (Int) Int) +(declare-fun hash_2 (Int) Int) +(declare-fun hash_3 (Int) Int) +(declare-fun hash_4 (Int) Int) +(declare-fun hash_5 (Int) Int) +(declare-fun hash_6 (Int) Int) +(declare-fun hash_7 (Int) Int) +(declare-fun hash_8 (Int) Int) +(declare-fun hash_9 (Int) Int) +(declare-fun hash_10 (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_2 x1)) (?v_5 (hash_2 x2)) (?v_6 (hash_2 x3)) (?v_7 (hash_2 x4)) (?v_8 (hash_3 x1)) (?v_9 (hash_3 x2)) (?v_10 (hash_3 x3)) (?v_11 (hash_3 x4)) (?v_12 (hash_4 x1)) (?v_13 (hash_4 x2)) (?v_14 (hash_4 x3)) (?v_15 (hash_4 x4)) (?v_16 (hash_5 x1)) (?v_17 (hash_5 x2)) (?v_18 (hash_5 x3)) (?v_19 (hash_5 x4)) (?v_20 (hash_6 x1)) (?v_21 (hash_6 x2)) (?v_22 (hash_6 x3)) (?v_23 (hash_6 x4)) (?v_24 (hash_7 x1)) (?v_25 (hash_7 x2)) (?v_26 (hash_7 x3)) (?v_27 (hash_7 x4)) (?v_28 (hash_8 x1)) (?v_29 (hash_8 x2)) (?v_30 (hash_8 x3)) (?v_31 (hash_8 x4)) (?v_32 (hash_9 x1)) (?v_33 (hash_9 x2)) (?v_34 (hash_9 x3)) (?v_35 (hash_9 x4)) (?v_36 (hash_10 x1)) (?v_37 (hash_10 x2)) (?v_38 (hash_10 x3)) (?v_39 (hash_10 x4))) (let ((?v_40 (= ?v_0 ?v_4))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_2 ?v_3)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_4 ?v_7)) (distinct ?v_5 ?v_6)) (distinct ?v_5 ?v_7)) (distinct ?v_6 ?v_7)) (distinct ?v_8 ?v_9)) (distinct ?v_8 ?v_10)) (distinct ?v_8 ?v_11)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_10 ?v_11)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_14 ?v_15)) (distinct ?v_16 ?v_17)) (distinct ?v_16 ?v_18)) (distinct ?v_16 ?v_19)) (distinct ?v_17 ?v_18)) (distinct ?v_17 ?v_19)) (distinct ?v_18 ?v_19)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_22 ?v_23)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_26 ?v_27)) (distinct ?v_28 ?v_29)) (distinct ?v_28 ?v_30)) (distinct ?v_28 ?v_31)) (distinct ?v_29 ?v_30)) (distinct ?v_29 ?v_31)) (distinct ?v_30 ?v_31)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_34 ?v_35)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_38 ?v_39)) (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4))) (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4))) (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4))) (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4))) (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4))) (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4))) (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4))) (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4))) (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4))) (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4))) (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4))) (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4))) (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4))) (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4))) (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4))) (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4))) (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4))) (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4))) (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4))) (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4))) (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4))) (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4))) (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4))) (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4))) (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4))) (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4))) (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4))) (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4))) (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4))) (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4))) (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4))) (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4))) (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4))) (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4))) (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4))) (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4))) (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4))) (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4))) (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4))) (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x2 x3)) (distinct x2 x4)) (distinct x3 x4)) (<= 0 x1)) (< x1 5)) (<= 0 x2)) (< x2 5)) (<= 0 x3)) (< x3 5)) (<= 0 x4)) (< x4 5)) (distinct (ite ?v_40 ?v_4 (+ ?v_0 ?v_0)) (ite ?v_40 ?v_4 (* 2 ?v_0))))))) +(check-sat) +(exit)