From 2633dc56abc23dc078b58694eb725fbe38954450 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Mar 2013 08:59:43 -0700 Subject: [PATCH 1/3] Fix non ASCII character Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 1 + src/muz_qe/dl_mk_karr_invariants.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 06120e2c4..257b1b295 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -520,6 +520,7 @@ def parse_options(): # Return a list containing a file names included using '#include' in # the given C/C++ file named fname. def extract_c_includes(fname): + print(fname) result = [] # We look for well behaved #include directives std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 18b152589..d44b31979 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -11,7 +11,7 @@ Abstract: The linear invariants are extracted according to Karr's method. A short description is in - Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation + Nikolaj Bjorner, Anca Browne and Zohar Manna. Automatic Generation of Invariants and Intermediate Assertions, in CP 95. The algorithm is here adapted to Horn clauses. From 5aa84c28a6dc9778e12e7b9d05fc8d5b2e309ed9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Mar 2013 09:00:19 -0700 Subject: [PATCH 2/3] Remove trace msg Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 257b1b295..06120e2c4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -520,7 +520,6 @@ def parse_options(): # Return a list containing a file names included using '#include' in # the given C/C++ file named fname. def extract_c_includes(fname): - print(fname) result = [] # We look for well behaved #include directives std_inc_pat = re.compile("[ \t]*#include[ \t]*\"(.*)\"[ \t]*") From 9d0b0df9859918f96d0c413db68200538064f41f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Mar 2013 09:07:51 -0700 Subject: [PATCH 3/3] Fix gcc compilation errors Signed-off-by: Leonardo de Moura --- src/muz_qe/hnf.cpp | 6 ++++-- src/util/bit_vector.cpp | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp index 88e28699e..47370e0e6 100644 --- a/src/muz_qe/hnf.cpp +++ b/src/muz_qe/hnf.cpp @@ -353,7 +353,8 @@ private: void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) { for (unsigned i = 0; i < body.size(); ++i) { - eliminate_disjunctions(body[i], proofs); + expr_ref_vector::element_ref r = body[i]; + eliminate_disjunctions(r, proofs); } } @@ -378,7 +379,8 @@ private: void eliminate_quantifier_body(expr_ref_vector& body, proof_ref_vector& proofs) { for (unsigned i = 0; i < body.size(); ++i) { - eliminate_quantifier_body(body[i], proofs); + expr_ref_vector::element_ref r = body[i]; + eliminate_quantifier_body(r, proofs); } } diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 2328a5849..e3a2bc331 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -16,7 +16,7 @@ Author: Revision History: --*/ - +#include #include"bit_vector.h" #include"trace.h"