From 6eabb667423f53a2d791aacae14b37614a39ba70 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 8 Oct 2019 17:04:32 +0100 Subject: [PATCH] fix for SMT-LIB2 scopes for function definitions and let SMT-LIB2 function definitions have scopes for the identifiers of the parameters. The same holds for let expressions. This was raised in #5143. The need to make the scoped identifiers unique will be removed once the IR bindings have scopes. --- .../function-scoping1.desc | 8 +++ .../function-scoping1.smt2 | 12 +++++ regression/smt2_solver/let1/let-scoping1.desc | 8 +++ regression/smt2_solver/let1/let-scoping1.smt2 | 12 +++++ .../quanitfiers/quantifier-scoping.desc | 7 +++ .../quanitfiers/quantifier-scoping.smt2 | 12 +++++ src/solvers/smt2/smt2_parser.cpp | 49 +++++++++++-------- src/solvers/smt2/smt2_parser.h | 1 + 8 files changed, 88 insertions(+), 21 deletions(-) create mode 100644 regression/smt2_solver/function-applications/function-scoping1.desc create mode 100644 regression/smt2_solver/function-applications/function-scoping1.smt2 create mode 100644 regression/smt2_solver/let1/let-scoping1.desc create mode 100644 regression/smt2_solver/let1/let-scoping1.smt2 create mode 100644 regression/smt2_solver/quanitfiers/quantifier-scoping.desc create mode 100644 regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 diff --git a/regression/smt2_solver/function-applications/function-scoping1.desc b/regression/smt2_solver/function-applications/function-scoping1.desc new file mode 100644 index 0000000000..d11ad10609 --- /dev/null +++ b/regression/smt2_solver/function-applications/function-scoping1.desc @@ -0,0 +1,8 @@ +CORE +function-scoping1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +^\(error diff --git a/regression/smt2_solver/function-applications/function-scoping1.smt2 b/regression/smt2_solver/function-applications/function-scoping1.smt2 new file mode 100644 index 0000000000..aec9f7eeae --- /dev/null +++ b/regression/smt2_solver/function-applications/function-scoping1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_BV) + +; the function parameters are in a separate scope + +(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) + (ite (bvule a b) a b)) + +(declare-const a (_ BitVec 32)) + +(assert (not (= a a))) + +(check-sat) diff --git a/regression/smt2_solver/let1/let-scoping1.desc b/regression/smt2_solver/let1/let-scoping1.desc new file mode 100644 index 0000000000..ed6e233f85 --- /dev/null +++ b/regression/smt2_solver/let1/let-scoping1.desc @@ -0,0 +1,8 @@ +CORE +let-scoping1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- +^\(error diff --git a/regression/smt2_solver/let1/let-scoping1.smt2 b/regression/smt2_solver/let1/let-scoping1.smt2 new file mode 100644 index 0000000000..be9c681edb --- /dev/null +++ b/regression/smt2_solver/let1/let-scoping1.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_BV) + +; the let parameters are in a separate scope +(define-fun let1 () Bool (let ((a true)) a)) +(declare-const a (_ BitVec 32)) +(assert (not (= a a))) + +; declare-const first +(declare-const b (_ BitVec 32)) +(define-fun let2 () Bool (let ((b true)) b)) + +(check-sat) diff --git a/regression/smt2_solver/quanitfiers/quantifier-scoping.desc b/regression/smt2_solver/quanitfiers/quantifier-scoping.desc new file mode 100644 index 0000000000..56b99e2b74 --- /dev/null +++ b/regression/smt2_solver/quanitfiers/quantifier-scoping.desc @@ -0,0 +1,7 @@ +CORE +quantifier-scoping.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 b/regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 new file mode 100644 index 0000000000..409e0f938c --- /dev/null +++ b/regression/smt2_solver/quanitfiers/quantifier-scoping.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_BV) + +; the quantified identifiers are in a separate scope +(define-fun q1 () Bool (exists ((a Bool)) a)) +(declare-const a (_ BitVec 32)) +(assert (not (= a a))) + +; declare-const first +(declare-const b (_ BitVec 32)) +(define-fun q2 () Bool (exists ((b Bool)) b)) + +(check-sat) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index fcf85854fd..7fa30c4d08 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -130,16 +130,6 @@ exprt::operandst smt2_parsert::operands() irep_idt smt2_parsert::add_fresh_id(const irep_idt &id, const exprt &expr) { - if(id_map - .emplace( - std::piecewise_construct, - std::forward_as_tuple(id), - std::forward_as_tuple(expr)) - .second) - { - return id; // id not yet used - } - auto &count=renaming_counters[id]; irep_idt new_id; do @@ -159,6 +149,20 @@ irep_idt smt2_parsert::add_fresh_id(const irep_idt &id, const exprt &expr) return new_id; } +void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr) +{ + if(!id_map + .emplace( + std::piecewise_construct, + std::forward_as_tuple(id), + std::forward_as_tuple(expr)) + .second) + { + // id already used + throw error() << "identifier '" << id << "' defined twice"; + } +} + irep_idt smt2_parsert::rename_id(const irep_idt &id) const { auto it=renaming_map.find(id); @@ -261,12 +265,16 @@ exprt smt2_parsert::quantifier_expression(irep_idt id) if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' at end of bindings"); - // go forwards, add to id_map - for(const auto &b : bindings) + // save the renaming map + renaming_mapt old_renaming_map = renaming_map; + + // go forwards, add to id_map, renaming if need be + for(auto &b : bindings) { const irep_idt id = add_fresh_id(b.get_identifier(), exprt(ID_nil, b.type())); - CHECK_RETURN(id == b.get_identifier()); + + b.set_identifier(id); } exprt expr=expression(); @@ -280,6 +288,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id) for(const auto &b : bindings) id_map.erase(b.get_identifier()); + // restore renaming map + renaming_map = old_renaming_map; + // go backwards, build quantified expression for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++) { @@ -1244,8 +1255,7 @@ void smt2_parsert::setup_commands() irep_idt id = smt2_tokenizer.get_buffer(); auto type = sort(); - if(add_fresh_id(id, exprt(ID_nil, type)) != id) - throw error() << "identifier '" << id << "' defined twice"; + add_unique_id(id, exprt(ID_nil, type)); }; // declare-var appears to be a synonym for declare-const that is @@ -1259,8 +1269,7 @@ void smt2_parsert::setup_commands() irep_idt id = smt2_tokenizer.get_buffer(); auto type = function_signature_declaration(); - if(add_fresh_id(id, exprt(ID_nil, type)) != id) - throw error() << "identifier '" << id << "' defined twice"; + add_unique_id(id, exprt(ID_nil, type)); }; commands["define-const"] = [this]() { @@ -1281,8 +1290,7 @@ void smt2_parsert::setup_commands() } // create the entry - if(add_fresh_id(id, value) != id) - throw error() << "identifier '" << id << "' defined twice"; + add_unique_id(id, value); }; commands["define-fun"] = [this]() { @@ -1319,8 +1327,7 @@ void smt2_parsert::setup_commands() } // create the entry - if(add_fresh_id(id, body) != id) - throw error() << "identifier '" << id << "' defined twice"; + add_unique_id(id, body); id_map.at(id).type = signature.type; id_map.at(id).parameters = signature.parameters; diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 29f30af8a7..7636e35ade 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -90,6 +90,7 @@ protected: using renaming_counterst=std::map; renaming_counterst renaming_counters; irep_idt add_fresh_id(const irep_idt &, const exprt &); + void add_unique_id(const irep_idt &, const exprt &); irep_idt rename_id(const irep_idt &) const; struct signature_with_parameter_idst