Skip to content

Commit 246472f

Browse files
author
Daniel Kroening
committed
an SMT2 solver using boolbv and satcheckt
1 parent a75ee3f commit 246472f

File tree

4 files changed

+287
-6
lines changed

4 files changed

+287
-6
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,8 @@ src/goto-instrument/goto-instrument.exe
104104
src/jbmc/jbmc
105105
src/musketeer/musketeer
106106
src/musketeer/musketeer.exe
107+
src/solvers/smt2/smt2_solver
108+
src/solvers/smt2/smt2_solver.exe
107109
src/symex/symex
108110
src/symex/symex.exe
109111
src/goto-diff/goto-diff

‎src/solvers/CMakeLists.txt

+8-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
set(CMAKE_CXX_STANDARD 11)
2+
set(CMAKE_CXX_STANDARD_REQUIRED true)
3+
14
# We may use one of several different solver libraries.
25
# The following files wrap the chosen solver library.
36
# We remove them all from the solver-library sources list, and then add the
@@ -104,6 +107,10 @@ elseif("${sat_impl}" STREQUAL "glucose")
104107
target_link_libraries(solvers glucose-condensed)
105108
endif()
106109

107-
target_link_libraries(solvers java_bytecode util)
110+
target_link_libraries(solvers util)
111+
112+
# Executable
113+
add_executable(smt2_solver smt2/smt2_solver.cpp)
114+
target_link_libraries(smt2_solver solvers)
108115

109116
generic_includes(solvers)

‎src/solvers/Makefile

