From 341239955adbadc6506e69c56b70e0eec6681e3c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 13 May 2015 12:46:41 +0200
Subject: [PATCH] Fix VC numbering, options, and solver names.
---
.../SMTLIBCVC4CounterExampleSolver.scala | 3 ++-
.../solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 3 ++-
.../smtlib/SMTLIBCVC4QuantifiedSolver.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBCVC4Solver.scala | 1 +
.../leon/solvers/smtlib/SMTLIBSolver.scala | 18 +++++++++---------
5 files changed, 15 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 6a42646e6..361806c2d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -7,11 +7,12 @@ import purescala.Definitions.Program
class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
- override val targetName = "cvc4-cex"
+ override def targetName = "cvc4-cex"
override def interpreterOps(ctx: LeonContext) = {
Seq(
"-q",
+ "--rewrite-divk",
"--produce-models",
"--print-success",
"--lang", "smt",
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 32bc12b4e..678d5915f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -7,7 +7,7 @@ import leon.purescala.Definitions.Program
class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
- override val targetName = "cvc4-proof"
+ override def targetName = "cvc4-proof"
override def interpreterOps(ctx: LeonContext) = {
Seq(
@@ -15,6 +15,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
"--print-success",
"--lang", "smt",
"--quant-ind",
+ "--rewrite-divk",
"--conjecture-gen",
"--conjecture-gen-per-round=3",
"--conjecture-gen-gt-enum=40",
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index f5de0bb34..3bdc59d25 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -16,7 +16,7 @@ import smtlib.theories.Core.Equals
// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
- override val targetName = "cvc4-quantified"
+ override def targetName = "cvc4-quantified"
private val typedFunDefExplorationLimit = 10000
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 69d12b686..cfc92dc44 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -33,6 +33,7 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
"--produce-models",
"--no-incremental",
"--tear-down-incremental",
+ "--rewrite-divk",
// "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
"--print-success",
"--lang", "smt"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 37e5908dc..37bedaebf 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -87,15 +87,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
/** Translation from Leon Expressions etc. */
- // Unique numbers
- protected object VCNumbers {
- private var nexts = Map[String, Int]().withDefaultValue(0)
- def getNext(id: String) = {
- val n = nexts(id)+1
- nexts += id -> n
- n
- }
- }
// Symbols
protected object SimpleSymbol {
@@ -904,3 +895,12 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
+// Unique numbers
+protected object VCNumbers {
+ private var nexts = Map[String, Int]().withDefaultValue(0)
+ def getNext(id: String) = {
+ val n = nexts(id)+1
+ nexts += id -> n
+ n
+ }
+}
--
GitLab