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

ajreynol · Dec 20, 2024 · 4f05d0a · 4f05d0a
2 parents 1502035 + 96a35d7
commit 4f05d0a
Show file tree

Hide file tree

Showing 14 changed files with 78 additions and 26 deletions.
diff --git a/proofs/eo/cpc/theories/BitVectors.eo b/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

diff --git a/proofs/eo/cpc/theories/Datatypes.eo b/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))
diff --git a/src/proof/alf/alf_node_converter.cpp b/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"
@@ -552,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())
+      if (op.getSkolemId() == SkolemId::SHARED_SELECTOR)
       {
-        return ret;
-      }
-      unsigned index = DType::indexOf(op);
-      const DType& dt = DType::datatypeOf(op);
-      if (dt.isTuple())
-      {
-        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

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
@@ -1139,7 +1139,7 @@ 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");

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/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];

diff --git a/src/theory/datatypes/proof_checker.cpp b/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)
 {
 }
 

diff --git a/src/theory/datatypes/proof_checker.h b/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

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/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);

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
@@ -74,6 +74,8 @@ class DeqCongProofGenerator : protected EnvObj, public ProofGenerator
     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);
     }
@@ -90,6 +92,10 @@ class DeqCongProofGenerator : protected EnvObj, public ProofGenerator
       {
         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]);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -727,6 +727,7 @@ set(regress_0_tests
   regress0/datatypes/pair-real-bool.smt2
   regress0/datatypes/par-updater-type-rule.smt2
   regress0/datatypes/parametric-alt-list.cvc.smt2
+  regress0/datatypes/pf-v2l60078.smt2
   regress0/datatypes/proj-issue172.smt2
   regress0/datatypes/proj-issue474-app-cons-value.smt2
   regress0/datatypes/proj-issue578-clash-pf.smt2
@@ -1468,6 +1469,7 @@ set(regress_0_tests
   regress0/quantifiers/dd_german169_semi_eval.smt2
   regress0/quantifiers/dd_spark2014-pat.smt2
   regress0/quantifiers/dd_TwoSquares.z3.611901.smt2
+  regress0/quantifiers/dd_SA10-027-dt-ipc.smt2
   regress0/quantifiers/dd.german169-ieval.smt2
   regress0/quantifiers/dd.german169-lemma-inp.smt2
   regress0/quantifiers/dd.ho-matching-enum.smt2
@@ -2890,6 +2892,7 @@ set(regress_1_tests
   regress1/quantifiers/nra-interleave-inst.smt2
   regress1/quantifiers/opisavailable-12.smt2
   regress1/quantifiers/parametric-lists.smt2
+  regress1/quantifiers/pivc-deq-cong.smt2
   regress1/quantifiers/pool-decidable-arrays-1.smt2
   regress1/quantifiers/pool-example.smt2
   regress1/quantifiers/pool-tuple.smt2

diff --git a/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2 b/test/regress/cli/regress0/datatypes/pf-v2l60078.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_DT)
+(declare-datatypes ((n 0) (l 0) (t 0)) (((z)) ((ln) (n (r l))) ((f))))
+(declare-fun x () l)
+(assert (and (not (= ln (r x))) (not ((_ is n) (r x)))))
+(check-sat)
diff --git a/test/regress/cli/regress0/proofs/t3_rw903.smt2 b/test/regress/cli/regress0/proofs/t3_rw903.smt2
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
+; DISABLE-TESTER: lfsc
 (set-logic UFNIA)
 (declare-fun pow2 (Int) Int)
 (declare-fun intor (Int Int Int) Int)

diff --git a/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2 b/test/regress/cli/regress0/quantifiers/dd_SA10-027-dt-ipc.smt2
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; DISABLE-TESTER: cpc
+; Disabled cpc due to congruence on overloaded user functions.
+(set-logic ALL)
+(declare-sort i 0)
+(declare-sort s 0)
+(declare-datatypes ((u 0)) (((us (r Bool) (e Int) (c s)))))
+(declare-datatypes ((us_ 0)) (((us (c i) (e u)))))
+(declare-datatypes ((_r 0)) (((s_ (_s us_)))))
+(declare-fun s_ (s) _r)
+(declare-fun us (_r) s)
+(assert (forall ((x _r)) (= x (s_ (us x)))))
+(declare-const n u)
+(assert (exists ((x_ us_)) (not (=> (r n) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c n)))) n))))))) (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (forall ((o u)) (or (forall ((x us_)) (or (exists ((t u)) (= (r o) (= (r o) (r (e (_s (s_ (c t)))))))) (= (s_ x_) (s_ (c (us false 0 (us (s_ (us (c (_s (s_ (c o)))) (us (r (e (_s (s_ (c (us false 0 (us (s_ x_)))))))) (e (e (_s (s_ (c o))))) (us (s_ x_))))))))))))))))))))))))))
+(check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2 b/test/regress/cli/regress1/quantifiers/pivc-deq-cong.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --enum-inst
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun V () Int)
+(declare-fun e () Int)
+(declare-fun a2 () (Array Int Int))
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(assert (and (< i V) (<= 0 i) (forall ((? Int)) (= 1 (select a2 i))) (forall ((? Int)) (= (select a ?) (select a2 ?))) (forall ((? Int)) (forall ((? Int)) (= 1 (select a2 ?)))) (forall ((? Int)) (or (distinct e (select a ?)) (> ? (- i 1)))) (or (and (= 1 V) (exists ((? Int)) (> 1 (select a 0)))) (exists ((? Int)) (and (<= ? i) (= e (select a ?)))))))
+(check-sat)