Skip to content

Commit 2a544f7

Browse files
tautschnigtautschnig
committed
Make IPASIR configuration build after solver hardness changes
In diffblue#5480 the solver hardness interface was updated, but changes were only implemented in the Minisat2 interface. Update the IPASIR interface to match these changes. Also fix the status tracking in do_prop_solve as the previous implementation would keep the solver in an UNSAT state, even when assumptions had been modified. This issue was surfaced by the cbmc-incr-oneloop suite of regression tests. To avoid future regressions, make the check-ubuntu-20_04-make-gcc GitHub action use IPASIR with Riss as the back-end solver.
1 parent ec21533 commit 2a544f7

File tree

3 files changed

+57
-47
lines changed

3 files changed

+57
-47
lines changed

‎.github/workflows/pull-request-checks.yaml

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,7 @@ jobs:
1616
# user input
1717
DEBIAN_FRONTEND: noninteractive
1818
run: |
19-
sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache
20-
make -C src minisat2-download
19+
sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake
2120
- name: Prepare ccache
2221
uses: actions/cache@v2
2322
with:
@@ -34,19 +33,24 @@ jobs:
3433
run: ccache -z --max-size=500M
3534
- name: Build with make
3635
run: |
37-
make -C src CXX='ccache /usr/bin/g++' -j2
38-
make -C unit CXX='ccache /usr/bin/g++' -j2
39-
make -C jbmc/src CXX='ccache /usr/bin/g++' -j2
40-
make -C jbmc/unit CXX='ccache /usr/bin/g++' -j2
36+
git clone https://github.com/conp-solutions/riss riss.git
37+
cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release
38+
make -C riss.git/release riss-coprocessor-lib-static -j2
39+
make -C src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
40+
make -C jbmc/src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
41+
42+
make -C unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
43+
44+
make -C jbmc/unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
4145
- name: Print ccache stats
4246
run: ccache -s
4347
- name: Run unit tests
4448
run: |
45-
make -C unit test
46-
make -C jbmc/unit test
49+
make -C unit test IPASIR=$PWD/riss.git/riss
50+
make -C jbmc/unit test IPASIR=$PWD/riss.git/riss
4751
echo "Running expected failure tests"
48-
make TAGS="[!shouldfail]" -C unit test
49-
make TAGS="[!shouldfail]" -C jbmc/unit test
52+
make TAGS="[!shouldfail]" -C unit test IPASIR=$PWD/riss.git/riss
53+
make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
5054
- name: Run regression tests
5155
run: |
5256
make -C regression test-parallel JOBS=2

‎src/solvers/sat/satcheck_ipasir.cpp

Lines changed: 40 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,22 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
9090
}
9191
ipasir_add(solver, 0); // terminate clause
9292

93-
with_solver_hardness(
94-
[&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
93+
with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
94+
// To map clauses to lines of program code, track clause indices in the
95+
// dimacs cnf output. Dimacs output is generated after processing
96+
// clauses to remove duplicates and clauses that are trivially true.
97+
// Here, a clause is checked to see if it can be thus eliminated. If
98+
// not, add the clause index to list of clauses in
99+
// solver_hardnesst::register_clause().
100+
static size_t cnf_clause_index = 0;
101+
bvt cnf;
102+
bool clause_removed = process_clause(bv, cnf);
103+
104+
if(!clause_removed)
105+
cnf_clause_index++;
106+
107+
hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
108+
});
95109

96110
clause_counter++;
97111
}
@@ -103,51 +117,40 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
103117
log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
104118
<< " clauses" << messaget::eom;
105119

106-
// use the internal representation, as ipasir does not support reporting the
107-
// status
108-
if(status==statust::UNSAT)
120+
// if assumptions contains false, we need this to be UNSAT
121+
bvt::const_iterator it =
122+
std::find_if(assumptions.begin(), assumptions.end(), is_false);
123+
const bool has_false = it != assumptions.end();
124+
125+
if(has_false)
109126
{
110-
log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
127+
log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
111128
<< messaget::eom;
112129
}
113130
else
114131
{
115-
// if assumptions contains false, we need this to be UNSAT
116-
bvt::const_iterator it = std::find_if(assumptions.begin(),
117-
assumptions.end(), is_false);
118-
const bool has_false = it != assumptions.end();
132+
forall_literals(it, assumptions)
133+
if(!it->is_false())
134+
ipasir_assume(solver, it->dimacs());
119135

120-
if(has_false)
136+
// solve the formula, and handle the return code (10=SAT, 20=UNSAT)
137+
int solver_state = ipasir_solve(solver);
138+
if(10 == solver_state)
121139
{
122-
log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
123-
<< messaget::eom;
140+
log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
141+
status = statust::SAT;
142+
return resultt::P_SATISFIABLE;
143+
}
144+
else if(20 == solver_state)
145+
{
146+
log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
124147
}
125148
else
126149
{
127-
forall_literals(it, assumptions)
128-
if(!it->is_false())
129-
ipasir_assume(solver, it->dimacs());
130-
131-
// solve the formula, and handle the return code (10=SAT, 20=UNSAT)
132-
int solver_state=ipasir_solve(solver);
133-
if(10==solver_state)
134-
{
135-
log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
136-
status=statust::SAT;
137-
return resultt::P_SATISFIABLE;
138-
}
139-
else if(20==solver_state)
140-
{
141-
log.status() << "SAT checker: instance is UNSATISFIABLE"
142-
<< messaget::eom;
143-
}
144-
else
145-
{
146-
log.status() << "SAT checker: solving returned without solution"
147-
<< messaget::eom;
148-
throw analysis_exceptiont(
149-
"solving inside IPASIR SAT solver has been interrupted");
150-
}
150+
log.status() << "SAT checker: solving returned without solution"
151+
<< messaget::eom;
152+
throw analysis_exceptiont(
153+
"solving inside IPASIR SAT solver has been interrupted");
151154
}
152155
}
153156

‎unit/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,9 @@ EXCLUDED_TESTS=expr_undefined_casts.cpp
225225
ifneq ($(WITH_MEMORY_ANALYZER),1)
226226
EXCLUDED_TESTS += gdb_api.cpp
227227
endif
228+
ifeq ($(MINISAT2),)
229+
EXCLUDED_TESTS += satcheck_minisat2.cpp
230+
endif
228231

229232
N_CATCH_TESTS = $(shell \
230233
cat $$(find . -name "*.cpp" \

0 commit comments

Comments
 (0)