diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 13:18:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-20 13:18:11 -0500 |
| commit | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (patch) | |
| tree | c50d4bbb5cfeee385b2f5d1bf8e5b9281def3859 | |
| parent | ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 (diff) | |
Do not assign higher-order representative if function does not exist (#4073)
| -rw-r--r-- | src/theory/theory_model.cpp | 6 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/ho/issue4065-no-rep.smt2 | 10 |
3 files changed, 14 insertions, 3 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index bf0a82a20..7bfb0e8f3 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -669,8 +669,8 @@ bool TheoryModel::areFunctionValuesEnabled() const } void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { - Assert(d_uf_models.find(f) == d_uf_models.end()); Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; + Assert(d_uf_models.find(f) == d_uf_models.end()); if( options::ufHo() ){ //we must rewrite the function value since the definition needs to be a constant value @@ -685,9 +685,9 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { d_uf_models[f] = f_def; } - if( options::ufHo() ){ + if (options::ufHo() && d_equalityEngine->hasTerm(f)) + { Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; - Assert(d_equalityEngine->hasTerm(f)); // assign to representative if higher-order Node r = d_equalityEngine->getRepresentative( f ); //always replace the representative, since it is initially assigned to itself diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fd4f2aef0..be96ca70d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1300,6 +1300,7 @@ set(regress_1_tests regress1/gensys_brn001.smt2 regress1/ho/fta0328.lfho.p regress1/ho/issue3136-fconst-bool-bool.smt2 + regress1/ho/issue4065-no-rep.smt2 regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 new file mode 100644 index 000000000..841d050a7 --- /dev/null +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -0,0 +1,10 @@ +(set-logic AUFBV) +(set-info :status sat) +(set-option :bv-div-zero-const false) +(set-option :fmf-bound-int true) +(set-option :uf-ho true) +(declare-fun _substvar_20_ () Bool) +(declare-sort S4 0) +(assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true))) +(check-sat) +(exit) |