cvc5.git
2014-05-08 Andrew ReynoldsFixes to quantifiers rewriter to prevent miniscoping...
2014-05-08 Andrew ReynoldsBasic optimizations for ambqi : only normalize UF appli...
2014-05-08 Dejan JovanovicAdding encoding of sha1 collision for the hashing example
2014-05-08 Tianyi Liangpatch to the last commit: add a single character case
2014-05-07 Tianyi Liangfix a bug in contain
2014-05-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-05-07 Tianyi Liangadd splits
2014-05-07 Tianyi Liangadd splits
2014-05-07 Andrew ReynoldsFixes to ambqi, now solution-sound.
2014-05-06 Andrew ReynoldsFirst draft of ambqi_builder (new implementation of...
2014-05-06 Tianyi Liangfix a bug in replace and contains
2014-05-05 Tianyi Liangadd constant regular expression check for intersection.
2014-05-05 Tim KingImproving documentation for glpk-cut-log switch.
2014-05-05 Morgan DetersValuation::entailmentCheck() proxy for TheoryEngine...
2014-05-02 Morgan DetersFix typo in bitvectors example; thanks to Adam Gashlin...
2014-05-02 Andrew ReynoldsSimplification of EqualityEngine::areDisequal. Compari...
2014-05-02 ajreynolFix assertion from previous commit.
2014-05-02 Andrew ReynoldsAdd option --dt-stc-ind for strengthening skolemization...
2014-05-02 ajreynolMore minor optimizations for datatypes.
2014-05-01 ajreynolMinor optimizations to datatypes, revert to checkClash...
2014-05-01 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-05-01 Kshitij Bansaldecision engine: cache start index for and/or nodes
2014-04-30 Tim KingT-entailment work, and QCF (quant conflict find) work...
2014-04-30 Morgan DetersFix warnings, cleanup in strings typechecker.
2014-04-30 Morgan DetersFix compiler warning re: TheoryUF destructor.
2014-04-30 Morgan DetersFix simplify output for SMT2 printer.
2014-04-30 Morgan DetersFix for (user) context-dependence of arith TO_INT/IS_IN...
2014-04-30 Morgan DetersMostly resolves bug #561 memory leaks, and more.
2014-04-29 Morgan DetersFix for --force-logic to extend its reach to the parser.
2014-04-29 Kshitij Bansalfixed couple of more warnings
2014-04-29 Kshitij Bansalfix was compiler warning in antlr_input, crashing test...
2014-04-29 Morgan DetersRevert a compiler warning fix from ea6a5a6.
2014-04-29 Tianyi Liangfix a typo: --string-exp => --strings-exp; fix a signed...
2014-04-29 Tianyi Liangadd leading zeros support for str.to.int
2014-04-29 ajreynolSignificantly improve performance for producing datatyp...
2014-04-28 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-28 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-04-28 Tianyi Liangadd strings-opt2 for regular splitting
2014-04-28 Kshitij Bansalcleanup
2014-04-28 Tianyi Liangminor change with kshitij's change
2014-04-28 Kshitij Bansalnodemanager robust skolem numbering
2014-04-28 Tianyi Liangadd strings-opt2 for regular splitting
2014-04-28 Kshitij BansalMerge pull request #25 from kbansal/sets
2014-04-28 Andrew ReynoldsPreparation for models for co-inductive datatypes....
2014-04-28 ajreynolOptimizations for datatypes: check for clashes modulo...
2014-04-28 Kshitij Bansalminor fix
2014-04-28 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-28 Kshitij Bansaltravis, please!
2014-04-27 Kshitij Bansalattempt to improve CVC4's "parse error" message
2014-04-27 Kshitij Bansalrm undocument/non-working* "feature"
2014-04-24 Tianyi Liangminor change: add a heuristic for preventing constant...
2014-04-24 Kshitij Bansaloptimization
2014-04-24 ajreynolAvoid assigning constructor terms to 1-constructor...
2014-04-24 Andrew ReynoldsCompute care graph for datatypes. Preliminary results...
2014-04-24 Andrew ReynoldsAdd --inst-max-level=N option for Kshitij. Support...
2014-04-22 Andrew ReynoldsMinor fix to avoid rewriting datatype equalities into...
2014-04-19 Kshitij BansalEh, what?
2014-04-19 Kshitij Bansalfix warnings in strings/
2014-04-17 Morgan DetersAllow fmf-bound-int to be set with set-option and via...
2014-04-17 Kshitij Bansalsimplify mkSkolem naming system: don't use $$
2014-04-17 Kshitij Bansaluse internal skolem numbering
2014-04-17 Andrew ReynoldsMinor refactoring and optimizing.
2014-04-14 Andrew ReynoldsFix bug in mbqi=fmc handling theory symbols. Fix mbqi...
2014-04-14 Andrew ReynoldsAdd initial support for co-datatypes.
2014-04-11 Morgan DetersBetter support for building with mingw64; thanks to...
2014-04-11 Morgan DeterssetType -> setOfType, resolves bug 556
2014-04-10 Morgan DetersFix the build; --check-proof works for UF but not for...
2014-04-10 Andrew ReynoldsExpand definitions in theory datatypes, now has the...
2014-04-10 Morgan DetersBoolean terms conversion fix for datatypes, fixes a...
2014-04-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-04-10 Tianyi Liangminor fix for strings
2014-04-10 Tianyi Liangminor fix for strings
2014-04-10 Andrew ReynoldsAdd support for cardinality constraints logic UFC....
2014-04-10 Kshitij Bansalrefactor .travis.yml
2014-04-09 Kshitij BansalMerge pull request #24 from kbansal/sets-model
2014-04-09 Morgan DetersMinor change to better support parameterized partial...
2014-04-09 Andrew ReynoldsRevert E-matching datatypes fix.
2014-04-09 Andrew ReynoldsHandle fmf.card as input from user, add support in...
2014-04-09 Kshitij Bansalfix get-info error-behavior
2014-04-09 Kshitij Bansaladd tests
2014-04-09 Kshitij Bansalfix
2014-04-09 Kshitij Bansalprep for fix
2014-04-09 Kshitij Bansaltry foreach on CD datastructure
2014-04-09 Kshitij Bansalinputs to trigger bug
2014-04-09 Kshitij Bansalmore
2014-04-09 Kshitij Bansalsome debugging changes
2014-04-06 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2014-04-06 Tim KingReduced example from pcc's bug report.
2014-04-06 Tim KingMerge pull request #21 from pcc/ite-fix
2014-04-06 Kshitij Bansalfix for hiding prompt/header in shell, error-behavior...
2014-04-04 Morgan DetersFor security, add --no-filesystem-access option, which...
2014-04-04 Morgan DetersAllow turning off the interactive prompt while in inter...
2014-04-03 Morgan DetersProperly quote symbols in SMT-LIB printer.
2014-04-03 Morgan DetersSome incremental bugs for Boolean terms, fixed. Thanks...
2014-04-01 Tim KingMerge branch '1.3.x'
2014-04-01 Tim KingFixing bug 552. There was a bug when integers are...
2014-04-01 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-04-01 Tianyi Liangwindows build fix for UINT32_MAX
2014-04-01 Tianyi Liangwindows build fix for UINT32_MAX
2014-03-31 Morgan DetersTravis-CI test for new-theory script, also related...
next