Age | Commit message (Collapse) | Author |
|
|
|
|
|
CASC proofs.
|
|
|
|
Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
|
|
direct handling of NOT
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sets).
|
|
|
|
|
|
|
|
contract is the same as for TheoryEngine version.
|
|
|
|
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5. Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
|
|
|
|
skolemization.
|
|
|
|
clean up.
|
|
|
|
This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.
This was triggerred by a benchmark sent by andy/viktor.
performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
|
|
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
|
|
|
|
|
|
rewrite-divk.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sets
|
|
|
|
building model at fullModel=false when possible. Minor cleanup.
|
|
|