From: Andrew Reynolds Date: Thu, 24 Sep 2020 20:02:04 +0000 (-0500) Subject: Function definition fmf preprocessing pass (#5064) X-Git-Tag: cvc5-1.0.0~2810 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3538f6f4700b3fa357e1c767ee6cd42be87a78b8;p=cvc5.git Function definition fmf preprocessing pass (#5064) This defines the function definition finite model finding as a proper preprocessing pass. This is required for cleaning/fixing bugs in the preprocessor on proof-new. There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e939915d5..db274ebfb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -68,6 +68,8 @@ libcvc4_add_sources( preprocessing/passes/bv_to_int.h preprocessing/passes/extended_rewriter_pass.cpp preprocessing/passes/extended_rewriter_pass.h + preprocessing/passes/fun_def_fmf.cpp + preprocessing/passes/fun_def_fmf.h preprocessing/passes/global_negate.cpp preprocessing/passes/global_negate.h preprocessing/passes/ho_elim.cpp @@ -607,8 +609,6 @@ libcvc4_add_sources( theory/quantifiers/fmf/model_engine.h theory/quantifiers/fun_def_evaluator.cpp theory/quantifiers/fun_def_evaluator.h - theory/quantifiers/fun_def_process.cpp - theory/quantifiers/fun_def_process.h theory/quantifiers/inst_match.cpp theory/quantifiers/inst_match.h theory/quantifiers/inst_match_trie.cpp diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp new file mode 100644 index 000000000..6095be228 --- /dev/null +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -0,0 +1,464 @@ +/********************* */ +/*! \file fun_def_fmf.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Function definition processor for finite model finding + **/ + +#include "preprocessing/passes/fun_def_fmf.h" + +#include "options/smt_options.h" +#include "proof/proof_manager.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +FunDefFmf::FunDefFmf(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "fun-def-fmf"), + d_fmfRecFunctionsDefined(nullptr) +{ + d_fmfRecFunctionsDefined = + new (true) NodeList(preprocContext->getUserContext()); +} + +FunDefFmf::~FunDefFmf() { d_fmfRecFunctionsDefined->deleteSelf(); } + +PreprocessingPassResult FunDefFmf::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + Assert(d_fmfRecFunctionsDefined != nullptr); + // reset + d_sorts.clear(); + d_input_arg_inj.clear(); + d_funcs.clear(); + // must carry over current definitions (in case of incremental) + for (context::CDList::const_iterator fit = + d_fmfRecFunctionsDefined->begin(); + fit != d_fmfRecFunctionsDefined->end(); + ++fit) + { + Node f = (*fit); + Assert(d_fmfRecFunctionsAbs.find(f) != d_fmfRecFunctionsAbs.end()); + TypeNode ft = d_fmfRecFunctionsAbs[f]; + d_sorts[f] = ft; + std::map>::iterator fcit = + d_fmfRecFunctionsConcrete.find(f); + Assert(fcit != d_fmfRecFunctionsConcrete.end()); + for (const Node& fcc : fcit->second) + { + d_input_arg_inj[f].push_back(fcc); + } + } + process(assertionsToPreprocess); + // must store new definitions (in case of incremental) + for (const Node& f : d_funcs) + { + d_fmfRecFunctionsAbs[f] = d_sorts[f]; + d_fmfRecFunctionsConcrete[f].clear(); + for (const Node& fcc : d_input_arg_inj[f]) + { + d_fmfRecFunctionsConcrete[f].push_back(fcc); + } + d_fmfRecFunctionsDefined->push_back(f); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) +{ + const std::vector& assertions = assertionsToPreprocess->ref(); + std::vector fd_assertions; + std::map subs_head; + // first pass : find defined functions, transform quantifiers + NodeManager* nm = NodeManager::currentNM(); + for (size_t i = 0, asize = assertions.size(); i < asize; i++) + { + Node n = QuantAttributes::getFunDefHead(assertions[i]); + if (!n.isNull()) + { + Assert(n.getKind() == APPLY_UF); + Node f = n.getOperator(); + + // check if already defined, if so, throw error + if (d_sorts.find(f) != d_sorts.end()) + { + Unhandled() << "Cannot define function " << f << " more than once."; + } + + Node bd = QuantAttributes::getFunDefBody(assertions[i]); + Trace("fmf-fun-def-debug") + << "Process function " << n << ", body = " << bd << std::endl; + if (!bd.isNull()) + { + d_funcs.push_back(f); + bd = nm->mkNode(EQUAL, n, bd); + + // create a sort S that represents the inputs of the function + std::stringstream ss; + ss << "I_" << f; + TypeNode iType = nm->mkSort(ss.str()); + AbsTypeFunDefAttribute atfda; + iType.setAttribute(atfda, true); + d_sorts[f] = iType; + + // create functions f1...fn mapping from this sort to concrete elements + size_t nchildn = n.getNumChildren(); + for (size_t j = 0; j < nchildn; j++) + { + TypeNode typ = nm->mkFunctionType(iType, n[j].getType()); + std::stringstream ssf; + ssf << f << "_arg_" << j; + d_input_arg_inj[f].push_back( + nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); + } + + // construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] + std::vector children; + Node bv = nm->mkBoundVar("?i", iType); + Node bvl = nm->mkNode(BOUND_VAR_LIST, bv); + std::vector subs; + std::vector vars; + for (size_t j = 0; j < nchildn; j++) + { + vars.push_back(n[j]); + subs.push_back(nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], bv)); + } + bd = bd.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + subs_head[i] = + n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + + Trace("fmf-fun-def") + << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def") << " to " << std::endl; + Node new_q = nm->mkNode(FORALL, bvl, bd); + new_q = Rewriter::rewrite(new_q); + assertionsToPreprocess->replace(i, new_q); + Trace("fmf-fun-def") << " " << assertions[i] << std::endl; + fd_assertions.push_back(i); + } + else + { + // can be, e.g. in corner cases forall x. f(x)=f(x), forall x. + // f(x)=f(x)+1 + } + } + } + // second pass : rewrite assertions + std::map> visited; + std::map> visited_cons; + for (size_t i = 0, asize = assertions.size(); i < asize; i++) + { + bool is_fd = std::find(fd_assertions.begin(), fd_assertions.end(), i) + != fd_assertions.end(); + std::vector constraints; + Trace("fmf-fun-def-rewrite") + << "Rewriting " << assertions[i] + << ", is function definition = " << is_fd << std::endl; + Node n = simplifyFormula(assertions[i], + true, + true, + constraints, + is_fd ? subs_head[i] : Node::null(), + is_fd, + visited, + visited_cons); + Assert(constraints.empty()); + if (n != assertions[i]) + { + n = Rewriter::rewrite(n); + Trace("fmf-fun-def-rewrite") + << "FMF fun def : rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def-rewrite") << " to " << std::endl; + Trace("fmf-fun-def-rewrite") << " " << n << std::endl; + assertionsToPreprocess->replace(i, n); + } + } +} + +Node FunDefFmf::simplifyFormula( + Node n, + bool pol, + bool hasPol, + std::vector& constraints, + Node hd, + bool is_fun_def, + std::map>& visited, + std::map>& visited_cons) +{ + Assert(constraints.empty()); + int index = (is_fun_def ? 1 : 0) + 2 * (hasPol ? (pol ? 1 : -1) : 0); + std::map::iterator itv = visited[index].find(n); + if (itv != visited[index].end()) + { + // constraints.insert( visited_cons[index] + std::map::iterator itvc = visited_cons[index].find(n); + if (itvc != visited_cons[index].end()) + { + constraints.push_back(itvc->second); + } + return itv->second; + } + NodeManager* nm = NodeManager::currentNM(); + Node ret; + Trace("fmf-fun-def-debug2") << "Simplify " << n << " " << pol << " " << hasPol + << " " << is_fun_def << std::endl; + if (n.getKind() == FORALL) + { + Node c = simplifyFormula( + n[1], pol, hasPol, constraints, hd, is_fun_def, visited, visited_cons); + // append prenex to constraints + for (unsigned i = 0; i < constraints.size(); i++) + { + constraints[i] = nm->mkNode(FORALL, n[0], constraints[i]); + constraints[i] = Rewriter::rewrite(constraints[i]); + } + if (c != n[1]) + { + ret = nm->mkNode(FORALL, n[0], c); + } + else + { + ret = n; + } + } + else + { + Node nn = n; + bool isBool = n.getType().isBoolean(); + if (isBool && n.getKind() != APPLY_UF) + { + std::vector children; + bool childChanged = false; + // are we at a branch position (not all children are necessarily + // relevant)? + bool branch_pos = + (n.getKind() == ITE || n.getKind() == OR || n.getKind() == AND); + std::vector branch_constraints; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + Node c = n[i]; + // do not process LHS of definition + if (!is_fun_def || c != hd) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol); + // get child constraints + std::vector cconstraints; + c = simplifyFormula(n[i], + newPol, + newHasPol, + cconstraints, + hd, + false, + visited, + visited_cons); + if (branch_pos) + { + // if at a branching position, the other constraints don't matter + // if this is satisfied + Node bcons = nm->mkAnd(cconstraints); + branch_constraints.push_back(bcons); + Trace("fmf-fun-def-debug2") << "Branching constraint at arg " << i + << " is " << bcons << std::endl; + } + constraints.insert( + constraints.end(), cconstraints.begin(), cconstraints.end()); + } + children.push_back(c); + childChanged = c != n[i] || childChanged; + } + if (childChanged) + { + nn = nm->mkNode(n.getKind(), children); + } + if (branch_pos && !constraints.empty()) + { + // if we are at a branching position in the formula, we can + // minimize recursive constraints on recursively defined predicates if + // we know one child forces the overall evaluation of this formula. + Node branch_cond; + if (n.getKind() == ITE) + { + // always care about constraints on the head of the ITE, but only + // care about one of the children depending on how it evaluates + branch_cond = nm->mkNode( + AND, + branch_constraints[0], + nm->mkNode( + ITE, n[0], branch_constraints[1], branch_constraints[2])); + } + else + { + // in the default case, we care about all conditions + branch_cond = nm->mkAnd(constraints); + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + // if this child holds with forcing polarity (true child of OR or + // false child of AND), then we only care about its associated + // recursive conditions + branch_cond = nm->mkNode(ITE, + (n.getKind() == OR ? n[i] : n[i].negate()), + branch_constraints[i], + branch_cond); + } + } + Trace("fmf-fun-def-debug2") + << "Made branching condition " << branch_cond << std::endl; + constraints.clear(); + constraints.push_back(branch_cond); + } + } + else + { + // simplify term + std::map visitedT; + getConstraints(n, constraints, visitedT); + } + if (!constraints.empty() && isBool && hasPol) + { + // conjoin with current + Node cons = nm->mkAnd(constraints); + if (pol) + { + ret = nm->mkNode(AND, nn, cons); + } + else + { + ret = nm->mkNode(OR, nn, cons.negate()); + } + Trace("fmf-fun-def-debug2") + << "Add constraint to obtain " << ret << std::endl; + constraints.clear(); + } + else + { + ret = nn; + } + } + if (!constraints.empty()) + { + Node cons; + // flatten to AND node for the purposes of caching + if (constraints.size() > 1) + { + cons = nm->mkNode(AND, constraints); + cons = Rewriter::rewrite(cons); + constraints.clear(); + constraints.push_back(cons); + } + else + { + cons = constraints[0]; + } + visited_cons[index][n] = cons; + Assert(constraints.size() == 1 && constraints[0] == cons); + } + visited[index][n] = ret; + return ret; +} + +void FunDefFmf::getConstraints(Node n, + std::vector& constraints, + std::map& visited) +{ + std::map::iterator itv = visited.find(n); + if (itv != visited.end()) + { + // already visited + if (!itv->second.isNull()) + { + // add the cached constraint if it does not already occur + if (std::find(constraints.begin(), constraints.end(), itv->second) + == constraints.end()) + { + constraints.push_back(itv->second); + } + } + return; + } + visited[n] = Node::null(); + std::vector currConstraints; + NodeManager* nm = NodeManager::currentNM(); + if (n.getKind() == ITE) + { + // collect constraints for the condition + getConstraints(n[0], currConstraints, visited); + // collect constraints for each branch + Node cs[2]; + for (unsigned i = 0; i < 2; i++) + { + std::vector ccons; + getConstraints(n[i + 1], ccons, visited); + cs[i] = nm->mkAnd(ccons); + } + if (!cs[0].isConst() || !cs[1].isConst()) + { + Node itec = nm->mkNode(ITE, n[0], cs[0], cs[1]); + currConstraints.push_back(itec); + Trace("fmf-fun-def-debug") + << "---> add constraint " << itec << " for " << n << std::endl; + } + } + else + { + if (n.getKind() == APPLY_UF) + { + // check if f is defined, if so, we must enforce domain constraints for + // this f-application + Node f = n.getOperator(); + std::map::iterator it = d_sorts.find(f); + if (it != d_sorts.end()) + { + // create existential + Node z = nm->mkBoundVar("?z", it->second); + Node bvl = nm->mkNode(BOUND_VAR_LIST, z); + std::vector children; + for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) + { + Node uz = nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], z); + children.push_back(uz.eqNode(n[j])); + } + Node bd = nm->mkAnd(children); + bd = bd.negate(); + Node ex = nm->mkNode(FORALL, bvl, bd); + ex = ex.negate(); + currConstraints.push_back(ex); + Trace("fmf-fun-def-debug") + << "---> add constraint " << ex << " for " << n << std::endl; + } + } + for (const Node& cn : n) + { + getConstraints(cn, currConstraints, visited); + } + } + // set the visited cache + if (!currConstraints.empty()) + { + Node finalc = nm->mkAnd(currConstraints); + visited[n] = finalc; + // add to constraints + getConstraints(n, constraints, visited); + } +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h new file mode 100644 index 000000000..36d1166b7 --- /dev/null +++ b/src/preprocessing/passes/fun_def_fmf.h @@ -0,0 +1,106 @@ +/********************* */ +/*! \file fun_def_fmf.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Function definition processor for finite model finding + **/ + +#ifndef CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H +#define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H + +#include +#include +#include + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * Preprocessing pass to allow finite model finding for admissible recursive + * function definitions. For details, see Reynolds et al "Model Finding for + * Recursive Functions" IJCAR 2016. + */ +class FunDefFmf : public PreprocessingPass +{ + /** The types for the recursive function definitions */ + typedef context::CDList NodeList; + + public: + FunDefFmf(PreprocessingPassContext* preprocContext); + ~FunDefFmf(); + + protected: + /** + * Run the preprocessing pass on the pipeline, taking into account the + * previous definitions. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /** Run the preprocessing pass on the pipeline. */ + void process(AssertionPipeline* assertionsToPreprocess); + /** simplify formula + * This is A_0 in Figure 1 of Reynolds et al "Model Finding for Recursive + * Functions". The input of A_0 in that paper is a pair ( term t, polarity p ) + * The return value of A_0 in that paper is a pair ( term t', set of formulas + * X ). + * + * This function implements this such that : + * n is t + * pol/hasPol is p + * the return value is t' + * the set of formulas X are stored in "constraints" + * + * Additionally, is_fun_def is whether we are currently processing the top of + * a function defintion, since this affects whether we process the head of the + * definition. + */ + Node simplifyFormula(Node n, + bool pol, + bool hasPol, + std::vector& constraints, + Node hd, + bool is_fun_def, + std::map>& visited, + std::map>& visited_cons); + /** get constraints + * + * This computes constraints for the final else branch of A_0 in Figure 1 + * of Reynolds et al "Model Finding for Recursive Functions". The range of + * the cache visited stores the constraint (if any) for each node. + */ + void getConstraints(Node n, + std::vector& constraints, + std::map& visited); + /** recursive function definition abstractions for fmf-fun */ + std::map d_fmfRecFunctionsAbs; + /** map to concrete definitions for fmf-fun */ + std::map> d_fmfRecFunctionsConcrete; + /** List of defined recursive functions processed by fmf-fun */ + NodeList* d_fmfRecFunctionsDefined; + // defined functions to input sort (alpha) + std::map d_sorts; + // defined functions to injections input -> argument elements (gamma) + std::map> d_input_arg_inj; + // (newly) defined functions + std::vector d_funcs; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 8f41a5d97..46c1fff68 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -33,6 +33,7 @@ #include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/passes/bv_to_int.h" #include "preprocessing/passes/extended_rewriter_pass.h" +#include "preprocessing/passes/fun_def_fmf.h" #include "preprocessing/passes/global_negate.h" #include "preprocessing/passes/ho_elim.h" #include "preprocessing/passes/int_to_bv.h" @@ -147,6 +148,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("nl-ext-purify", callCtor); registerPassInfo("bool-to-bv", callCtor); registerPassInfo("ho-elim", callCtor); + registerPassInfo("fun-def-fmf", callCtor); } } // namespace preprocessing diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 3712d1914..504814e07 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -32,7 +32,6 @@ #include "smt/dump.h" #include "smt/smt_engine.h" #include "theory/logic_info.h" -#include "theory/quantifiers/fun_def_process.h" #include "theory/theory_engine.h" using namespace CVC4::preprocessing; @@ -54,18 +53,13 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm) - : d_smt(smt), - d_resourceManager(rm), - d_preprocessingPassContext(nullptr), - d_fmfRecFunctionsDefined(nullptr) + : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr) { d_true = NodeManager::currentNM()->mkConst(true); - d_fmfRecFunctionsDefined = new (true) NodeList(d_smt.getUserContext()); } ProcessAssertions::~ProcessAssertions() { - d_fmfRecFunctionsDefined->deleteSelf(); } void ProcessAssertions::finishInit(PreprocessingPassContext* pc) @@ -140,7 +134,11 @@ bool ProcessAssertions::apply(Assertions& as) unordered_map cache; for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) { - assertions.replace(i, expandDefinitions(assertions[i], cache)); + Node expd = expandDefinitions(assertions[i], cache); + if (expd != assertions[i]) + { + assertions.replace(i, expd); + } } } Trace("smt-proc") @@ -247,38 +245,7 @@ bool ProcessAssertions::apply(Assertions& as) // to FMF if (options::fmfFunWellDefined()) { - quantifiers::FunDefFmf fdf; - Assert(d_fmfRecFunctionsDefined != NULL); - // must carry over current definitions (in case of incremental) - for (context::CDList::const_iterator fit = - d_fmfRecFunctionsDefined->begin(); - fit != d_fmfRecFunctionsDefined->end(); - ++fit) - { - Node f = (*fit); - Assert(d_fmfRecFunctionsAbs.find(f) != d_fmfRecFunctionsAbs.end()); - TypeNode ft = d_fmfRecFunctionsAbs[f]; - fdf.d_sorts[f] = ft; - std::map>::iterator fcit = - d_fmfRecFunctionsConcrete.find(f); - Assert(fcit != d_fmfRecFunctionsConcrete.end()); - for (const Node& fcc : fcit->second) - { - fdf.d_input_arg_inj[f].push_back(fcc); - } - } - fdf.simplify(assertions.ref()); - // must store new definitions (in case of incremental) - for (const Node& f : fdf.d_funcs) - { - d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f]; - d_fmfRecFunctionsConcrete[f].clear(); - for (const Node& fcc : fdf.d_input_arg_inj[f]) - { - d_fmfRecFunctionsConcrete[f].push_back(fcc); - } - d_fmfRecFunctionsDefined->push_back(f); - } + d_passes["fun-def-fmf"]->apply(&assertions); } } diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index ba5298abe..a4f16ab1d 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -107,12 +107,6 @@ class ProcessAssertions * Number of calls of simplify assertions active. */ unsigned d_simplifyAssertionsDepth; - /** recursive function definition abstractions for fmf-fun */ - std::map d_fmfRecFunctionsAbs; - /** map to concrete definitions for fmf-fun */ - std::map> d_fmfRecFunctionsConcrete; - /** List of defined recursive functions processed by fmf-fun */ - NodeList* d_fmfRecFunctionsDefined; /** Spend resource r by the resource manager of this class. */ void spendResource(ResourceManager::Resource r); /** diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index d41cd7310..796ee85fa 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -17,7 +17,6 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" -#include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp deleted file mode 100644 index 350da8003..000000000 --- a/src/theory/quantifiers/fun_def_process.cpp +++ /dev/null @@ -1,356 +0,0 @@ -/********************* */ -/*! \file fun_def_process.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Sort inference module - ** - ** This class implements pre-process steps for admissible recursive function definitions (Reynolds et al IJCAR2016) - **/ - -#include "theory/quantifiers/fun_def_process.h" - -#include - -#include "options/smt_options.h" -#include "proof/proof_manager.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -void FunDefFmf::simplify( std::vector< Node >& assertions ) { - std::vector< int > fd_assertions; - std::map< int, Node > subs_head; - //first pass : find defined functions, transform quantifiers - NodeManager* nm = NodeManager::currentNM(); - for( unsigned i=0; imkSort( ss.str() ); - AbsTypeFunDefAttribute atfda; - iType.setAttribute(atfda,true); - d_sorts[f] = iType; - - //create functions f1...fn mapping from this sort to concrete elements - for( unsigned j=0; jmkFunctionType( iType, n[j].getType() ); - std::stringstream ssf; - ssf << f << "_arg_" << j; - d_input_arg_inj[f].push_back( - nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); - } - - //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] - std::vector< Node > children; - Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType ); - Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv ); - std::vector< Node > subs; - std::vector< Node > vars; - for( unsigned j=0; jmkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); - } - bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - subs_head[i] = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - - Trace("fmf-fun-def") << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl; - Trace("fmf-fun-def") << " to " << std::endl; - Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - new_q = Rewriter::rewrite( new_q ); - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(new_q, assertions[i]); - } - assertions[i] = new_q; - Trace("fmf-fun-def") << " " << assertions[i] << std::endl; - fd_assertions.push_back( i ); - }else{ - //can be, e.g. in corner cases forall x. f(x)=f(x), forall x. f(x)=f(x)+1 - } - } - } - //second pass : rewrite assertions - std::map< int, std::map< Node, Node > > visited; - std::map< int, std::map< Node, Node > > visited_cons; - for( unsigned i=0; i constraints; - Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] - << ", is function definition = " << is_fd - << std::endl; - Node n = simplifyFormula(assertions[i], - true, - true, - constraints, - is_fd ? subs_head[i] : Node::null(), - is_fd, - visited, - visited_cons); - Assert(constraints.empty()); - if (n != assertions[i]) - { - n = Rewriter::rewrite(n); - Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] - << std::endl; - Trace("fmf-fun-def-rewrite") << " to " << std::endl; - Trace("fmf-fun-def-rewrite") << " " << n << std::endl; - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, assertions[i]); - } - assertions[i] = n; - } - } -} - -Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, - std::map< int, std::map< Node, Node > >& visited, - std::map< int, std::map< Node, Node > >& visited_cons ) { - Assert(constraints.empty()); - int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 ); - std::map< Node, Node >::iterator itv = visited[index].find( n ); - if( itv!=visited[index].end() ){ - //constraints.insert( visited_cons[index] - std::map< Node, Node >::iterator itvc = visited_cons[index].find( n ); - if( itvc != visited_cons[index].end() ){ - constraints.push_back( itvc->second ); - } - return itv->second; - }else{ - Node ret; - Trace("fmf-fun-def-debug2") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; - if( n.getKind()==FORALL ){ - Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def, visited, visited_cons ); - //append prenex to constraints - for( unsigned i=0; imkNode( FORALL, n[0], constraints[i] ); - constraints[i] = Rewriter::rewrite( constraints[i] ); - } - if( c!=n[1] ){ - ret = NodeManager::currentNM()->mkNode( FORALL, n[0], c ); - }else{ - ret = n; - } - }else{ - Node nn = n; - bool isBool = n.getType().isBoolean(); - if( isBool && n.getKind()!=APPLY_UF ){ - std::vector< Node > children; - bool childChanged = false; - // are we at a branch position (not all children are necessarily relevant)? - bool branch_pos = ( n.getKind()==ITE || n.getKind()==OR || n.getKind()==AND ); - std::vector< Node > branch_constraints; - for( unsigned i=0; i cconstraints; - c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, false, visited, visited_cons ); - if( branch_pos ){ - // if at a branching position, the other constraints don't matter if this is satisfied - Node bcons = cconstraints.empty() - ? NodeManager::currentNM()->mkConst(true) - : (cconstraints.size() == 1 - ? cconstraints[0] - : NodeManager::currentNM()->mkNode( - AND, cconstraints)); - branch_constraints.push_back( bcons ); - Trace("fmf-fun-def-debug2") << "Branching constraint at arg " << i << " is " << bcons << std::endl; - } - constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); - } - children.push_back( c ); - childChanged = c!=n[i] || childChanged; - } - if( childChanged ){ - nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - if( branch_pos && !constraints.empty() ){ - // if we are at a branching position in the formula, we can - // minimize recursive constraints on recursively defined predicates if we know one child forces - // the overall evaluation of this formula. - Node branch_cond; - if( n.getKind()==ITE ){ - // always care about constraints on the head of the ITE, but only care about one of the children depending on how it evaluates - branch_cond = NodeManager::currentNM()->mkNode( kind::AND, branch_constraints[0], - NodeManager::currentNM()->mkNode( kind::ITE, n[0], branch_constraints[1], branch_constraints[2] ) ); - }else{ - // in the default case, we care about all conditions - branch_cond = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints ); - for( unsigned i=0; imkNode( - kind::ITE, - (n.getKind() == OR ? n[i] : n[i].negate()), - branch_constraints[i], - branch_cond); - } - } - Trace("fmf-fun-def-debug2") << "Made branching condition " << branch_cond << std::endl; - constraints.clear(); - constraints.push_back( branch_cond ); - } - }else{ - //simplify term - std::map visitedT; - getConstraints(n, constraints, visitedT); - } - if( !constraints.empty() && isBool && hasPol ){ - //conjoin with current - Node cons = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints ); - if( pol ){ - ret = NodeManager::currentNM()->mkNode( AND, nn, cons ); - }else{ - ret = NodeManager::currentNM()->mkNode( OR, nn, cons.negate() ); - } - Trace("fmf-fun-def-debug2") << "Add constraint to obtain " << ret << std::endl; - constraints.clear(); - }else{ - ret = nn; - } - } - if( !constraints.empty() ){ - Node cons; - //flatten to AND node for the purposes of caching - if( constraints.size()>1 ){ - cons = NodeManager::currentNM()->mkNode( AND, constraints ); - cons = Rewriter::rewrite( cons ); - constraints.clear(); - constraints.push_back( cons ); - }else{ - cons = constraints[0]; - } - visited_cons[index][n] = cons; - Assert(constraints.size() == 1 && constraints[0] == cons); - } - visited[index][n] = ret; - return ret; - } -} - -void FunDefFmf::getConstraints(Node n, - std::vector& constraints, - std::map& visited) -{ - std::map::iterator itv = visited.find(n); - if (itv != visited.end()) - { - // already visited - if (!itv->second.isNull()) - { - // add the cached constraint if it does not already occur - if (std::find(constraints.begin(), constraints.end(), itv->second) - == constraints.end()) - { - constraints.push_back(itv->second); - } - } - return; - } - visited[n] = Node::null(); - std::vector currConstraints; - NodeManager* nm = NodeManager::currentNM(); - if (n.getKind() == ITE) - { - // collect constraints for the condition - getConstraints(n[0], currConstraints, visited); - // collect constraints for each branch - Node cs[2]; - for (unsigned i = 0; i < 2; i++) - { - std::vector ccons; - getConstraints(n[i + 1], ccons, visited); - cs[i] = ccons.empty() - ? nm->mkConst(true) - : (ccons.size() == 1 ? ccons[0] : nm->mkNode(AND, ccons)); - } - if (!cs[0].isConst() || !cs[1].isConst()) - { - Node itec = nm->mkNode(ITE, n[0], cs[0], cs[1]); - currConstraints.push_back(itec); - Trace("fmf-fun-def-debug") - << "---> add constraint " << itec << " for " << n << std::endl; - } - } - else - { - if (n.getKind() == APPLY_UF) - { - // check if f is defined, if so, we must enforce domain constraints for - // this f-application - Node f = n.getOperator(); - std::map::iterator it = d_sorts.find(f); - if (it != d_sorts.end()) - { - // create existential - Node z = nm->mkBoundVar("?z", it->second); - Node bvl = nm->mkNode(BOUND_VAR_LIST, z); - std::vector children; - for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) - { - Node uz = nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], z); - children.push_back(uz.eqNode(n[j])); - } - Node bd = - children.size() == 1 ? children[0] : nm->mkNode(AND, children); - bd = bd.negate(); - Node ex = nm->mkNode(FORALL, bvl, bd); - ex = ex.negate(); - currConstraints.push_back(ex); - Trace("fmf-fun-def-debug") - << "---> add constraint " << ex << " for " << n << std::endl; - } - } - for (const Node& cn : n) - { - getConstraints(cn, currConstraints, visited); - } - } - // set the visited cache - if (!currConstraints.empty()) - { - Node finalc = currConstraints.size() == 1 - ? currConstraints[0] - : nm->mkNode(AND, currConstraints); - visited[n] = finalc; - // add to constraints - getConstraints(n, constraints, visited); - } -} diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h deleted file mode 100644 index 1f687d4f3..000000000 --- a/src/theory/quantifiers/fun_def_process.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file fun_def_process.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Pre-process step for admissible recursively defined functions - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H -#define CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H - -#include -#include -#include "expr/attribute.h" -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { -namespace theory { - -/** - * Attribute marked true for types that are used as abstraction types in - * the algorithm below. - */ -struct AbsTypeFunDefAttributeId -{ -}; -typedef expr::Attribute AbsTypeFunDefAttribute; - -namespace quantifiers { - -//Preprocessing pass to allow finite model finding for admissible recursive function definitions -// For details, see Reynolds et al "Model Finding for Recursive Functions" IJCAR 2016 -class FunDefFmf { -private: - /** simplify formula - * This is A_0 in Figure 1 of Reynolds et al "Model Finding for Recursive Functions". - * The input of A_0 in that paper is a pair ( term t, polarity p ) - * The return value of A_0 in that paper is a pair ( term t', set of formulas X ). - * - * This function implements this such that : - * n is t - * pol/hasPol is p - * the return value is t' - * the set of formulas X are stored in "constraints" - * - * Additionally, is_fun_def is whether we are currently processing the top of a function defintion, - * since this affects whether we process the head of the definition. - */ - Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, - std::map< int, std::map< Node, Node > >& visited, - std::map< int, std::map< Node, Node > >& visited_cons ); -public: - FunDefFmf(){} - ~FunDefFmf(){} - //defined functions to input sort (alpha) - std::map< Node, TypeNode > d_sorts; - //defined functions to injections input -> argument elements (gamma) - std::map< Node, std::vector< Node > > d_input_arg_inj; - // (newly) defined functions - std::vector< Node > d_funcs; - /** simplify, which does the following: - * (1) records all top-level recursive function definitions in assertions, - * (2) runs Figure 1 of Reynolds et al "Model Finding for Recursive Functions" - * IJCAR 2016 on all formulas in assertions based on the definitions from part (1), - * which are Sigma^{dfn} in that paper. - */ - void simplify( std::vector< Node >& assertions ); - /** get constraints - * - * This computes constraints for the final else branch of A_0 in Figure 1 - * of Reynolds et al "Model Finding for Recursive Functions". The range of - * the cache visited stores the constraint (if any) for each node. - */ - void getConstraints(Node n, - std::vector& constraints, - std::map& visited); -}; - - -} -} -} - -#endif diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 88f291b2b..9fdb127e6 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -88,6 +88,15 @@ struct SygusVarToTermAttributeId typedef expr::Attribute SygusVarToTermAttribute; +/** + * Attribute marked true for types that are used as abstraction types in + * the finite model finding for function definitions algorithm. + */ +struct AbsTypeFunDefAttributeId +{ +}; +typedef expr::Attribute AbsTypeFunDefAttribute; + /** * Attribute true for quantifiers that have been internally generated, e.g. * for reductions of string operators.