rpms
/
cvc4
2
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add -boolean, -minisat, and -signed patches to fix test failures. 

Also:
- Fix boost detection with g++ 5.0.
- Fix access to an uninitialized variable.
- Help the documentation generator find COPYING.
- Build with -fsigned-char to fix the arm build.
- Prevent rebuilds while running %check.
This commit is contained in:
Jerry James 2015-03-11 22:26:03 -06:00
parent 6e15f19fbe
commit ebc8ce8c1a
4 changed files with 145 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
cvc4-boolean.patch Normal file
View File

@ -0,0 +1,22 @@
--- ./src/theory/bv/bv_subtheory_algebraic.cpp.orig 2014-07-13 11:32:35.951598886 -0600
+++ ./src/theory/bv/bv_subtheory_algebraic.cpp 2015-03-08 20:00:000000000000 -0600
@@ -465,7 +465,7 @@ bool AlgebraicSolver::solve(TNode fact,
if (right.getKind() == kind::BITVECTOR_XOR &&
left.getKind() == kind::BITVECTOR_XOR) {
TNode var = left[0];
- if (!var.getMetaKind() == kind::metakind::VARIABLE)
+ if (var.getMetaKind() != kind::metakind::VARIABLE)
return false;
// simplify xor with same variable on both sides
--- ./src/theory/bv/bv_subtheory_core.cpp.orig 2014-07-13 11:32:35.959599119 -0600
+++ ./src/theory/bv/bv_subtheory_core.cpp 2015-03-08 20:00:00.000000000 -0600
@@ -291,7 +291,7 @@ void CoreSolver::buildModel() {
bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
// Notify the equality engine
- if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+ if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_CORE)) {
Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
// Debug("bv-slicer-eq") << " reason=" << reason << endl;
bool negated = fact.getKind() == kind::NOT;

30
cvc4-minisat.patch Normal file
View File

@ -0,0 +1,30 @@
--- ./src/prop/minisat/core/SolverTypes.h.orig 2014-06-22 01:17:45.510946923 -0600
+++ ./src/prop/minisat/core/SolverTypes.h 2015-03-11 21:00:00.000000000 -0600
@@ -340,7 +340,7 @@ class OccLists
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
- void resizeTo (const Idx& idx){ int shrinkSize = occs.size() - (toInt(idx) + 1); occs.shrink(shrinkSize); }
+ void resizeTo (const Idx& idx);
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
@@ -386,6 +386,18 @@ void OccLists<Idx,Vec,Deleted>::clean(co
}
+template<class Idx, class Vec, class Deleted>
+void OccLists<Idx,Vec,Deleted>::resizeTo(const Idx& idx)
+{
+ for (int i = 0; i < dirties.size(); i++)
+ if (toInt(dirties[i]) > toInt(idx))
+ clean(dirties[i]);
+
+ int shrinkSize = occs.size() - (toInt(idx) + 1);
+ occs.shrink(shrinkSize);
+}
+
+
//=================================================================================================
// CMap -- a class for mapping clauses to values:

50
cvc4-signed.patch Normal file
View File

@ -0,0 +1,50 @@
--- ./src/theory/uf/theory_uf_strong_solver.cpp.orig 2014-07-13 11:32:36.091602875 -0600
+++ ./src/theory/uf/theory_uf_strong_solver.cpp 2015-01-02 20:00:00.000000000 -0700
@@ -199,7 +199,7 @@ struct sortExternalDegree {
int gmcCount = 0;
bool StrongSolverTheoryUF::SortModel::Region::getMustCombine( int cardinality ){
- if( options::ufssRegions() && d_total_diseq_external>=long(cardinality) ){
+ if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){
//The number of external disequalities is greater than or equal to cardinality.
//Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions
//Check if this is actually the case: must have n nodes with outgoing degree (cardinality+1-n) for some n>0
@@ -238,7 +238,7 @@ bool StrongSolverTheoryUF::SortModel::Re
}
bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
- if( d_reps_size>long(cardinality) ){
+ if( d_reps_size>unsigned(cardinality) ){
if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
if( d_reps_size>1 ){
//quick clique check, all reps form a clique
@@ -254,9 +254,9 @@ bool StrongSolverTheoryUF::SortModel::Re
}
}else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){
//build test clique, up to size cardinality+1
- if( d_testCliqueSize<=long(cardinality) ){
+ if( d_testCliqueSize<=unsigned(cardinality) ){
std::vector< Node > newClique;
- if( d_testCliqueSize<long(cardinality) ){
+ if( d_testCliqueSize<unsigned(cardinality) ){
for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
//if not in the test clique, add it to the set of new members
if( it->second->d_valid && ( d_testClique.find( it->first )==d_testClique.end() || !d_testClique[ it->first ] ) ){
@@ -312,7 +312,7 @@ bool StrongSolverTheoryUF::SortModel::Re
}
}
//check if test clique has larger size than cardinality, and forms a clique
- if( d_testCliqueSize>=long(cardinality+1) && d_splitsSize==0 ){
+ if( d_testCliqueSize>=unsigned(cardinality+1) && d_splitsSize==0 ){
//test clique is a clique
for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
if( (*it).second ){
@@ -327,7 +327,7 @@ bool StrongSolverTheoryUF::SortModel::Re
}
bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) {
- if( d_testCliqueSize>=long(cardinality+1) ){
+ if( d_testCliqueSize>=unsigned(cardinality+1) ){
//test clique is a clique
for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){
if( (*it).second ){

53
cvc4.spec
View File

@ -27,6 +27,12 @@ Source0: http://cvc4.cs.nyu.edu/builds/src/%{name}-%{version}.tar.gz
Patch0: %{name}-doxygen.patch
# Adapt to the way the Fedora ABC package is constructed.
Patch1: %{name}-abc.patch
# Fix some mixed signed/unsigned comparisons
Patch2: %{name}-signed.patch
# Fix some broken boolean expressions
Patch3: %{name}-boolean.patch
# Fix out-of-bounds array accesses in the minisat code
Patch4: %%{name}-minisat.patch
BuildRequires: abc-devel
BuildRequires: antlr3-C-devel
@ -105,25 +111,36 @@ Java interface to %{name}.
# regenerating the very files we're trying to patch.
patch -p0 -T < %{PATCH0}
%patch1
%patch2
%patch3
%patch4
# Don't change the build flags we want to use, avoid hardcoded rpaths, adapt to
# antlr 3.5, and allow boost to use g++ 4.9.
# antlr 3.5, and allow boost to use g++ 5.0.
sed -e '/^if test "$enable_debug_symbols"/,/fi/d' \
-e 's,^hardcode_libdir_flag_spec=.*,hardcode_libdir_flag_spec="",g' \
-e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \
-e 's,\([^.]\)3\.4,\13.5,g' \
-e 's,\(__GNUC_MINOR__ == \)8\(.*\)gcc48,\19\2gcc49,' \
-e 's,\$ac_cpp conftest,$ac_cpp -P conftest,' \
-e 's,\(__GNUC__ == \)4\(.*_MINOR__ == \)8\(.*\)gcc48,\15\20\3gcc50,' \
-i configure
# Change the Java installation paths for Fedora
sed -i "s|^\(javalibdir =.*\)jni|\1java/%{name}|" src/bindings/Makefile.in
# Fix access to an uninitialized variable
sed -e 's/Kind k;/Kind k = kind::UNDEFINED_KIND;/' \
-i src/parser/cvc/generated/CvcParser.c
# Make lfsc documentation available
cp -p proofs/lfsc_checker/AUTHORS AUTHORS.lfsc
cp -p proofs/lfsc_checker/COPYING COPYING.lfsc
cp -p proofs/lfsc_checker/NEWS NEWS.lfsc
cp -p proofs/lfsc_checker/README README.lfsc
# Help the documentation generator
cp -p COPYING src/bindings/compat/c
# Preserve timestamps when installing
for fil in $(find . -name Makefile\*); do
sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil
@ -136,16 +153,18 @@ CPPFLAGS+=" -DLIN64"
%else
CPPFLAGS+=" -DLIN"
%endif
export CFLAGS="%{optflags} -fsigned-char"
export CXXFLAGS="%{optflags} -fsigned-char"
%configure --enable-gpl --enable-proof --enable-language-bindings=all \
%if 0%{?have_perftools}
--with-google-perftools \
%endif
--with-portfolio --with-abc --with-abc-dir=%{_prefix} --with-readline \
--without-compat
--disable-silent-rules --with-portfolio --with-abc --with-abc-dir=%{_prefix} \
--with-readline --without-compat
# Workaround libtool reordering -Wl,--as-needed after all the libraries
sed -i 's/CC=.g../& -Wl,--as-needed/' \
builds/*-linux-gnu*/production-abc-proof/libtool
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
sed -i 's/CC=.g../& -Wl,--as-needed/' $BUILDS/libtool
make %{?_smp_mflags}
make doc
@ -173,14 +192,14 @@ chrpath -d %{buildroot}%{_bindir}/* \
%{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.*
# Help the debuginfo generator
BUILDS=$(echo builds/*-*-linux-gnu*)
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
for dir in decision expr main parser printer prop smt theory theory/arith \
theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \
theory/quantifiers theory/rewriterules theory/strings theory/uf; do
ln -s $PWD/src/$dir/options $BUILDS/production-abc-proof/src/$dir
ln -s $PWD/src/$dir/options $BUILDS/src/$dir
done
ln -s production-abc-proof/src $BUILDS
ln -s $PWD/src/options/base_options $BUILDS/production-abc-proof/src/options
ln -s production-abc-proof/src $BUILDS/../src
ln -s $PWD/src/options/base_options $BUILDS/src/options
ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options
ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options
ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options
@ -194,6 +213,12 @@ ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt
# The tests use a large amount of stack space
ulimit -s unlimited
# Do not rebuild when checking
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
sed -e 's/\(units.*:\) all/\1/' \
-e 's/\(regress.*:\) all/\1/' \
-i $BUILDS/Makefile $BUILDS/Makefile.builds
export LD_LIBRARY_PATH=$PWD/builds%{_libdir}
make check
@ -222,6 +247,14 @@ make check
%{_jnidir}/%{name}/
%changelog
* Wed Mar 11 2015 Jerry James <loganjerry@gmail.com> - 1.4-2
- Add -boolean, -minisat, and -signed patches to fix test failures
- Fix boost detection with g++ 5.0
- Fix access to an uninitialized variable
- Help the documentation generator find COPYING
- Build with -fsigned-char to fix the arm build
- Prevent rebuilds while running checks
* Tue Jan 27 2015 Petr Machata <pmachata@redhat.com> - 1.4-2
- Rebuild for boost 1.57.0