summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-05-08Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. ↵Andrew Reynolds
Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
2014-05-08Basic optimizations for ambqi : only normalize UF applied to variables, ↵Andrew Reynolds
direct handling of NOT
2014-05-07patch to the last commit: add a single character caseTianyi Liang
2014-05-07fix a bug in containTianyi Liang
2014-05-07add splitsTianyi Liang
2014-05-07Fixes to ambqi, now solution-sound.Andrew Reynolds
2014-05-06First draft of ambqi_builder (new implementation of MBQI based on disjoint ↵Andrew Reynolds
sets).
2014-05-05fix a bug in replace and containsTianyi Liang
2014-05-05add constant regular expression check for intersection.Tianyi Liang
2014-05-05Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and ↵Morgan Deters
contract is the same as for TheoryEngine version.
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : ↵Andrew Reynolds
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.
2014-05-02Fix assertion from previous commit.ajreynol
2014-05-02Add option --dt-stc-ind for strengthening skolemization. Refactor ↵Andrew Reynolds
skolemization.
2014-05-02More minor optimizations for datatypes.ajreynol
2014-05-01Minor optimizations to datatypes, revert to checkClash not mod eq. Minor ↵ajreynol
clean up.
2014-05-01Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-30decision engine: cache start index for and/or nodesKshitij Bansal
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
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
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>
2014-04-29Fix warnings, cleanup in strings typechecker.Morgan Deters
2014-04-29Fix compiler warning re: TheoryUF destructor.Morgan Deters
2014-04-29Fix simplify output for SMT2 printer.Morgan Deters
2014-04-29Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and ↵Morgan Deters
rewrite-divk.
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-29Fix for --force-logic to extend its reach to the parser.Morgan Deters
2014-04-29fixed couple of more warningsKshitij Bansal
2014-04-29fix was compiler warning in antlr_input, crashing test case with the old fixKshitij Bansal
2014-04-29Revert a compiler warning fix from ea6a5a6.Morgan Deters
2014-04-29fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlrTianyi Liang
2014-04-29add leading zeros support for str.to.intTianyi Liang
2014-04-29Significantly improve performance for producing datatypes models.ajreynol
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-28add strings-opt2 for regular splittingTianyi Liang
2014-04-28cleanupKshitij Bansal
2014-04-28nodemanager robust skolem numberingKshitij Bansal
2014-04-28Merge pull request #25 from kbansal/setsKshitij Bansal
Sets
2014-04-28Preparation for models for co-inductive datatypes. Minor cleanup.Andrew Reynolds
2014-04-28Optimizations for datatypes: check for clashes modulo equality. Avoid ↵ajreynol
building model at fullModel=false when possible. Minor cleanup.
2014-04-28minor fixKshitij Bansal
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-27attempt to improve CVC4's "parse error" messageKshitij Bansal
2014-04-27rm undocument/non-working* "feature"Kshitij Bansal
*test of unsigned for negative
2014-04-24minor change: add a heuristic for preventing constant splitting.Tianyi Liang
2014-04-24optimizationKshitij Bansal
2014-04-24Avoid assigning constructor terms to 1-constructor datatype eqcs, when ↵ajreynol
possible, to ensure termination for codatatypes. Minor changes.
2014-04-24Compute care graph for datatypes. Preliminary results show 20x speed up on ↵Andrew Reynolds
larger problems. Improve datatypes rewriter.
2014-04-24Add --inst-max-level=N option for Kshitij. Support define-const command in ↵Andrew Reynolds
Smt2.
2014-04-22Minor fix to avoid rewriting datatype equalities into non-equalitiers, as ↵Andrew Reynolds
required. Add APPLY_UF to congruence types to avoid model construction bugs.
2014-04-19Eh, what?Kshitij Bansal
2014-04-19fix warnings in strings/Kshitij Bansal
2014-04-17Allow fmf-bound-int to be set with set-option and via API.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback