diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 15:20:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 15:20:37 -0500 |
commit | 4b580ea3876055f701b13e67e0e4e78abbe47674 (patch) | |
tree | 35d1cd8f48077dfed5a5bae682f2efc90d80703f /src/theory/quantifiers/skolemize.cpp | |
parent | 13e452be03bef09e2f54f42e2bc42383505ffcea (diff) |
(Refactor) Split term util (#1303)
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
Diffstat (limited to 'src/theory/quantifiers/skolemize.cpp')
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 385 |
1 files changed, 385 insertions, 0 deletions
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp new file mode 100644 index 000000000..2f210cc20 --- /dev/null +++ b/src/theory/quantifiers/skolemize.cpp @@ -0,0 +1,385 @@ +/********************* */ +/*! \file skolemize.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 skolemization utility + **/ + +#include "theory/quantifiers/skolemize.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/sort_inference.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u) + : d_quantEngine(qe), d_skolemized(u) +{ +} + +Node Skolemize::process(Node q) +{ + // do skolemization + if (d_skolemized.find(q) == d_skolemized.end()) + { + Node body = getSkolemizedBody(q); + NodeBuilder<> nb(kind::OR); + nb << q << body.notNode(); + Node lem = nb; + d_skolemized[q] = lem; + return lem; + } + return Node::null(); +} + +bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) +{ + std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it = + d_skolem_constants.find(q); + if (it != d_skolem_constants.end()) + { + skolems.insert(skolems.end(), it->second.begin(), it->second.end()); + return true; + } + return false; +} + +Node Skolemize::getSkolemConstant(Node q, unsigned i) +{ + std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it = + d_skolem_constants.find(q); + if (it != d_skolem_constants.end()) + { + if (i < it->second.size()) + { + return it->second[i]; + } + } + return Node::null(); +} + +void Skolemize::getSelfSel(const Datatype& dt, + const DatatypeConstructor& dc, + Node n, + TypeNode ntn, + std::vector<Node>& selfSel) +{ + TypeNode tspec; + if (dt.isParametric()) + { + tspec = TypeNode::fromType( + dc.getSpecializedConstructorType(n.getType().toType())); + Trace("sk-ind-debug") << "Specialized constructor type : " << tspec + << std::endl; + Assert(tspec.getNumChildren() == dc.getNumArgs()); + } + Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " + << dt.getName() << std::endl; + for (unsigned j = 0; j < dc.getNumArgs(); j++) + { + std::vector<Node> ssc; + if (dt.isParametric()) + { + Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn + << std::endl; + if (tspec[j] == ntn) + { + ssc.push_back(n); + } + } + else + { + TypeNode tn = TypeNode::fromType(dc[j].getRangeType()); + Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl; + if (tn == ntn) + { + ssc.push_back(n); + } + } + /* TODO: more than weak structural induction + else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn + )==visited.end() ){ + visited.push_back( tn ); + const Datatype& dt = + ((DatatypeType)(subs[0].getType()).toType()).getDatatype(); + std::vector< Node > disj; + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + getSelfSel( dt[i], n, ntn, ssc ); + } + visited.pop_back(); + } + */ + for (unsigned k = 0; k < ssc.size(); k++) + { + Node ss = NodeManager::currentNM()->mkNode( + APPLY_SELECTOR_TOTAL, + dc.getSelectorInternal(n.getType().toType(), j), + n); + if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end()) + { + selfSel.push_back(ss); + } + } + } +} + +Node Skolemize::mkSkolemizedBody(Node f, + Node n, + std::vector<TypeNode>& argTypes, + std::vector<TNode>& fvs, + std::vector<Node>& sk, + Node& sub, + std::vector<unsigned>& sub_vars) +{ + Assert(sk.empty() || sk.size() == f[0].getNumChildren()); + // calculate the variables and substitution + std::vector<TNode> ind_vars; + std::vector<unsigned> ind_var_indicies; + std::vector<TNode> vars; + std::vector<unsigned> var_indicies; + for (unsigned i = 0; i < f[0].getNumChildren(); i++) + { + if (isInductionTerm(f[0][i])) + { + ind_vars.push_back(f[0][i]); + ind_var_indicies.push_back(i); + } + else + { + vars.push_back(f[0][i]); + var_indicies.push_back(i); + } + Node s; + // make the new function symbol or use existing + if (i >= sk.size()) + { + if (argTypes.empty()) + { + s = NodeManager::currentNM()->mkSkolem( + "skv", f[0][i].getType(), "created during skolemization"); + } + else + { + TypeNode typ = NodeManager::currentNM()->mkFunctionType( + argTypes, f[0][i].getType()); + Node op = NodeManager::currentNM()->mkSkolem( + "skop", typ, "op created during pre-skolemization"); + // DOTHIS: set attribute on op, marking that it should not be selected + // as trigger + std::vector<Node> funcArgs; + funcArgs.push_back(op); + funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end()); + s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs); + } + sk.push_back(s); + } + else + { + Assert(sk[i].getType() == f[0][i].getType()); + } + } + Node ret; + if (vars.empty()) + { + ret = n; + } + else + { + std::vector<Node> var_sk; + for (unsigned i = 0; i < var_indicies.size(); i++) + { + var_sk.push_back(sk[var_indicies[i]]); + } + Assert(vars.size() == var_sk.size()); + ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end()); + } + if (!ind_vars.empty()) + { + Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl; + Trace("sk-ind") << "Skolemized is : " << ret << std::endl; + Node n_str_ind; + TypeNode tn = ind_vars[0].getType(); + Node k = sk[ind_var_indicies[0]]; + Node nret = ret.substitute(ind_vars[0], k); + // note : everything is under a negation + // the following constructs ~( R( x, k ) => ~P( x ) ) + if (options::dtStcInduction() && tn.isDatatype()) + { + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + std::vector<Node> disj; + for (unsigned i = 0; i < dt.getNumConstructors(); i++) + { + std::vector<Node> selfSel; + getSelfSel(dt, dt[i], k, tn, selfSel); + std::vector<Node> conj; + conj.push_back( + NodeManager::currentNM() + ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k) + .negate()); + for (unsigned j = 0; j < selfSel.size(); j++) + { + conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate()); + } + disj.push_back(conj.size() == 1 + ? conj[0] + : NodeManager::currentNM()->mkNode(OR, conj)); + } + Assert(!disj.empty()); + n_str_ind = disj.size() == 1 + ? disj[0] + : NodeManager::currentNM()->mkNode(AND, disj); + } + else if (options::intWfInduction() && tn.isInteger()) + { + Node icond = NodeManager::currentNM()->mkNode( + GEQ, k, NodeManager::currentNM()->mkConst(Rational(0))); + Node iret = + ret.substitute( + ind_vars[0], + NodeManager::currentNM()->mkNode( + MINUS, k, NodeManager::currentNM()->mkConst(Rational(1)))) + .negate(); + n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret); + n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind); + } + else + { + Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] + << ", type = " << tn << std::endl; + Assert(false); + } + Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl; + + std::vector<Node> rem_ind_vars; + rem_ind_vars.insert( + rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end()); + if (!rem_ind_vars.empty()) + { + Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars); + nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret); + nret = Rewriter::rewrite(nret); + sub = nret; + sub_vars.insert( + sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end()); + n_str_ind = NodeManager::currentNM() + ->mkNode(FORALL, bvl, n_str_ind.negate()) + .negate(); + } + ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind); + } + Trace("quantifiers-sk-debug") << "mkSkolem body for " << f + << " returns : " << ret << std::endl; + // if it has an instantiation level, set the skolemized body to that level + if (f.hasAttribute(InstLevelAttribute())) + { + theory::QuantifiersEngine::setInstantiationLevelAttr( + ret, f.getAttribute(InstLevelAttribute())); + } + + if (Trace.isOn("quantifiers-sk")) + { + Trace("quantifiers-sk") << "Skolemize : "; + for (unsigned i = 0; i < sk.size(); i++) + { + Trace("quantifiers-sk") << sk[i] << " "; + } + Trace("quantifiers-sk") << "for " << std::endl; + Trace("quantifiers-sk") << " " << f << std::endl; + } + + return ret; +} + +Node Skolemize::getSkolemizedBody(Node f) +{ + Assert(f.getKind() == FORALL); + if (d_skolem_body.find(f) == d_skolem_body.end()) + { + std::vector<TypeNode> fvTypes; + std::vector<TNode> fvs; + Node sub; + std::vector<unsigned> sub_vars; + d_skolem_body[f] = mkSkolemizedBody( + f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars); + // store sub quantifier information + if (!sub.isNull()) + { + // if we are skolemizing one at a time, we already know the skolem + // constants of the sub-quantified formula, store them + Assert(d_skolem_constants[sub].empty()); + for (unsigned i = 0; i < sub_vars.size(); i++) + { + d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]); + } + } + Assert(d_skolem_constants[f].size() == f[0].getNumChildren()); + if (options::sortInference()) + { + for (unsigned i = 0; i < d_skolem_constants[f].size(); i++) + { + // carry information for sort inference + d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( + f, f[0][i], d_skolem_constants[f][i]); + } + } + } + return d_skolem_body[f]; +} + +bool Skolemize::isInductionTerm(Node n) +{ + TypeNode tn = n.getType(); + if (options::dtStcInduction() && tn.isDatatype()) + { + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + return !dt.isCodatatype(); + } + if (options::intWfInduction() && n.getType().isInteger()) + { + return true; + } + return false; +} + +bool Skolemize::printSkolemization(std::ostream& out) +{ + bool printed = false; + for (NodeNodeMap::iterator it = d_skolemized.begin(); + it != d_skolemized.end(); + ++it) + { + Node q = (*it).first; + printed = true; + out << "(skolem " << q << std::endl; + out << " ( "; + for (unsigned i = 0; i < d_skolem_constants[q].size(); i++) + { + if (i > 0) + { + out << " "; + } + out << d_skolem_constants[q][i]; + } + out << " )" << std::endl; + out << ")" << std::endl; + } + return printed; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |