now qepcad-sat checks whether input is quantifier-free or not and giv…

…es a helpful message if not.
chriswestbrown · Jul 19, 2024 · 2f3270a · 2f3270a
1 parent 9a9b9bf
commit 2f3270a
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/interpreter/src/shell/qepcad-inter/qepcad-inter.h b/interpreter/src/shell/qepcad-inter/qepcad-inter.h
@@ -95,6 +95,9 @@ class CommQepcadSat : public EICommand
       else return new ErrObj("Symbol not understood");
     }
     // TODO!! check that F is quantifier free
+    if (!isQuantifierFree(F)) {
+      return new ErrObj("Input has quantifiers: 'qepcad-sat' requires a quantifier-free formula.  Try 'qepcad-qe'.  See (help 'qepcad-sat).");
+    }
     TAndRef Fp = new TAndObj();
     Fp->AND(F);
     bool conjunctionCase = isConjunctionOfAtoms(Fp);