Merge pull request #3556 from peterschrammel/remove-old-cvc

Remove refs to obsolete solver modules

Author: peterschrammel

CODEOWNERS

@@ -17,7 +17,6 @@
 /src/langapi/ @kroening @tautschnig @peterschrammel
 /src/xmllang/ @kroening @tautschnig @peterschrammel
 /src/nonstd/ @smowton @peterschrammel
-/src/solvers/cvc @martin-cs @kroening
 /src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
 /src/solvers/floatbv @martin-cs @kroening
 /src/solvers/miniBDD @tautschnig @kroening

doc/man/cbmc.1

@@ -158,8 +158,10 @@ Output subgoals in SMT2 syntax
 Use Boolector (experimental)
 .IP --mathsat
 Use MathSAT (experimental)
-.IP --cvc
+.IP --cvc3
 Use CVC3 (experimental)
+.IP --cvc4
+Use CVC4 (experimental)
 .IP --yices
 Use Yices (experimental)
 .IP --z3

doc/slides/cprover-overview-latex-beamer/cprover-overview-slides.tex

@@ -105,8 +105,7 @@
   \node[rectangle,fill=tachameleon!25!white] (solvers) [right of=engine4,xshift=2cm,yshift=-0.5cm]
    {\begin{tikzpicture}[node distance=0.75cm]
     \node[rectangle,fill=tachameleon!50!white] (sat)                { SAT };
-    \node[rectangle,fill=tachameleon!50!white] (smt1) [below of=sat] { SMT1 };
-    \node[rectangle,fill=tachameleon!50!white] (smt2) [below of=smt1] { SMT2 };
+    \node[rectangle,fill=tachameleon!50!white] (smt2) [below of=sat] { SMT2 };
     \node (decproc) [below of=smt2] { \tiny decision procedure };
     \end{tikzpicture}};
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -50,7 +50,7 @@ class optionst;
   "(classpath):(cp):(main-class):" \
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(json-ui)" \
-  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
+  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\

scripts/vpath-setup.sh

@@ -60,7 +60,7 @@ perl -p -i -e 's/^(irep_ids.cpp:)/#$1/' $DEST/src/util/Makefile
 # create sub-directories
 mkdir -p $DEST/src/ansi-c/library $DEST/src/ansi-c/literals
 mkdir -p $DEST/src/goto-instrument/{accelerate,wmm}
-mkdir -p $DEST/src/solvers/{cvc,flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt1,smt2}
+mkdir -p $DEST/src/solvers/{flattening,floatbv,miniBDD,prop,qbf,refinement,sat,smt2}
 
 # copy generated files for coverage reports
 for f in \

src/solvers/README.md

@@ -33,22 +33,10 @@ different decision procedures, roughly one per directory.
   including calling the conversions in `floatbv` as necessary. Is
   implemented as a simple conversion (with caching) and then a
   post-processing function that adds extra constraints. This is not used
-  by the SMT or CVC back-ends.
+  by the SMT2 back-ends.
 
-* dplib/:   Provides the `dplib_dect` object which used the decision
-  procedure library from “Decision Procedures : An Algorithmic Point of
-  View”.
-
-* cvc/:   Provides the `cvc_dect` type which interfaces to the old (pre
-  SMTLib) input format for the CVC family of solvers.  This format is
-  still supported by depreciated in favour of SMTLib 2.
-
-* smt1/:   Provides the `smt1_dect` type which converts the formulae to
-  SMTLib version 1 and then invokes one of Boolector, CVC3, OpenSMT,
-  Yices, MathSAT or Z3. Again, note that this format is depreciated.
-
-* smt2/:   Provides the `smt2_dect` type which functions in a similar
-  way to `smt1_dect`, calling Boolector, CVC3, MathSAT, Yices or Z3.
+* smt2/:   Provides the `smt2_dect` type which converts the formulae to
+  SMTLib 2 and then invokes one of Boolector, CVC3, CVC4, MathSAT, Yices or Z3.
   Note that the interaction with the solver is batched and uses
   temporary files rather than using the interactive command supported by
   SMTLib 2. With the `–fpa` option, this output mode will not flatten