Skip to content

Commit 1d685bf

Browse files
committed
Track conversion and use identifier instead of expression
This tracks when an expression is converted by storing the identifier in the SMT output in the defined_expressions map. Then when asserting this expression, merely assert the identifier and don't duplicate the expression in the output.
1 parent 3e0007f commit 1d685bf

File tree

1 file changed

+22
-6
lines changed

1 file changed

+22
-6
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 22 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -744,6 +744,14 @@ literalt smt2_convt::convert(const exprt &expr)
744744
no_boolean_variables++;
745745

746746
out << "; convert\n";
747+
out << "; Converting var_no " << l.var_no() << " with expr ID of "
748+
<< expr.id_string() << "\n";
749+
// We're converting the expression, so store it in the defined_expressions
750+
// store and in future we use the literal instead of the whole expression
751+
// Note that here we are always converting, so we do not need to consider
752+
// other literal kinds, only "|B###|"
753+
defined_expressions[expr] =
754+
std::string{"|B"} + std::to_string(l.var_no()) + "|";
747755
out << "(define-fun ";
748756
convert_literal(l);
749757
out << " () Bool ";
@@ -4332,18 +4340,26 @@ void smt2_convt::set_to(const exprt &expr, bool value)
43324340

43334341
out << "; set_to " << (value?"true":"false") << "\n"
43344342
<< "(assert ";
4335-
43364343
if(!value)
43374344
{
43384345
out << "(not ";
4339-
convert_expr(prepared_expr);
4340-
out << ")";
4346+
}
4347+
const auto found_literal = defined_expressions.find(expr);
4348+
if(!(found_literal == defined_expressions.end()))
4349+
{
4350+
// This is a converted expression, we can just assert the literal name
4351+
// since the expression is already defined
4352+
out << found_literal->second;
43414353
}
43424354
else
4355+
{
43434356
convert_expr(prepared_expr);
4344-
4345-
out << ")" << "\n"; // assert
4346-
4357+
}
4358+
if(!value)
4359+
{
4360+
out << ")";
4361+
}
4362+
out << ")\n";
43474363
return;
43484364
}
43494365

0 commit comments

Comments
 (0)