diff options
-rw-r--r-- | src/theory/strings/core_solver.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 14 | ||||
-rw-r--r-- | src/theory/strings/proof_checker.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 6 |
4 files changed, 19 insertions, 12 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index d182f20f2..d8d75ea24 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1518,8 +1518,6 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant); // Add premises for x != "" ^ y != "" - // TODO: necessary? - /* for (unsigned xory = 0; xory < 2; xory++) { Node t = xory == 0 ? x : y; @@ -1535,7 +1533,6 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, iinfo.d_noExplain.push_back(tnz); } } - */ SkolemCache* skc = d_termReg.getSkolemCache(); std::vector<Node> newSkolems; // make the conclusion diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 77b8dbcb7..548fa757e 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -514,14 +514,24 @@ Node InferProofCons::convert(Inference infer, case Inference::REDUCTION: { size_t nchild = conc.getNumChildren(); - if (conc.getKind() != AND || conc[nchild - 1].getKind() != EQUAL) + Node mainEq; + if (conc.getKind()==EQUAL) + { + mainEq = conc; + } + else if (conc.getKind()== AND && conc[nchild - 1].getKind() == EQUAL) + { + mainEq = conc[nchild - 1]; + } + if (mainEq.isNull()) { + Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl; Assert(false); break; } std::vector<Node> argsRed; // the left hand side of the last conjunct is the term we are reducing - argsRed.push_back(conc[nchild - 1][0]); + argsRed.push_back(mainEq[0]); Node red = d_psb.tryStep(PfRule::STRINGS_REDUCTION, emptyVec, argsRed); Trace("strings-ipc-red") << "Reduction : " << red << std::endl; if (!red.isNull()) diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 983ef9acf..5394d7193 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -200,7 +200,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - if (!s0.isConst() || Word::isEmpty(s0)) + if (!s0.isConst() || !s0.getType().isStringLike() || Word::isEmpty(s0)) { return Node::null(); } @@ -263,14 +263,14 @@ Node StringProofRuleChecker::checkInternal(PfRule id, return Node::null(); } Node w1 = tvec[isRev ? nchildt - 2 : 1]; - if (!w1.isConst() || Word::isEmpty(w1)) + if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1)) { Trace("pfcheck-strings-cprop") << "...failed adjacent constant content" << std::endl; return Node::null(); } Node w2 = s0; - if (!w2.isConst() || Word::isEmpty(w2)) + if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2)) { Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl; return Node::null(); @@ -370,7 +370,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id, Assert(args.empty()); Node nemp = children[0]; if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL || - !nemp[0][1].isConst()) + !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike()) { return Node::null(); } diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 3ba250714..3bd723511 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -406,16 +406,16 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, std::map<Node, std::vector<ProofNode*>> famap; pfConc->getFreeAssumptionsMap(famap); // we first ensure the assumptions are flattened - std::vector<Node> ac; + std::unordered_set<Node, NodeHashFunction> ac; for (const TNode& a : assumps) { if (a.getKind() == AND) { - ac.insert(ac.end(), a.begin(), a.end()); + ac.insert(a.begin(), a.end()); } else { - ac.push_back(a); + ac.insert(a); } } std::map<Node, std::vector<ProofNode*>>::iterator itf; |