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.
This commit is contained in:
parent
db4c76b208
commit
6eabb66742
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
function-scoping1.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
||||
^\(error
|
|
@ -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)
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
let-scoping1.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
||||
^\(error
|
|
@ -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)
|
|
@ -0,0 +1,7 @@
|
|||
CORE
|
||||
quantifier-scoping.smt2
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^unsat$
|
||||
--
|
|
@ -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)
|
|
@ -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;
|
||||
|
|
|
@ -90,6 +90,7 @@ protected:
|
|||
using renaming_counterst=std::map<irep_idt, unsigned>;
|
||||
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
|
||||
|
|
Loading…
Reference in New Issue