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

New upstream release. 

Also:
- Drop upstreamed patches: -signed, -boolean, -minisat.
- Add -constant patch to fix undefined symbols in the JNI shared object.
- Add cryptominisat4 support.
This commit is contained in:
Jerry James 2017-07-15 20:54:40 -06:00
parent 0451dab84d
commit 7e5614b256
9 changed files with 160 additions and 409 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1 +1,2 @@
/cvc4-1.4.tar.gz
/cvc4-1.5.tar.gz

22
cvc4-boolean.patch
View File

@ -1,22 +0,0 @@
--- ./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;

25
cvc4-constant.patch Normal file
View File

@ -0,0 +1,25 @@
--- src/theory/datatypes/kinds.orig 2017-06-23 15:54:52.988063375 -0600
+++ src/theory/datatypes/kinds 2017-07-15 20:30:31.268986539 -0600
@@ -108,4 +108,22 @@ typerule DT_SIZE ::CVC4::theory::datatyp
operator DT_HEIGHT_BOUND 2 "datatypes height bound"
typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
+constant TUPLE_SELECT_OP \
+ ::CVC4::TupleSelect \
+ ::CVC4::TupleSelectHashFunction \
+ "util/tuple.h" \
+ "operator for a tuple select"
+
+constant RECORD_OP \
+ ::CVC4::Record \
+ ::CVC4::RecordHashFunction \
+ "expr/record.h" \
+ "operator for a record"
+
+constant RECORD_SELECT_OP \
+ ::CVC4::RecordSelect \
+ ::CVC4::RecordSelectHashFunction \
+ "expr/record.h" \
+ "operator for a record select"
+
endtheory

356
cvc4-doxygen.patch
View File