+11-5
Original file line numberDiff line numberDiff line change
@@ -216,9 +216,9 @@ INCLUDES += -I .. \
216216
$(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
217217
$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
218218

219-
CLEANFILES = solvers$(LIBEXT)
219+
CLEANFILES = solvers$(LIBEXT) smt2_solver$(EXEEXT)
220220

221-
all: solvers$(LIBEXT)
221+
all: solvers$(LIBEXT) smt2_solver$(EXEEXT)
222222

223223
ifneq ($(SQUOLEM2),)
224224
CP_CXXFLAGS += -DHAVE_QBF_CORE
@@ -232,9 +232,15 @@ endif
232232

233233
-include $(SRC:.cpp=.d)
234234

235-
###############################################################################
236-
237-
solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
235+
SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
238236
$(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
239237
$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
238+
239+
###############################################################################
240+
241+
solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
240242
$(LINKLIB) $(LIBSOLVER)
243+
244+
smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
245+
../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
246+
$(LINKBIN) $(LIBSOLVER)

‎src/solvers/smt2/smt2_solver.cpp

+266
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,266 @@
1+
/*******************************************************************\
2+
3+
Module: SMT2 Solver that uses boolbv and the default SAT solver
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <fstream>
10+
#include <iostream>
11+
12+
#include "smt2_parser.h"
13+
14+
#include <util/namespace.h>
15+
#include <util/symbol_table.h>
16+
#include <util/cout_message.h>
17+
#include <util/simplify_expr.h>
18+
#include <util/replace_symbol.h>
19+
20+
#include <solvers/sat/satcheck.h>
21+
#include <solvers/flattening/boolbv.h>
22+
23+
class smt2_solvert:public smt2_parsert
24+
{
25+
public:
26+
smt2_solvert(
27+
std::istream &_in,
28+
decision_proceduret &_solver):
29+
smt2_parsert(_in),
30+
solver(_solver)
31+
{
32+
}
33+
34+
protected:
35+
decision_proceduret &solver;
36+
37+
void command(const std::string &) override;
38+
void define_constants(const exprt &);
39+
void expand_function_applications(exprt &);
40+
41+
std::set<irep_idt> constants_done;
42+
};
43+
44+
void smt2_solvert::define_constants(const exprt &expr)
45+
{
46+
for(const auto &op : expr.operands())
47+
define_constants(op);
48+
49+
if(expr.id()==ID_symbol)
50+
{
51+
irep_idt identifier=to_symbol_expr(expr).get_identifier();
52+
53+
// already done?
54+
if(constants_done.find(identifier)!=constants_done.end())
55+
return;
56+
57+
constants_done.insert(identifier);
58+
59+
auto f_it=id_map.find(identifier);
60+
61+
if(f_it!=id_map.end())
62+
{
63+
const auto &f=f_it->second;
64+
65+
if(f.type.id()!=ID_mathematical_function &&
66+
f.definition.is_not_nil())
67+
{
68+
exprt def=f.definition;
69+
expand_function_applications(def);
70+
define_constants(def); // recursive!
71+
solver.set_to_true(equal_exprt(expr, def));
72+
}
73+
}
74+
}
75+
}
76+
77+
void smt2_solvert::expand_function_applications(exprt &expr)
78+
{
79+
for(exprt &op : expr.operands())
80+
expand_function_applications(op);
81+
82+
if(expr.id()==ID_function_application)
83+
{
84+
auto &app=to_function_application_expr(expr);
85+
86+
// look it up
87+
irep_idt identifier=app.function().get_identifier();
88+
auto f_it=id_map.find(identifier);
89+
90+
if(f_it!=id_map.end())
91+
{
92+
const auto &f=f_it->second;
93+
94+
DATA_INVARIANT(f.type.id()==ID_mathematical_function,
95+
"type of function symbol must be mathematical_function_type");
96+
97+
const auto f_type=
98+
to_mathematical_function_type(f.type);
99+
100+
DATA_INVARIANT(f_type.domain().size()==
101+
app.arguments().size(),
102+
"number of function parameters");
103+
104+
replace_symbolt replace_symbol;
105+
106+
std::map<irep_idt, exprt> parameter_map;
107+
for(std::size_t i=0; i<f_type.domain().size(); i++)
108+
{
109+
const irep_idt p_identifier=
110+
f_type.domain()[i].get_identifier();
111+
112+
replace_symbol.insert(p_identifier, app.arguments()[i]);
113+
}
114+
115+
exprt body=f.definition;
116+
replace_symbol(body);
117+
expand_function_applications(body);
118+
expr=body;
119+
}
120+
}
121+
}
122+
123+
void smt2_solvert::command(const std::string &c)
124+
{
125+
try
126+
{
127+
if(c=="assert")
128+
{
129+
exprt e=expression();
130+
if(e.is_not_nil())
131+
{
132+
expand_function_applications(e);
133+
define_constants(e);
134+
solver.set_to_true(e);
135+
}
136+
}
137+
else if(c=="check-sat")
138+
{
139+
switch(solver())
140+
{
141+
case decision_proceduret::resultt::D_SATISFIABLE:
142+
std::cout << "sat\n";
143+
break;
144+
145+
case decision_proceduret::resultt::D_UNSATISFIABLE:
146+
std::cout << "unsat\n";
147+
break;
148+
149+
case decision_proceduret::resultt::D_ERROR:
150+
std::cout << "error\n";
151+
}
152+
}
153+
else if(c=="check-sat-assuming")
154+
{
155+
std::cout << "not yet implemented\n";
156+
}
157+
else if(c=="display")
158+
{
159+
// this is a command that Z3 appears to implement
160+
exprt e=expression();
161+
if(e.is_not_nil())
162+
{
163+
std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
164+
}
165+
}
166+
else if(c=="simplify")
167+
{
168+
// this is a command that Z3 appears to implement
169+
exprt e=expression();
170+
if(e.is_not_nil())
171+
{
172+
const symbol_tablet symbol_table;
173+
const namespacet ns(symbol_table);
174+
exprt e_simplified=simplify_expr(e, ns);
175+
std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
176+
}
177+
}
178+
#if 0
179+
// TODO:
180+
| ( declare-const hsymboli hsorti )
181+
| ( declare-datatype hsymboli hdatatype_deci)
182+
| ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
183+
| ( declare-fun hsymboli ( hsorti ??? ) hsorti )
184+
| ( declare-sort hsymboli hnumerali )
185+
| ( define-fun hfunction_def i )
186+
| ( define-fun-rec hfunction_def i )
187+
| ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
188+
| ( define-sort hsymboli ( hsymboli ??? ) hsorti )
189+
| ( echo hstringi )
190+
| ( exit )
191+
| ( get-assertions )
192+
| ( get-assignment )
193+
| ( get-info hinfo_flag i )
194+
| ( get-model )
195+
| ( get-option hkeywordi )
196+
| ( get-proof )
197+
| ( get-unsat-assumptions )
198+
| ( get-unsat-core )
199+
| ( get-value ( htermi + ) )
200+
| ( pop hnumerali )
201+
| ( push hnumerali )
202+
| ( reset )
203+
| ( reset-assertions )
204+
| ( set-info hattributei )
205+
| ( set-option hoptioni )
206+
#endif
207+
else
208+
smt2_parsert::command(c);
209+
}
210+
catch(const char *error)
211+
{
212+
std::cout << "error: " << error << '\n';
213+
}
214+
catch(const std::string &error)
215+
{
216+
std::cout << "error: " << error << '\n';
217+
}
218+
}
219+
220+
int solver(std::istream &in)
221+
{
222+
symbol_tablet symbol_table;
223+
namespacet ns(symbol_table);
224+
225+
console_message_handlert message_handler;
226+
messaget message(message_handler);
227+
228+
// this is our default verbosity
229+
message_handler.set_verbosity(messaget::M_STATISTICS);
230+
231+
satcheckt satcheck;
232+
boolbvt boolbv(ns, satcheck);
233+
satcheck.set_message_handler(message_handler);
234+
boolbv.set_message_handler(message_handler);
235+
236+
smt2_solvert smt2_solver(in, boolbv);
237+
smt2_solver.set_message_handler(message_handler);
238+
239+
smt2_solver.parse();
240+
241+
if(!smt2_solver)
242+
return 20;
243+
else
244+
return 0;
245+
}
246+
247+
int main(int argc, const char *argv[])
248+
{
249+
if(argc==1)
250+
return solver(std::cin);
251+
252+
if(argc!=2)
253+
{
254+
std::cerr << "usage: smt2_solver file\n";
255+
return 1;
256+
}
257+
258+
std::ifstream in(argv[1]);
259+
if(!in)
260+
{
261+
std::cerr << "failed to open " << argv[1] << '\n';
262+
return 1;
263+
}
264+
265+
return solver(in);
266+
}

0 commit comments

Comments
 (0)