From 7841167c829fe524b350f7c1b05647e13aac59be Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Apr 2022 05:31:27 -0500 Subject: [PATCH] Fix for get-value with empty uninterpreted sort domain (#8547) Alternative for https://github.com/cvc5/cvc5/pull/8546. We were mistakenly using `mkGroundTerm` instead of `mkGroundValue` to make the domain of an uninterpreted sort non-empty. This ensures that get-value calls do not throw a spurious exception when there is a declared uninterpreted sort and there are no terms of that sort. As a result, this also required fixing a few further issues regarding how uninterpreted sort constants are printed in models, and fixing the expected results on 2 more regressions. --- src/parser/parser.cpp | 12 +++++++++- src/printer/smt2/smt2_printer.cpp | 24 ++++++++++++++----- src/theory/theory_model.cpp | 4 +++- test/regress/cli/CMakeLists.txt | 1 + .../regress0/cvc5-printing.cpp-sample.smt2 | 24 +++++++++++++++++++ test/regress/cli/regress0/models-print-2.smt2 | 3 ++- .../cli/regress0/printer/empty_sort.smt2 | 6 ++--- 7 files changed, 62 insertions(+), 12 deletions(-) create mode 100644 test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5e82012dd..5bd4c1c9c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -731,9 +731,19 @@ void Parser::pushGetValueScope() for (const cvc5::Sort& s : declareSorts) { std::vector elements = d_solver->getModelDomainElements(s); + Trace("parser") << "elements for " << s << ":" << std::endl; for (const cvc5::Term& e : elements) { - defineVar(e.getUninterpretedSortValue(), e); + Trace("parser") << " " << e.getKind() << " " << e << std::endl; + if (e.getKind() == Kind::UNINTERPRETED_SORT_VALUE) + { + defineVar(e.getUninterpretedSortValue(), e); + } + else + { + Assert(false) + << "model domain element is not an uninterpreted sort value: " << e; + } } } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2aab3d980..f8f3af1b5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1403,15 +1403,27 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, // print the representatives for (const Node& trn : elements) { - if (trn.isVar()) + if (options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DeclSortAndFun + || options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DeclFun) { - if (options::modelUninterpPrint() - == options::ModelUninterpPrintMode::DeclSortAndFun - || options::modelUninterpPrint() - == options::ModelUninterpPrintMode::DeclFun) + out << "(declare-fun "; + if (trn.getKind() == kind::UNINTERPRETED_SORT_VALUE) { - out << "(declare-fun " << trn << " () " << tn << ")" << endl; + // prints as raw symbol + const UninterpretedSortValue& av = + trn.getConst(); + out << av; } + else + { + Assert(false) + << "model domain element is not an uninterpreted sort value: " + << trn; + out << trn; + } + out << " () " << tn << ")" << endl; } else { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index c6962d171..87c9ce21c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -118,8 +118,10 @@ std::vector TheoryModel::getDomainElements(TypeNode tn) const { // This is called when t is a sort that does not occur in this model. // Sorts are always interpreted as non-empty, thus we add a single element. + // We use mkGroundValue here, since domain elements must all be + // of UNINTERPRETED_SORT_VALUE kind. NodeManager* nm = NodeManager::currentNM(); - elements.push_back(nm->mkGroundTerm(tn)); + elements.push_back(nm->mkGroundValue(tn)); return elements; } return *type_refs; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index d6be8cafd..e40ee670e 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -490,6 +490,7 @@ set(regress_0_tests regress0/cvc3.userdoc.04.cvc.smt2 regress0/cvc3.userdoc.05.cvc.smt2 regress0/cvc3.userdoc.06.cvc.smt2 + regress0/cvc5-printing.cpp-sample.smt2 regress0/datatypes/4482-unc-simp-one.smt2 regress0/datatypes/boolean-equality.cvc.smt2 regress0/datatypes/boolean-terms-datatype.cvc.smt2 diff --git a/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 b/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 new file mode 100644 index 000000000..da362a21e --- /dev/null +++ b/test/regress/cli/regress0/cvc5-printing.cpp-sample.smt2 @@ -0,0 +1,24 @@ +; SCRUBBER: sed -e 's/((x.*//g' +; EXPECT: unsat +; EXPECT: sat +(set-option :bv-print-consts-as-indexed-symbols true) +(set-logic QF_AUFBV) +(set-option :produce-models true) +(set-option :incremental true) +(set-option :produce-unsat-assumptions true) +(declare-sort S 0) +(declare-fun x () (_ BitVec 32)) +(declare-fun y () (_ BitVec 32)) +(declare-fun arr () (Array (_ BitVec 32) (_ BitVec 32))) +(declare-fun f ((_ BitVec 32) ) S) +(declare-fun s () S) +(declare-fun ind1 () Bool) +(push 1) +(assert ind1) +(assert (= ind1 (= (f x) s))) +(assert (= (f x) s)) +(assert (not (=> (= x y) (= (select arr x) (select arr y))))) +(check-sat-assuming (ind1 )) +(pop 1) +(check-sat) +(get-value (x)) diff --git a/test/regress/cli/regress0/models-print-2.smt2 b/test/regress/cli/regress0/models-print-2.smt2 index 1e176d5c2..286bbc13b 100644 --- a/test/regress/cli/regress0/models-print-2.smt2 +++ b/test/regress/cli/regress0/models-print-2.smt2 @@ -1,7 +1,8 @@ ; the purpose of this test is to verify that there is a `as` term in the output. ; the scrubber excludes all lines without "(as @", and replaces this pattern by "AS". -; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /^($/d; /^)$/d' +; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /rep/d; /^($/d; /^)$/d' +; EXPECT: AS ; EXPECT: AS (set-logic QF_UF) (set-option :produce-models true) diff --git a/test/regress/cli/regress0/printer/empty_sort.smt2 b/test/regress/cli/regress0/printer/empty_sort.smt2 index eb963e443..5c4ec7a9e 100644 --- a/test/regress/cli/regress0/printer/empty_sort.smt2 +++ b/test/regress/cli/regress0/printer/empty_sort.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --model-u-print=decl-fun -; EXPECT: (declare-fun gt () us_image) -; EXPECT: (declare-fun gt () ||) -; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun gt/g' +; EXPECT: (declare-fun a () us_image) +; EXPECT: (declare-fun a () ||) +; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun a/g' (set-option :produce-models true) (set-logic QF_UF) (declare-sort us_image 0) -- 2.30.2