@ -1,285 +1,81 @@
--- ./src/decision/options.h.orig 2014-07-13 11:48:44.263172259 -0600
+++ ./src/decision/options.h 2014-07-13 11:48:44.263172259 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file decision/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/expr/expr_manager_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/expr_manager_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.h
+/*! \file expr_manager.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/expr_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/expr_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_template.h
+/*! \file expr.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/kind_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/kind_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file kind_template.h
+/*! \file kind.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/options.h.orig 2014-07-13 11:48:13.930308852 -0600
+++ ./src/expr/options.h 2014-07-13 11:48:13.930308852 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file expr/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/main/options.h.orig 2014-07-13 11:48:47.275258010 -0600
+++ ./src/main/options.h 2014-07-13 11:48:47.275258010 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file main/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options.h.orig 2014-07-13 11:48:12.830277541 -0600
+++ ./src/options/base_options.h 2014-07-13 11:48:12.830277541 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file options/base_options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options_template.h.orig 2014-07-13 11:32:35.579588292 -0600
+++ ./src/options/base_options_template.h 2014-07-13 11:32:35.579588292 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file base_options_template.h
+/*! \file options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/options.h.orig 2014-07-01 12:37:15.061881767 -0600
+++ ./src/options/options.h 2014-07-01 12:37:15.061881767 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file options.h
+/*! \file options/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/parser/options.h.orig 2014-07-13 11:48:48.427290778 -0600
+++ ./src/parser/options.h 2014-07-13 11:48:48.427290778 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file parser/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/printer/options.h.orig 2014-07-13 11:48:37.070967532 -0600
+++ ./src/printer/options.h 2014-07-13 11:48:37.070967532 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file printer/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/proof/options.h.orig 2014-07-13 11:48:36.346946926 -0600
+++ ./src/proof/options.h 2014-07-13 11:48:36.346946926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file proof/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/prop/options.h.orig 2014-07-13 11:48:35.870933374 -0600
+++ ./src/prop/options.h 2014-07-13 11:48:35.870933374 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file prop/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/smt/options.h.orig 2014-07-13 11:48:42.683127279 -0600
+++ ./src/smt/options.h 2014-07-13 11:48:42.683127279 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file smt/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arith/options.h.orig 2014-07-13 11:48:23.866591680 -0600
+++ ./src/theory/arith/options.h 2014-07-13 11:48:23.866591680 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/arith/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arrays/options.h.orig 2014-07-13 11:48:26.966679925 -0600
+++ ./src/theory/arrays/options.h 2014-07-13 11:48:26.966679925 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/arrays/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/booleans/options.h.orig 2014-07-13 11:48:14.450323654 -0600
+++ ./src/theory/booleans/options.h 2014-07-13 11:48:14.450323654 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/booleans/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/builtin/options.h.orig 2014-07-13 11:48:18.334434213 -0600
+++ ./src/theory/builtin/options.h 2014-07-13 11:48:18.334434213 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/builtin/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/bv/options.h.orig 2014-07-13 11:48:17.270403926 -0600
+++ ./src/theory/bv/options.h 2014-07-13 11:48:17.270403926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/bv/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/datatypes/options.h.orig 2014-07-13 11:48:17.930422713 -0600
+++ ./src/theory/datatypes/options.h 2014-07-13 11:48:17.930422713 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/datatypes/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/idl/options.h.orig 2014-07-13 11:48:49.099309909 -0600
+++ ./src/theory/idl/options.h 2014-07-13 11:48:49.099309909 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/idl/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/options.h.orig 2014-07-13 11:48:15.082341645 -0600
+++ ./src/theory/options.h 2014-07-13 11:48:15.082341645 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/quantifiers/options.h.orig 2014-07-13 11:48:32.886848435 -0600
+++ ./src/theory/quantifiers/options.h 2014-07-13 11:48:32.886848435 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/quantifiers/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/sets/options.h.orig 2014-07-13 11:48:49.839330972 -0600
+++ ./src/theory/sets/options.h 2014-07-13 11:48:49.839330972 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/sets/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/strings/options.h.orig 2014-07-13 11:48:34.382891021 -0600
+++ ./src/theory/strings/options.h 2014-07-13 11:48:34.382891021 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/strings/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/uf/options.h.orig 2014-07-13 11:48:25.926650321 -0600
+++ ./src/theory/uf/options.h 2014-07-13 11:48:25.926650321 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/uf/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/util/tls.h.in.orig 2014-07-13 11:32:36.123603789 -0600
+++ ./src/util/tls.h.in 2014-07-13 11:32:36.123603789 -0600
--- src/base/tls.h.in.orig 2017-07-07 16:15:02.906706503 -0600
+++ src/base/tls.h.in 2017-07-12 19:10:48.346237676 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file tls.h.in
+/*! \file tls.h
** \verbatim
** Original author: ACSYS
** Major contributors: Morgan Deters
** Top contributors (to current version):
** Morgan Deters, ACSYS, Paul Meng
--- src/expr/expr_manager_template.cpp.orig 2017-07-07 16:15:02.958707425 -0600
+++ src/expr/expr_manager_template.cpp 2017-07-12 19:09:30.706471535 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.cpp
+/*! \file expr_manager.cpp
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Tim King, Christopher L. Conway
--- src/expr/expr_manager_template.h.orig 2017-07-07 16:15:02.959707443 -0600
+++ src/expr/expr_manager_template.h 2017-07-12 19:07:01.962904981 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.h
+/*! \file expr_manager.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
--- src/expr/expr_template.h.orig 2017-07-07 16:15:02.962707496 -0600
+++ src/expr/expr_template.h 2017-07-12 19:07:17.361860105 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_template.h
+/*! \file expr.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
--- src/expr/kind_template.h.orig 2017-07-07 16:15:02.964707531 -0600
+++ src/expr/kind_template.h 2017-07-12 19:07:36.314804876 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file kind_template.h
+/*! \file kind.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Paul Meng
--- src/expr/metakind_template.h.orig 2017-07-07 16:15:02.966707567 -0600
+++ src/expr/metakind_template.h 2017-07-12 19:08:17.474684935 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file metakind_template.h
+/*! \file metakind.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Paul Meng, Tim King
--- src/expr/type_checker_template.cpp.orig 2017-07-07 16:15:02.991708010 -0600
+++ src/expr/type_checker_template.cpp 2017-07-12 19:08:59.234563245 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file type_checker_template.cpp
+/*! \file type_checker.cpp
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Tim King, Paul Meng
--- src/expr/type_properties_template.h.orig 2017-07-07 16:15:02.995708080 -0600
+++ src/expr/type_properties_template.h 2017-07-12 19:08:31.650643627 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file type_properties_template.h
+/*! \file type_properties.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Paul Meng, Tim King
--- src/util/rational.h.in.orig 2017-07-07 16:15:03.587718569 -0600
+++ src/util/rational.h.in 2017-07-12 19:11:15.186152866 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file rational.h.in
+/*! \file rational.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Paul Meng, Tim King

25
cvc4-abc.patch → cvc4-libs.patch
View File

@ -1,6 +1,6 @@
--- ./configure.orig 2014-07-13 11:47:37.469270988 -0600
+++ ./configure 2015-01-01 21:00:00.000000000 -0700
@@ -19368,7 +19368,7 @@ See \`config.log' for more details" "$LI
--- configure.orig 2017-07-10 11:00:38.291785982 -0600
+++ configure 2017-07-15 12:34:56.893412904 -0600
@@ -20324,7 +20324,7 @@ See \`config.log' for more details" "$LI
fi
@ -9,7 +9,7 @@
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "either $ABC_HOME is not an abc source tree or it's not yet built
@@ -19377,15 +19377,15 @@ See \`config.log' for more details" "$LI
@@ -20333,15 +20333,15 @@ See \`config.log' for more details" "$LI
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for arch_flags to use with libabc" >&5
$as_echo_n "checking for arch_flags to use with libabc... " >&6; }
@ -28,3 +28,20 @@
LDFLAGS="$LDFLAGS $ABC_LDFLAGS"
ac_fn_c_check_header_mongrel "$LINENO" "base/abc/abc.h" "ac_cv_header_base_abc_abc_h" "$ac_includes_default"
if test "x$ac_cv_header_base_abc_abc_h" = xyes; then :
@@ -21274,14 +21274,14 @@ See \`config.log' for more details" "$LI
fi
- if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat" ; then
+ if ! test -d "$CRYPTOMINISAT_HOME" ; then
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built
See \`config.log' for more details" "$LINENO" 5; }
fi
- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
+ CPPFLAGS="$CPPFLAGS -I/usr/include/cryptominisat4"
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking how to link cryptominisat" >&5
$as_echo_n "checking how to link cryptominisat... " >&6; }

30
cvc4-minisat.patch
View File

@ -1,30 +0,0 @@
--- ./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
View File

@ -1,50 +0,0 @@
--- ./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 ){

58
cvc4.spec
View File

@ -2,8 +2,8 @@
# we currently build without glpk support.
Name: cvc4
Version: 1.4
Release: 15%{?dist}
Version: 1.5
Release: 1%{?dist}
Summary: Automatic theorem prover for SMT problems
# License breakdown:
@ -18,23 +18,20 @@ Summary: Automatic theorem prover for SMT problems
# But we link with readline, so it all gets subsumed by GPLv3+ anyway.
License: GPLv3+
URL: http://cvc4.cs.stanford.edu/
Source0: http://cvc4.cs.nyu.edu/builds/src/%{name}-%{version}.tar.gz
Source0: http://cvc4.cs.stanford.edu/downloads/builds/src/%{name}-%{version}.tar.gz
# Fix some doxygen problems. Upstream plans to fix this differently.
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
# Adapt to the way the Fedora libraries are constructed.
Patch1: %{name}-libs.patch
# Fix undefined symbols in the JNI interface
Patch2: %{name}-constant.patch
BuildRequires: abc-devel
BuildRequires: antlr3-C-devel
BuildRequires: antlr3-tool
BuildRequires: boost-devel
BuildRequires: chrpath
BuildRequires: cryptominisat4-devel
BuildRequires: cxxtest
BuildRequires: doxygen-latex
BuildRequires: gcc-c++
@ -42,6 +39,7 @@ BuildRequires: ghostscript-core
BuildRequires: gmp-devel
BuildRequires: java-devel
BuildRequires: jpackage-utils
BuildRequires: libtool
BuildRequires: perl-interpreter
BuildRequires: python2
BuildRequires: readline-devel
@ -98,13 +96,9 @@ Java interface to %{name}.
%prep
%setup -q
# The rpm patch macro doesn't understand -T, and we need it to to avoid
# regenerating the very files we're trying to patch.
patch -p0 -T < %{PATCH0}
%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++ 5.0 and higher.
@ -113,17 +107,17 @@ sed -e '/^if test "$enable_debug_symbols"/,/fi/d' \
-e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \
-e 's,\([^.]\)3\.4,\13.5,g' \
-e 's,\$ac_cpp conftest,$ac_cpp -P conftest,' \
-e '/gcc48/i\ "defined __GNUC__ && __GNUC__ == 7 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc70" \\\n "defined __GNUC__ && __GNUC__ == 6 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc60" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 3 && !defined __ICC @ gcc53" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 2 && !defined __ICC @ gcc52" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 1 && !defined __ICC @ gcc51" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc50" \\' \
-e '/gcc48/i\ "defined __GNUC__ && __GNUC__ == 7 && !defined __ICC @ gcc70" \\\n "defined __GNUC__ && __GNUC__ == 6 && !defined __ICC @ gcc60" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 3 && !defined __ICC @ gcc53" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 2 && !defined __ICC @ gcc52" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 1 && !defined __ICC @ gcc51" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc50" \\' \
-i configure
# Change the Java installation paths for Fedora and fix FTBFS
sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \
-e 's/ -Wno-all//' \
-i src/bindings/Makefile.in
-i src/bindings/Makefile.am
# Fix access to an uninitialized variable
sed -e 's/Kind k;/Kind k = kind::UNDEFINED_KIND;/' \
-i src/parser/cvc/generated/CvcParser.c
-i src/parser/cvc/CvcParser.c
# Make lfsc documentation available
cp -p proofs/lfsc_checker/AUTHORS AUTHORS.lfsc
@ -139,6 +133,9 @@ for fil in $(find . -name Makefile\*); do
sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil
done
# Fix an include path in the tests
sed -i 's,@CXXTEST@,%{_includedir}/cxxtest,' test/unit/Makefile.am
%build
export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
if [ "%{__isa_bits}" == "64" ]; then
@ -147,10 +144,11 @@ else
CPPFLAGS+=" -DLIN"
fi
export CFLAGS="%{optflags} -fsigned-char"
export CXXFLAGS="%{optflags} -fsigned-char -std=gnu++98"
export CXXFLAGS="%{optflags} -fsigned-char"
%configure --enable-gpl --enable-proof --enable-language-bindings=all \
--disable-silent-rules --with-portfolio --with-abc --with-abc-dir=%{_prefix} \
--with-readline --without-compat
--with-cryptominisat --with-cryptominisat-dir=%{_prefix} --with-readline \
--without-compat
# Workaround libtool reordering -Wl,--as-needed after all the libraries
BUILDS=$(echo $PWD/builds/*linux*/*abc*)
@ -209,7 +207,17 @@ sed -e 's/\(units.*:\) all/\1/' \
-e 's/\(regress.*:\) all/\1/' \
-i $BUILDS/Makefile $BUILDS/Makefile.builds
export LD_LIBRARY_PATH=$PWD/builds%{_libdir}
# Fix bad include paths in the test code
sed 's,/barrett/scratch.*/expr/,./,' \
test/unit/expr/expr_manager_public.cpp \
test/unit/expr/expr_public.cpp \
test/unit/expr/type_cardinality_public.cpp
# Fix the Java test's access to the JNI object it needs
sed 's,loadLibrary("cvc4jni"),load("%{buildroot}%{_jnidir}/%{name}/libcvc4jni.so"),' \
-i test/system/CVC4JavaTest.java
export LD_LIBRARY_PATH=%{buildroot}%{_libdir}
make check
%files
@ -237,6 +245,12 @@ make check
%{_jnidir}/%{name}/
%changelog
* Sat Jul 15 2017 Jerry James <loganjerry@gmail.com> - 1.5-1
- New upstream release
- Drop upstreamed patches: -signed, -boolean, -minisat
- Add -constant patch to fix undefined symbols in the JNI shared object
- Add cryptominisat4 support
* Mon May 15 2017 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.4-15
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_27_Mass_Rebuild

2
sources
View File

@ -1 +1 @@
581c559c02b94fcb18b2e5b11432e009 cvc4-1.4.tar.gz
SHA512 (cvc4-1.5.tar.gz) = 654a8e4eee499bce34cc82e002bbcc1ed8e124425a341435750d2dc65097e5e4f6bcf3376663800d644bef0bcdf94b98b862eb5e9f8d63823f416c7775ba17dc