diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_macros.cpp | 283 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_macros.h | 98 | ||||
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 9 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 2 |
5 files changed, 419 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp new file mode 100644 index 000000000..c7d74228f --- /dev/null +++ b/src/theory/quantifiers/quantifiers_macros.cpp @@ -0,0 +1,283 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utility for quantifiers macro definitions. + */ + +#include "theory/quantifiers/quantifiers_macros.h" + +#include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" +#include "options/quantifiers_options.h" +#include "proof/proof_manager.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/quantifiers_registry.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +QuantifiersMacros::QuantifiersMacros(QuantifiersRegistry& qr) : d_qreg(qr) {} + +Node QuantifiersMacros::solve(Node lit, bool reqGround) +{ + Trace("macros-debug") << "QuantifiersMacros::solve " << lit << std::endl; + if (lit.getKind() != FORALL) + { + return Node::null(); + } + lit = lit[1]; + bool pol = lit.getKind() != NOT; + Node n = pol ? lit : lit[0]; + NodeManager* nm = NodeManager::currentNM(); + if (n.getKind() == APPLY_UF) + { + // predicate case + if (isBoundVarApplyUf(n)) + { + Node op = n.getOperator(); + Node n_def = nm->mkConst(pol); + Node fdef = solveEq(n, n_def); + Assert(!fdef.isNull()); + return fdef; + } + } + else if (pol && n.getKind() == EQUAL) + { + // literal case + Trace("macros-debug") << "Check macro literal : " << n << std::endl; + std::map<Node, bool> visited; + std::vector<Node> candidates; + for (const Node& nc : n) + { + getMacroCandidates(nc, candidates, visited); + } + for (const Node& m : candidates) + { + Node op = m.getOperator(); + Trace("macros-debug") << "Check macro candidate : " << m << std::endl; + // get definition and condition + Node n_def = solveInEquality(m, n); // definition for the macro + if (n_def.isNull()) + { + continue; + } + Trace("macros-debug") + << m << " is possible macro in " << lit << std::endl; + Trace("macros-debug") + << " corresponding definition is : " << n_def << std::endl; + visited.clear(); + // cannot contain a defined operator + if (!containsBadOp(n_def, op, reqGround)) + { + Trace("macros-debug") + << "...does not contain bad (recursive) operator." << std::endl; + // must be ground UF term if mode is GROUND_UF + if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF + || preservesTriggerVariables(lit, n_def)) + { + Trace("macros-debug") + << "...respects ground-uf constraint." << std::endl; + Node fdef = solveEq(m, n_def); + if (!fdef.isNull()) + { + return fdef; + } + } + } + } + } + return Node::null(); +} + +bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround) +{ + std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited.insert(cur); + if (cur.isClosure() && reqGround) + { + return true; + } + else if (cur == op) + { + return true; + } + else if (cur.hasOperator() && cur.getOperator() == op) + { + return true; + } + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); + return false; +} + +bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n) +{ + Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q); + Trace("macros-debug2") << "Get free variables in " << icn << std::endl; + std::vector<Node> var; + quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var); + Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; + std::vector<Node> trigger_var; + inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var); + Trace("macros-debug2") << "Done." << std::endl; + // only if all variables are also trigger variables + return trigger_var.size() >= var.size(); +} + +bool QuantifiersMacros::isBoundVarApplyUf(Node n) +{ + Assert(n.getKind() == APPLY_UF); + TypeNode tno = n.getOperator().getType(); + std::map<Node, bool> vars; + // allow if a vector of unique variables of the same type as UF arguments + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + if (n[i].getKind() != BOUND_VARIABLE) + { + return false; + } + if (n[i].getType() != tno[i]) + { + return false; + } + if (vars.find(n[i]) == vars.end()) + { + vars[n[i]] = true; + } + else + { + return false; + } + } + return true; +} + +void QuantifiersMacros::getMacroCandidates(Node n, + std::vector<Node>& candidates, + std::map<Node, bool>& visited) +{ + if (visited.find(n) == visited.end()) + { + visited[n] = true; + if (n.getKind() == APPLY_UF) + { + if (isBoundVarApplyUf(n)) + { + candidates.push_back(n); + } + } + else if (n.getKind() == PLUS) + { + for (size_t i = 0; i < n.getNumChildren(); i++) + { + getMacroCandidates(n[i], candidates, visited); + } + } + else if (n.getKind() == MULT) + { + // if the LHS is a constant + if (n.getNumChildren() == 2 && n[0].isConst()) + { + getMacroCandidates(n[1], candidates, visited); + } + } + else if (n.getKind() == NOT) + { + getMacroCandidates(n[0], candidates, visited); + } + } +} + +Node QuantifiersMacros::solveInEquality(Node n, Node lit) +{ + if (lit.getKind() == EQUAL) + { + // return the opposite side of the equality if defined that way + for (int i = 0; i < 2; i++) + { + if (lit[i] == n) + { + return lit[i == 0 ? 1 : 0]; + } + else if (lit[i].getKind() == NOT && lit[i][0] == n) + { + return lit[i == 0 ? 1 : 0].negate(); + } + } + std::map<Node, Node> msum; + if (ArithMSum::getMonomialSumLit(lit, msum)) + { + Node veq_c; + Node val; + int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL); + if (res != 0 && veq_c.isNull()) + { + return val; + } + } + } + Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl; + return Node::null(); +} + +Node QuantifiersMacros::solveEq(Node n, Node ndef) +{ + Assert(n.getKind() == APPLY_UF); + NodeManager* nm = NodeManager::currentNM(); + Trace("macros-debug") << "Add macro eq for " << n << std::endl; + Trace("macros-debug") << " def: " << ndef << std::endl; + std::vector<Node> vars; + std::vector<Node> fvars; + for (const Node& nc : n) + { + vars.push_back(nc); + Node v = nm->mkBoundVar(nc.getType()); + fvars.push_back(v); + } + Node fdef = + ndef.substitute(vars.begin(), vars.end(), fvars.begin(), fvars.end()); + fdef = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, fvars), fdef); + // If the definition has a free variable, it is malformed. This can happen + // if the right hand side of a macro definition contains a variable not + // contained in the left hand side + if (expr::hasFreeVar(fdef)) + { + return Node::null(); + } + TNode op = n.getOperator(); + TNode fdeft = fdef; + Assert(op.getType().isComparableTo(fdef.getType())); + return op.eqNode(fdef); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_macros.h b/src/theory/quantifiers/quantifiers_macros.h new file mode 100644 index 000000000..77ce91829 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_macros.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Utility for detecting quantifier macro definitions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H + +#include <map> +#include <vector> +#include "expr/node.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class QuantifiersRegistry; + +/** + * A utility for inferring macros from quantified formulas. This can be seen as + * a method for putting quantified formulas in solved form, e.g. + * forall x. P(x) ---> P = (lambda x. true) + */ +class QuantifiersMacros +{ + public: + QuantifiersMacros(QuantifiersRegistry& qr); + ~QuantifiersMacros() {} + /** + * Called on quantified formulas lit of the form + * forall x1 ... xn. n = ndef + * where n is of the form U(x1...xn). Returns an equality of the form + * U = lambda x1 ... xn. ndef + * if this is a legal macro definition for U, and the null node otherwise. + * + * @param lit The body of the quantified formula + * @param reqGround Whether we require the macro definition to be ground, + * i.e. does not contain quantified formulas as subterms. + * @return If a macro can be inferred, an equality of the form + * (op = lambda x1 ... xn. def)), or the null node otherwise. + */ + Node solve(Node lit, bool reqGround = false); + + private: + /** + * Return true n is an APPLY_UF with pairwise unique BOUND_VARIABLE as + * children. + */ + bool isBoundVarApplyUf(Node n); + /** + * Returns true if n contains op, or if n contains a quantified formula + * as a subterm and reqGround is true. + */ + bool containsBadOp(Node n, Node op, bool reqGround); + /** + * Return true if n preserves trigger variables in quantified formula q, that + * is, triggers can be inferred containing all variables in q in term n. + */ + bool preservesTriggerVariables(Node q, Node n); + /** + * From n, get a list of possible subterms of n that could be the head of a + * macro definition. + */ + void getMacroCandidates(Node n, + std::vector<Node>& candidates, + std::map<Node, bool>& visited); + /** + * Solve n in literal lit, return n' such that n = n' is equivalent to lit + * if possible, or null otherwise. + */ + Node solveInEquality(Node n, Node lit); + /** + * Called when we have inferred a quantified formula is of the form + * forall x1 ... xn. n = ndef + * where n is of the form U(x1...xn). + */ + Node solveEq(Node n, Node ndef); + /** Reference to the quantifiers registry */ + QuantifiersRegistry& d_qreg; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /*CVC5__THEORY__QUANTIFIERS__QUANTIFIER_MACROS_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index b1ea5762f..27b16e411 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -17,8 +17,10 @@ #include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/quantifiers_macros.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" using namespace cvc5::kind; @@ -68,6 +70,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, // pointer will be retreived by TheoryEngine and set to all theories // post-construction. d_quantEngine = d_qengine.get(); + + if (options::macrosQuant()) + { + d_qmacros.reset(new QuantifiersMacros(d_qreg)); + } } TheoryQuantifiers::~TheoryQuantifiers() { @@ -116,6 +123,26 @@ void TheoryQuantifiers::presolve() { } } +Theory::PPAssertStatus TheoryQuantifiers::ppAssert( + TrustNode tin, TrustSubstitutionMap& outSubstitutions) +{ + if (d_qmacros != nullptr) + { + bool reqGround = + options::macrosQuantMode() != options::MacrosQuantMode::ALL; + Node eq = d_qmacros->solve(tin.getProven(), reqGround); + if (!eq.isNull()) + { + // must be legal + if (isLegalElimination(eq[0], eq[1])) + { + outSubstitutions.addSubstitution(eq[0], eq[1]); + return Theory::PP_ASSERT_STATUS_SOLVED; + } + } + } + return Theory::PP_ASSERT_STATUS_UNSOLVED; +} void TheoryQuantifiers::ppNotifyAssertions( const std::vector<Node>& assertions) { Trace("quantifiers-presolve") diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b5411aaba..544be84d6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -33,6 +33,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { +class QuantifiersMacros; + class TheoryQuantifiers : public Theory { public: TheoryQuantifiers(context::Context* c, @@ -56,6 +58,11 @@ class TheoryQuantifiers : public Theory { void preRegisterTerm(TNode n) override; void presolve() override; + /** + * Preprocess assert, which solves for quantifier macros when enabled. + */ + PPAssertStatus ppAssert(TrustNode tin, + TrustSubstitutionMap& outSubstitutions) override; void ppNotifyAssertions(const std::vector<Node>& assertions) override; //--------------------------------- standard check /** Post-check, called after the fact queue of the theory is processed. */ @@ -95,6 +102,8 @@ class TheoryQuantifiers : public Theory { QuantifiersInferenceManager d_qim; /** The quantifiers engine, which lives here */ std::unique_ptr<QuantifiersEngine> d_qengine; + /** The quantifiers macro module, used for ppAssert. */ + std::unique_ptr<QuantifiersMacros> d_qmacros; };/* class TheoryQuantifiers */ } // namespace quantifiers diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 402cb9a3d..6793e5e02 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -715,6 +715,8 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){ Node n = it->first; Assert(!n.isNull()); + // should not have been solved for in a substitution + Assert(d_substitutions.apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; if( options::ufHo() ){ |