Regression

ajreynol · Feb 24, 2025 · 62a7349 · 62a7349
1 parent b936ead
commit 62a7349
Show file tree

Hide file tree

Showing 7 changed files with 18 additions and 2 deletions.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -3580,6 +3580,8 @@ enum ENUM(ProofRewriteRule)
   EVALUE(ARITH_INT_EQ_CONFLICT),
   /** Auto-generated from RARE rule arith-int-geq-tighten */
   EVALUE(ARITH_INT_GEQ_TIGHTEN),
+  /** Auto-generated from RARE rule arith-divisible-elim */
+  EVALUE(ARITH_DIVISIBLE_ELIM),
   /** Auto-generated from RARE rule arith-abs-eq */
   EVALUE(ARITH_ABS_EQ),
   /** Auto-generated from RARE rule arith-abs-int-gt */

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
@@ -1009,7 +1009,7 @@ bool Smt2Printer::toStreamBase(std::ostream& out,
       size_t cindex = DType::cindexOf(op);
       if (dt.isTuple())
       {
-        out << "(_ tuple.update " << DType::indexOf(op) << ")";
+        out << "(_ tuple.update " << index << ")";
       }
       else
       {
@@ -1217,6 +1217,7 @@ std::string Smt2Printer::smtKindString(Kind k)
     case Kind::TO_INTEGER: return "to_int";
     case Kind::TO_REAL: return "to_real";
     case Kind::POW: return "^";
+    case Kind::DIVISIBLE: return "divisible";
 
     // arrays theory
     case Kind::SELECT: return "select";

diff --git a/src/rewriter/mkrewrites.py b/src/rewriter/mkrewrites.py
@@ -101,7 +101,7 @@ def gen_mk_node(defns, expr):
     elif isinstance(expr, App):
         args = ",".join(gen_mk_node(defns, child) for child in expr.children)
         if expr.op in {Op.EXTRACT, Op.REPEAT, Op.ZERO_EXTEND,  Op.SIGN_EXTEND,
-                       Op.ROTATE_LEFT, Op.ROTATE_RIGHT, Op.INT_TO_BV, Op.REGEXP_LOOP}:
+                       Op.ROTATE_LEFT, Op.ROTATE_RIGHT, Op.INT_TO_BV, Op.REGEXP_LOOP, Op.DIVISIBLE}:
           args = f'nm->mkConst(GenericOp(Kind::{gen_kind(expr.op)})),' + args
           return f'nm->mkNode(Kind::APPLY_INDEXED_SYMBOLIC, {{ {args} }})'
         elif expr.op in {Op.REAL_PI}:

diff --git a/src/rewriter/node.py b/src/rewriter/node.py
@@ -130,6 +130,7 @@ def __new__(cls, symbol, kind):
     TO_INT = ('to_int', 'TO_INTEGER')
     TO_REAL = ('to_real', 'TO_REAL')
     IS_INT = ('is_int', 'IS_INTEGER')
+    DIVISIBLE = ('divisible', 'DIVISIBLE')
 
     SINE = ('sin', 'SINE')
     COSINE = ('cos', 'COSINE')

diff --git a/src/theory/arith/rewrites b/src/theory/arith/rewrites
@@ -77,6 +77,11 @@
   (>= (to_real t) c)
   (>= t cc))
 
+(define-cond-rule arith-divisible-elim ((n Int) (t Int))
+  (not (= n 0))
+  (divisible n t)
+  (= (mod_total t n) 0))
+
 ; absolute value comparisons
 
 (define-rule arith-abs-eq ((x ?) (y ?))

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -42,6 +42,7 @@ set(regress_0_tests
   regress0/arith/div.04.smt2
   regress0/arith/div.05.smt2
   regress0/arith/div.07.smt2
+  regress0/arith/divisible-unsat.smt2
   regress0/arith/exp-in-model.smt2
   regress0/arith/fuzz_3-eq.smtv1.smt2
   regress0/arith/incorrect1.smtv1.smt2

diff --git a/test/regress/cli/regress0/arith/divisible-unsat.smt2 b/test/regress/cli/regress0/arith/divisible-unsat.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () Int)
+(assert ((_ divisible 14) x))
+(assert (not ((_ divisible 7) x)))
+(check-sat)