diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-23 23:08:03 +0000 |
commit | 5a20a19a30929ad58a9e64a9d8d1f877f3a07ae6 (patch) | |
tree | 2a800e6b1d6773e1c844767f5daed51148b5660b /src/main | |
parent | 1f2590541aa60f4b62b7c96659362ee4431d2d63 (diff) |
Added ability to set a "cvc4-specific logic" in standards-compliant
SMT-LIBv1 and SMT-LIBv2 input:
In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:
(benchmark actually_a_sat_benchmark_but_looks_like_uf
:logic QF_UF
:cvc4_logic { QF_SAT }
[...]
In SMT-LIBv2, you use a set-info; for instance:
(set-logic QF_UF)
(set-info :cvc4-logic "QF_SAT")
[...]
Right now, the only thing this does is disable the symmetry breaker for
benchmarks like the above ones.
As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).
Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class. This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem. A bug report is pending.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver.cpp | 8 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 8 |
2 files changed, 0 insertions, 16 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index e9bfde024..fa42e0b28 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -331,14 +331,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { status = doCommand(smt, *subcmd, options) && status; } } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - if(options.verbosity > 0) { *options.out << "Invoking: " << *cmd << endl; } diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index 5c8f908f8..7b0c70a8a 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -655,14 +655,6 @@ static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) { status = doCommand(smt, *subcmd, options) && status; } } else { - // by default, symmetry breaker is on only for QF_UF - if(! options.ufSymmetryBreakerSetByUser) { - SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd); - if(logic != NULL) { - options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF"); - } - } - if(options.verbosity > 0) { *options.out << "Invoking: " << *cmd << endl; } |