-
jim_grundy added rkieburtz to the Decision Procedure Toolkit project.
2009-05-18 22:11:25 UTC by jim_grundy
-
Problems for the integer solver are canonized using rational division.
In particular "x/k = y" should not be reduced to "x = k*y", but to "(x = k*y + r) AND (0
2009-03-25 23:08:55 UTC by jim_grundy
-
Current assertions in the code formalize an assumption that the decision level of the SAT solver and the theory solvers move in lock-step. This can be violated in the case of theory solvers that do not detect conflict eagerly (are able to perform inference to detect conflicts when literals are set).
Subsequent releases of DPT will support lazy conflict detection in theory solvers.
2009-02-23 19:38:57 UTC by jim_grundy
-
The program "Why" can generate SMT-LIB verification conditions from source code, but the DPT seems to choke on them. What's worse, it just says: "Fatal error: exception Parsing.Parse_error"
Notice the lack of line#, never mind column#. Eeek. Not much to go on.
I've installed an "smtlib" directory with "logics" and "theories" subdirs, which contain:
./logics:
AUFLIA.smt
./theories...
2008-08-01 22:05:14 UTC by dwheeler
-
Completed in release 1.1.
2007-10-01 23:55:10 UTC by jim_grundy
-
Feature added in 1.1 release.
2007-10-01 23:52:02 UTC by jim_grundy
-
Fixed in the 1.1 release.
2007-10-01 23:50:27 UTC by jim_grundy
-
Expand the installation instructions to document the various settings and targets in the make file. In particular, people should know how to build it in FAST mode.
2007-03-15 17:16:27 UTC by jim_grundy
-
Currently Dpll_core.add_clause requires that
decision_level is 0. This may require starting the
solver if you need to add clauses incrementally. This
need not be the case.
The solver may not need to backtrack at all if the clause
is not conflicting in the current state. Otherwise we
should backtrack the solver as needed to make an
inference or deduce a conflict.
It is...
2007-03-07 21:00:31 UTC by jim_grundy
-
Levent noted that checking something that is trivially a contradiction, like "p & ~p" gets you an assertion violation.
Exception: Assert_failure (".../dpt-1.0/src/solver/dpll/dpll_core.ml", 400, 2).
The problem is just that we added an over eager assertion to the conflict detection routine that is valid only when we detect a contradiction during inference. If we detect the contradiction...
2007-02-22 22:28:12 UTC by jim_grundy
