diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 37cc49b0ef8..30f1c6cd1c0 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -469,10 +469,9 @@ TypeNode SkolemManager::getTypeFor(SkolemId id, case SkolemId::WITNESS_INV_CONDITION: { Assert(cacheVals.size() == 1); - Assert(cacheVals[0].getKind() == Kind::NOT); - Assert(cacheVals[0][0].getKind() == Kind::FORALL); - Assert(cacheVals[0][0][0].getNumChildren() == 1); - return cacheVals[0][0][0][0].getType(); + Assert(cacheVals[0].getKind() == Kind::EXISTS); + Assert(cacheVals[0][0].getNumChildren() == 1); + return cacheVals[0][0][0].getType(); } break; // skolems that return the set element type diff --git a/src/proof/valid_witness_proof_generator.cpp b/src/proof/valid_witness_proof_generator.cpp index a92b3604508..5370dcd0b90 100644 --- a/src/proof/valid_witness_proof_generator.cpp +++ b/src/proof/valid_witness_proof_generator.cpp @@ -62,17 +62,20 @@ bool ValidWitnessProofGenerator::getProofSpec(const Node& attr, { if (attr.getKind() == Kind::INST_ATTRIBUTE && attr.getNumChildren() == 2) { - std::string str = attr[0].getConst().toString(); - if (str == "witness" && attr[1].getKind() == Kind::SEXPR + if (attr[0].getKind()==Kind::CONST_STRING && attr[1].getKind() == Kind::SEXPR && attr[1].getNumChildren() > 0) { - Node rn = attr[1][0]; - uint32_t rval; - if (ProofRuleChecker::getUInt32(rn, rval)) + std::string str = attr[0].getConst().toString(); + if (str=="witness") { - r = static_cast(rval); - args.insert(args.end(), attr[1].begin() + 1, attr[1].end()); - return true; + Node rn = attr[1][0]; + uint32_t rval; + if (ProofRuleChecker::getUInt32(rn, rval)) + { + r = static_cast(rval); + args.insert(args.end(), attr[1].begin() + 1, attr[1].end()); + return true; + } } } } diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 4a8132296aa..a4b136a6896 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -26,6 +26,9 @@ #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "util/bitvector.h" +#include "proof/proof_rule_checker.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::internal::kind; @@ -54,7 +57,7 @@ Node BvInverter::getSolveVariable(TypeNode tn) /*---------------------------------------------------------------------------*/ -Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) +Node BvInverter::getInversionNode(Node cond, Node annot, TypeNode tn, BvInverterQuery* m) { TNode solve_var = getSolveVariable(tn); @@ -95,8 +98,10 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) { Node x = m->getBoundVariable(tn); Node ccond = new_cond.substitute(solve_var, x); + Assert (!annot.isNull()); + Node ipl = NodeManager::mkNode(Kind::INST_PATTERN_LIST, annot); c = NodeManager::mkNode( - Kind::WITNESS, NodeManager::mkNode(Kind::BOUND_VAR_LIST, x), ccond); + Kind::WITNESS, NodeManager::mkNode(Kind::BOUND_VAR_LIST, x), ccond, ipl); Trace("cegqi-bv-skvinv") << "SKVINV : Make " << c << " for " << new_cond << std::endl; } @@ -417,7 +422,8 @@ Node BvInverter::solveBvLit(Node sv, litk = Kind::EQUAL; pol = true; /* t = fresh skolem constant */ - t = getInversionNode(ic, solve_tn, m); + Node annot = mkAnnotation(d_nm, litk, pol, t, sv_t, index); + t = getInversionNode(ic, annot, solve_tn, m); if (t.isNull()) { return t; @@ -447,21 +453,23 @@ Node BvInverter::solveBvLit(Node sv, Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic << std::endl; } - - return ic.isNull() ? t : getInversionNode(ic, solve_tn, m); + if (ic.isNull()) + { + return t; + } + Node annot = mkAnnotationBase(d_nm, litk, pol, t); + return getInversionNode(ic, annot, solve_tn, m); } -Node BvInverter::mkInvertibilityCondition(const Node& x, const Node& f) +Node BvInverter::mkInvertibilityCondition(const Node& x, const Node& exists) { - Trace("ajr-temp") << "Make invertibility condition for " << x << " " << f + Trace("ajr-temp") << "Make invertibility condition for " << x << " " << exists << std::endl; - Assert(f.getKind() == Kind::NOT); - Node exists = f[0]; - Assert(exists.getKind() == Kind::FORALL); + Assert(exists.getKind() == Kind::EXISTS); Assert(exists[0].getNumChildren() == 1); Node v = exists[0][0]; Assert(x.getType() == v.getType()); - Node body = exists[1].negate(); + Node body = exists[1]; bool pol = body.getKind() != Kind::NOT; body = pol ? body : body[0]; Assert(body.getNumChildren() == 2); @@ -558,6 +566,34 @@ Node BvInverter::mkInvertibilityCondition(const Node& x, const Node& f) return ic; } +Node BvInverter::mkAnnotationBase(NodeManager * nm, Kind litk, bool pol,Node t) +{ + Node svt; + return mkAnnotation(nm, litk, pol, t, svt, 0); +} + +Node BvInverter::mkAnnotation(NodeManager * nm, Kind litk, bool pol, Node t, Node svt, unsigned index) +{ + std::vector sargs; + sargs.push_back(ProofRuleChecker::mkKindNode(litk)); + sargs.push_back(nm->mkConst(pol)); + sargs.push_back(t); + if (!svt.isNull()) + { + sargs.push_back(svt); + sargs.push_back(nm->mkConstInt(Rational(index))); + } + std::vector pfspec; + pfspec.push_back(nm->mkConst(String("witness-inv-condition"))); + pfspec.push_back(nm->mkNode(Kind::SEXPR, sargs)); + return nm->mkNode(Kind::INST_ATTRIBUTE, pfspec); +} + +Node BvInverter::mkExistsForAnnotation(NodeManager * nm, const Node& v, const Node& n) +{ + return Node::null(); +} + } // namespace quantifiers } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 6b7fd23c746..23d9712dcee 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -139,7 +139,14 @@ class BvInverter * This function will return the null node if the BvInverterQuery m provided * to this call is null. */ - Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); + Node getInversionNode(Node cond, Node annot, TypeNode tn, BvInverterQuery* m); + /** + */ + static Node mkAnnotation(NodeManager * nm, Kind litk, bool pol, Node t, Node svt, unsigned index); + static Node mkAnnotationBase(NodeManager * nm, Kind litk, bool pol, Node t); + /** + */ + static Node mkExistsForAnnotation(NodeManager * nm, const Node& v, const Node& n); /** Reference to options */ const Options& d_opts; /** Pointer to node manager */