Change syntax for const/var in cpc proofs (cvc5#11512)

This makes the syntax of CPC proofs not have `eo::` in it, which is
ideally hidden in the *.eo signature.

It also changes generic free constants `const` -> `@const`, which was
not properly named.

---------

Co-authored-by: Hans-Jörg <[email protected]>

proofs/eo/cpc/Cpc.eo

@@ -81,6 +81,15 @@
 ;   and are used to model cvc5's internal symbols, including its skolems,
 ;   other internally introduced terms, and extensions.
 
+; note: >
+;   @const corresponds to generic abstract constants, which correspond to internally
+;   introduced terms that do not have a formal definition in the signature.
+(declare-const @const (-> (! Int :opaque) (! Type :opaque :var T) T))
+
+; note: >
+;   @var is an alias of eo::var to ensure the cpc proof does not use eo::var.
+(define @var ((s String) (T Type)) (eo::var s T))
+
 ; disclaimer: this function is not in SMT-LIB.
 (declare-const fmf.card (-> Type Int Bool))
 ; disclaimer: this function is not in SMT-LIB.

proofs/eo/cpc/theories/Builtin.eo

@@ -53,9 +53,5 @@
 
 (declare-const distinct (-> (! Type :var A :implicit) A A Bool) :pairwise and)
 
-; generic variables
-; NOTE: does not check that U is a numeral
-(declare-const const (-> (! Type :var U :implicit) (! U :opaque) (! Type :opaque :var T) T))
-
 ; The purification skolem.
 (declare-const @purify (-> (! Type :var A :implicit) (! A :opaque) A))

src/proof/alf/alf_node_converter.cpp

@@ -83,7 +83,14 @@ Node AlfNodeConverter::postConvert(Node n)
     // dummy node, return it
     return n;
   }
-  if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM || k == Kind::INST_CONSTANT)
+  // case for skolems, unhandled variables, and other unhandled terms
+  // These should print as @const, or otherwise be printed as a skolem,
+  // which may need further processing below. In the case of unhandled
+  // terms (e.g. DT_SYGUS_EVAL), we prefer printing them as @const instead
+  // of using their smt2 printer, which would lead to undeclared identifiers in
+  // the proof.
+  if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM || k == Kind::INST_CONSTANT
+      || k == Kind::DT_SYGUS_EVAL)
   {
     TypeNode tn = n.getType();
     // constructors/selectors are represented by skolems, which are defined
@@ -110,7 +117,7 @@ Node AlfNodeConverter::postConvert(Node n)
     // is used as (var N T) throughout.
     Node index = d_nm->mkConstInt(Rational(getOrAssignIndexForConst(n)));
     Node tc = typeAsNode(tn);
-    return mkInternalApp("const", {index, tc}, tn);
+    return mkInternalApp("@const", {index, tc}, tn);
   }
   else if (k == Kind::BOUND_VARIABLE)
   {
@@ -127,15 +134,16 @@ Node AlfNodeConverter::postConvert(Node n)
       ss << n;
       sname = ss.str();
     }
-    // A variable x of type T can unambiguously referred to as (eo::var "x" T).
+    // A variable x of type T can unambiguously referred to as (@var "x" T),
+    // which is a macro for (eo::var "x" T) in the cpc signature.
     // We convert to this representation here, which will often be letified.
     TypeNode tn = n.getType();
     std::vector<Node> args;
     Node nn = d_nm->mkConst(String(sname));
     args.push_back(nn);
     Node tnn = typeAsNode(tn);
     args.push_back(tnn);
-    return mkInternalApp("eo::var", args, tn);
+    return mkInternalApp("@var", args, tn);
   }
   else if (k == Kind::VARIABLE)
   {
@@ -615,7 +623,6 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n)
 
 size_t AlfNodeConverter::getOrAssignIndexForConst(Node v)
 {
-  Assert(v.isVar());
   std::map<Node, size_t>::iterator it = d_constIndex.find(v);
   if (it != d_constIndex.end())
   {

test/regress/cli/CMakeLists.txt

@@ -2830,6 +2830,7 @@ set(regress_1_tests
   regress1/quantifiers/choice-move-delta-relt.smt2
   regress1/quantifiers/const.cvc.smt2
   regress1/quantifiers/constfunc.cvc.smt2
+  regress1/quantifiers/dd_verisec-dt-sygus.smt2
   regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
   regress1/quantifiers/dd.bug812-ieval.smt2
   regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2

test/regress/cli/regress1/quantifiers/dd_verisec-dt-sygus.smt2

@@ -0,0 +1,6 @@
+; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+(set-logic NIA)
+(declare-const x Int)
+(assert (or (forall ((v Int) (v_ Int)) (or (= 1 v) (< 16777215 (mod (+ v_ (mod (+ x (mod v_ 8)) 53687091)) 33554432))))))
+(check-sat)