Simplify and fix check models (#5685)

Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.

However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.

Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.

This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.

A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.

Fixes #5645.

1 files changed, 5 insertions, 0 deletions

diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
new file mode 100644
index 000000000..0d3f711bf
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((Enum1 0)) (((None) (cons (data Bool)))))
+(assert (forall ((var_1 Enum1)) (data var_1)))
+(check-sat)