A Brief Description of SMT-LIB, Alt-Ergo and CVC4
SMT-LIB:
SMT-LIB is a global initiative on facilitating research & development in the field of satisfiability modulo theories. As per their website, the goal of the SMT-LIB has been to:
· Provide standard rigorous descriptions of background theories used in SMT systems;
· Develop and promote common input and output languages for SMT solvers;
· Establish and make available to the research community a large library of benchmarks for SMT solvers.
SMT-LIB holds annual competitions (called SMT-COMP), where various SMT solvers are pitted against each other, comparing the power of these solvers (in terms of the range of theories recognized) and the efficiency of these solvers. Also, SMT-LIB has succeeded in creating a common input-output format and huge database of theories that SMT solvers can support. The latest version of the SMT-LIB is the SMT-LIBv2.0.
SMT-LIB is a global initiative on facilitating research & development in the field of satisfiability modulo theories. As per their website, the goal of the SMT-LIB has been to:
· Provide standard rigorous descriptions of background theories used in SMT systems;
· Develop and promote common input and output languages for SMT solvers;
· Establish and make available to the research community a large library of benchmarks for SMT solvers.
SMT-LIB holds annual competitions (called SMT-COMP), where various SMT solvers are pitted against each other, comparing the power of these solvers (in terms of the range of theories recognized) and the efficiency of these solvers. Also, SMT-LIB has succeeded in creating a common input-output format and huge database of theories that SMT solvers can support. The latest version of the SMT-LIB is the SMT-LIBv2.0.
Alt-Ergo:
Alt-Ergo is a SMT solver initiative from LRI, France. The Alt-Ergo solver makes use of an indigenous SAT Solver. Also, it uses its own algorithm for combining theories, called CC(X). Other features of Alt-Ergo are that it is highly modular and has its own quantifier instantiation logic. According to its website, it provides built-in support to the following theories:
· the free theory of equality with uninterpreted symbols,
· linear arithmetic over integers and rationals,
· non-linear arithmetic,
· polymorphic functional arrays,
· enumerated datatypes,
· record datatypes,
· associative and commutative (AC) symbols,
· fixed-sized bit-vectors.
Alt-Ergo is a SMT solver initiative from LRI, France. The Alt-Ergo solver makes use of an indigenous SAT Solver. Also, it uses its own algorithm for combining theories, called CC(X). Other features of Alt-Ergo are that it is highly modular and has its own quantifier instantiation logic. According to its website, it provides built-in support to the following theories:
· the free theory of equality with uninterpreted symbols,
· linear arithmetic over integers and rationals,
· non-linear arithmetic,
· polymorphic functional arrays,
· enumerated datatypes,
· record datatypes,
· associative and commutative (AC) symbols,
· fixed-sized bit-vectors.
CVC4:
CVC4 is the latest version of the Cooperating Validity Checker tools. It is an initiative of NYU and U Iowa. It aims at maintaining support to the previous version of the tool, while optimizing the core architecture for efficiency. According to its website, a few of the features of this tool are:
· several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit-vectors, and equality over uninterpreted function symbols;
· support for quantifiers;
· an interactive text-based interface;
· a rich C++ API for embedding in other systems;
· model generation abilities.
CVC4 is the latest version of the Cooperating Validity Checker tools. It is an initiative of NYU and U Iowa. It aims at maintaining support to the previous version of the tool, while optimizing the core architecture for efficiency. According to its website, a few of the features of this tool are:
· several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit-vectors, and equality over uninterpreted function symbols;
· support for quantifiers;
· an interactive text-based interface;
· a rich C++ API for embedding in other systems;
· model generation abilities.