summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/lfsc_checker/check.cpp10
-rw-r--r--proofs/lfsc_checker/expr.cpp41
-rw-r--r--src/Makefile.theories2
-rw-r--r--src/expr/node_manager.cpp2
-rw-r--r--src/options/options.h2
-rw-r--r--src/options/options_public_functions.cpp2
-rw-r--r--src/smt/ite_removal.cpp4
-rw-r--r--src/theory/bv/bv_subtheory_inequality.h4
-rw-r--r--src/theory/quantifiers_engine.h1
-rw-r--r--src/theory/rep_set.h3
-rw-r--r--src/theory/theory_engine.cpp3
-rw-r--r--test/regress/regress0/bv/Makefile.am3
-rw-r--r--test/regress/regress0/bv/bench_38.delta.smt27
13 files changed, 47 insertions, 37 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 493b3ecc7..e100efa69 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -87,10 +87,10 @@ char our_getc_c = 0;
int IDBUF_LEN = 2048;
char idbuf[2048];
-Expr *statType = new CExpr(TYPE, 0);
-Expr *statKind = new CExpr(KIND, 0);
-Expr *statMpz = new CExpr(MPZ,0);
-Expr *statMpq = new CExpr(MPQ,0);
+Expr *statType = new CExpr(TYPE);
+Expr *statKind = new CExpr(KIND);
+Expr *statMpz = new CExpr(MPZ);
+Expr *statMpq = new CExpr(MPQ);
int open_parens = 0;
@@ -466,7 +466,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
SymExpr *sym = new SymExpr(id);
#endif
int prev_open = open_parens;
- Expr *tp_of_trm;
+ Expr *tp_of_trm = NULL;
Expr *trm = check(true, NULL, &tp_of_trm);
eat_excess(prev_open);
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 784a0ad2f..7bd26db2c 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -205,13 +205,12 @@ Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) {
return hd;
else
{
- CExpr *ret = new CExpr( APP );
- ret->kids = new Expr* [args.size()-start+2];
- ret->kids[0] = hd;
+ Expr **kids = new Expr *[args.size() - start + 2];
+ kids[0] = hd;
for (int i = start, iend = args.size(); i < iend; i++)
- ret->kids[i-start+1] = args[i];
- ret->kids[args.size()-start+1] = NULL;
- return ret;
+ kids[i - start + 1] = args[i];
+ kids[args.size() - start + 1] = NULL;
+ return new CExpr(APP, true /* dummy */, kids);
}
#endif
}
@@ -229,16 +228,16 @@ Expr* Expr::make_app(Expr* e1, Expr* e2 )
while( ((CExpr*)e1)->kids[counter] ){
counter++;
}
- ret = new CExpr( APP );
- ret->kids = new Expr* [counter+2];
+ Expr **kids = new Expr *[counter + 2];
counter = 0;
while( ((CExpr*)e1)->kids[counter] ){
- ret->kids[counter] = ((CExpr*)e1)->kids[counter];
- ret->kids[counter]->inc();
- counter++;
+ kids[counter] = ((CExpr *)e1)->kids[counter];
+ kids[counter]->inc();
+ counter++;
}
- ret->kids[counter] = e2;
- ret->kids[counter+1] = NULL;
+ kids[counter] = e2;
+ kids[counter + 1] = NULL;
+ ret = new CExpr(APP, true /* dummy */, kids);
}else{
ret = new CExpr( APP, e1, e2 );
}
@@ -369,14 +368,13 @@ Expr* CExpr::convert_to_flat_app( Expr* e )
{
std::vector< Expr* > args;
Expr* hd = ((CExpr*)e)->collect_args( args );
- CExpr* nce = new CExpr( APP );
- nce->kids = new Expr *[(int)args.size()+2];
- nce->kids[0] = hd;
- for( int a=0; a<(int)args.size(); a++ )
- {
- nce->kids[a+1] = convert_to_flat_app( args[a] );
+ Expr **kids = new Expr *[args.size() + 2];
+ kids[0] = hd;
+ for (size_t a = 0; a < args.size(); a++) {
+ kids[a + 1] = convert_to_flat_app(args[a]);
}
- nce->kids[(int)args.size()+1] = 0;
+ kids[args.size() + 1] = 0;
+ CExpr *nce = new CExpr(APP, true /* dummy */, kids);
nce->inc();
return nce;
}
@@ -647,8 +645,7 @@ bool Expr::free_in(Expr *x) {
Expr *tmp;
Expr **cur = e->kids;
while ((tmp = *cur++))
- if (tmp->free_in(x))
- return true;
+ if (tmp->free_in(x)) return true;
return false;
}
}
diff --git a/src/Makefile.theories b/src/Makefile.theories
index 003128a3c..276663cc5 100644
--- a/src/Makefile.theories
+++ b/src/Makefile.theories
@@ -1,3 +1,3 @@
-THEORIES = builtin booleans uf arith bv fp arrays datatypes sets sep strings quantifiers idl
+THEORIES = builtin booleans uf arith bv fp arrays datatypes sep sets strings quantifiers idl
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1d54d0f9d..a9be51418 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -383,7 +383,7 @@ std::vector<NodeValue*> NodeManager::TopologicalSort(
stack.back().first = true;
Assert(visited.count(current) == 0);
visited.insert(current);
- for (int i = 0; i < current->getNumChildren(); ++i) {
+ for (unsigned i = 0; i < current->getNumChildren(); ++i) {
expr::NodeValue* child = current->getChild(i);
if (visited.find(child) == visited.end()) {
stack.push_back(std::make_pair(false, child));
diff --git a/src/options/options.h b/src/options/options.h
index 33bd94e46..3551d82ae 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -222,7 +222,7 @@ public:
bool getStatsEveryQuery() const;
bool getStatsHideZeros() const;
bool getStrictParsing() const;
- bool getTearDownIncremental() const;
+ int getTearDownIncremental() const;
bool getVersion() const;
bool getWaitToJoin() const;
const std::string& getForceLogicString() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 8f3a63175..111b5482a 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -159,7 +159,7 @@ bool Options::getStrictParsing() const{
return (*this)[options::strictParsing];
}
-bool Options::getTearDownIncremental() const{
+int Options::getTearDownIncremental() const{
return (*this)[options::tearDownIncremental];
}
diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp
index fcd0c3254..d31d54121 100644
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/ite_removal.cpp
@@ -17,6 +17,7 @@
#include <vector>
+#include "options/proof_options.h"
#include "proof/proof_manager.h"
#include "theory/ite_utilities.h"
@@ -55,7 +56,8 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool
// fixes the bug on clang on Mac OS
Node itesRemoved = run(output[i], output, iteSkolemMap, false);
// In some calling contexts, not necessary to report dependence information.
- if(reportDeps && options::unsatCores()) {
+ if (reportDeps &&
+ (options::unsatCores() || options::fewerPreprocessingHoles())) {
// new assertions have a dependence on the node
PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
while(n < output.size()) {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 5fbdf74ab..617e3b761 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -47,8 +47,8 @@ class InequalitySolver: public SubtheorySolver {
InequalityGraph d_inequalityGraph;
context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
context::CDO<bool> d_isComplete;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
- TNodeSet d_ineqTerms;
+ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+ NodeSet d_ineqTerms;
bool isInequalityOnly(TNode node);
bool addInequality(TNode a, TNode b, bool strict, TNode fact);
Statistics d_statistics;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 83076c51a..150b3945b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -47,6 +47,7 @@ namespace quantifiers {
class InstantiationNotify {
public:
InstantiationNotify(){}
+ virtual ~InstantiationNotify() {}
virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
virtual void filterInstantiations() = 0;
};
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 2a2110cfa..9368d3681 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -58,7 +58,8 @@ typedef std::vector< int > RepDomain;
class RepBoundExt {
-public:
+ public:
+ virtual ~RepBoundExt() {}
virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
};
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5ef768fd3..8da1dfc1b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -25,6 +25,7 @@
#include "expr/node_builder.h"
#include "options/bv_options.h"
#include "options/options.h"
+#include "options/proof_options.h"
#include "options/quantifiers_options.h"
#include "proof/cnf_proof.h"
#include "proof/lemma_proof.h"
@@ -1945,7 +1946,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
// This pass does not support dependency tracking yet
// (learns substitutions from all assertions so just
// adding addDependence is not enough)
- if (options::unsatCores()) {
+ if (options::unsatCores() || options::fewerPreprocessingHoles()) {
return true;
}
bool result = true;
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index bb5c1e587..0c49af306 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -100,7 +100,8 @@ SMT_TESTS = \
bv2nat-simp-range.smt2 \
bv-int-collapse1.smt2 \
bv-int-collapse2.smt2 \
- bv-int-collapse2-sat.smt2
+ bv-int-collapse2-sat.smt2 \
+ bench_38.delta.smt2
# Regression tests for SMT2 inputs
SMT2_TESTS = divtest.smt2
diff --git a/test/regress/regress0/bv/bench_38.delta.smt2 b/test/regress/regress0/bv/bench_38.delta.smt2
new file mode 100644
index 000000000..760614348
--- /dev/null
+++ b/test/regress/regress0/bv/bench_38.delta.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 4))
+(assert (and (= (bvudiv (_ bv2 4) x) (_ bv2 4)) (= (_ bv0 4) x) (= (_ bv1 4) x)))
+(check-sat)
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback