Merge branch 'main' of https://github.com/cvc5/cvc5 into eoTrust

proofs/eo/cpc/theories/BitVectors.eo

@@ -343,8 +343,6 @@
   (BitVec m) Int)
 )
 
-(declare-const BITVECTOR_EAGER_ATOM (-> Bool Bool))
-
 ; internal operators
 
 (declare-const @bit

proofs/eo/cpc/theories/Datatypes.eo

@@ -59,5 +59,5 @@
 ; disclaimer: This function is not in the SMT-LIB standard.
 (declare-const nullable.lift (-> (! Type :var F :implicit) F ($get_type_nullable_lift F)))
 
-; skolems
-;SHARED_SELECTOR
+; shared selector
+(declare-const @shared_selector (-> (! Type :var D) (! Type :var T) Int D T))

src/printer/ast/ast_printer.cpp

@@ -83,6 +83,7 @@ void AstPrinter::toStream(std::ostream& out,
   {
     for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
     {
+      out << ' ';
       // body is re-letified
       if (i == 1)
       {

src/printer/smt2/smt2_printer.cpp

@@ -1116,6 +1116,10 @@ void Smt2Printer::toStream(std::ostream& out,
       {
         visit.pop_back();
         out << "(...)";
+        if (cur.getNumChildren() > 0)
+        {
+          out << ')';
+        }
         continue;
       }
     }

src/proof/alf/alf_node_converter.cpp

@@ -25,6 +25,7 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/sequence.h"
+#include "expr/sort_to_term.h"
 #include "printer/smt2/smt2_printer.h"
 #include "theory/builtin/generic_op.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -294,6 +295,13 @@ Node AlfNodeConverter::postConvert(Node n)
       return mkInternalApp("to_fp_bv", children, tn);
     }
   }
+  else if (k == Kind::BITVECTOR_EAGER_ATOM)
+  {
+    // For now, we explicity remove the application.
+    // https://github.com/cvc5/cvc5-wishues/issues/156: if the smt2 printer
+    // is refactored to silently ignore this kind, this case can be deleted.
+    return n[0];
+  }
   else if (GenericOp::isIndexedOperatorKind(k))
   {
     TypeNode tn = n.getType();
@@ -545,22 +553,30 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast)
     else if (k == Kind::APPLY_SELECTOR)
     {
       // maybe a shared selector
-      ret = maybeMkSkolemFun(op);
-      if (!ret.isNull())
-      {
-        return ret;
-      }
-      unsigned index = DType::indexOf(op);
-      const DType& dt = DType::datatypeOf(op);
-      if (dt.isTuple())
+      if (op.getSkolemId() == SkolemId::SHARED_SELECTOR)
       {
-        indices.push_back(d_nm->mkConstInt(index));
-        opName << "tuple.select";
+        std::vector<Node> kindices = op.getSkolemIndices();
+        opName << "@shared_selector";
+        indices.push_back(
+            typeAsNode(kindices[0].getConst<SortToTerm>().getType()));
+        indices.push_back(
+            typeAsNode(kindices[1].getConst<SortToTerm>().getType()));
+        indices.push_back(kindices[2]);
       }
       else
       {
-        unsigned cindex = DType::cindexOf(op);
-        opName << dt[cindex][index].getSelector();
+        unsigned index = DType::indexOf(op);
+        const DType& dt = DType::datatypeOf(op);
+        if (dt.isTuple())
+        {
+          indices.push_back(d_nm->mkConstInt(index));
+          opName << "tuple.select";
+        }
+        else
+        {
+          unsigned cindex = DType::cindexOf(op);
+          opName << dt[cindex][index].getSelector();
+        }
       }
     }
     else

src/proof/alf/alf_printer.cpp

@@ -180,6 +180,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
     case ProofRule::QUANT_VAR_REORDERING:
     case ProofRule::ENCODE_EQ_INTRO:
     case ProofRule::HO_APP_ENCODE:
+    case ProofRule::BV_EAGER_ATOM:
     case ProofRule::ACI_NORM:
     case ProofRule::ARITH_POLY_NORM:
     case ProofRule::ARITH_POLY_NORM_REL:
@@ -496,7 +497,8 @@ std::string AlfPrinter::getRuleName(const ProofNode* pfn) const
     ss << id;
     return ss.str();
   }
-  else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE)
+  else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE
+           || r == ProofRule::BV_EAGER_ATOM)
   {
     // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t,
     // where (convert t) is indistinguishable from t according to the proof.

src/smt/proof_post_processor.cpp

@@ -218,20 +218,11 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
   {
     TrustId tid;
     getTrustId(args[0], tid);
-    // we don't do this for steps that are already extended theory rewrite
-    // steps, or we would get an infinite loop in reconstruction.
-    if (tid == TrustId::EXT_THEORY_REWRITE)
-    {
-      return Node::null();
-    }
-    // maybe we can show it rewrites to true based on (extended) rewriting
+    // maybe we can show it rewrites to true based on rewriting
     // modulo original forms (MACRO_SR_PRED_INTRO).
     TheoryProofStepBuffer psb(d_pc);
-    if (psb.applyPredIntro(res,
-                           {},
-                           MethodId::SB_DEFAULT,
-                           MethodId::SBA_SEQUENTIAL,
-                           MethodId::RW_EXT_REWRITE))
+    if (psb.applyPredIntro(
+            res, {}, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL))
     {
       cdp->addSteps(psb);
       return res;

src/smt/set_defaults.cpp

@@ -1139,11 +1139,12 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
   if (opts.smt.proofMode == options::ProofMode::FULL_STRICT)
   {
     // symmetry breaking does not have proof support
-    SET_AND_NOTIFY_VAL_SYM(uf, ufSymmetryBreaker, false, "full strict proofs");
+    SET_AND_NOTIFY(uf, ufSymmetryBreaker, false, "full strict proofs");
     // CEGQI with deltas and infinities is not supported
     SET_AND_NOTIFY(quantifiers, cegqiMidpoint, true, "full strict proofs");
     SET_AND_NOTIFY(quantifiers, cegqiUseInfInt, false, "full strict proofs");
     SET_AND_NOTIFY(quantifiers, cegqiUseInfReal, false, "full strict proofs");
+    // shared selectors are not supported
     SET_AND_NOTIFY(datatypes, dtSharedSelectors, false, "full strict proofs");
   }
   return false;

src/theory/datatypes/datatypes_rewriter.cpp

@@ -78,8 +78,10 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
       Assert(tn.isDatatype());
       const DType& dt = tn.getDType();
       size_t i = utils::indexOf(n.getOperator());
-      bool sharedSel = d_opts.datatypes.dtSharedSelectors;
-      Node ticons = utils::getInstCons(t, dt, i, sharedSel);
+      // Note that we set shared selectors to false. This proof rule will
+      // be (unintentionally) unsuccessful when reconstructing proofs of the
+      // rewriter when using shared selectors.
+      Node ticons = utils::getInstCons(t, dt, i, false);
       return t.eqNode(ticons);
     }
     case ProofRewriteRule::DT_COLLAPSE_SELECTOR:
@@ -90,6 +92,11 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
         return Node::null();
       }
       Node selector = n.getOperator();
+      // shared selectors are not supported
+      if (selector.getSkolemId() == SkolemId::SHARED_SELECTOR)
+      {
+        return Node::null();
+      }
       size_t constructorIndex = utils::indexOf(n[0].getOperator());
       const DType& dt = utils::datatypeOf(selector);
       const DTypeConstructor& c = dt[constructorIndex];

src/theory/datatypes/inference_manager.cpp

@@ -150,11 +150,6 @@ Node InferenceManager::prepareDtInference(Node conc,
 {
   Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
                           << " by " << id << std::endl;
-  if (conc.getKind() == Kind::EQUAL && conc[0].getType().isBoolean())
-  {
-    // must turn (= conc false) into (not conc)
-    conc = rewrite(conc);
-  }
   if (isProofEnabled())
   {
     Assert(ipc != nullptr);

src/theory/datatypes/proof_checker.cpp

@@ -23,9 +23,8 @@ namespace cvc5::internal {
 namespace theory {
 namespace datatypes {
 
-DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm,
-                                                     bool sharedSel)
-    : ProofRuleChecker(nm), d_sharedSel(sharedSel)
+DatatypesProofRuleChecker::DatatypesProofRuleChecker(NodeManager* nm)
+    : ProofRuleChecker(nm)
 {
 }
 

src/theory/datatypes/proof_checker.h

@@ -30,7 +30,7 @@ namespace datatypes {
 class DatatypesProofRuleChecker : public ProofRuleChecker
 {
  public:
-  DatatypesProofRuleChecker(NodeManager* nm, bool sharedSel);
+  DatatypesProofRuleChecker(NodeManager* nm);
 
   /** Register all rules owned by this rule checker into pc. */
   void registerTo(ProofChecker* pc) override;
@@ -40,8 +40,6 @@ class DatatypesProofRuleChecker : public ProofRuleChecker
   Node checkInternal(ProofRule id,
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
-  /** Whether we are using shared selectors */
-  bool d_sharedSel;
 };
 
 }  // namespace datatypes

src/theory/datatypes/theory_datatypes.cpp

@@ -64,7 +64,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env,
       d_state(env, valuation),
       d_im(env, *this, d_state),
       d_notify(d_im, *this),
-      d_checker(nodeManager(), options().datatypes.dtSharedSelectors),
+      d_checker(nodeManager()),
       d_cpacb(*this)
 {
   d_true = nodeManager()->mkConst(true);

src/theory/quantifiers/ho_term_database.cpp

@@ -155,15 +155,14 @@ bool HoTermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
   {
     return false;
   }
-  exp.push_back(a.eqNode(b));
   // operators might be disequal
   Node af = getMatchOperator(a);
   Node bf = getMatchOperator(b);
   if (af != bf)
   {
     if (a.getKind() == Kind::APPLY_UF && b.getKind() == Kind::APPLY_UF)
     {
-      exp.push_back(af.eqNode(bf).negate());
+      exp.push_back(af.eqNode(bf));
       Assert(d_qstate.areEqual(af, bf))
           << af << " and " << bf << " are not equal";
     }

src/theory/quantifiers/term_database.cpp

@@ -23,6 +23,10 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "proof/proof.h"
+#include "proof/proof_generator.h"
+#include "proof/proof_node_algorithm.h"
+#include "proof/proof_node_manager.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
@@ -39,6 +43,68 @@ namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
+/**
+ * A proof generator for proving simple congruence lemmas discovered by TermDb.
+ */
+class DeqCongProofGenerator : protected EnvObj, public ProofGenerator
+{
+ public:
+  DeqCongProofGenerator(Env& env) : EnvObj(env) {}
+  virtual ~DeqCongProofGenerator() {}
+  /**
+   * The lemma is of the form:
+   * (=> (and (= ti si) .. (= tj sj)) (= (f t1 ... tn) (f s1 ... sn)))
+   * which can be proven by a congruence step.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override
+  {
+    Assert(fact.getKind() == Kind::IMPLIES);
+    Assert(fact[1].getKind() == Kind::EQUAL);
+    Node a = fact[1][0];
+    Node b = fact[1][1];
+    std::vector<Node> assumps;
+    if (fact[0].getKind() == Kind::AND)
+    {
+      assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
+    }
+    else
+    {
+      assumps.push_back(fact[0]);
+    }
+    CDProof cdp(d_env);
+    if (a.getOperator() != b.getOperator())
+    {
+      // TODO: wishue #158, likely corresponds to a higher-order term
+      // indexing conflict.
+      cdp.addTrustedStep(fact, TrustId::QUANTIFIERS_PREPROCESS, {}, {});
+      return cdp.getProofFor(fact);
+    }
+    Assert(a.getNumChildren() == b.getNumChildren());
+    std::vector<Node> cargs;
+    ProofRule cr = expr::getCongRule(a, cargs);
+    size_t nchild = a.getNumChildren();
+    std::vector<Node> premises;
+    for (size_t i = 0; i < nchild; i++)
+    {
+      Node eq = a[i].eqNode(b[i]);
+      premises.push_back(eq);
+      if (a[i] == b[i])
+      {
+        cdp.addStep(eq, ProofRule::REFL, {}, {a[i]});
+      }
+      else
+      {
+        Assert(std::find(assumps.begin(), assumps.end(), eq) != assumps.end());
+      }
+    }
+    cdp.addStep(fact[1], cr, premises, cargs);
+    std::shared_ptr<ProofNode> pfn = cdp.getProofFor(fact[1]);
+    return d_env.getProofNodeManager()->mkScope(pfn, assumps);
+  }
+  /** identify */
+  std::string identify() const override { return "DeqCongProofGenerator"; }
+};
+
 TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
     : QuantifiersUtil(env),
       d_qstate(qs),
@@ -48,7 +114,9 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
       d_typeMap(context()),
       d_ops(context()),
       d_opMap(context()),
-      d_inactive_map(context())
+      d_inactive_map(context()),
+      d_dcproof(options().smt.produceProofs ? new DeqCongProofGenerator(d_env)
+                                            : nullptr)
 {
   d_true = nodeManager()->mkConst(true);
   d_false = nodeManager()->mkConst(false);
@@ -390,19 +458,19 @@ void TermDb::computeUfTerms( TNode f ) {
         congruentCount++;
         continue;
       }
-      std::vector<Node> lits;
-      if (checkCongruentDisequal(at, n, lits))
+      std::vector<Node> antec;
+      if (checkCongruentDisequal(at, n, antec))
       {
         Assert(at.getNumChildren() == n.getNumChildren());
         for (size_t k = 0, size = at.getNumChildren(); k < size; k++)
         {
           if (at[k] != n[k])
           {
-            lits.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]).negate());
+            antec.push_back(nm->mkNode(Kind::EQUAL, at[k], n[k]));
             Assert(d_qstate.areEqual(at[k], n[k]));
           }
         }
-        Node lem = nm->mkOr(lits);
+        Node lem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(antec), at.eqNode(n));
         if (TraceIsOn("term-db-lemma"))
         {
           Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
@@ -415,7 +483,10 @@ void TermDb::computeUfTerms( TNode f ) {
           }
           Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
         }
-        d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG);
+        d_qim->addPendingLemma(lem,
+                               InferenceId::QUANTIFIERS_TDB_DEQ_CONG,
+                               LemmaProperty::NONE,
+                               d_dcproof.get());
         d_qstate.notifyInConflict();
         return;
       }
@@ -442,7 +513,6 @@ bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp)
 {
   if (d_qstate.areDisequal(a, b))
   {
-    exp.push_back(a.eqNode(b));
     return true;
   }
   return false;