Skip to content

smt2 id_map: Do not use nil_typet when we mean "optional" [blocks: #3800] #3948

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 27, 2019
Merged

smt2 id_map: Do not use nil_typet when we mean "optional" [blocks: #3800] #3948

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
228f512
SMT2: Function parameters have local scope
tautschnig Jan 27, 2019
7792612
smt2 id_map: Do not use nil_typet to detect map insert
tautschnig Jan 25, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions regression/smt2_solver/basic-bv1/basic-bv1.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@
(= a #x4)
(= a #x8))))

; make sure this still type checks as we have used x with a different type above
(define-fun d02 () Bool (= (bvand (bvnot x) (bvnot y)) (bvnot (bvor x y))))

; Predicates over Bitvectors

(define-fun p1 () Bool (= (bvule #x0a #xf0) true)) ; unsigned less or equal
Expand Down
75 changes: 36 additions & 39 deletions src/solvers/smt2/smt2_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,22 +118,33 @@ exprt::operandst smt2_parsert::operands()
return result;
}

irep_idt smt2_parsert::get_fresh_id(const irep_idt &id)
irep_idt smt2_parsert::add_fresh_id(const irep_idt &id, const exprt &expr)
{
if(id_map[id].type.is_nil())
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
{
new_id=id2string(id)+'#'+std::to_string(count);
count++;
}
while(id_map.find(new_id)!=id_map.end());
} while(!id_map
.emplace(
std::piecewise_construct,
std::forward_as_tuple(new_id),
std::forward_as_tuple(expr))
.second);

// record renaming
renaming_map[id]=new_id;
renaming_map[id] = new_id;

return new_id;
}
Expand Down Expand Up @@ -184,10 +195,7 @@ exprt smt2_parsert::let_expression()
for(auto &b : bindings)
{
// get a fresh id for it
b.first=get_fresh_id(b.first);
auto &entry=id_map[b.first];
entry.type=b.second.type();
entry.definition=b.second;
b.first = add_fresh_id(b.first, b.second);
}

exprt expr=expression();
Expand Down Expand Up @@ -246,9 +254,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
// go forwards, add to id_map
for(const auto &b : bindings)
{
auto &entry=id_map[b.get_identifier()];
entry.type=b.type();
entry.definition=nil_exprt();
const irep_idt id =
add_fresh_id(b.get_identifier(), exprt(ID_nil, b.type()));
CHECK_RETURN(id == b.get_identifier());
}

exprt expr=expression();
Expand Down Expand Up @@ -1131,12 +1139,9 @@ smt2_parsert::function_signature_definition()
throw error("expected symbol in parameter");

irep_idt id = smt2_tokenizer.get_buffer();
parameters.push_back(id);
domain.push_back(sort());

auto &entry=id_map[id];
entry.type = domain.back();
entry.definition=nil_exprt();
parameters.push_back(add_fresh_id(id, exprt(ID_nil, domain.back())));

if(next_token() != smt2_tokenizert::CLOSE)
throw error("expected ')' at end of parameter");
Expand Down Expand Up @@ -1196,12 +1201,8 @@ void smt2_parsert::command(const std::string &c)
irep_idt id = smt2_tokenizer.get_buffer();
auto type = sort();

if(id_map.find(id)!=id_map.end())
if(add_fresh_id(id, exprt(ID_nil, type)) != id)
throw error() << "identifier `" << id << "' defined twice";

auto &entry = id_map[id];
entry.type = type;
entry.definition = nil_exprt();
}
else if(c=="declare-fun")
{
Expand All @@ -1211,12 +1212,8 @@ void smt2_parsert::command(const std::string &c)
irep_idt id = smt2_tokenizer.get_buffer();
auto type = function_signature_declaration();

if(id_map.find(id)!=id_map.end())
if(add_fresh_id(id, exprt(ID_nil, type)) != id)
throw error() << "identifier `" << id << "' defined twice";

auto &entry = id_map[id];
entry.type = type;
entry.definition = nil_exprt();
}
else if(c == "define-const")
{
Expand All @@ -1225,9 +1222,6 @@ void smt2_parsert::command(const std::string &c)

const irep_idt id = smt2_tokenizer.get_buffer();

if(id_map.find(id) != id_map.end())
throw error() << "identifier `" << id << "' defined twice";

const auto type = sort();
const auto value = expression();

Expand All @@ -1240,23 +1234,25 @@ void smt2_parsert::command(const std::string &c)
}

// create the entry
auto &entry = id_map[id];
entry.type = type;
entry.definition = value;
if(add_fresh_id(id, value) != id)
throw error() << "identifier `" << id << "' defined twice";
}
else if(c=="define-fun")
{
if(next_token() != smt2_tokenizert::SYMBOL)
throw error("expected a symbol after define-fun");

const irep_idt id = smt2_tokenizer.get_buffer();
// save the renaming map
renaming_mapt old_renaming_map = renaming_map;

if(id_map.find(id)!=id_map.end())
throw error() << "identifier `" << id << "' defined twice";
const irep_idt id = smt2_tokenizer.get_buffer();

const auto signature = function_signature_definition();
const auto body = expression();

// restore renamings
std::swap(renaming_map, old_renaming_map);

// check type of body
if(signature.type.id() == ID_mathematical_function)
{
Expand All @@ -1276,10 +1272,11 @@ void smt2_parsert::command(const std::string &c)
}

// create the entry
auto &entry = id_map[id];
entry.type = signature.type;
entry.parameters = signature.parameters;
entry.definition = body;
if(add_fresh_id(id, body) != id)
throw error() << "identifier `" << id << "' defined twice";

id_map.at(id).type = signature.type;
id_map.at(id).parameters = signature.parameters;
}
else if(c=="exit")
{
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/smt2/smt2_parser.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ class smt2_parsert

struct idt
{
idt():type(nil_typet())
explicit idt(const exprt &expr) : type(expr.type()), definition(expr)
{
}

Expand Down Expand Up @@ -84,7 +84,7 @@ class smt2_parsert
renaming_mapt renaming_map;
using renaming_counterst=std::map<irep_idt, unsigned>;
renaming_counterst renaming_counters;
irep_idt get_fresh_id(const irep_idt &);
irep_idt add_fresh_id(const irep_idt &, const exprt &);
irep_idt rename_id(const irep_idt &) const;

struct signature_with_parameter_idst
Expand Down