summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt2/smt2.cpp1
-rw-r--r--src/proof/proof_manager.cpp7
-rw-r--r--src/proof/proof_manager.h1
-rw-r--r--src/smt/options4
-rw-r--r--src/smt/smt_engine.cpp126
-rw-r--r--src/smt/smt_engine.h12
-rw-r--r--src/smt/smt_engine_check_proof.cpp7
-rw-r--r--src/theory/logic_info.cpp6
-rw-r--r--src/util/unsat_core.h7
-rw-r--r--test/regress/regress0/arith/bug569.smt22
-rw-r--r--test/regress/regress0/datatypes/empty_tuprec.cvc2
-rw-r--r--test/regress/regress0/fmf/Makefile8
-rw-r--r--test/regress/regress0/fmf/PUZ001+1.smt22
-rwxr-xr-xtest/regress/run_regression21
14 files changed, 180 insertions, 26 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index def9308bb..bf0e57eca 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -228,6 +228,7 @@ void Smt2::addTheory(Theory theory) {
case THEORY_STRINGS:
defineType("String", getExprManager()->stringType());
+ defineType("Int", getExprManager()->integerType());
addStringOperators();
break;
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 0f9cfa710..2d8c4178a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -204,7 +204,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
Debug("cores") << "assert: " << formula << std::endl;
d_inputFormulas.insert(formula);
d_deps[Node::fromExpr(formula)]; // empty vector of deps
- if(inUnsatCore || options::dumpUnsatCores()) {
+ if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) {
Debug("cores") << "adding to input core forms: " << formula << std::endl;
d_inputCoreFormulas.insert(formula);
}
@@ -221,6 +221,11 @@ void ProofManager::addDependence(TNode n, TNode dep) {
}
}
+void ProofManager::addUnsatCore(Expr formula) {
+ Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
+ d_outputCoreFormulas.insert(formula);
+}
+
void ProofManager::setLogic(const LogicInfo& logic) {
d_logic = logic;
}
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 43d6723fa..ee99b0159 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -171,6 +171,7 @@ public:
void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
// note that n depends on dep (for cores)
void addDependence(TNode n, TNode dep);
+ void addUnsatCore(Expr formula);
assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
diff --git a/src/smt/options b/src/smt/options
index 593fc4887..b23d73943 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -31,7 +31,7 @@ option dumpModels --dump-models bool :default false :link --produce-models
output models after every SAT/INVALID/UNKNOWN response
option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
turn on proof generation
-option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
after UNSAT/VALID, machine-check the generated proof
option dumpProofs --dump-proofs bool :default false :link --proof
output proofs after every UNSAT/VALID response
@@ -41,6 +41,8 @@ option dumpSynth --dump-synth bool :default false
output solution for synthesis conjectures after every UNSAT/VALID response
option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
turn on unsat core generation
+option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
+ after UNSAT/VALID, produce and check an unsat core (expensive)
option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
output unsat cores after every UNSAT/VALID response
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 229cc7c7c..b2bdea13f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -199,6 +199,8 @@ struct SmtEngineStatistics {
TimerStat d_checkModelTime;
/** time spent in checkProof() */
TimerStat d_checkProofTime;
+ /** time spent in checkUnsatCore() */
+ TimerStat d_checkUnsatCoreTime;
/** time spent in PropEngine::checkSat() */
TimerStat d_solveTime;
/** time spent in pushing/popping */
@@ -229,6 +231,7 @@ struct SmtEngineStatistics {
d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
d_checkModelTime("smt::SmtEngine::checkModelTime"),
d_checkProofTime("smt::SmtEngine::checkProofTime"),
+ d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
d_solveTime("smt::SmtEngine::solveTime"),
d_pushPopTime("smt::SmtEngine::pushPopTime"),
d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
@@ -253,6 +256,7 @@ struct SmtEngineStatistics {
StatisticsRegistry::registerStat(&d_numAssertionsPost);
StatisticsRegistry::registerStat(&d_checkModelTime);
StatisticsRegistry::registerStat(&d_checkProofTime);
+ StatisticsRegistry::registerStat(&d_checkUnsatCoreTime);
StatisticsRegistry::registerStat(&d_solveTime);
StatisticsRegistry::registerStat(&d_pushPopTime);
StatisticsRegistry::registerStat(&d_processAssertionsTime);
@@ -278,6 +282,7 @@ struct SmtEngineStatistics {
StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
StatisticsRegistry::unregisterStat(&d_checkModelTime);
StatisticsRegistry::unregisterStat(&d_checkProofTime);
+ StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime);
StatisticsRegistry::unregisterStat(&d_solveTime);
StatisticsRegistry::unregisterStat(&d_pushPopTime);
StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
@@ -695,6 +700,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_modelGlobalCommands(),
d_modelCommands(NULL),
d_dumpCommands(),
+#ifdef CVC4_PROOF
+ d_defineCommands(),
+#endif
d_logic(),
d_originalOptions(em->getOptions()),
d_pendingPops(0),
@@ -1029,6 +1037,14 @@ void SmtEngine::setDefaults() {
Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl;
setOption("bv-intro-pow2", false);
}
+ if(options::repeatSimp()) {
+ if(options::repeatSimp.wasSetByUser()) {
+ throw OptionException("repeat-simp not supported with unsat cores");
+ }
+ Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
+ setOption("repeat-simp", false);
+ }
+
}
if(options::produceAssignments() && !options::produceModels()) {
@@ -1047,6 +1063,24 @@ void SmtEngine::setDefaults() {
}
}
+ // strings require LIA, UF; widen the logic
+ if(d_logic.isTheoryEnabled(THEORY_STRINGS)) {
+ LogicInfo log(d_logic.getUnlockedCopy());
+ // Strings requires arith for length constraints, and also UF
+ if(!d_logic.isTheoryEnabled(THEORY_UF)) {
+ Trace("smt") << "because strings are enabled, also enabling UF" << endl;
+ log.enableTheory(THEORY_UF);
+ }
+ if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) {
+ Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl;
+ log.enableTheory(THEORY_ARITH);
+ log.enableIntegers();
+ log.arithOnlyLinear();
+ }
+ d_logic = log;
+ d_logic.lock();
+ }
+
// by default, symmetry breaker is on only for QF_UF
if(! options::ufSymmetryBreaker.wasSetByUser()) {
bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
@@ -1133,16 +1167,25 @@ void SmtEngine::setDefaults() {
// Turn on multiple-pass non-clausal simplification for QF_AUFBV
if(! options::repeatSimp.wasSetByUser()) {
bool repeatSimp = !d_logic.isQuantified() &&
- (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
+ (d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV)) &&
+ !options::unsatCores();
Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
options::repeatSimp.set(repeatSimp);
}
// Turn on unconstrained simplification for QF_AUFBV
- if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
+ if(!options::unconstrainedSimp.wasSetByUser() ||
+ options::incrementalSolving()) {
// bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
// bool uncSimp = false && !qf_sat && !options::incrementalSolving();
- bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() &&
- (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
+ bool uncSimp = !options::incrementalSolving() &&
+ !d_logic.isQuantified() &&
+ !options::produceModels() &&
+ !options::produceAssignments() &&
+ !options::checkModels() &&
+ !options::unsatCores() &&
+ (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
options::unconstrainedSimp.set(uncSimp);
}
@@ -1660,6 +1703,11 @@ void SmtEngine::defineFunction(Expr func,
SmtScope smts(this);
+ PROOF( if (options::checkUnsatCores()) {
+ d_defineCommands.push_back(c.clone());
+ });
+
+
// Substitute out any abstract values in formula
Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
@@ -3033,7 +3081,7 @@ void SmtEnginePrivate::processAssertions() {
Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
+
if (d_assertions.size() == 0) {
// nothing to do
return;
@@ -3331,8 +3379,7 @@ void SmtEnginePrivate::processAssertions() {
d_iteSkolemMap.erase(toErase.back());
toErase.pop_back();
}
- d_assertions[d_realAssertionsEnd - 1] =
- Rewriter::rewrite(Node(builder));
+ d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
}
// For some reason this is needed for some benchmarks, such as
// http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -3442,6 +3489,12 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
// n is the result of an unknown preprocessing step, add it to dependency map to null
ProofManager::currentPM()->addDependence(n, Node::null());
}
+ // rewrite rules are by default in the unsat core because
+ // they need to be applied until saturation
+ if(options::unsatCores() &&
+ n.getKind() == kind::REWRITE_RULE ){
+ ProofManager::currentPM()->addUnsatCore(n.toExpr());
+ }
);
// Add the normalized formula to the queue
@@ -3512,7 +3565,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
// Dump the query if requested
if(Dump.isOn("benchmark")) {
// the expr already got dumped out if assertion-dumping is on
- Dump("benchmark") << CheckSatCommand();
+ Dump("benchmark") << CheckSatCommand(ex);
}
// Pop the context
@@ -3539,6 +3592,13 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
checkProof();
}
}
+ // Check that UNSAT results generate an unsat core correctly.
+ if(options::checkUnsatCores()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+ TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
+ checkUnsatCore();
+ }
+ }
return r;
} catch (UnsafeInterruptException& e) {
@@ -3596,7 +3656,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
// Dump the query if requested
if(Dump.isOn("benchmark")) {
// the expr already got dumped out if assertion-dumping is on
- Dump("benchmark") << CheckSatCommand();
+ Dump("benchmark") << QueryCommand(ex);
}
// Pop the context
@@ -3623,6 +3683,13 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
checkProof();
}
}
+ // Check that UNSAT results generate an unsat core correctly.
+ if(options::checkUnsatCores()) {
+ if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+ TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
+ checkUnsatCore();
+ }
+ }
return r;
} catch (UnsafeInterruptException& e) {
@@ -3943,6 +4010,47 @@ Model* SmtEngine::getModel() throw(ModalException, UnsafeInterruptException) {
return m;
}
+void SmtEngine::checkUnsatCore() {
+ Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
+
+ Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
+ UnsatCore core = getUnsatCore();
+
+ SmtEngine coreChecker(d_exprManager);
+ coreChecker.setLogic(getLogicInfo());
+
+ PROOF(
+ std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
+ for (; itg != d_defineCommands.end(); ++itg) {
+ (*itg)->invoke(&coreChecker);
+ }
+ );
+
+ Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
+ for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
+ Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
+ coreChecker.assertFormula(*i);
+ }
+ const bool checkUnsatCores = options::checkUnsatCores();
+ Result r;
+ try {
+ options::checkUnsatCores.set(false);
+ options::checkProofs.set(false);
+ r = coreChecker.checkSat();
+ } catch(...) {
+ options::checkUnsatCores.set(checkUnsatCores);
+ throw;
+ }
+ Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
+ if(r.asSatisfiabilityResult().isUnknown()) {
+ InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
+ }
+
+ if(r.asSatisfiabilityResult().isSat()) {
+ InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
+ }
+}
+
void SmtEngine::checkModel(bool hardFailure) {
// --check-model implies --produce-assertions, which enables the
// assertion list, so we should be ok.
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7c5c45e42..de9b8127d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -186,6 +186,13 @@ class CVC4_PUBLIC SmtEngine {
std::vector<Command*> d_dumpCommands;
/**
+ *A vector of command definitions to be imported in the new
+ *SmtEngine when checking unsat-cores.
+ */
+#ifdef CVC4_PROOF
+ std::vector<Command*> d_defineCommands;
+#endif
+ /**
* The logic we're in.
*/
LogicInfo d_logic;
@@ -261,6 +268,11 @@ class CVC4_PUBLIC SmtEngine {
void checkProof();
/**
+ * Check that an unsatisfiable core is indeed unsatisfiable.
+ */
+ void checkUnsatCore();
+
+ /**
* Check that a generated Model (via getModel()) actually satisfies
* all user assertions.
*/
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 2080c772a..4c35bd863 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -57,9 +57,10 @@ void SmtEngine::checkProof() {
Chat() << "checking proof..." << endl;
- if( ! ( d_logic.isPure(theory::THEORY_BOOL) ||
- ( d_logic.isPure(theory::THEORY_UF) &&
- ! d_logic.hasCardinalityConstraints() ) ) ) {
+ if( !(d_logic.isPure(theory::THEORY_BOOL) ||
+ (d_logic.isPure(theory::THEORY_UF) &&
+ ! d_logic.hasCardinalityConstraints())) ||
+ d_logic.isQuantified()) {
// no checking for these yet
Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl;
return;
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 635262a1e..1df304061 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -223,13 +223,7 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
p += 2;
}
if(*p == 'S') {
- // Strings requires arith for length constraints,
- // and UF for equality (?)
enableTheory(THEORY_STRINGS);
- enableTheory(THEORY_UF);
- enableTheory(THEORY_ARITH);
- enableIntegers();
- arithOnlyLinear();
++p;
}
if(!strncmp(p, "IDL", 3)) {
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
index 27cf86488..8f497688a 100644
--- a/src/util/unsat_core.h
+++ b/src/util/unsat_core.h
@@ -23,6 +23,7 @@
#include <iostream>
#include <vector>
#include "expr/expr.h"
+#include "util/output.h"
namespace CVC4 {
@@ -43,13 +44,17 @@ public:
UnsatCore() : d_smt(NULL) {}
template <class T>
- UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {}
+ UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {
+ Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
+ }
~UnsatCore() {}
/** get the smt engine that this unsat core is hooked up to */
SmtEngine* getSmtEngine() { return d_smt; }
+ size_t size() const { return d_core.size(); }
+
typedef std::vector<Expr>::const_iterator iterator;
typedef std::vector<Expr>::const_iterator const_iterator;
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index acb6ffcdf..e1ca49ac5 100644
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
(set-logic QF_AUFLIRA)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc
index 5fe17b412..4f6320028 100644
--- a/test/regress/regress0/datatypes/empty_tuprec.cvc
+++ b/test/regress/regress0/datatypes/empty_tuprec.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --no-check-proofs
+% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
%
OPTION "incremental";
diff --git a/test/regress/regress0/fmf/Makefile b/test/regress/regress0/fmf/Makefile
new file mode 100644
index 000000000..1e68a1e9e
--- /dev/null
+++ b/test/regress/regress0/fmf/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/fmf
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2
index f0e53fc98..f3db78491 100644
--- a/test/regress/regress0/fmf/PUZ001+1.smt2
+++ b/test/regress/regress0/fmf/PUZ001+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --no-check-proofs
+; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core
; EXPECT: unsat
;%------------------------------------------------------------------------------
;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0.
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 7b215dc2a..b6fb735fe 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -230,16 +230,28 @@ if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/d
fi
fi
check_proofs=false
+check_unsat_cores=false
if [ "$proof" = yes ]; then
# proofs not currently supported in incremental mode, turn it off
if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then
if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null &&
! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null &&
! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
- ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null &&
+ ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null &&
+ ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then
# later on, we'll run another test with --check-proofs on
check_proofs=true
fi
+ if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-unsat-cores' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-unsat-cores' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null &&
+ ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null &&
+ ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then
+ # later on, we'll run another test with --check-unsat-cores on
+ check_unsat_cores=true
+ fi
fi
fi
if [ -z "$expected_error" ]; then
@@ -315,7 +327,7 @@ if [ "$exit_status" != "$expected_exit_status" ]; then
exitcode=1
fi
-if $check_models || $check_proofs; then
+if $check_models || $check_proofs || $check_unsat_cores; then
check_cmdline=
if $check_models; then
check_cmdline="$check_cmdline --check-models"
@@ -323,7 +335,10 @@ if $check_models || $check_proofs; then
if $check_proofs; then
check_cmdline="$check_cmdline --check-proofs"
fi
- # at least one sat/invalid response: run an extra model/proof-checking pass
+ if $check_unsat_cores; then
+ check_cmdline="$check_cmdline --check-unsat-cores"
+ fi
+ # run an extra model/proof/core-checking pass
if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then
exitcode=1
fi
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback