[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] What kind of decision procedure is used for integerlinear inequalities



Hi Yegor,

The decision procedures in PVS are very old (the original code is 25
years old, though it has been updated and modified many times since).
Shankar is the best person to describe exactly what is in them and I
expect he'll reply soon (he's attending conferences in Europe right now).

We've been developing decision procedures that can be used outside PVS
for several years now and will incorporate some of these back into PVS
soon.  The current standalone decision procedure is called ICS; it's
used in the infinite bounded model checker of SAL (sal.csl.sri.com)
and is available at ics.csl.sri.com.

Your message is well-timed because just yesterday a competition on
decision procedures (actually, satisfaction modulo theories--SMT) was
completed at CAV.  Our prototypes for the next ICS are called Yices
and Simplics and they did very well--winning all the hard categories
and coming a very close second in the easy ones.  See
http://www.csl.sri.com/users/demoura/smt-comp/index.shtml

You can download benchmarks in a standard format from the SMT web
pages.  The categories for integer arithmetic are IDL (integer
difference logic), UFIDL (uninterpreted functions plus IDL), LIA
(linear integer arithmetic), and AUFLIA (arrays with uninterpreted
functions plus LIA).  LIA alone is of very little interest: it's the
integration of several theories that makes for a useful tool.  Yices,
ICS, and the PVS decision procedures all handle a superset of even
AUFLIA.

By the way, the examples called "spider_benchmarks" in the QF_LRA
(linear real arithmetic) category came from model checking conjectures
from a PVS proof: See Lee Pike, Paul Miner, Wilfredo Torres. Model
Checking Failed Conjectures in Theorem Proving: A Case Study. NASA
Technical Memorandum NASA/TM-2004-213278, 2004.  Available at
http://shemesh.larc.nasa.gov/fm/spider/spider_pubs.html

Randomly generated tests are a poor way to evaluate decision
procedures: you need representative real problems.  There's quite a
literature on benchmarking in the SAT and FOL communities.  See, for
example, Benchmarking SAT Solvers for Bounded Model Checking by
Emmanuel Zarpas, SAT'05, LNCS vol 3569

Note that modern decision procedures like Yices are thousands, maybe
millions, of times faster than those in PVS and handle arbitrary
propositional combinations of decided terms, not just conjunctions.
However, the capabilities needed of decision procedures in an
interactive prover may be different than those for applications like
bounded model checking.  We conjecture that in future several tools
having different capabilities will be used in combination, and we are
working toward that end.

Regards,
John Rushby