interfacing to `cvc5`

[johnyf]

The automatic theorem prover cvc5 for SMT problems is the successor of CVC4. Currently, tlapm can call CVC4:

tlapm/library/TLAPS.tla

Lines 43 to 54 in 3543f7f

	(**************************************************************************)
	(* Backend pragma: CVC4 SMT solver *)
	(* *)
	(* These methods translate the proof obligation to SMTLIB2 and call CVC4. *)
	(**************************************************************************)
	(* The CVC3* methods are here for backward compatibility. They call CVC4. *)
	CVC3 == TRUE (*{ by (prover: "cvc33") }*)
	CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)
	CVC4 == TRUE (*{ by (prover: "cvc33") }*)
	CVC4T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*)

• consider adding a proof directive named CVC (without a specific version number) to the module TLAPS

  • if a proof directive CVC is introduced, consider using this in the TLA+ modules in the directories library/, examples/, and examples-draft/

• consider adding a proof directive named CVC5

• update TLA+ modules in the directories library/, examples/, and examples-draft/ to use the proof directive CVC5 (or possibly CVC)

• perhaps consider removing the CVC3 proof directives, and show messages in the TLA+ Toolbox and stdout that inform the users to update to the CVC5 proof directive. The motivation is that solvers evolve, and explicitly mentioning the solver where relevant records requirements.

• consider renaming the (internal) method names from cvc3 to either cvc5, or cvc, for example at:
  

  tlapm/src/method.ml

  Line 25 in 3543f7f

  | Cvc3T of float

  
  and other places

• consider whether to interface to both cvc5 and CVC4, with distinct proof directives associated with each (and perhaps with the proof directive CVC being defined as the latest version of the cvc solver

• update the command invocation at:
  

  tlapm/src/params.ml

  Lines 172 to 176 in 3543f7f

  	let cvc4 =
  	if Sys.os_type = "Cygwin" then
  	make_exec "cvc4" "cvc4 --lang=smt2 \"$winfile\"" "cvc4 --version"
  	else
  	make_exec "cvc4" "cvc4 --lang=smt2 \"$file\"" "cvc4 --version"

  
  to cvc5, or add an additional function for calling cvc5 (depending on whether it is decided to interface to both cvc5 and CVC4 and call whichever solver the user requests)

• in case only cvc5 will be interfaced to, consider whether to call cvc5 also for occurrences of the proof directive CVC4, motivated by backwards compatibility (for some period of time), or to instead inform the user with messages to replace occurrences of the proof directive CVC4 with CVC5 (or possibly CVC)

• remember to update the help text of tlapm according to whether both cvc5 and CVC4 will be callable from tlapm, and how tlapm will behave for the proof directives CVC4 and CVC3:
  

  tlapm/src/params.ml

  Line 293 in 3543f7f

  printf " cvc4 -- CVC4\n";

• update the website files under the directory doc/web/content/ to mention cvc5, and possibly also CVC4 (in case it will be callable from tlapm)

• consider updating the fingerprinting:
  

  tlapm/src/backend/fpfile.ml

  Line 781 in 3543f7f

  | Cvc3T of floatomega

  
  In more detail:
  • existing fingerprints files appear to label information as related to CVC3. However, this information is related to CVC4. If switching to cvc5, then this information could be understood as relating to cvc5. However, doing this implies assuming that every input provable by CVC4 is provable, with the same command-line options, by cvc5.

  So to be explicit, it may be worth renaming the labeling within the fingerprints to cvc5. This would create a new version of the fingerprints file, so it seems that bumping the magic number would be needed.

  Moreover, it may be a good idea to choose this naming scheme, and update it, even for later cvc versions (e.g., cvc6), even if a CVC proof directive is introduced. A consequence would be that such a CVC proof directive would then save its results labeled as cvc5 first, and later labeled as cvc6, but that seems a reasonable (internal) evolution. This approach explicitly records the solver used in a proof.

  Any updates to the module src/backend/fpfile.ml and related code need to happen only after Fingerprinting variables and bound identifiers #23 has been merged, because code for loading older versions of the fingerprints has been removed in that pull request.

• it may be relevant to update the naming of identifiers in the SMT backend to either "cvc" or "cvc5":
  

  tlapm/src/smt/axioms.ml

  Line 459 in 3543f7f

  if !Smt.mode <> Smt.Z3 && !Smt.mode <> Smt.CVC3 then begin [ (** The following operators are built-in on Z3 *)

• update a test and its module name:

  tlapm/test/fast/basic/cvc3_false_test.tla

  Line 5 in 3543f7f

  THEOREM t == FALSE BY CVC3T(35)

• may be relevant to update the commented code in the packager:
  

  tlapm/tools/installer/tlaps-release.sh.in

  Lines 188 to 218 in 3543f7f

  	# CVC4_VERS=1.5
  	# CVC4=CVC4-$CVC4_VERS
  	# banner "Downloading and packaging $CVC4"
  	# case "@host_os@" in
  	# *linux*) CVC_DIR=https://tla.msr-inria.inria.fr/tlaps/dist/cvc4
  	# CVC_FILE=cvc4-1.5-x86_64-linux-opt
  	# ;;
  	# *cygwin*) CVC_DIR=https://tla.msr-inria.inria.fr/tlaps/dist/cvc4
  	# CVC_FILE=cvc4-1.5-win32-opt.exe
  	# ;;
  	# *darwin*) CVC_DIR=https://tla.msr-inria.inria.fr/tlaps/dist/cvc4
  	# CVC_FILE=cvc4-1.5-x86_64-macos-10.12-opt
  	# ;;
  	# *) echo "unknown architecture: @host_os@" >&2; exit 3;;
  	# esac
  	# mkdir -p "$INSTDIR/lib/tlaps/bin"
  	# cd "$DOWNDIR"
  	# if test -f "$CVC_FILE" ; then
  	# echo " [x] $CVC4 ALREADY downloaded"
  	# else
  	# @WGET@ "$CVC_DIR/$CVC_FILE"
  	# echo " [x] $CVC4 distribution downloaded"
  	# fi
  	# chmod +x "$CVC_FILE"
  	# cp "$CVC_FILE" "$INSTDIR/lib/tlaps/bin/cvc4"@EXE@
  	# echo " [x] $CVC4 extracted"