ff: fix rewriter (cvc5#10632)

I'm not sure combining like terms can be expressed in a single pass (without fully flattening) Thanks for setting up the fuzzer, Mathias! fixes cvc5/cvc5-projects#704
HanielB · Apr 17, 2024 · f8c069c · f8c069c
1 parent 58a68cf
commit f8c069c
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git a/src/theory/ff/theory_ff_rewriter.cpp b/src/theory/ff/theory_ff_rewriter.cpp
@@ -62,7 +62,8 @@ Node TheoryFiniteFieldsRewriter::preRewriteFfNeg(TNode t)
 {
   Assert(t.getKind() == Kind::FINITE_FIELD_NEG);
   NodeManager* const nm = nodeManager();
-  const Node negOne = nm->mkConst(FiniteFieldValue(Integer(-1), t.getType().getFfSize()));
+  const Node negOne =
+      nm->mkConst(FiniteFieldValue(Integer(-1), t.getType().getFfSize()));
   return nm->mkNode(Kind::FINITE_FIELD_MULT, negOne, t[0]);
 }
 
@@ -213,7 +214,10 @@ RewriteResponse TheoryFiniteFieldsRewriter::postRewrite(TNode t)
   {
     case Kind::FINITE_FIELD_NEG: return RewriteResponse(REWRITE_DONE, t);
     case Kind::FINITE_FIELD_ADD:
-      return RewriteResponse(REWRITE_DONE, postRewriteFfAdd(t));
+    {
+      Node nt = postRewriteFfAdd(t);
+      return RewriteResponse(nt == t ? REWRITE_DONE : REWRITE_AGAIN, nt);
+    }
     case Kind::FINITE_FIELD_MULT:
       return RewriteResponse(REWRITE_DONE, postRewriteFfMult(t));
     case Kind::EQUAL: return RewriteResponse(REWRITE_DONE, postRewriteFfEq(t));

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -787,6 +787,7 @@ set(regress_0_tests
   regress0/ff/bool_nary_or_unsound.smt2
   regress0/ff/combination.smt2
   regress0/ff/ctx.smt2
+  regress0/ff/proj-issue704.smt2
   regress0/ff/ff_is_zero_sound.smt2
   regress0/ff/ff_is_zero_unsound.smt2
   regress0/ff/ff_xor_sound.smt2

diff --git a/test/regress/cli/regress0/ff/proj-issue704.smt2 b/test/regress/cli/regress0/ff/proj-issue704.smt2
@@ -0,0 +1,8 @@
+; SCRUBBER: grep -w 'sat'
+(set-option :check-models true)
+(set-logic QF_FF)
+(set-info :status sat)
+(declare-const x (_ FiniteField 13))
+(check-sat)
+(get-value ((ff.add (ff.mul x x) (ff.mul (ff.mul #f93m13 (ff.neg #f93m13)) (ff.add #f93m13 (ff.mul x x) (ff.mul #f93m13 (ff.neg #f93m13)))) (ff.mul (ff.mul #f93m13 (ff.neg #f93m13)) (ff.add #f93m13 (ff.mul x x) (ff.mul #f93m13 (ff.neg #f93m13)))) (ff.mul (ff.mul #f93m13 (ff.neg #f93m13)) (ff.add #f93m13 (ff.mul x x) (ff.mul #f93m13 (ff.neg #f93m13)))))))
+